在伊莎貝爾

Question

創建具有不平等的數據類型，我很新的Isabelle和想實現一個數據類型，如

數據類型的水果=蘋果|香蕉|哈密​​瓜

（字的選擇是空洞這裏不嘗試做別的混淆）

然而，它需要注意的是蘋果≤香蕉≤哈密瓜。

什麼是在伊莎貝爾實施的最佳方式？數據類型是否合適？

獎金問題：你如何實例化一個變量爲這3個選項之一？

Answer 1

關於你的主要問題。

我假設你想指定一個手動排序，即你想拼出所有的情況。如果您對標準詞典順序感到滿意，那麼有一個AFP entry可以自動完成。

是的，實現你想要的正確方法是通過數據類型開始。然後，您將需要定義≤運算符。爲此，您需要實例化一個類。 documentation of type classes的前兩部分將告訴您這是如何工作的。對於你的榜樣，它會是這個樣子：

instantiation fruit :: linorder begin 

fun less_fruit where 
"Apple < Apple ⟷ False" | 
"Apple < _ ⟷ True" | 
"Banana < Apple ⟷ False" | 
"Banana < Banana ⟷ False" | 
"Banana < _ ⟷ True" | 
"Cantaloupe < _ ⟷ False" 

definition less_eq_fruit :: "fruit ⇒ fruit ⇒ bool" where 
[simp]: "less_eq_fruit x y ⟷ x = y ∨ x < y" 

instance sorry 

end 

最後，你將不得不進行實例證明，那就是：你需要證明你確實定義的運營商形成線性順序。在上面的示例中，我使用sorry命令進行了欺騙。

正確的做法直接導致您的獎金問題。

您可以使用cases策略實例化變量。看到它在行動的實例證明：

instance proof 
    fix x y :: fruit 
    show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" 
    by (cases x; cases y; simp) 
next 
    (* more stuff to prove here *) 
qed 

的cases方法接受一個變量名，將分割當前目標爲多個的情況下（此處爲三個）。 ;（順序組合）運算符將應用第一種方法並在所有新的子目標上應用第二種方法。最後，一切都可以用simp來解決。