# HG changeset patch
# User wenzelm
# Date 1665665355 -7200
# Node ID e381884c09d4f47e5b7d28c1dd43361fe82abd1c
# Parent  2d4ff8c166d299d3b16e63fe6084567964584d3b# Parent  cee0b9fccf6f075e3083f4cb4df30c1e128ce697
merged

diff -r 2d4ff8c166d2 -r e381884c09d4 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Oct 13 11:22:32 2022 +0200
+++ b/Admin/components/components.sha1	Thu Oct 13 14:49:15 2022 +0200
@@ -374,6 +374,8 @@
 33568f69ce813b7405386ddbefa14ad0342bb8f0 polyml-test-a3cfdf648da.tar.gz
 4bedaac4f1fb9a9199aa63695735063c47059003 polyml-test-a444f281ccec.tar.gz
 f3031692edcc5d8028a42861e4e40779f0f9d3e1 polyml-test-b68438d33c69.tar.gz
+b2901b604124cfe46a6c28041f47c5a3bd3673f0 polyml-test-bafe319bc3a6-1.tar.gz
+3ac7e916832c07accebeada9a81b301c299e1930 polyml-test-bafe319bc3a6.tar.gz
 cb2318cff6ea9293cd16a4435a4fe28ad9dbe0b8 polyml-test-cf46747fee61.tar.gz
 67ffed2f98864721bdb1e87f0ef250e4c69e6160 polyml-test-d68c6736402e.tar.gz
 b4ceeaac47f3baae41c2491a8368b03217946166 polyml-test-e7a662f8f9c4.tar.gz
diff -r 2d4ff8c166d2 -r e381884c09d4 CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Oct 13 11:22:32 2022 +0200
+++ b/CONTRIBUTORS	Thu Oct 13 14:49:15 2022 +0200
@@ -3,6 +3,10 @@
 listed as an author in one of the source files of this Isabelle distribution.
 
 
+Contributions to this Isabelle version
+--------------------------------------
+
+
 Contributions to Isabelle2022
 -----------------------------
 
diff -r 2d4ff8c166d2 -r e381884c09d4 NEWS
--- a/NEWS	Thu Oct 13 11:22:32 2022 +0200
+++ b/NEWS	Thu Oct 13 14:49:15 2022 +0200
@@ -4,6 +4,38 @@
 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
 
 
+New in this Isabelle version
+----------------------------
+
+*** HOL ***
+
+* Theory "HOL.Relation":
+  - Strengthened lemma total_on_singleton. Minor INCOMPATIBILITY.
+  - Added lemmas.
+      antisym_if_asymp
+      antisymp_ge[simp]
+      antisymp_greater[simp]
+      antisymp_if_asymp
+      antisymp_le[simp]
+      antisymp_less[simp]
+      irreflD
+      irreflpD
+      reflp_ge[simp]
+      reflp_le[simp]
+      totalp_on_singleton[simp]
+
+* Theory "HOL.Wellfounded":
+  - Added lemmas.
+      wfP_if_convertible_to_nat
+      wfP_if_convertible_to_wfP
+      wf_if_convertible_to_wf
+
+* Theory "HOL-Library.FSet":
+  - Added lemmas.
+      fimage_strict_mono
+      inj_on_strict_fsubset
+
+
 New in Isabelle2022 (October 2022)
 ----------------------------------
 
diff -r 2d4ff8c166d2 -r e381884c09d4 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Thu Oct 13 14:49:15 2022 +0200
@@ -3985,9 +3985,9 @@
       by simp
   next
     case False
-    then show ?thesis
-      by (cases y \<open>smult a (x div y)\<close> \<open>smult a (x mod y)\<close> \<open>smult a x\<close> rule: euclidean_relation_polyI)
-        (simp_all add: dvd_smult_iff degree_mod_less_degree flip: smult_add_right)
+    show ?thesis
+      by (rule euclidean_relation_polyI)
+        (use False in \<open>simp_all add: dvd_smult_iff degree_mod_less_degree flip: smult_add_right\<close>)
   qed
   then show ?Q and ?R
     by simp_all
@@ -4006,7 +4006,7 @@
   for x y z :: \<open>'a::field poly\<close>
 proof -
   have \<open>((x + y) div z, (x + y) mod z) = (x div z + y div z, x mod z + y mod z)\<close>
-  proof (cases z \<open>x div z + y div z\<close> \<open>x mod z + y mod z\<close> \<open>x + y\<close> rule: euclidean_relation_polyI)
+  proof (induction rule: euclidean_relation_polyI)
     case by0
     then show ?case by simp
   next
@@ -4045,7 +4045,7 @@
   and mod_smult_right: \<open>x mod smult a y = (if a = 0 then x else x mod y)\<close> (is ?R)
 proof -
   have \<open>(x div smult a y, x mod smult a y) = (smult (inverse a) (x div y), (if a = 0 then x else x mod y))\<close>
-  proof (cases \<open>smult a y\<close> \<open>smult (inverse a) (x div y)\<close> \<open>(if a = 0 then x else x mod y)\<close> x rule: euclidean_relation_polyI)
+  proof (induction rule: euclidean_relation_polyI)
     case by0
     then show ?case by auto
   next
@@ -4077,7 +4077,7 @@
   for x y z :: \<open>'a::field poly\<close>
 proof -
   have \<open>(x div (y * z), x mod (y * z)) = ((x div y) div z, y * (x div y mod z) + x mod y)\<close>
-  proof (cases \<open>y * z\<close> \<open>(x div y) div z\<close> \<open>y * (x div y mod z) + x mod y\<close> x rule: euclidean_relation_polyI)
+  proof (induction rule: euclidean_relation_polyI)
     case by0
     then show ?case by auto
   next
@@ -4143,7 +4143,7 @@
     define b where \<open>b = coeff (pCons a (p mod q)) (degree q) / lead_coeff q\<close>
     have \<open>(pCons a p div q, pCons a p mod q) =
       (pCons b (p div q), (pCons a (p mod q) - smult b q))\<close> (is \<open>_ = (?q, ?r)\<close>)
-    proof (cases q ?q ?r \<open>pCons a p\<close> rule: euclidean_relation_polyI)
+    proof (induction rule: euclidean_relation_polyI)
       case by0
       with \<open>q \<noteq> 0\<close> show ?case by simp
     next
diff -r 2d4ff8c166d2 -r e381884c09d4 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/HOL/Euclidean_Division.thy	Thu Oct 13 14:49:15 2022 +0200
@@ -672,7 +672,7 @@
   fix a b c
   assume \<open>b \<noteq> 0\<close>
   have \<open>((a + c * b) div b, (a + c * b) mod b) = (c + a div b, a mod b)\<close>
