1

我仍在尝试对 Isabelle 中的语义平等进行推理。我想比较两个公式，看看它们是否相等。之前有人告诉我，我需要商类型。所以我试图给自己定义一个quotiernttype，但显然我的定义并不完整，因为我似乎无法在我的定义之后编写任何代码。到目前为止，我的代码是：

theory Scratch
imports Main
begin
no_notation plus (infixl "+" 65)

typedecl basicForm
datatype form_rep = af basicForm
axiomatization
equals ::  "form_rep ⇒ form_rep ⇒ bool" (infix "≐" 1) and
plus :: "form_rep ⇒ form_rep ⇒ form_rep" (infixl "+" 35)
  where
  reflexive: "x ≐ x" and
  symmetric: "x ≐ y ⟹ y ≐ x" and
  transitiv: "x ≐ y ⟹ y ≐ z ⟹ x ≐ z" and   

  commut:  "x + y         ≐ y + x"  and
  associatPlus:  "(x + y) + z  ≐ x + (y + z)"   and
  idemo:  "x + x           ≐ x" 

quotient_type formula = "form_rep" / "equals"

我有一些基本公式和它的复杂版本，我想对复杂类型进行推理，因此我用相等关系的三个公理和另外三个简单的公理定义了 equals。

编辑：显然我是一个忘记添加引号的白痴-.-仍然不知道如何从这里继续思考。

4

1 回答 1

0

这些quotient_type命令需要证明才能正确完成。查看证明状态输出需要证明的内容。这些事情在isar-ref手册中有明确或隐含的解释。

无关注释：

  • 最好避免重复使用基本符号，如+. Prover IDE 中的Symbols面板提供了很多选择。

  • 最好避免自由形式的公理化，尤其是对于初始示例。只需采用 Isabelle/HOL 已经提供的内容，并在此之上进行定义（datatype、definition、inductive等fun）

  • 在 Isabelle 中不使用驼峰式。

于 2016-01-20T16:52:30.287 回答