# HG changeset patch
# User haftmann
# Date 1743502245 -7200
# Node ID 88064da0ae76ac6f98fd3e77585c0b7189a6e166
# Parent  b161057bdd41daa02d931f65e1c951e863041e24
more on sorting

diff -r b161057bdd41 -r 88064da0ae76 src/HOL/Library/Comparator.thy
--- a/src/HOL/Library/Comparator.thy	Tue Apr 01 10:20:14 2025 +0200
+++ b/src/HOL/Library/Comparator.thy	Tue Apr 01 12:10:45 2025 +0200
@@ -188,6 +188,18 @@
 
 end
 
+lemma compare_default_eq_Less_iff [simp]:
+  \<open>compare default x y = Less \<longleftrightarrow> x < y\<close>
+  by transfer simp
+
+lemma compare_default_eq_Equiv_iff [simp]:
+  \<open>compare default x y = Equiv \<longleftrightarrow> x = y\<close>
+  by transfer auto
+
+lemma compare_default_eq_Greater_iff [simp]:
+  \<open>compare default x y = Greater \<longleftrightarrow> x > y\<close>
+  by transfer auto
+
 text \<open>A rudimentary quickcheck setup\<close>
 
 instantiation comparator :: (enum) equal
@@ -237,6 +249,10 @@
     by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
 qed
 
+lemma compare_reversed_apply [simp]:
+  \<open>compare (reversed cmp) x y = compare cmp y x\<close>
+  by transfer simp
+
 lift_definition key :: \<open>('b \<Rightarrow> 'a) \<Rightarrow> 'a comparator \<Rightarrow> 'b comparator\<close>
   is \<open>\<lambda>f cmp a b. cmp (f a) (f b)\<close>
 proof -
@@ -247,6 +263,43 @@
     by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
 qed
 
+lemma compare_key_apply [simp]:
+  \<open>compare (key f cmp) x y = compare cmp (f x) (f y)\<close>
+  by transfer simp
+
+lift_definition prod_lex :: \<open>'a comparator \<Rightarrow> 'b comparator \<Rightarrow> ('a \<times> 'b) comparator\<close>
+  is \<open>\<lambda>f g (a, c) (b, d). case f a b of Less \<Rightarrow> Less | Equiv \<Rightarrow> g c d | Greater \<Rightarrow> Greater\<close>
+proof -
+  fix f :: \<open>'a \<Rightarrow> 'a \<Rightarrow> comp\<close> and g :: \<open>'b \<Rightarrow> 'b \<Rightarrow> comp\<close>
+  assume \<open>comparator f\<close>
+  then interpret f: comparator f .
+  assume \<open>comparator g\<close>
+  then interpret g: comparator g .
+  define h where \<open>h = (\<lambda>(a, c) (b, d). case f a b of Less \<Rightarrow> Less | Equiv \<Rightarrow> g c d | Greater \<Rightarrow> Greater)\<close>
+  then have h_apply [simp]: \<open>h (a, c) (b, d) = (case f a b of Less \<Rightarrow> Less | Equiv \<Rightarrow> g c d | Greater \<Rightarrow> Greater)\<close> for a b c d
+    by simp
+  have h_equiv: \<open>h p q = Equiv \<longleftrightarrow> f (fst p) (fst q) = Equiv \<and> g (snd p) (snd q) = Equiv\<close> for p q
+    by (cases p; cases q) (simp split: comp.split)
+  have h_less: \<open>h p q = Less \<longleftrightarrow> f (fst p) (fst q) = Less \<or> f (fst p) (fst q) = Equiv \<and> g (snd p) (snd q) = Less\<close> for p q
+    by (cases p; cases q) (simp split: comp.split)
+  have h_greater: \<open>h p q = Greater \<longleftrightarrow> f (fst p) (fst q) = Greater \<or> f (fst p) (fst q) = Equiv \<and> g (snd p) (snd q) = Greater\<close> for p q
+    by (cases p; cases q) (simp split: comp.split)
+  have \<open>comparator h\<close>
+    apply standard
+       apply (simp_all add: h_equiv h_less h_greater f.greater_iff_sym_less g.greater_iff_sym_less f.sym g.sym)
+      apply (auto intro: f.trans_equiv g.trans_equiv f.trans_less g.trans_less f.trans_less_equiv f.trans_equiv_less)
+    done
+  then show \<open>comparator (\<lambda>(a, c) (b, d). case f a b of Less \<Rightarrow> Less
+    | Equiv \<Rightarrow> g c d
+    | Greater \<Rightarrow> Greater)\<close>
+    by (simp add: h_def)
+qed
+
+lemma compare_prod_lex_apply:
+  \<open>compare (prod_lex cmp1 cmp2) p q =
+    (case compare (key fst cmp1) p q of Less \<Rightarrow> Less | Equiv \<Rightarrow> compare (key snd cmp2) p q | Greater \<Rightarrow> Greater)\<close>
+  by transfer (simp add: split_def)
+
 
 subsection \<open>Direct implementations for linear orders on selected types\<close>
 
@@ -257,7 +310,7 @@
   \<open>compare comparator_bool = (\<lambda>p q.
     if p then if q then Equiv else Greater
     else if q then Less else Equiv)\<close>
-  by (auto simp add: fun_eq_iff) (transfer; simp)+
+  by (auto simp add: fun_eq_iff)
 
 definition raw_comparator_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> comp\<close>
   where [simp]: \<open>raw_comparator_nat = compare default\<close>
