Isabelle: linord доказательство

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

При определении операции класса типа (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, но в логике более высокого порядка нельзя определить равенство. Это определяется тем, как вы создали свой тип. Если вы действительно хотите идентифицировать строки, эквивалентные в соответствии с вашим заказом, сначала нужно построить фактор, например, используя пакет quotient.

Фиолетовая подсветка by(simp ...) указывает, что метод доказательства simp все еще работает. В вашем случае он не будет завершен, потому что simp будет продолжать разворачивать определяющее уравнение для solf_str_int: его правая часть содержит экземпляр левой стороны. Я рекомендую вам определить свои функции путем сопоставления шаблонов с левой стороны от =. Затем уравнения используются только тогда, когда они могут потреблять шаблон. Таким образом, вы должны сами инициировать различие случаев (например, используя cases), но вы также получаете больше контроля над автоматизированной тактикой.