Isabelle / isar:实施等式推理

Question

我还在努力研究平等关系，以及如何定义伊莎贝尔的平等关系。幸运的是，在isar参考手册2.3.1 p38f中有关于这一点的一章。

我试着重建给定的例子。为了避免与已建立的语法重叠，我重新命名了所有内容。此外，我还添加了一些引号，因为它们似乎在示例中缺失。

theory playground
imports Main
begin

typedecl i_play
typedecl u_play

下一步是我不太明白的判断，但是嘿，哪里会出错：

judgment
Trueprop :: "u_play => prop" ("_play" 5)

error: Attempt to redeclare object-logic judgment

即使重命名Trueprop也不会产生另一个结果。

我就不能在这里用bool来代替定义我自己的对象命题吗？还是我需要在其他地方介绍u_play？

但让我们走得更远。下一步是相等关系，也是复制和重命名的关系。

axiomatization
equal :: "i_play => i_play => u_play" (infix "EQ" 50)
where
refl [intro]: "x EQ x" and
subst [elim]: "x EQ y ⟹ B x ⟹ B y"

这给出了一个Type unification failed: Clash of types "u_play" and "bool"错误。当我用bool替换u_play时，一切都很好，我甚至可以在一些琐碎的事情上使用EQ，比如lemma t : "x EQ x"，但是替代规则似乎不起作用，这就引出了两个B是什么的问题。我在HOL.thy中看到了与P相同的构造，而在isar的后面，则忽略了它们。只是陈述了impD [dest]: (A --> B) ==> A ==> B

要让替代品发挥作用，需要做些什么？

Answer 1

理论playground导入了定义了很多的Main。如果你想从空旷的场地开始，你应该用Pure代替。另一个问题是("_play" 5)应该读取("_" 5) (它定义了一个语法)。在这两个更改之后，您可以继续。