Impressum 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 🪙🚫 ==> 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 🪙🚫 ==> 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 🪙🚫 ∨ 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 🪙🚫 ∨ 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 🪙🚫 ∨ 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 🪙🚫 ∨ 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 🪙🚫 ∨ x = y ∧ xs [🪙🚫ys›
  by (auto intro: refl antisym)

lemma less_eq_lex_Cons_iff [simp]:
  ‹x # xs [🪙≤] y # ys ⟷ x 🪙🚫 ∨ 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