定义谓词；需要道具=>布尔答案

【问题标题】：Defining a predicate; need prop=>bool定义谓词；需要道具=>布尔
【发布时间】：2021-07-14 02:08:48
【问题描述】：

我正在尝试定义一个函数，它接受一个集合和一个关系并返回一个布尔值，告诉该关系是否在集合上是自反的。我试图这样定义它：

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，但我得到了同样的错误。定义我的函数的正确方法是什么？

【问题讨论】：

标签： isabelle

【解决方案1】：

您不能从prop 转到bool。但您不必：只需使用对象级连接词（⟶ 和 ∀）而不是元逻辑连接词（⟹ 和 ⋀）。它们在逻辑上是等价的，所以这不是问题。

元逻辑连接词应该（并且通常可以）只用于命题的“最外层”。

但是请注意，当您可以使用宏逻辑时，使用它们通常更方便，因为对象级的对于 Isabelle 和 Isar 证明语言是不透明的（即它们是功能就像任何其他功能一样），而 Isar“知道”⟹ 和 ⋀ 的含义。例如，如果您使用⟹ 和⋀ 声明了一个事实，您可以立即使用of/OF 属性在其中实例化变量并解除假设。

【讨论】：

【解决方案2】：

您首先需要编写它以使值不是prop - 没有转换。在这种情况下，您在∀x. x ∈ A 和(x, x) ∈ R 之间使用了道具级别的暗示⟹。您可以改用单角箭头-->，这是布尔值的含义。

【讨论】：