# HG changeset patch
# User haftmann
# Date 1622637927 0
# Node ID e75635a0bafd22d334f7cff6a81f822900ea320e
# Parent  26c0ccf17f318614a645ec9136edea1e845989e2
lexorders the locale way

diff -r 26c0ccf17f31 -r e75635a0bafd src/HOL/Library/Lexord.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Lexord.thy	Wed Jun 02 12:45:27 2021 +0000
@@ -0,0 +1,208 @@
+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
+  apply (rule lex_preordering.intro)
+  apply standard
+    apply (auto simp add: dvd_strict_def)
+  done
+
+print_theorems
+
+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
diff -r 26c0ccf17f31 -r e75635a0bafd src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Orderings.thy	Wed Jun 02 12:45:27 2021 +0000
@@ -279,6 +279,16 @@
 
 end
 
+lemma preordering_preorderI:
+  \<open>class.preorder (\<^bold>\<le>) (\<^bold><)\<close> if \<open>preordering (\<^bold>\<le>) (\<^bold><)\<close>
+    for less_eq (infix \<open>\<^bold>\<le>\<close> 50) and less (infix \<open>\<^bold><\<close> 50)
+proof -
+  from that interpret preordering \<open>(\<^bold>\<le>)\<close> \<open>(\<^bold><)\<close> .
+  show ?thesis
+    by standard (auto simp add: strict_iff_not refl intro: trans)
+qed
+
+
 
 subsection \<open>Partial orders\<close>
 
@@ -409,12 +419,12 @@
 qed
 
 lemma order_strictI:
-  fixes less (infix "\<sqsubset>" 50)
-    and less_eq (infix "\<sqsubseteq>" 50)
-  assumes "\<And>a b. a \<sqsubseteq> b \<longleftrightarrow> a \<sqsubset> b \<or> a = b"
-    assumes "\<And>a b. a \<sqsubset> b \<Longrightarrow> \<not> b \<sqsubset> a"
-  assumes "\<And>a. \<not> a \<sqsubset> a"
-  assumes "\<And>a b c. a \<sqsubset> b \<Longrightarrow> b \<sqsubset> c \<Longrightarrow> a \<sqsubset> c"
+  fixes less (infix "\<^bold><" 50)
+    and less_eq (infix "\<^bold>\<le>" 50)
+  assumes "\<And>a b. a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>< b \<or> a = b"
+    assumes "\<And>a b. a \<^bold>< b \<Longrightarrow> \<not> b \<^bold>< a"
+  assumes "\<And>a. \<not> a \<^bold>< a"
+  assumes "\<And>a b c. a \<^bold>< b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
   shows "class.order less_eq less"
   by (rule ordering_orderI) (rule ordering_strictI, (fact assms)+)