在Isabelle中定义quotient_type

Question

我还在尝试对Isabelle中的语义平等进行推理。我想比较两个公式，看看它们是否相等。以前有人告诉我，我需要使用quotienttypes。所以我试着给自己定义一个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"

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

编辑:显然，我是一个忘记添加引号的笨蛋-仍然不知道如何从这里继续思考。

Answer 1

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

不相关的注释：

• 最好避免重复使用像+这样的基本表示法。Prover IDE中的Symbols面板提供了大量避免自由形式公理的alternatives.
• Better，特别是对于初始示例。只需使用Isabelle/HOL已经提供的，并在此基础上进行定义(datatype，definition，inductive，fun Isabelle不使用definition。