diff -r b161057bdd41 -r 88064da0ae76 src/HOL/Library/Sorting_Algorithms.thy
--- a/src/HOL/Library/Sorting_Algorithms.thy	Tue Apr 01 10:20:14 2025 +0200
+++ b/src/HOL/Library/Sorting_Algorithms.thy	Tue Apr 01 12:10:45 2025 +0200
@@ -667,4 +667,89 @@
 
 end
 
+
+subsection \<open>Lexicographic products\<close>
+
+lemma sorted_prod_lex_imp_sorted_fst:
+  \<open>sorted (key fst cmp1) ps\<close> if \<open>sorted (prod_lex cmp1 cmp2) ps\<close>
+using that proof (induction rule: sorted_induct)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons p ps)
+  have \<open>compare (key fst cmp1) p q \<noteq> Greater\<close> if \<open>ps = q # qs\<close> for q qs
+    using that Cons.hyps(2) [of q] by (simp add: compare_prod_lex_apply split: comp.splits)
+  with Cons.IH show ?case
+    by (rule sorted_ConsI) simp
+qed
+
+lemma sorted_prod_lex_imp_sorted_snd:
+  \<open>sorted (key snd cmp2) ps\<close> if \<open>sorted (prod_lex cmp1 cmp2) ps\<close> \<open>\<And>a' b'. (a', b') \<in> set ps \<Longrightarrow> compare cmp1 a a' = Equiv\<close>
+using that proof (induction rule: sorted_induct)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons p ps)
+  then show ?case 
+    apply (cases p)
+    apply (rule sorted_ConsI)
+     apply (simp_all add: compare_prod_lex_apply)
+     apply (auto cong del: comp.case_cong_weak)
+    apply (metis comp.simps(8) compare.equiv_subst_left)
+    done
+qed
+
+lemma sort_comp_fst_snd_eq_sort_prod_lex:
+  \<open>sort (key fst cmp1) \<circ> sort (key snd cmp2) = sort (prod_lex cmp1 cmp2)\<close>  (is \<open>sort ?cmp1 \<circ> sort ?cmp2 = sort ?cmp\<close>)
+proof
+  fix ps :: \<open>('a \<times> 'b) list\<close>
+  have \<open>sort ?cmp1 (sort ?cmp2 ps) = sort ?cmp ps\<close>
+  proof (rule sort_eqI)
+    show \<open>mset (sort ?cmp2 ps) = mset (sort ?cmp ps)\<close>
+      by simp
+    show \<open>sorted ?cmp1 (sort ?cmp ps)\<close>
+      by (rule sorted_prod_lex_imp_sorted_fst [of _ cmp2]) simp
+  next
+    fix p :: \<open>'a \<times> 'b\<close>
+    define a b where ab: \<open>a = fst p\<close> \<open>b = snd p\<close>
+    moreover assume \<open>p \<in> set (sort ?cmp2 ps)\<close>
+    ultimately have \<open>(a, b) \<in> set (sort ?cmp2 ps)\<close>
+      by simp
+    let ?qs = \<open>filter (\<lambda>(a', _). compare cmp1 a a' = Equiv) ps\<close>
+    have \<open>sort ?cmp2 ?qs = sort ?cmp ?qs\<close>
+    proof (rule sort_eqI)
+      show \<open>mset ?qs = mset (sort ?cmp ?qs)\<close>
+        by simp
+      show \<open>sorted ?cmp2 (sort ?cmp ?qs)\<close>
+        by (rule sorted_prod_lex_imp_sorted_snd) auto
+    next
+      fix q :: \<open>'a \<times> 'b\<close>
+      define c d where \<open>c = fst q\<close> \<open>d = snd q\<close>
+      moreover assume \<open>q \<in> set ?qs\<close>
+      ultimately have \<open>(c, d) \<in> set ?qs\<close>
+        by simp
+      from sorted_stable_segment [of ?cmp \<open>(a, d)\<close> ps]
+      have \<open>sorted ?cmp (filter (\<lambda>(c, b). compare (prod_lex cmp1 cmp2) (a, d) (c, b) = Equiv) ps)\<close>
+        by (simp only: case_prod_unfold prod.collapse)
+      also have \<open>(\<lambda>(c, b). compare (prod_lex cmp1 cmp2) (a, d) (c, b) = Equiv) =
+        (\<lambda>(c, b). compare cmp1 a c = Equiv \<and> compare cmp2 d b = Equiv)\<close>
+        by (simp add: fun_eq_iff compare_prod_lex_apply split: comp.split)
+      finally have *: \<open>sorted ?cmp (filter (\<lambda>(c, b). compare cmp1 a c = Equiv \<and> compare cmp2 d b = Equiv) ps)\<close> .
+      let ?rs = \<open>filter (\<lambda>(_, d'). compare cmp2 d d' = Equiv) ?qs\<close>
+      have \<open>sort ?cmp ?rs = ?rs\<close>
+        by (rule sort_eqI) (use * in \<open>simp_all add: case_prod_unfold\<close>)
+      then show \<open>filter (\<lambda>r. compare ?cmp2 q r = Equiv) ?qs =
+        filter (\<lambda>r. compare ?cmp2 q r = Equiv) (sort ?cmp ?qs)\<close>
+        by (simp add: filter_sort case_prod_unfold flip: \<open>d = snd q\<close>)
+    qed      
+    then show \<open>filter (\<lambda>q. compare ?cmp1 p q = Equiv) (sort ?cmp2 ps) =
+      filter (\<lambda>q. compare ?cmp1 p q = Equiv) (sort ?cmp ps)\<close>
+      by (simp add: filter_sort case_prod_unfold flip: ab)
+  qed
+  then show \<open>(sort (key fst cmp1) \<circ> sort (key snd cmp2)) ps = sort (prod_lex cmp1 cmp2) ps\<close>
+    by simp
+qed
+
 end