equality - 伊莎贝尔/伊萨尔 : Implementing equational reasoning

Question

我仍在努力思考平等关系以及如何在 Isabelle 中定义平等关系。幸运的是，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's 而不是在 isar rm 更远的地方，它们被省略了。只是说明 impD [dest]: (A --> B) ==> A ==> B
需要做什么才能使替代工作？

Answer 1

理论playground进口Main这定义了很多。如果你想从裸地开始，你应该使用Pure反而。另一个问题是 ("_play" 5)应该是 ("_" 5) (它定义了一种语法)。在这两个更改之后，您可以继续。