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>