伊莎貝爾：linord證明

我試圖創建失敗的自定義數據類型定製的線性順序，下面是我的代碼：伊莎貝爾：linord證明

theory Scratch 
imports Main 
begin 

    datatype st = Str "string" 

    fun solf_str_int:: "string ⇒ int" where 
    "solf_str_int str = (if (size str) > 0 
         then int(nat_of_char (hd str) + 1) + 100 *  (solf_str_int (tl str)) 
         else 0)" 

    fun soflord:: "st ⇒ st ⇒ bool" where 
    "soflord s1 s2 = (case s1 of Str ss1 ⇒ (case s2 of Str ss2 ⇒ 
         (solf_str_int ss1) ≤ (solf_str_int ss2)))" 

instantiation st :: linorder 
begin 
    definition nleq: "less_eq n1 n2 == soflord n1 n2" 
    definition neq: "eq n1 n2 == (n1 ≤ n2) ∧ (n2 ≤ n1)" 
    definition nle: "less n1 n2 == (n1 ≤ n2) ∧ (¬(n1 = n2))" (* ++ *) 

    instance proof 
    fix n1 n2 x y :: st 
    show "n1 ≤ n1" by (simp add:nleq split:st.split) 
    show "(n1 ≤ n2) ∨ (n2 ≤ n1)" by (simp add:nleq split:st.split)  (*why is 'by()' highlited?*) 
    (*this fail if I comment line ++ out*) 
    show "(x < y) = (x ≤ y ∧ (¬ (y ≤ x)))" by (simp add:nleq neq split:node.split) 

    qed 
end 
end

標有（* ++ *）的定義是不正確的，如果刪除它最後一個節目給出了問題。

如何糾正證明？爲什麼第二個顯示部分突出顯示？

來源

2015-12-07 Johan

當定義類型的類（less_eq和less在linorder的情況下）的操作中，如果推斷出的類型的動作的恰好正在定義過載的實例相匹配只能用於過載操作的名稱。特別是，如果結果太籠統，這種類型不是專門的。

爲less_eq作品的定義，因爲soflord限制類型的n1和n2到st，所以less_eq使用與st => st => bool類型，它是這裏需要正是。對於less，類型推斷計算最常用的類型'b :: ord => 'b => bool。由於這不是預期類型st => st => bool，Isabelle不承認定義爲重載操作的定義，因此抱怨您要重新定義現有操作的完整通用性。如果您根據需要限制類型，則該定義按預期工作。

definition nle: "less n1 (n2 :: st) == (n1 ≤ n2) ∧ (¬(n1 = n2))"

但是，您的定義沒有在st上定義線性順序。問題是違反反對稱性。例如，兩個字符串Str ''d''和Str [Char Nibble0 Nibble0, Char Nibble0 Nibble0]（即，由代碼點0上的兩個字符組成的字符串）在您的順序中是「等價的」，儘管它們是不同的值。您也嘗試在st上定義相等性，但在高階邏輯中，不能定義相等性。這取決於你構建你的類型的方式。如果您確實想要根據您的訂單確定相同的字符串，則必須先構造商，例如使用商數包。

by(simp ...)的紫色突出顯示證明方法simp仍在運行。在你的情況下，它不會終止，因爲simp將繼續展開solf_str_int的定義方程：其右側包含左側的一個實例。我建議您在=的左側通過模式匹配來定義您的功能。然後，方程式僅在消耗模式時才使用。因此，您必須自己觸發案例區分（例如使用cases），但您也可以更好地控制自動化策略。

來源

2015-12-08 07:41:53

伊莎貝爾：linord證明

回答

相關問題