-  proof (cases b \<open>c + a div b\<close> \<open>a mod b\<close> \<open>a + c * b\<close> rule: euclidean_relationI)
+  proof (induction rule: euclidean_relationI)
     case by0
     with \<open>b \<noteq> 0\<close>
     show ?case
@@ -698,7 +698,7 @@
   fix a b c
   assume \<open>c \<noteq> 0\<close>
   have \<open>((c * a) div (c * b), (c * a) mod (c * b)) = (a div b, c * (a mod b))\<close>
-  proof (cases \<open>c * b\<close> \<open>a div b\<close> \<open>c * (a mod b)\<close> \<open>c * a\<close> rule: euclidean_relationI)
+  proof (induction rule: euclidean_relationI)
     case by0
     with \<open>c \<noteq> 0\<close> show ?case
       by simp
@@ -745,7 +745,7 @@
   next
     assume \<open>euclidean_size a < euclidean_size b\<close>
     have \<open>(a div b, a mod b) = (0, a)\<close>
-    proof (cases b 0 a a rule: euclidean_relationI)
+    proof (induction rule: euclidean_relationI)
       case by0
       show ?case
         by simp
@@ -783,7 +783,7 @@
       by (simp add: algebra_simps)
   qed
   have \<open>((a * b) div c, (a * b) mod c) = (a * (b div c) + a * (b mod c) div c, (a * b) mod c)\<close>
-  proof (cases c \<open>a * (b div c) + a * (b mod c) div c\<close> \<open>(a * b) mod c\<close> \<open>a * b\<close> rule: euclidean_relationI)
+  proof (induction rule: euclidean_relationI)
     case by0
     then show ?case by simp
   next
@@ -817,7 +817,7 @@
       by (simp add: mod_mult_div_eq)
   qed
   have \<open>((a + b) div c, (a + b) mod c) = (a div c + b div c + (a mod c + b mod c) div c, (a + b) mod c)\<close>
-  proof (cases c \<open>a div c + b div c + (a mod c + b mod c) div c\<close> \<open>(a + b) mod c\<close> \<open>a + b\<close> rule: euclidean_relationI)
+  proof (induction rule: euclidean_relationI)
     case by0
     then show ?case
       by simp
@@ -978,7 +978,7 @@
   \<open>m div n = q\<close> if \<open>n * q \<le> m\<close> and \<open>m < n * Suc q\<close> for m n q :: nat
 proof -
   have \<open>(m div n, m mod n) = (q, m - n * q)\<close>
-  proof (cases n q \<open>m - n * q\<close>  m rule: euclidean_relation_natI)
+  proof (induction rule: euclidean_relation_natI)
     case by0
     with that show ?case
       by simp
@@ -1004,7 +1004,7 @@
   \<open>m mod n = r\<close> if \<open>r < n\<close> and \<open>r \<le> m\<close> and \<open>n dvd m - r\<close> for m n r :: nat
 proof -
   have \<open>(m div n, m mod n) = ((m - r) div n, r)\<close>
-  proof (cases n \<open>(m - r) div n\<close> r  m rule: euclidean_relation_natI)
+  proof (induction rule: euclidean_relation_natI)
     case by0
     with that show ?case
       by simp
@@ -1268,7 +1268,7 @@
   for m n q :: nat
 proof -
   have \<open>(m div (n * q), m mod (n * q)) = ((m div n) div q, n * (m div n mod q) + m mod n)\<close>
-  proof (cases \<open>n * q\<close> \<open>(m div n) div q\<close> \<open>n * (m div n mod q) + m mod n\<close> m rule: euclidean_relation_natI)
+  proof (induction rule: euclidean_relation_natI)
     case by0
     then show ?case
       by auto
@@ -1411,7 +1411,7 @@
   using div_less_iff_less_mult [of q n m] that by auto
 
 lemma div_Suc:
-  \<open>Suc m div n = (if Suc m mod n = 0 then Suc (m div n) else m div n)\<close>  (is "_ = ?rhs")
+  \<open>Suc m div n = (if Suc m mod n = 0 then Suc (m div n) else m div n)\<close>
 proof (cases \<open>n = 0 \<or> n = 1\<close>)
   case True
   then show ?thesis by auto
@@ -1419,34 +1419,15 @@
   case False
   then have \<open>n > 1\<close>
     by simp
-  then have *: \<open>Suc 0 div n = 0\<close>
-    by (simp add: div_eq_0_iff)
-  have \<open>(m + 1) div n = ?rhs\<close>
+  then have \<open>Suc m div n = m div n + Suc (m mod n) div n\<close>
+    using div_add1_eq [of m 1 n] by simp
+  also have \<open>Suc (m mod n) div n = of_bool (n dvd Suc m)\<close>
   proof (cases \<open>n dvd Suc m\<close>)
-    case True
-    then obtain q where \<open>Suc m = n * q\<close> ..
-    then have m: \<open>m = n * q - 1\<close>
-      by simp
-    have \<open>q > 0\<close> by (rule ccontr)
-      (use \<open>Suc m = n * q\<close> in simp)
-    from m have \<open>m mod n = (n * q - 1) mod n\<close>
-      by simp
-    also have \<open>\<dots> = (n * q - 1 + n) mod n\<close>
-      by simp
-    also have \<open>n * q - 1 + n = n * q + (n - 1)\<close>
-      using \<open>n > 1\<close> \<open>q > 0\<close> by (simp add: algebra_simps)
-    finally have \<open>m mod n = (n - 1) mod n\<close>
-      by simp
-    with \<open>n > 1\<close> have \<open>m mod n = n - 1\<close>
-      by simp
-    with True \<open>n > 1\<close> show ?thesis
-      by (subst div_add1_eq) auto
-  next
     case False
-    have \<open>Suc (m mod n) \<noteq> n\<close>
+    moreover have \<open>Suc (m mod n) \<noteq> n\<close>
     proof (rule ccontr)
       assume \<open>\<not> Suc (m mod n) \<noteq> n\<close>
-      then have \<open>m mod n = n - 1\<close>
+      then have \<open>m mod n = n - Suc 0\<close>
         by simp
       with \<open>n > 1\<close> have \<open>(m + 1) mod n = 0\<close>
         by (subst mod_add_left_eq [symmetric]) simp
@@ -1456,28 +1437,35 @@
     qed
     moreover have \<open>Suc (m mod n) \<le> n\<close>
       using \<open>n > 1\<close> by (simp add: Suc_le_eq)
