问题描述
我正在尝试定义一个函数,该函数接受一个集合和一个关系,并返回一个布尔值,告诉该关系是否在集合上是自反的。我试着这样定义它:
deFinition refl::"'a set⇒('a×'a) set⇒bool" where
"refl A R = (∀x. x∈A⟹(x,x)∈R)"
但伊莎贝尔给了我以下错误:
Type unification Failed: Clash of types "prop" and "bool"
Type error in application: incompatible operand type
Operator: (=) (refl A R) :: bool ⇒ bool
Operand: ∀x. x ∈ A ⟹ (x,x) ∈ R :: prop
我似乎找不到任何函数将“prop”强制转换为“bool”。我还尝试更改定义以设置 RHS = True,但出现相同的错误。 定义我的函数的正确方法是什么?
解决方法
您首先需要将其编写为值不是 prop
— 没有转换。在本例中,您在 ⟹
和 ∀x. x ∈ A
之间使用了道具级蕴涵 (x,x) ∈ R
。您可以改用单宽度箭头 -->
,这是 bool 的含义。
您不能从 prop
转到 bool
。但您不必:只需使用对象级连接词(⟶
和 ∀
)而不是元逻辑连接词(⟹
和 ⋀
)。它们在逻辑上是等价的,所以这不是问题。
元逻辑连接词应该(并且通常可以)仅用于命题的“最外层”。
但是请注意,当您可以使用超级逻辑时,使用它们通常更方便,因为对象级的对 Isabelle 和 Isar 证明语言是不透明的(即它们是函数就像任何其他函数一样),而 Isar“知道”⟹
和 ⋀
的含义。例如,如果您有一个用 ⟹
和 ⋀
陈述的事实,您可以使用 of
/OF
属性立即实例化变量并解除其中的假设。