4

我仍在努力了解平等关系以及如何在 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"错误。当我将 u_play 替换为 bool 时，一切都很好，我什至可以EQ在一些琐碎的东西中使用lemma t : "x EQ x"，但是替换规则似乎不起作用，这让我想到了两个 B 在那里的问题。我在 HOL.thy 中看到了相同的构造，但使用了 P，而在 isar rm 的下方，它们被省略了。只是说明impD [dest]: (A --> B) ==> A ==> B

需要做什么才能使替换起作用？

4

1 回答 1

3

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

于 2016-01-12T17:02:58.387 回答