--- a/src/HOL/Divides.thy Fri Sep 30 21:03:58 2022 +0200
+++ b/src/HOL/Divides.thy Sat Oct 01 07:56:53 2022 +0000
@@ -1,25 +1,32 @@
(* Title: HOL/Divides.thy
*)
-section \<open>Lemmas of doubtful value\<close>
+section \<open>Misc lemmas on division, to be sorted out finally\<close>
theory Divides
imports Parity
begin
class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + linordered_semidom +
- assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
- and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
- and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
- and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
- and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
- and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
- and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
- and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
- assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
+ assumes div_less [no_atp]: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
+ and mod_less [no_atp]: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
+ and div_positive [no_atp]: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
+ and mod_less_eq_dividend [no_atp]: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
+ and pos_mod_bound [no_atp]: "0 < b \<Longrightarrow> a mod b < b"
+ and pos_mod_sign [no_atp]: "0 < b \<Longrightarrow> 0 \<le> a mod b"
+ and mod_mult2_eq [no_atp]: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
+ and div_mult2_eq [no_atp]: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
+ assumes discrete [no_atp]: "a < b \<longleftrightarrow> a + 1 \<le> b"
+
+hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
+
+context unique_euclidean_semiring_numeral
begin
-lemma divmod_digit_1:
+context
+begin
+
+lemma divmod_digit_1 [no_atp]:
assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
and "a mod (2 * b) - b = a mod b" (is "?Q")
@@ -43,7 +50,7 @@
by (simp_all add: div mod add_implies_diff [symmetric])
qed
-lemma divmod_digit_0:
+lemma divmod_digit_0 [no_atp]:
assumes "0 < b" and "a mod (2 * b) < b"
shows "2 * (a div (2 * b)) = a div b" (is "?P")
and "a mod (2 * b) = a mod b" (is "?Q")
@@ -68,7 +75,7 @@
by (simp_all add: div mod)
qed
-lemma mod_double_modulus:
+lemma mod_double_modulus: \<comment>\<open>This is actually useful and should be transferred to a suitable type class\<close>
assumes "m > 0" "x \<ge> 0"
shows "x mod (2 * m) = x mod m \<or> x mod (2 * m) = x mod m + m"
proof (cases "x mod (2 * m) < m")
@@ -85,7 +92,7 @@
end
-hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
+end
instance nat :: unique_euclidean_semiring_numeral
by standard
@@ -95,29 +102,29 @@
by standard (auto intro: zmod_le_nonneg_dividend simp add:
pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
-lemma div_geq: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
- by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
-
-lemma mod_geq: "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
- by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
-
-lemma mod_eq_0D: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
- using that by (auto simp add: mod_eq_0_iff_dvd)
-
-lemma pos_mod_conj: "0 < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b" for a b :: int
- by simp
-
-lemma neg_mod_conj: "b < 0 \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b" for a b :: int
- by simp
-
-lemma zmod_eq_0_iff: "m mod d = 0 \<longleftrightarrow> (\<exists>q. m = d * q)" for m d :: int
- by (auto simp add: mod_eq_0_iff_dvd)
-
(* REVISIT: should this be generalized to all semiring_div types? *)
lemma zmod_eq_0D [dest!]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int
using that by auto
-lemma div_positive_int:
+lemma div_geq [no_atp]: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
+ by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
+
+lemma mod_geq [no_atp]: "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
+ by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
+
+lemma mod_eq_0D [no_atp]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
+ using that by (auto simp add: mod_eq_0_iff_dvd)
+
+lemma pos_mod_conj [no_atp]: "0 < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b" for a b :: int
+ by simp
+
+lemma neg_mod_conj [no_atp]: "b < 0 \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b" for a b :: int
+ by simp
+
+lemma zmod_eq_0_iff [no_atp]: "m mod d = 0 \<longleftrightarrow> (\<exists>q. m = d * q)" for m d :: int
+ by (auto simp add: mod_eq_0_iff_dvd)
+
+lemma div_positive_int [no_atp]:
"k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
using that by (simp add: nonneg1_imp_zdiv_pos_iff)
--- a/src/HOL/Euclidean_Division.thy Fri Sep 30 21:03:58 2022 +0200
+++ b/src/HOL/Euclidean_Division.thy Sat Oct 01 07:56:53 2022 +0000
@@ -1410,10 +1410,63 @@
\<open>m \<le> n div q \<longleftrightarrow> m * q \<le> n\<close> if \<open>q > 0\<close> for m n q :: nat
using div_less_iff_less_mult [of q n m] that by auto
-text \<open>A fact for the mutilated chess board\<close>
+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")
+proof (cases \<open>n = 0 \<or> n = 1\<close>)
+ case True
+ then show ?thesis by auto
+next
+ 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>
+ 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>
+ proof (rule ccontr)
+ assume \<open>\<not> Suc (m mod n) \<noteq> n\<close>
+ then have \<open>m mod n = n - 1\<close>
+ by simp
+ with \<open>n > 1\<close> have \<open>(m + 1) mod n = 0\<close>
+ by (subst mod_add_left_eq [symmetric]) simp
+ then have \<open>n dvd Suc m\<close>
+ by auto
+ with False show False ..
+ 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>
+ 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
+qed
lemma mod_Suc:
- "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
+ \<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")
case True
then show ?thesis
@@ -1559,6 +1612,10 @@
finally show ?Q ..
qed
+lemma mod_eq_iff_dvd_symdiff_nat:
+ \<open>m mod q = n mod q \<longleftrightarrow> q dvd nat \<bar>int m - int n\<bar>\<close>
+ by (auto simp add: abs_if mod_eq_dvd_iff_nat nat_diff_distrib dest: sym intro: sym)
+
lemma mod_eq_nat1E:
fixes m n q :: nat
assumes "m mod q = n mod q" and "m \<ge> n"
--- a/src/HOL/Library/Numeral_Type.thy Fri Sep 30 21:03:58 2022 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Sat Oct 01 07:56:53 2022 +0000
@@ -156,7 +156,7 @@
by (rule type_definition.Abs_inverse [OF type])
lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
-by (simp add: Abs_inverse pos_mod_conj [OF size0])
+ using size0 by (simp add: Abs_inverse)
lemma Rep_Abs_0: "Rep (Abs 0) = 0"
by (simp add: Abs_inverse size0)
--- a/src/HOL/Library/Omega_Words_Fun.thy Fri Sep 30 21:03:58 2022 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy Sat Oct 01 07:56:53 2022 +0000
@@ -108,7 +108,7 @@
lemma iter_unroll: "0 < length w \<Longrightarrow> w\<^sup>\<omega> = w \<frown> w\<^sup>\<omega>"
- by (rule ext) (simp add: conc_def mod_geq)
+ by (simp add: fun_eq_iff mod_if)
subsection \<open>Subsequence, Prefix, and Suffix\<close>
--- a/src/HOL/Library/Word.thy Fri Sep 30 21:03:58 2022 +0200
+++ b/src/HOL/Library/Word.thy Sat Oct 01 07:56:53 2022 +0000
@@ -749,9 +749,8 @@
from length have \<open>k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2\<close>
by simp
moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
- with \<open>LENGTH('a) = Suc n\<close>
- have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close>
- by (simp add: take_bit_eq_mod divmod_digit_0)
+ with \<open>LENGTH('a) = Suc n\<close> have \<open>take_bit LENGTH('a) k = take_bit n k\<close>
+ by (auto simp add: take_bit_Suc_from_most)
ultimately have \<open>take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\<close>
by (simp add: take_bit_eq_mod)
with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2)
@@ -768,9 +767,8 @@
from length have \<open>(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2\<close>
using pos_zmod_mult_2 [of \<open>2 ^ n\<close> k] by (simp add: ac_simps)
moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
- with \<open>LENGTH('a) = Suc n\<close>
- have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close>
- by (simp add: take_bit_eq_mod divmod_digit_0)
+ with \<open>LENGTH('a) = Suc n\<close> have \<open>take_bit LENGTH('a) k = take_bit n k\<close>
+ by (auto simp add: take_bit_Suc_from_most)
ultimately have \<open>take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\<close>
by (simp add: take_bit_eq_mod)
with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2)
@@ -2926,16 +2924,7 @@
lemma int_mod_ge: \<open>a \<le> a mod n\<close> if \<open>a < n\<close> \<open>0 < n\<close>
for a n :: int
-proof (cases \<open>a < 0\<close>)
- case True
- with \<open>0 < n\<close> show ?thesis
- by (metis less_trans not_less pos_mod_conj)
-
-next
- case False
- with \<open>a < n\<close> show ?thesis
- by simp
-qed
+ using that order.trans [of a 0 \<open>a mod n\<close>] by (cases \<open>a < 0\<close>) auto
lemma mod_add_if_z:
"\<lbrakk>x < z; y < z; 0 \<le> y; 0 \<le> x; 0 \<le> z\<rbrakk> \<Longrightarrow>
--- a/src/HOL/Number_Theory/Cong.thy Fri Sep 30 21:03:58 2022 +0200
+++ b/src/HOL/Number_Theory/Cong.thy Sat Oct 01 07:56:53 2022 +0000
@@ -342,11 +342,11 @@
lemma cong_less_unique_nat: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
for a m :: nat
- by (auto simp: cong_def) (metis mod_less_divisor mod_mod_trivial)
+ by (auto simp: cong_def) (metis mod_mod_trivial mod_less_divisor)
lemma cong_less_unique_int: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
for a m :: int
- by (auto simp: cong_def) (metis mod_mod_trivial pos_mod_conj)
+ by (auto simp add: cong_def) (metis mod_mod_trivial pos_mod_bound pos_mod_sign)
lemma cong_iff_lin_nat: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
for a b :: nat
@@ -518,12 +518,8 @@
fixes m :: int
assumes "m > 0"
shows "coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = 1] (mod m))"
-proof -
- have "\<And>b. \<lbrakk>0 < m; [a * b = 1] (mod m)\<rbrakk> \<Longrightarrow> \<exists>b'<m. [a * b' = 1] (mod m)"
- by (meson cong_less_unique_int cong_scalar_left cong_sym cong_trans)
- then show ?thesis
- by (metis assms coprime_iff_invertible_int cong_def cong_mult_lcancel mod_pos_pos_trivial pos_mod_conj)
-qed
+ using assms by (simp add: coprime_iff_invertible_int)
+ (metis assms cong_mod_left mod_mult_right_eq pos_mod_bound pos_mod_sign)
lemma cong_cong_lcm_nat: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
for x y :: nat
--- a/src/HOL/Number_Theory/Pocklington.thy Fri Sep 30 21:03:58 2022 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy Sat Oct 01 07:56:53 2022 +0000
@@ -691,8 +691,8 @@
next
case 2
from assms have "x mod 8 = 3 \<or> x mod 8 = 5" by auto
- hence x': "x mod 16 = 3 \<or> x mod 16 = 5 \<or> x mod 16 = 11 \<or> x mod 16 = 13"
- using mod_double_modulus[of 8 x] by auto
+ then have x': "x mod 16 = 3 \<or> x mod 16 = 5 \<or> x mod 16 = 11 \<or> x mod 16 = 13"
+ using mod_double_modulus [of 8 x] by auto
hence "[x ^ 4 = 1] (mod 16)" using assms
by (auto simp: cong_def simp flip: power_mod[of x])
hence "ord 16 x dvd 2\<^sup>2" by (simp add: ord_divides')
@@ -729,11 +729,11 @@
have "2 ^ k' + 1 < 2 ^ k' + (2 ^ k' :: nat)"
using one_less_power[of "2::nat" k'] k' by (intro add_strict_left_mono) auto
with cong notcong have cong': "x ^ (2 ^ (k' - 2)) mod 2 ^ Suc k' = 1 + 2 ^ k'"
- using mod_double_modulus[of "2 ^ k'" "x ^ 2 ^ (k' - 2)"] k' by (auto simp: cong_def)
+ using mod_double_modulus [of "2 ^ k'" "x ^ 2 ^ (k' - 2)"] k' by (auto simp: cong_def)
hence "x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' \<or>
x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' + 2 ^ Suc k'"
- using mod_double_modulus[of "2 ^ Suc k'" "x ^ 2 ^ (k' - 2)"] by auto
+ using mod_double_modulus [of "2 ^ Suc k'" "x ^ 2 ^ (k' - 2)"] by auto
hence eq: "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
proof
assume *: "x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 2 ^ k'"
--- a/src/HOL/UNITY/Simple/Token.thy Fri Sep 30 21:03:58 2022 +0200
+++ b/src/HOL/UNITY/Simple/Token.thy Sat Oct 01 07:56:53 2022 +0000
@@ -80,10 +80,11 @@
lemma nodeOrder_eq:
"[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
-apply (unfold nodeOrder_def next_def)
-apply (auto simp add: mod_Suc mod_geq)
-apply (auto split: nat_diff_split simp add: linorder_neq_iff mod_geq)
-done
+ apply (cases \<open>i < j\<close>)
+ apply (auto simp add: nodeOrder_def next_def mod_Suc add.commute [of _ N])
+ apply (simp only: diff_add_assoc mod_add_self1)
+ apply simp
+ done
text\<open>From "A Logic for Concurrent Programming", but not used in Chapter 4.
Note the use of \<open>cases\<close>. Reasoning about leadsTo takes practice!\<close>