--- 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>
--- 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