-    ultimately have \<open>Suc (m mod n) < n\<close>
+    ultimately show ?thesis
+      by (simp add: div_eq_0_iff)
+  next
+    case True
+    then obtain q where q: \<open>Suc m = n * q\<close> ..
+    moreover have \<open>q > 0\<close> by (rule ccontr)
+      (use q in simp)
+    ultimately have \<open>m mod n = n - Suc 0\<close>
+      using \<open>n > 1\<close> mult_le_cancel1 [of n \<open>Suc 0\<close> q]
+      by (auto intro: mod_nat_eqI)
+    with True \<open>n > 1\<close> show ?thesis
       by simp
-    with False \<open>n > 1\<close> show ?thesis
-      by (subst div_add1_eq) (auto simp add: div_eq_0_iff mod_greater_zero_iff_not_dvd)
   qed
-  then show ?thesis
-    by simp
+  finally show ?thesis
+    by (simp add: mod_greater_zero_iff_not_dvd)
 qed
 
 lemma mod_Suc:
-  \<open>Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))\<close>  (is "_ = ?rhs")
-proof (cases "n = 0")
+  \<open>Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))\<close>
+proof (cases \<open>n = 0\<close>)
   case True
   then show ?thesis
     by simp
 next
   case False
-  have "Suc m mod n = Suc (m mod n) mod n"
+  moreover have \<open>Suc m mod n = Suc (m mod n) mod n\<close>
     by (simp add: mod_simps)
-  also have "\<dots> = ?rhs"
-    using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
-  finally show ?thesis .
+  ultimately show ?thesis
+    by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
 qed
 
 lemma Suc_times_mod_eq:
@@ -1948,7 +1936,7 @@
     and divides': \<open>l \<noteq> 0 \<Longrightarrow> l dvd k \<Longrightarrow> r = 0 \<and> k = q * l\<close>
     and euclidean_relation': \<open>l \<noteq> 0 \<Longrightarrow> \<not> l dvd k \<Longrightarrow> sgn r = sgn l
       \<and> \<bar>r\<bar> < \<bar>l\<bar> \<and> k = q * l + r\<close> for k l :: int
