src/HOL/Library/Lexord.thy

added lemmas image_mset_eq_{image_mset_plus,plus,plus_image_mset}D, and multp_image_mset_image_msetD

section \<open>Lexicographic orderings\<close>

theory Lexord
  imports Main
begin

subsection \<open>The preorder case\<close>

locale lex_preordering = preordering
begin

inductive lex_less :: \<open>'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close>  (infix \<open>[\<^bold><]\<close> 50) 
where
  Nil: \<open>[] [\<^bold><] y # ys\<close>
| Cons: \<open>x \<^bold>< y \<Longrightarrow> x # xs [\<^bold><] y # ys\<close>
| Cons_eq: \<open>x \<^bold>\<le> y \<Longrightarrow> y \<^bold>\<le> x \<Longrightarrow> xs [\<^bold><] ys \<Longrightarrow> x # xs [\<^bold><] y # ys\<close>

inductive lex_less_eq :: \<open>'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close>  (infix \<open>[\<^bold>\<le>]\<close> 50)
where
  Nil: \<open>[] [\<^bold>\<le>] ys\<close>
| Cons: \<open>x \<^bold>< y \<Longrightarrow> x # xs [\<^bold>\<le>] y # ys\<close>
| Cons_eq: \<open>x \<^bold>\<le> y \<Longrightarrow> y \<^bold>\<le> x \<Longrightarrow> xs [\<^bold>\<le>] ys \<Longrightarrow> x # xs [\<^bold>\<le>] y # ys\<close>

lemma lex_less_simps [simp]:
  \<open>[] [\<^bold><] y # ys\<close>
  \<open>\<not> xs [\<^bold><] []\<close>
  \<open>x # xs [\<^bold><] y # ys \<longleftrightarrow> x \<^bold>< y \<or> x \<^bold>\<le> y \<and> y \<^bold>\<le> x \<and> xs [\<^bold><] ys\<close>
  by (auto intro: lex_less.intros elim: lex_less.cases)

lemma lex_less_eq_simps [simp]:
  \<open>[] [\<^bold>\<le>] ys\<close>
  \<open>\<not> x # xs [\<^bold>\<le>] []\<close>
  \<open>x # xs [\<^bold>\<le>] y # ys \<longleftrightarrow> x \<^bold>< y \<or> x \<^bold>\<le> y \<and> y \<^bold>\<le> x \<and> xs [\<^bold>\<le>] ys\<close>
  by (auto intro: lex_less_eq.intros elim: lex_less_eq.cases)

lemma lex_less_code [code]:
  \<open>[] [\<^bold><] y # ys \<longleftrightarrow> True\<close>
  \<open>xs [\<^bold><] [] \<longleftrightarrow> False\<close>
  \<open>x # xs [\<^bold><] y # ys \<longleftrightarrow> x \<^bold>< y \<or> x \<^bold>\<le> y \<and> y \<^bold>\<le> x \<and> xs [\<^bold><] ys\<close>
  by simp_all

lemma lex_less_eq_code [code]:
  \<open>[] [\<^bold>\<le>] ys \<longleftrightarrow> True\<close>
  \<open>x # xs [\<^bold>\<le>] [] \<longleftrightarrow> False\<close>
  \<open>x # xs [\<^bold>\<le>] y # ys \<longleftrightarrow> x \<^bold>< y \<or> x \<^bold>\<le> y \<and> y \<^bold>\<le> x \<and> xs [\<^bold>\<le>] ys\<close>
  by simp_all

lemma preordering:
  \<open>preordering ([\<^bold>\<le>]) ([\<^bold><])\<close>
proof
  fix xs ys zs
  show \<open>xs [\<^bold>\<le>] xs\<close>
    by (induction xs) (simp_all add: refl)
  show \<open>xs [\<^bold>\<le>] zs\<close> if \<open>xs [\<^bold>\<le>] ys\<close> \<open>ys [\<^bold>\<le>] zs\<close>
  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 \<open>xs [\<^bold><] ys \<longleftrightarrow> xs [\<^bold>\<le>] ys \<and> \<not> ys [\<^bold>\<le>] xs\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
  proof
    assume ?P
    then have \<open>xs [\<^bold>\<le>] ys\<close>
      by induction simp_all
    moreover have \<open>\<not> ys [\<^bold>\<le>] xs\<close>
      using \<open>?P\<close>
      by induction (simp_all, simp_all add: strict_iff_not asym)
    ultimately show ?Q ..
  next
    assume ?Q
    then have \<open>xs [\<^bold>\<le>] ys\<close> \<open>\<not> ys [\<^bold>\<le>] xs\<close>
      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 \<open>([\<^bold>\<le>])\<close> \<open>([\<^bold><])\<close>
  by (fact preordering)

end


subsection \<open>The order case\<close>

locale lex_ordering = lex_preordering + ordering
begin

interpretation lex: preordering \<open>([\<^bold>\<le>])\<close> \<open>([\<^bold><])\<close>
  by (fact preordering)

lemma less_lex_Cons_iff [simp]:
  \<open>x # xs [\<^bold><] y # ys \<longleftrightarrow> x \<^bold>< y \<or> x = y \<and> xs [\<^bold><] ys\<close>
  by (auto intro: refl antisym)

lemma less_eq_lex_Cons_iff [simp]:
  \<open>x # xs [\<^bold>\<le>] y # ys \<longleftrightarrow> x \<^bold>< y \<or> x = y \<and> xs [\<^bold>\<le>] ys\<close>
  by (auto intro: refl antisym)

lemma ordering:
  \<open>ordering ([\<^bold>\<le>]) ([\<^bold><])\<close>
proof
  fix xs ys
  show *: \<open>xs = ys\<close> if \<open>xs [\<^bold>\<le>] ys\<close> \<open>ys [\<^bold>\<le>] xs\<close>
  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 \<open>xs [\<^bold><] ys \<longleftrightarrow> xs [\<^bold>\<le>] ys \<and> xs \<noteq> ys\<close>
    by (auto simp add: lex.strict_iff_not dest: *)
qed

interpretation lex: ordering \<open>([\<^bold>\<le>])\<close> \<open>([\<^bold><])\<close>
  by (fact ordering)

end


subsection \<open>Canonical instance\<close>

instantiation list :: (preorder) preorder
begin

global_interpretation lex: lex_preordering \<open>(\<le>) :: 'a::preorder \<Rightarrow> 'a \<Rightarrow> bool\<close> \<open>(<) :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>
  defines less_eq_list = lex.lex_less_eq
    and less_list = lex.lex_less ..

instance
  by (rule class.preorder.of_class.intro, rule preordering_preorderI, fact lex.preordering)

end

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

instance list :: (order) order
  by (rule class.order.of_class.intro, rule ordering_orderI, fact lex.ordering)

export_code \<open>(\<le>) :: _ list \<Rightarrow> _ list \<Rightarrow> bool\<close> \<open>(<) :: _ list \<Rightarrow> _ list \<Rightarrow> bool\<close> in Haskell


subsection \<open>Non-canonical instance\<close>

context comm_monoid_mult
begin

definition dvd_strict :: \<open>'a \<Rightarrow> 'a \<Rightarrow> bool\<close>
  where \<open>dvd_strict a b \<longleftrightarrow> a dvd b \<and> \<not> b dvd a\<close>

end

global_interpretation dvd: lex_preordering \<open>(dvd) :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> bool\<close> 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)

definition \<open>example = lex_dvd [(4::int), - 7, 8] [- 8, 13, 5]\<close>

export_code example in Haskell

value example

end