Quelle  Lexord.thy

section ‹Lexicographic orderings›

theory Lexord
  imports Main
begin

subsection ‹The preorder case›

locale lex_preordering = preordering
begin

inductive lex_less :: ‹'a list ==> 'a list ==> bool›  (infix ‹[<]› 50) 
where
  Nil: ‹[] [<] y # ys›
| Cons: ‹x < y ==> x # xs [<] y # ys›
| Cons_eq: ‹x \≤ y ==> y \≤ x ==> xs [<] ys ==> x # xs [<] y # ys›

inductive lex_less_eq :: ‹'a list ==> 'a list ==> bool›  (infix ‹[\≤]› 50)
where
  Nil: ‹[] [\≤] ys›
| Cons: ‹x < y ==> x # xs [\≤] y # ys›
| Cons_eq: ‹x \≤ y ==> y \≤ x ==> xs [\≤] ys ==> x # xs [\≤] y # ys›

lemma lex_less_simps [simp]:
  ‹[] [<] y # ys›
  ‹¬ xs [<] []›
  ‹x # xs [<] y # ys ⟷ x < y ∨ x \≤ y ∧ y \≤ x ∧ xs [<] ys›
  by (auto intro: lex_less.intros elim: lex_less.cases)

lemma lex_less_eq_simps [simp]:
  ‹[] [\≤] ys›
  ‹¬ x # xs [\≤] []›
  ‹x # xs [\≤] y # ys ⟷ x < y ∨ x \≤ y ∧ y \≤ x ∧ xs [\≤] ys›
  by (auto intro: lex_less_eq.intros elim: lex_less_eq.cases)

lemma lex_less_code [code]:
  ‹[] [<] y # ys ⟷ True›
  ‹xs [<] [] ⟷ False›
  ‹x # xs [<] y # ys ⟷ x < y ∨ x \≤ y ∧ y \≤ x ∧ xs [<] ys›
  by simp_all

lemma lex_less_eq_code [code]:
  ‹[] [\≤] ys ⟷ True›
  ‹x # xs [\≤] [] ⟷ False›
  ‹x # xs [\≤] y # ys ⟷ x < y ∨ x \≤ y ∧ y \≤ x ∧ xs [\≤] ys›
  by simp_all

lemma preordering:
  ‹preordering ([\≤]) ([<])›
proof
  fix xs ys zs
  show ‹xs [\≤] xs›
    by (induction xs) (simp_all add: refl)
  show ‹xs [\≤] zs› if ‹xs [\≤] ys› ‹ys [\≤] zs›
  using that proof (induction arbitrary: zs)
    case (Nil ys)
    then show ?case by simp
  next
    case (Cons x y xs ys)
    then show ?case
      by (cases zs) (auto dest: strict_trans strict_trans2)
  next
    case (Cons_eq x y xs ys)
    then show ?case
      by (cases zs) (auto dest: strict_trans1 intro: trans)
  qed
  show ‹xs [<] ys ⟷ xs [\≤] ys ∧ ¬ ys [\≤] xs› (is ‹?P ⟷ ?Q›)
  proof
    assume ?P
    then have ‹xs [\≤] ys›
      by induction simp_all
    moreover have ‹¬ ys [\≤] xs›
      using ‹?P›
      by induction (simp_all, simp_all add: strict_iff_not asym)
    ultimately show ?Q ..
  next
    assume ?Q
    then have ‹xs [\≤] ys› ‹¬ ys [\≤] xs›
      by auto
    then show ?P
    proof induction
      case (Nil ys)
      then show ?case
        by (cases ys) simp_all
    next
      case (Cons x y xs ys)
      then show ?case
        by simp
    next
      case (Cons_eq x y xs ys)
      then show ?case
        by simp
    qed
  qed
qed

interpretation lex: preordering ‹([\≤])› ‹([<])›
  by (fact preordering)

end


subsection ‹The order case›

locale lex_ordering = lex_preordering + ordering
begin

interpretation lex: preordering ‹([\≤])› ‹([<])›
  by (fact preordering)

lemma less_lex_Cons_iff [simp]:
  ‹x # xs [<] y # ys ⟷ x < y ∨ x = y ∧ xs [<] ys›
  by (auto intro: refl antisym)

lemma less_eq_lex_Cons_iff [simp]:
  ‹x # xs [\≤] y # ys ⟷ x < y ∨ x = y ∧ xs [\≤] ys›
  by (auto intro: refl antisym)

lemma ordering:
  ‹ordering ([\≤]) ([<])›
proof
  fix xs ys
  show *: ‹xs = ys› if ‹xs [\≤] ys› ‹ys [\≤] xs›
  using that proof induction
  case (Nil ys)
    then show ?case by (cases ys) simp
  next
    case (Cons x y xs ys)
    then show ?case by (auto dest: asym intro: antisym)
      (simp add: strict_iff_not)
  next
    case (Cons_eq x y xs ys)
    then show ?case by (auto intro: antisym)
      (simp add: strict_iff_not)
  qed
  show ‹xs [<] ys ⟷ xs [\≤] ys ∧ xs ≠ ys›
    by (auto simp add: lex.strict_iff_not dest: *)
qed

interpretation lex: ordering ‹([\≤])› ‹([<])›
  by (fact ordering)

end


subsection ‹Canonical instance›

instantiation list :: (preorder) preorder
begin

global_interpretation lex: lex_preordering ‹(≤) :: 'a::preorder ==> 'a ==> bool› ‹(<) :: 'a ==> 'a ==> bool›
  defines less_eq_list = lex.lex_less_eq
    and less_list = lex.lex_less ..

instance
  by (rule preorder.intro_of_class, rule preordering_preorderI, fact lex.preordering)

end

global_interpretation lex: lex_ordering ‹(≤) :: 'a::order ==> 'a ==> bool› ‹(<) :: 'a ==> 'a ==> bool›
  rewrites ‹lex_preordering.lex_less_eq (≤) (<) = ((≤) :: 'a list ==> 'a list ==> bool)›
    and ‹lex_preordering.lex_less (≤) (<) = ((<) :: 'a list ==> 'a list ==> bool)›
proof -
  interpret lex_ordering ‹(≤) :: 'a ==> 'a ==> bool› ‹(<) :: 'a ==> 'a ==> bool› ..
  show ‹lex_ordering ((≤) :: 'a ==> 'a ==> bool) (<)\›
    by (fact lex_ordering_axioms)
  show ‹lex_preordering.lex_less_eq (≤) (<) = (≤)›
    by (simp add: less_eq_list_def)
  show ‹lex_preordering.lex_less (≤) (<) = (<)\›
    by (simp add: less_list_def)
qed

instance list :: (order) order
  by (rule order.intro_of_class, rule ordering_orderI, fact lex.ordering)


subsection ‹Non-canonical instance›

context comm_monoid_mult
begin

definition dvd_strict :: ‹'a ==> 'a ==> bool›
  where ‹dvd_strict a b ⟷ a dvd b ∧ ¬ b dvd a›

end

global_interpretation dvd: lex_preordering ‹(dvd) :: 'a::comm_monoid_mult ==> 'a ==> bool› dvd_strict
  defines lex_dvd = dvd.lex_less_eq
    and lex_dvd_strict = dvd.lex_less
  by unfold_locales (auto simp add: dvd_strict_def)

global_interpretation lex_dvd: preordering lex_dvd lex_dvd_strict
  by (fact dvd.preordering)

end