-proof (cases l q r k rule: euclidean_relationI)
+proof (induction rule: euclidean_relationI)
   case by0
   then show ?case
     by (rule by0')
@@ -2274,7 +2262,7 @@
   from that have \<open>l < 0\<close>
     by simp
   have \<open>(k div l, k mod l) = (- 1, k + l)\<close>
-  proof (cases l \<open>- 1 :: int\<close> \<open>k + l\<close> k rule: euclidean_relation_intI)
+  proof (induction rule: euclidean_relation_intI)
     case by0
     with \<open>l < 0\<close> show ?case
       by simp
@@ -2316,9 +2304,9 @@
     and int_mod_pos_eq:
       \<open>a mod b = r\<close> (is ?R)
 proof -
-  from assms have \<open>(a div b, a mod b) = (q, r)\<close>
-    by (cases b q r a rule: euclidean_relation_intI)
-      (auto simp add: ac_simps dvd_add_left_iff sgn_1_pos le_less dest: zdvd_imp_le)
+  have \<open>(a div b, a mod b) = (q, r)\<close>
+    by (induction rule: euclidean_relation_intI)
+      (use assms in \<open>auto simp add: ac_simps dvd_add_left_iff sgn_1_pos le_less dest: zdvd_imp_le\<close>)
   then show ?Q and ?R
     by simp_all
 qed
@@ -2868,7 +2856,7 @@
   if \<open>0 \<le> a\<close> for a b :: int
 proof -
   have \<open>((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = (b div a, 1 + 2 * (b mod a))\<close>
-  proof (cases \<open>2 * a\<close> \<open>b div a\<close> \<open>1 + 2 * (b mod a)\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI)
+  proof (induction rule: euclidean_relation_intI)
     case by0
     then show ?case
       by simp
@@ -2908,7 +2896,7 @@
   if \<open>a \<le> 0\<close> for a b :: int
 proof -
   have \<open>((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = ((b + 1) div a, 2 * ((b + 1) mod a) - 1)\<close>
-  proof (cases \<open>2 * a\<close> \<open>(b + 1) div a\<close> \<open>2 * ((b + 1) mod a) - 1\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI)
+  proof (induction rule: euclidean_relation_intI)
     case by0
     then show ?case
       by simp
diff -r 2d4ff8c166d2 -r e381884c09d4 src/HOL/Examples/Gauss_Numbers.thy
--- a/src/HOL/Examples/Gauss_Numbers.thy	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/HOL/Examples/Gauss_Numbers.thy	Thu Oct 13 14:49:15 2022 +0200
@@ -311,18 +311,94 @@
     \<open>Re (x div y) = (Re x * Re y + Im x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
   | \<open>Im (x div y) = (Im x * Re y - Re x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
 
-definition modulo_gauss :: \<open>gauss \<Rightarrow> gauss \<Rightarrow> gauss\<close>
+primcorec modulo_gauss :: \<open>gauss \<Rightarrow> gauss \<Rightarrow> gauss\<close>
   where
-    \<open>x mod y = x - x div y * y\<close> for x y :: gauss
+    \<open>Re (x mod y) = Re x -
+      ((Re x * Re y + Im x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Re y -
+       (Im x * Re y - Re x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Im y)\<close>
+  | \<open>Im (x mod y) = Im x -
+      ((Re x * Re y + Im x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Im y +
+       (Im x * Re y - Re x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Re y)\<close>
+
+instance proof
+  fix x y :: gauss
+  show \<open>x div 0 = 0\<close>
+    by (simp add: gauss_eq_iff)
+  show \<open>x * y div y = x\<close> if \<open>y \<noteq> 0\<close>
+  proof -
+    define Y where \<open>Y = (Re y)\<^sup>2 + (Im y)\<^sup>2\<close>
+    moreover have \<open>Y > 0\<close>
+      using that by (simp add: gauss_eq_0 less_le Y_def)
+    have *: \<open>Im y * (Im y * Re x) + Re x * (Re y * Re y) = Re x * Y\<close>
+      \<open>Im x * (Im y * Im y) + Im x * (Re y * Re y) = Im x * Y\<close>
+      \<open>(Im y)\<^sup>2 + (Re y)\<^sup>2 = Y\<close>
+      by (simp_all add: power2_eq_square algebra_simps Y_def)
+    from \<open>Y > 0\<close> show ?thesis
+      by (simp add: gauss_eq_iff algebra_simps) (simp add: * nonzero_mult_rdiv_cancel_right)
+  qed
+  show \<open>x div y * y + x mod y = x\<close>
+    by (simp add: gauss_eq_iff)
+qed
+
+end
+
+instantiation gauss :: euclidean_ring
+begin
+
+definition euclidean_size_gauss :: \<open>gauss \<Rightarrow> nat\<close>
+  where \<open>euclidean_size x = nat ((Re x)\<^sup>2 + (Im x)\<^sup>2)\<close>
 
-instance
-  apply standard
-  apply (simp_all add: modulo_gauss_def)
-  apply (auto simp add: gauss_eq_iff algebra_simps power2_eq_square)
-           apply (simp_all only: flip: mult.assoc distrib_right)
-       apply (simp_all only: mult.assoc [of \<open>Im k\<close> \<open>Re l\<close> \<open>Re r\<close> for k l r])
-     apply (simp_all add: sum_squares_eq_zero_iff mult.commute nonzero_mult_rdiv_cancel_right flip: distrib_left)
-  done
+instance proof
+  show \<open>euclidean_size (0::gauss) = 0\<close>
+    by (simp add: euclidean_size_gauss_def)
+  show \<open>euclidean_size (x mod y) < euclidean_size y\<close> if \<open>y \<noteq> 0\<close> for x y :: gauss
+  proof-
+    define X and Y and R and I
+      where \<open>X = (Re x)\<^sup>2 + (Im x)\<^sup>2\<close> and \<open>Y = (Re y)\<^sup>2 + (Im y)\<^sup>2\<close>
+        and \<open>R = Re x * Re y + Im x * Im y\<close> and \<open>I = Im x * Re y - Re x * Im y\<close>
+    with that have \<open>0 < Y\<close> and rhs: \<open>int (euclidean_size y) = Y\<close>
+      by (simp_all add: gauss_neq_0 euclidean_size_gauss_def)
+    have \<open>X * Y = R\<^sup>2 + I\<^sup>2\<close>
+      by (simp add: R_def I_def X_def Y_def power2_eq_square algebra_simps)
+    let ?lhs = \<open>X - I * (I rdiv Y) - R * (R rdiv Y)
+        - I rdiv Y * (I rmod Y) - R rdiv Y * (R rmod Y)\<close>
+    have \<open>?lhs = X + Y * (R rdiv Y) * (R rdiv Y) + Y * (I rdiv Y) * (I rdiv Y)
+        - 2 * (R rdiv Y * R + I rdiv Y * I)\<close>
+      by (simp flip: minus_rmod_eq_mult_rdiv add: algebra_simps)
+    also have \<open>\<dots> = (Re (x mod y))\<^sup>2 + (Im (x mod y))\<^sup>2\<close>
+      by (simp add: X_def Y_def R_def I_def algebra_simps power2_eq_square)
+    finally have lhs: \<open>int (euclidean_size (x mod y)) = ?lhs\<close>
+      by (simp add: euclidean_size_gauss_def)
+    have \<open>?lhs * Y = (I rmod Y)\<^sup>2 + (R rmod Y)\<^sup>2\<close>
+      apply (simp add: algebra_simps power2_eq_square \<open>X * Y = R\<^sup>2 + I\<^sup>2\<close>)
+      apply (simp flip: mult.assoc add.assoc minus_rmod_eq_mult_rdiv)
+      apply (simp add: algebra_simps)
+      done
+    also have \<open>\<dots> \<le> (Y div 2)\<^sup>2 + (Y div 2)\<^sup>2\<close>
+      by (rule add_mono) (use \<open>Y > 0\<close> abs_rmod_less_equal [of Y] in \<open>simp_all add: power2_le_iff_abs_le\<close>)
+    also have \<open>\<dots> < Y\<^sup>2\<close>
+      using \<open>Y > 0\<close> by (cases \<open>Y = 1\<close>) (simp_all add: power2_eq_square mult_le_less_imp_less flip: mult.assoc)
+    finally have \<open>?lhs * Y < Y\<^sup>2\<close> .
+    with \<open>Y > 0\<close> have \<open>?lhs < Y\<close>
+      by (simp add: power2_eq_square)
+    then have \<open>int (euclidean_size (x mod y)) < int (euclidean_size y)\<close>
+      by (simp only: lhs rhs)
+    then show ?thesis
+      by simp
+  qed
+  show \<open>euclidean_size x \<le> euclidean_size (x * y)\<close> if \<open>y \<noteq> 0\<close> for x y :: gauss
+  proof -
+    from that have \<open>euclidean_size y > 0\<close>
+      by (simp add: euclidean_size_gauss_def gauss_neq_0)
+    then have \<open>euclidean_size x \<le> euclidean_size x * euclidean_size y\<close>
+      by simp
+    also have \<open>\<dots> = nat (((Re x)\<^sup>2 + (Im x)\<^sup>2) * ((Re y)\<^sup>2 + (Im y)\<^sup>2))\<close>
+      by (simp add: euclidean_size_gauss_def nat_mult_distrib)
+    also have \<open>\<dots> = euclidean_size (x * y)\<close>
+      by (simp add: euclidean_size_gauss_def eq_nat_nat_iff) (simp add: algebra_simps power2_eq_square)
+    finally show ?thesis .
+  qed
+qed
 
 end
 
diff -r 2d4ff8c166d2 -r e381884c09d4 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/HOL/Fun.thy	Thu Oct 13 14:49:15 2022 +0200
@@ -208,7 +208,7 @@
 lemma bij_id[simp]: "bij id"
   by (simp add: bij_betw_def)
 
-lemma bij_uminus: "bij (uminus :: 'a \<Rightarrow> 'a::ab_group_add)"
+lemma bij_uminus: "bij (uminus :: 'a \<Rightarrow> 'a::group_add)"
   unfolding bij_betw_def inj_on_def
   by (force intro: minus_minus [symmetric])
 
@@ -591,9 +591,6 @@
 lemma inj_on_vimage_singleton: "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}"
   by (auto simp add: inj_on_def intro: the_equality [symmetric])
 
-lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
-  by (auto intro!: inj_onI)
-
 lemma bij_betw_byWitness:
   assumes left: "\<forall>a \<in> A. f' (f a) = a"
     and right: "\<forall>a' \<in> A'. f (f' a') = a'"
@@ -696,7 +693,7 @@
 qed
 
 
-subsubsection \<open>Important examples\<close>
+subsubsection \<open>Inj/surj/bij of Algebraic Operations\<close>
 
 context cancel_semigroup_add
 begin
@@ -705,10 +702,6 @@
   "inj_on ((+) a) A"
   by (rule inj_onI) simp
 
-lemma inj_add_left:
-  \<open>inj ((+) a)\<close>
-  by simp
-
 lemma inj_on_add' [simp]:
   "inj_on (\<lambda>b. b + a) A"
   by (rule inj_onI) simp
@@ -719,26 +712,89 @@
 
 end
 
-context ab_group_add
+context group_add
 begin
 
+lemma diff_left_imp_eq: "a - b = a - c \<Longrightarrow> b = c"
+unfolding add_uminus_conv_diff[symmetric]
+by(drule local.add_left_imp_eq) simp
+
+lemma inj_uminus[simp, intro]: "inj_on uminus A"
+  by (auto intro!: inj_onI)
+
+lemma surj_uminus[simp]: "surj uminus"
+using surjI minus_minus by blast
+
 lemma surj_plus [simp]:
   "surj ((+) a)"
-  by (auto intro!: range_eqI [of b "(+) a" "b - a" for b]) (simp add: algebra_simps)
+proof (standard, simp, standard, simp)
+  fix x
+  have "x = a + (-a + x)" by (simp add: add.assoc)
+  thus "x \<in> range ((+) a)" by blast
+qed
+
+lemma surj_plus_right [simp]:
+  "surj (\<lambda>b. b+a)"
+proof (standard, simp, standard, simp)
+  fix b show "b \<in> range (\<lambda>b. b+a)"
+    using diff_add_cancel[of b a, symmetric] by blast
+qed
 
-lemma inj_diff_right [simp]:
-  \<open>inj (\<lambda>b. b - a)\<close>
-proof -
-  have \<open>inj ((+) (- a))\<close>
-    by (fact inj_add_left)
-  also have \<open>(+) (- a) = (\<lambda>b. b - a)\<close>
-    by (simp add: fun_eq_iff)
-  finally show ?thesis .
+lemma inj_on_diff_left [simp]:
+  \<open>inj_on ((-) a) A\<close>
+by (auto intro: inj_onI dest!: diff_left_imp_eq)
+
+lemma inj_on_diff_right [simp]:
+  \<open>inj_on (\<lambda>b. b - a) A\<close>
+by (auto intro: inj_onI simp add: algebra_simps)
+
+lemma surj_diff [simp]:
+  "surj ((-) a)"
+proof (standard, simp, standard, simp)
+  fix x
+  have "x = a - (- x + a)" by (simp add: algebra_simps)
+  thus "x \<in> range ((-) a)" by blast
 qed
 
 lemma surj_diff_right [simp]:
   "surj (\<lambda>x. x - a)"
-  using surj_plus [of "- a"] by (simp cong: image_cong_simp)
+proof (standard, simp, standard, simp)
+  fix x
+  have "x = x + a - a" by simp
+  thus "x \<in> range (\<lambda>x. x - a)" by fast
+qed
+
+lemma shows bij_plus: "bij ((+) a)" and bij_plus_right: "bij (\<lambda>x. x + a)"
+  and bij_uminus: "bij uminus"
+  and bij_diff: "bij ((-) a)" and bij_diff_right: "bij (\<lambda>x. x - a)"
+by(simp_all add: bij_def)
+
+lemma translation_subtract_Compl:
+  "(\<lambda>x. x - a) ` (- t) = - ((\<lambda>x. x - a) ` t)"
+by(rule bij_image_Compl_eq)
+  (auto simp add: bij_def surj_def inj_def diff_eq_eq intro!: add_diff_cancel[symmetric])
+
+lemma translation_diff:
+  "(+) a ` (s - t) = ((+) a ` s) - ((+) a ` t)"
+  by auto
+
+lemma translation_subtract_diff:
+  "(\<lambda>x. x - a) ` (s - t) = ((\<lambda>x. x - a) ` s) - ((\<lambda>x. x - a) ` t)"
+by(rule image_set_diff)(simp add: inj_on_def diff_eq_eq)
+
+lemma translation_Int:
+  "(+) a ` (s \<inter> t) = ((+) a ` s) \<inter> ((+) a ` t)"
+  by auto
+
+lemma translation_subtract_Int:
+  "(\<lambda>x. x - a) ` (s \<inter> t) = ((\<lambda>x. x - a) ` s) \<inter> ((\<lambda>x. x - a) ` t)"
+by(rule image_Int)(simp add: inj_on_def diff_eq_eq)
+
+end
+
+(* TODO: prove in group_add *)
+context ab_group_add
+begin
 
 lemma translation_Compl:
   "(+) a ` (- t) = - ((+) a ` t)"
@@ -748,26 +804,6 @@
     by (auto simp: image_iff algebra_simps intro!: bexI [of _ "b - a"])
 qed
 
-lemma translation_subtract_Compl:
-  "(\<lambda>x. x - a) ` (- t) = - ((\<lambda>x. x - a) ` t)"
-  using translation_Compl [of "- a" t] by (simp cong: image_cong_simp)
-
-lemma translation_diff:
-  "(+) a ` (s - t) = ((+) a ` s) - ((+) a ` t)"
-  by auto
-
-lemma translation_subtract_diff:
-  "(\<lambda>x. x - a) ` (s - t) = ((\<lambda>x. x - a) ` s) - ((\<lambda>x. x - a) ` t)"
-  using translation_diff [of "- a"] by (simp cong: image_cong_simp)
-
-lemma translation_Int:
-  "(+) a ` (s \<inter> t) = ((+) a ` s) \<inter> ((+) a ` t)"
-  by auto
-
-lemma translation_subtract_Int:
-  "(\<lambda>x. x - a) ` (s \<inter> t) = ((\<lambda>x. x - a) ` s) \<inter> ((\<lambda>x. x - a) ` t)"
-  using translation_Int [of " -a"] by (simp cong: image_cong_simp)
-
 end
 
 
@@ -918,20 +954,6 @@
   using that UNIV_I by (rule the_inv_into_f_f)
 
 
-subsection \<open>Cantor's Paradox\<close>
-
-theorem Cantors_paradox: "\<nexists>f. f ` A = Pow A"
-proof
-  assume "\<exists>f. f ` A = Pow A"
-  then obtain f where f: "f ` A = Pow A" ..
-  let ?X = "{a \<in> A. a \<notin> f a}"
-  have "?X \<in> Pow A" by blast
-  then have "?X \<in> f ` A" by (simp only: f)
-  then obtain x where "x \<in> A" and "f x = ?X" by blast
-  then show False by blast
-qed
-
-
 subsection \<open>Monotonicity\<close>
 
 definition monotone_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
diff -r 2d4ff8c166d2 -r e381884c09d4 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/HOL/Library/FSet.thy	Thu Oct 13 14:49:15 2022 +0200
@@ -556,6 +556,31 @@
 lemma subset_fimage_iff: "(B |\<subseteq>| f|`|A) = (\<exists> AA. AA |\<subseteq>| A \<and> B = f|`|AA)"
 by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff)
 
+lemma fimage_strict_mono:
+  assumes "inj_on f (fset B)" and "A |\<subset>| B"
+  shows "f |`| A |\<subset>| f |`| B"
+  \<comment> \<open>TODO: Configure transfer framework to lift @{thm Fun.inj_on_strict_subset}.\<close>
+proof (rule pfsubsetI)
+  from \<open>A |\<subset>| B\<close> have "A |\<subseteq>| B"
+    by (rule pfsubset_imp_fsubset)
+  thus "f |`| A |\<subseteq>| f |`| B"
+    by (rule fimage_mono)
+next
+  from \<open>A |\<subset>| B\<close> have "A |\<subseteq>| B" and "A \<noteq> B"
+    by (simp_all add: pfsubset_eq)
+
+  have "fset A \<noteq> fset B"
+    using \<open>A \<noteq> B\<close>
+    by (simp add: fset_cong)
+  hence "f ` fset A \<noteq> f ` fset B"
+    using \<open>A |\<subseteq>| B\<close>
+    by (simp add: inj_on_image_eq_iff[OF \<open>inj_on f (fset B)\<close>] less_eq_fset.rep_eq)
+  hence "fset (f |`| A) \<noteq> fset (f |`| B)"
+    by (simp add: fimage.rep_eq)
+  thus "f |`| A \<noteq> f |`| B"
+    by (simp add: fset_cong)
+qed
+
 
 subsubsection \<open>bounded quantification\<close>
 
@@ -745,6 +770,15 @@
 end
 
 
+subsubsection \<open>@{term fsubset}\<close>
+
+lemma wfP_pfsubset: "wfP (|\<subset>|)"
+proof (rule wfP_if_convertible_to_nat)
+  show "\<And>x y. x |\<subset>| y \<Longrightarrow> fcard x < fcard y"
+    by (rule pfsubset_fcard_mono)
+qed
+
+
 subsubsection \<open>Group operations\<close>
 
 locale comm_monoid_fset = comm_monoid
diff -r 2d4ff8c166d2 -r e381884c09d4 src/HOL/Library/Rounded_Division.thy
--- a/src/HOL/Library/Rounded_Division.thy	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/HOL/Library/Rounded_Division.thy	Thu Oct 13 14:49:15 2022 +0200
@@ -1,21 +1,30 @@
 (*  Author:  Florian Haftmann, TU Muenchen
 *)
 
-subsection \<open>Rounded division: modulus centered towars zero.\<close>
+subsection \<open>Rounded division: modulus centered towards zero.\<close>
 
 theory Rounded_Division
   imports Main
 begin
 
+lemma off_iff_abs_mod_2_eq_one:
+  \<open>odd l \<longleftrightarrow> \<bar>l\<bar> mod 2 = 1\<close> for l :: int
+  by (simp flip: odd_iff_mod_2_eq_one)
+
 definition rounded_divide :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>rdiv\<close> 70)
-  where \<open>k rdiv l = (k + l div 2 + of_bool (l < 0)) div l\<close>
+  where \<open>k rdiv l = sgn l * ((k + \<bar>l\<bar> div 2) div \<bar>l\<bar>)\<close>
 
 definition rounded_modulo :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>rmod\<close> 70)
-  where \<open>k rmod l = k - k rdiv l * l\<close>
+  where \<open>k rmod l = (k + \<bar>l\<bar> div 2) mod \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
 
 lemma rdiv_mult_rmod_eq:
   \<open>k rdiv l * l + k rmod l = k\<close>
-  by (simp add: rounded_divide_def rounded_modulo_def)
+proof -
+  have *: \<open>l * (sgn l * j) = \<bar>l\<bar> * j\<close> for j
+    by (simp add: ac_simps abs_sgn)
+  show ?thesis
+    by (simp add: rounded_divide_def rounded_modulo_def algebra_simps *)
+qed
 
 lemma mult_rdiv_rmod_eq:
   \<open>l * (k rdiv l) + k rmod l = k\<close>
@@ -67,11 +76,32 @@
 
 lemma zero_rmod_eq [simp]:
   \<open>0 rmod k = 0\<close>
+  by (auto simp add: rounded_modulo_def not_less zmod_trivial_iff)
+
+lemma rdiv_minus_eq:
+  \<open>k rdiv - l = - (k rdiv l)\<close>
+  by (simp add: rounded_divide_def)
+
+lemma rmod_minus_eq [simp]:
+  \<open>k rmod - l = k rmod l\<close>
+  by (simp add: rounded_modulo_def)
+
+lemma rdiv_abs_eq:
+  \<open>k rdiv \<bar>l\<bar> = sgn l * (k rdiv l)\<close>
+  by (simp add: rounded_divide_def)
+
+lemma rmod_abs_eq [simp]:
+  \<open>k rmod \<bar>l\<bar> = k rmod l\<close>
   by (simp add: rounded_modulo_def)
 
 lemma nonzero_mult_rdiv_cancel_right:
   \<open>k * l rdiv l = k\<close> if \<open>l \<noteq> 0\<close>
-  using that by (auto simp add: rounded_divide_def ac_simps)
+proof -
+  have \<open>sgn l * k * \<bar>l\<bar> rdiv l = k\<close>
+    using that by (simp add: rounded_divide_def)
+  with that show ?thesis
+    by (simp add: ac_simps abs_sgn)
+qed
 
 lemma rdiv_self_eq [simp]:
   \<open>k rdiv k = 1\<close> if \<open>k \<noteq> 0\<close>
@@ -79,6 +109,53 @@
 
 lemma rmod_self_eq [simp]:
   \<open>k rmod k = 0\<close>
-  by (cases \<open>k = 0\<close>) (simp_all add: rounded_modulo_def)
+proof -
+  have \<open>(sgn k * \<bar>k\<bar> + \<bar>k\<bar> div 2) mod \<bar>k\<bar> = \<bar>k\<bar> div 2\<close>
+    by (auto simp add: zmod_trivial_iff)
+  also have \<open>sgn k * \<bar>k\<bar> = k\<close>
+    by (simp add: abs_sgn)
+  finally show ?thesis
+    by (simp add: rounded_modulo_def algebra_simps)
+qed
+
+lemma signed_take_bit_eq_rmod:
+  \<open>signed_take_bit n k = k rmod (2 ^ Suc n)\<close>
+  by (simp only: rounded_modulo_def power_abs abs_numeral flip: take_bit_eq_mod)
+    (simp add: signed_take_bit_eq_take_bit_shift)
+
+lemma rmod_less_divisor:
+  \<open>k rmod l < \<bar>l\<bar> - \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
+  using that pos_mod_bound [of \<open>\<bar>l\<bar>\<close>] by (simp add: rounded_modulo_def)
+
+lemma rmod_less_equal_divisor:
+  \<open>k rmod l \<le> \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
+proof -
+  from that rmod_less_divisor [of l k]
+  have \<open>k rmod l < \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
+    by simp
+  also have \<open>\<bar>l\<bar> - \<bar>l\<bar> div 2 = \<bar>l\<bar> div 2 + of_bool (odd l)\<close>
+    by auto
+  finally show ?thesis
+    by (cases \<open>even l\<close>) simp_all
+qed
+
+lemma divisor_less_equal_rmod':
+  \<open>\<bar>l\<bar> div 2 - \<bar>l\<bar> \<le> k rmod l\<close> if \<open>l \<noteq> 0\<close>
+proof -
+  have \<open>0 \<le> (k + \<bar>l\<bar> div 2) mod \<bar>l\<bar>\<close>
+    using that pos_mod_sign [of \<open>\<bar>l\<bar>\<close>] by simp
+  then show ?thesis
+    by (simp_all add: rounded_modulo_def)
+qed
+
+lemma divisor_less_equal_rmod:
+  \<open>- (\<bar>l\<bar> div 2) \<le> k rmod l\<close> if \<open>l \<noteq> 0\<close>
+  using that divisor_less_equal_rmod' [of l k]
+  by (simp add: rounded_modulo_def)
+
+lemma abs_rmod_less_equal:
+  \<open>\<bar>k rmod l\<bar> \<le> \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
+  using that divisor_less_equal_rmod [of l k]
+  by (simp add: abs_le_iff rmod_less_equal_divisor)
 
 end
diff -r 2d4ff8c166d2 -r e381884c09d4 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Thu Oct 13 14:49:15 2022 +0200
@@ -163,12 +163,6 @@
     by (auto simp add: B_def inj_on_def A_def) metis
 qed
 
-lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E"
-  apply (auto simp add: E_def C_def B_def A_def)
-  apply (rule inj_on_inverseI [where g = "(-) (int p)"])
-  apply auto
-  done
-
 lemma nonzero_mod_p: "0 < x \<Longrightarrow> x < int p \<Longrightarrow> [x \<noteq> 0](mod p)"
   for x :: int
   by (simp add: cong_def)
@@ -241,7 +235,7 @@
   by (simp add: B_card_eq_A A_card_eq)
 
 lemma F_card_eq_E: "card F = card E"
-  using finite_E by (simp add: F_def inj_on_pminusx_E card_image)
+  using finite_E by (simp add: F_def card_image)
 
 lemma C_card_eq_B: "card C = card B"
 proof -
@@ -312,11 +306,7 @@
 lemma prod_F_zcong: "[prod id F = ((-1) ^ (card E)) * prod id E] (mod p)"
 proof -
   have FE: "prod id F = prod ((-) p) E"
-    apply (auto simp add: F_def)
-    apply (insert finite_E inj_on_pminusx_E)
-    apply (drule prod.reindex)
-    apply auto
-    done
+    using finite_E prod.reindex[OF inj_on_diff_left] by (auto simp add: F_def)
   then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
     by (metis cong_def minus_mod_self1 mod_mod_trivial)
   then have "[prod ((\<lambda>x. x mod p) \<circ> ((-) p)) E = prod (uminus) E](mod p)"
@@ -356,7 +346,7 @@
     by simp
   then have "[prod id A = ((-1)^(card E) * a^(card A) * prod id A)](mod p)"
     by (rule cong_trans)
-      (simp add: cong_scalar_left cong_scalar_right finite_A prod_constant ac_simps)
+      (simp add: cong_scalar_left cong_scalar_right finite_A ac_simps)
   then have a: "[prod id A * (-1)^(card E) =
       ((-1)^(card E) * a^(card A) * prod id A * (-1)^(card E))](mod p)"
     by (rule cong_scalar_right)
diff -r 2d4ff8c166d2 -r e381884c09d4 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/HOL/Relation.thy	Thu Oct 13 14:49:15 2022 +0200
@@ -173,7 +173,7 @@
   unfolding refl_on_def by (iprover intro!: ballI)
 
 lemma reflp_onI:
-  "(\<And>x y. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> reflp_on A R"
+  "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> reflp_on A R"
   by (simp add: reflp_on_def)
 
 lemma reflpI[intro?]: "(\<And>x. R x x) \<Longrightarrow> reflp R"
@@ -256,6 +256,12 @@
 lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp Q"
   by (rule reflp_on_mono[of UNIV R Q]) simp_all
 
+lemma (in preorder) reflp_le[simp]: "reflp (\<le>)"
+  by (simp add: reflpI)
+
+lemma (in preorder) reflp_ge[simp]: "reflp (\<ge>)"
+  by (simp add: reflpI)
+
 
 subsubsection \<open>Irreflexivity\<close>
 
@@ -274,6 +280,12 @@
 lemma irreflpI [intro?]: "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R"
   by (fact irreflI [to_pred])
 
+lemma irreflD: "irrefl r \<Longrightarrow> (x, x) \<notin> r"
+  unfolding irrefl_def by simp
+
+lemma irreflpD: "irreflp R \<Longrightarrow> \<not> R x x"
+  unfolding irreflp_def by simp
+
 lemma irrefl_distinct [code]: "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)"
   by (auto simp add: irrefl_def)
 
@@ -423,6 +435,24 @@
   "antisym {x}"
   by (blast intro: antisymI)
 
+lemma antisym_if_asym: "asym r \<Longrightarrow> antisym r"
+  by (auto intro: antisymI elim: asym.cases)
+
+lemma antisymp_if_asymp: "asymp R \<Longrightarrow> antisymp R"
+  by (rule antisym_if_asym[to_pred])
+
+lemma (in preorder) antisymp_less[simp]: "antisymp (<)"
+  by (rule antisymp_if_asymp[OF asymp_less])
+
+lemma (in preorder) antisymp_greater[simp]: "antisymp (>)"
+  by (rule antisymp_if_asymp[OF asymp_greater])
+
+lemma (in order) antisymp_le[simp]: "antisymp (\<le>)"
+  by (simp add: antisympI)
+
+lemma (in order) antisymp_ge[simp]: "antisymp (\<ge>)"
+  by (simp add: antisympI)
+
 
 subsubsection \<open>Transitivity\<close>
 
@@ -555,10 +585,13 @@
   by (simp add: total_on_def)
 
 lemma totalp_on_empty [simp]: "totalp_on {} R"
-  by (auto intro: totalp_onI)
+  by (simp add: totalp_on_def)
 
-lemma total_on_singleton [simp]: "total_on {x} {(x, x)}"
-  unfolding total_on_def by blast
+lemma total_on_singleton [simp]: "total_on {x} r"
+  by (simp add: total_on_def)
+
+lemma totalp_on_singleton [simp]: "totalp_on {x} R"
+  by (simp add: totalp_on_def)
 
 
 subsubsection \<open>Single valued relations\<close>
diff -r 2d4ff8c166d2 -r e381884c09d4 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/HOL/Set.thy	Thu Oct 13 14:49:15 2022 +0200
@@ -952,6 +952,16 @@
 lemma image_add_0 [simp]: "(+) (0::'a::comm_monoid_add) ` S = S"
   by auto
 
+theorem Cantors_paradox: "\<nexists>f. f ` A = Pow A"
+proof
+  assume "\<exists>f. f ` A = Pow A"
+  then obtain f where f: "f ` A = Pow A" ..
+  let ?X = "{a \<in> A. a \<notin> f a}"
+  have "?X \<in> Pow A" by blast
+  then have "?X \<in> f ` A" by (simp only: f)
+  then obtain x where "x \<in> A" and "f x = ?X" by blast
+  then show False by blast
+qed
 
 text \<open>\<^medskip> Range of a function -- just an abbreviation for image!\<close>
 
diff -r 2d4ff8c166d2 -r e381884c09d4 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/HOL/Wellfounded.thy	Thu Oct 13 14:49:15 2022 +0200
@@ -772,7 +772,35 @@
     by (clarsimp simp: inv_image_def wf_eq_minimal)
 qed
 
-text \<open>Measure functions into \<^typ>\<open>nat\<close>\<close>
+
+subsubsection \<open>Conversion to a known well-founded relation\<close>
+
+lemma wf_if_convertible_to_wf:
+  fixes r :: "'a rel" and s :: "'b rel" and f :: "'a \<Rightarrow> 'b"
+  assumes "wf s" and convertible: "\<And>x y. (x, y) \<in> r \<Longrightarrow> (f x, f y) \<in> s"
+  shows "wf r"
+proof (rule wfI_min[of r])
+  fix x :: 'a and Q :: "'a set"
+  assume "x \<in> Q"
+  then obtain y where "y \<in> Q" and "\<And>z. (f z, f y) \<in> s \<Longrightarrow> z \<notin> Q"
+    by (auto elim: wfE_min[OF wf_inv_image[of s f, OF \<open>wf s\<close>], unfolded in_inv_image])
+  thus "\<exists>z \<in> Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
+    by (auto intro: convertible)
+qed
+
+lemma wfP_if_convertible_to_wfP: "wfP S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> wfP R"
+  using wf_if_convertible_to_wf[to_pred, of S R f] by simp
+
+text \<open>Converting to @{typ nat} is a very common special case that might be found more easily by
+  Sledgehammer.\<close>
+
+lemma wfP_if_convertible_to_nat:
+  fixes f :: "_ \<Rightarrow> nat"
+  shows "(\<And>x y. R x y \<Longrightarrow> f x < f y) \<Longrightarrow> wfP R"
+  by (rule wfP_if_convertible_to_wfP[of "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool", simplified])
+
+
+subsubsection \<open>Measure functions into \<^typ>\<open>nat\<close>\<close>
 
 definition measure :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set"
   where "measure = inv_image less_than"
diff -r 2d4ff8c166d2 -r e381884c09d4 src/HOL/ex/Note_on_signed_division_on_words.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Note_on_signed_division_on_words.thy	Thu Oct 13 14:49:15 2022 +0200
@@ -0,0 +1,50 @@
+theory Note_on_signed_division_on_words
+  imports "HOL-Library.Word" "HOL-Library.Rounded_Division"
+begin
+
+unbundle bit_operations_syntax
+
+context semiring_bit_operations
+begin
+	
+lemma take_bit_Suc_from_most:
+  \<open>take_bit (Suc n) a = 2 ^ n * of_bool (bit a n) OR take_bit n a\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps less_Suc_eq)
+	
+end
+	
+context ring_bit_operations
+begin
+	
+lemma signed_take_bit_exp_eq_int:
+  \<open>signed_take_bit m (2 ^ n) =
+    (if n < m then 2 ^ n else if n = m then - (2 ^ n) else 0)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)
+	
+end
+
+lift_definition signed_divide_word :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>  (infixl \<open>wdiv\<close> 70)
+  is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a rdiv signed_take_bit (LENGTH('a) - Suc 0) b\<close>
+  by (simp flip: signed_take_bit_decr_length_iff)
+
+lift_definition signed_modulo_word :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>  (infixl \<open>wmod\<close> 70)
+  is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a rmod signed_take_bit (LENGTH('a) - Suc 0) b\<close>
+  by (simp flip: signed_take_bit_decr_length_iff)
+
+lemma signed_take_bit_eq_wmod:
+  \<open>signed_take_bit n w = w wmod (2 ^ Suc n)\<close>
+proof (transfer fixing: n)
+  show \<open>take_bit LENGTH('a) (signed_take_bit n (take_bit LENGTH('a) k)) =
+    take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k rmod signed_take_bit (LENGTH('a) - Suc 0) (2 ^ Suc n))\<close> for k :: int
+  proof (cases \<open>LENGTH('a) = Suc (Suc n)\<close>)
+    case True
+    then show ?thesis
+      by (simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit rmod_minus_eq flip: power_Suc signed_take_bit_eq_rmod)
+  next
+    case False
+    then show ?thesis
+      by (auto simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit take_bit_signed_take_bit simp flip: power_Suc signed_take_bit_eq_rmod)
+  qed
+qed
+  
+end
diff -r 2d4ff8c166d2 -r e381884c09d4 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 11:22:32 2022 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 14:49:15 2022 +0200
@@ -344,7 +344,7 @@
           options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
           detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"))),
       List(
-        Remote_Build("macOS 10.15 Catalina", "monterey", user = "makarius",
+        Remote_Build("macOS 12 Monterey", "monterey", user = "makarius",
           options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
           args = "-a -d '~~/src/Benchmarks'")),
       List(