Theory Lexord_List

theory Lexord_List
imports Main
begin

typedef 'a lexlist = "{xs::'a list. True}"
  morphisms unlex Lex
by auto

definition "lexlist ≡ Lex"

lemma lexlist_ext:
  "Lex xs = Lex ys ⟹ xs = ys"
by (auto simp: Lex_inject)

lemma Lex_unlex [simp, code abstype]:
  "Lex (unlex lxs) = lxs"
  by (fact unlex_inverse)

lemma unlex_lexlist [simp, code abstract]:
  "unlex (lexlist xs) = xs"
  by (metis lexlist_ext unlex_inverse lexlist_def)

definition list_less :: "'a :: ord list ⇒ 'a list ⇒ bool" where 
  "list_less xs ys ⟷ (xs, ys) ∈ lexord {(u, v). u < v}"

definition list_le where
  "list_le xs ys ⟷ list_less xs ys ∨ xs = ys"

lemma not_less_Nil [simp]: "¬ list_less x []"
  by (simp add: list_less_def)

lemma Nil_less_Cons [simp]: "list_less [] (a # x)"
  by (simp add: list_less_def)

lemma Cons_less_Cons [simp]: "list_less (a # x) (b # y) ⟷ a < b ∨ a = b ∧ list_less x y"
  by (simp add: list_less_def)

lemma le_Nil [simp]: "list_le x [] ⟷ x = []"
  unfolding list_le_def by (cases x) auto

lemma Nil_le_Cons [simp]: "list_le [] x"
  unfolding list_le_def by (cases x) auto

lemma Cons_le_Cons [simp]: "list_le (a # x) (b # y) ⟷ a < b ∨ a = b ∧ list_le x y"
  unfolding list_le_def by auto

lemma less_list_code [code]:
  "list_less xs [] ⟷ False"
  "list_less [] (x # xs) ⟷ True"
  "list_less (x # xs) (y # ys) ⟷ x < y ∨ x = y ∧ list_less xs ys"
  by simp_all

lemma less_eq_list_code [code]:
  "list_le (x # xs) [] ⟷ False"
  "list_le [] xs ⟷ True"
  "list_le (x # xs) (y # ys) ⟷ x < y ∨ x = y ∧ list_le xs ys"
  by simp_all

instantiation  lexlist :: (ord) ord
begin

definition
  lexlist_less_def: "xs < ys ⟷ list_less (unlex xs) (unlex ys)"

definition
  lexlist_le_def: "(xs :: _ lexlist) ≤ ys ⟷ list_le (unlex xs) (unlex ys)"

instance ..

lemmas lexlist_ord_defs = lexlist_le_def lexlist_less_def list_le_def list_less_def

end

instance lexlist :: (order) order
proof
  fix xs :: "'a lexlist"
  show "xs ≤ xs" by (simp add: lexlist_le_def list_le_def)
next
  fix xs ys zs :: "'a lexlist"
  assume "xs ≤ ys" and "ys ≤ zs"
  then show "xs ≤ zs"
    apply (auto simp add: lexlist_ord_defs)
    apply (rule lexord_trans)
    apply (auto intro: transI)
    done
next
  fix xs ys :: "'a lexlist"
  assume "xs ≤ ys" and "ys ≤ xs"
  then show "xs = ys"
    apply (auto simp add: lexlist_ord_defs)
    apply (rule lexord_irreflexive [THEN notE])
    defer
    apply (rule lexord_trans)
    apply (auto intro: transI simp: unlex_inject)
    done
next
  fix xs ys :: "'a lexlist"
  show "xs < ys ⟷ xs ≤ ys ∧ ¬ ys ≤ xs"
    apply (auto simp add: lexlist_ord_defs)
    defer
    apply (rule lexord_irreflexive [THEN notE])
    apply auto
    apply (rule lexord_irreflexive [THEN notE])
    defer
    apply (rule lexord_trans)
    apply (auto intro: transI)
    done
qed

instance lexlist :: (linorder) linorder
proof
  fix xs ys :: "'a lexlist"
  have "(unlex xs, unlex ys) ∈ lexord {(u, v). u < v} ∨ unlex xs = unlex ys ∨ (unlex ys, unlex xs) ∈ lexord {(u, v). u < v}"
    by (rule lexord_linear) auto
  then show "xs ≤ ys ∨ ys ≤ xs"
    by (auto simp add: lexlist_ord_defs unlex_inject)
qed

end