在Isabelle中定義quotient_type

Question

我仍然試圖在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" 

我已經有了一些基本的公式，它的複雜的版本，我想的複雜類型理智戰勝了，所以我定義的三個公理的平等關係和3個附加等於容易的公理。

編輯：顯然我是一個白癡誰忘了添加引號-.- 還不知道如何從這裏繼續思想。

Answer 1

quotient_type命令需要證明才能正確完成。查看證明狀態輸出需要證明的內容。這些內容在手冊中明確或隱含地解釋。

無關筆記：

• 較好地避免重複使用的基本符號像+。 Prover IDE中的符號面板提供了很多選擇。

• 更好地避免自由形式的公理化，特別是對於最初的例子。只要看看什麼伊莎貝爾/ HOL已經提供，並在此基礎之上（datatype，definition，inductive，fun等）

• 駱駝病例定義在伊莎貝爾未使用。