代码之家 › 专栏 › 技术社区 › lburski

Isabelle中的范围限制/域限制

isabelle restriction symbols range set

0

lburski · 技术社区 · 8 年前

我试图在Isabelle中输入一个模式,但是当我将范围限制或域限制添加到它不想解析的定理证明器中时。我在LaTeX中有以下模式:

\begin{schema}{VideoShop}
members: \power PERSON \\
rented: PERSON \rel TITLE \\
stockLevel: TITLE \pfun \nat
\where
\dom rented \subseteq members \\
\ran rented \subseteq \dom stockLevel \\
\forall t: \ran rented @ \# (rented \rres \{t\}) \leq stockLevel~t
\end{schema}

当将此输入到Isabelle时,我会得到以下结果:

locale videoshop = 
fixes members :: "PERSON set"
and rented :: "(PERSON * TITLE) set"
and stockLevel :: "(TITLE * nat) set"
assumes "Domain rented \<subseteq> members" 
 and "Range rented \<subseteq> Domain stockLevel" 
 and "(\<forall> t. (t \<in> Range rented) \<and> (card (rented \<rhd> {t}) \<le> stockLevel t))"
begin
.....

除了最后一个表达式之外,它都会进行解析 \<forall> t.....

我只是不明白如何给伊莎贝尔增加射程限制。

1 回复 | 直到 8 年前

1

larsrh 8 年前

您的输入存在多个问题。

这个 â³ 表达式中使用的符号
```
(rented â³ {t})
```
未与任何运算符关联,因此无法对其进行分析。我不太确定这是什么意思。从规范的高层观点来看,我猜大概是“所有租用特定头衔的人”。这可以用一套理解来表达:
```
{p. (p, t) â rented}
```
您将有界通用量词转换为包含连词的量词。这很可能不是你想要的,因为它说“为了所有人” t , t型 在范围内 rented 和 Isabelle有有界量词的符号。
```
ât â Range rented. ...
```
您正在尝试使用 stockLevel 作为一个函数,它不是。从你的LaTeX输入中,我推断它应该是一个偏函数。Isabelle称之为 map s、合适的类型是:
```
TITLE â nat
```
请注意“鱼叉”符号而不是功能箭头。映射的域函数被调用 dom 第二语言环境假设可以表示为:
```
Range rented â dom stockLevel
```
鉴于此,您可以使用 库存水平 作为来自的函数 TITLE 到 nat option .