Quelle  Lexord.thy   Sprache: Isabelle

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