如何解决定义谓词；需要道具=>布尔
我正在尝试定义一个函数，该函数接受一个集合和一个关系，并返回一个布尔值，告诉该关系是否在集合上是自反的。我试着这样定义它：
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 属性立即实例化变量并解除其中的假设。
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
