--- 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
--- 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
-----------------------------
--- 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)
----------------------------------
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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)
--- 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>
--- 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>
--- 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"
--- /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
--- 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(