伊莎贝尔：林诺证明

Question

我尝试为自定义数据类型创建自定义线性顺序失败，下面是我的代码：

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

标有(*++*)的定义不对，删掉最后的节目会出问题

如何更正证明？为什么倒数第二个节目部分突出显示？

Answer 1

当你定义一个类型class的操作时（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 处的两个字符组成的字符串）在您的顺序中是 "equivalent"，尽管它们是不同的值。您也尝试在 st 上定义相等性，但在高阶逻辑中，无法定义相等性。它取决于您构建类型的方式。如果你真的想根据你的顺序识别等价的字符串，你必须先构造一个商，例如，使用 quotient 包。

by(simp ...)的紫色高亮表示证明方法simp仍然是运行。在你的例子中，它不会终止，因为 simp 将继续展开 solf_str_int 的定义方程：它的右侧包含左侧的一个实例。我建议您通过 = 左侧的模式匹配来定义您的函数。然后，仅当方程可以消耗模式时才使用方程。因此，您必须自己触发大小写区分（例如使用 cases），但您也可以更好地控制自动策略。

伊莎贝尔：林诺证明

Isabelle: linord proof

isabelle