# HG changeset patch
# User wenzelm
# Date 1664654288 -7200
# Node ID 0a44395a25f0bafa7497c1ce0bda7f55417b9536
# Parent  a7ccb744047b320777c0dbfa350319f6eee3fea1# Parent  03dd2f19f1d738d3bbf44668e7df32c568ef9477
merged

diff -r 03dd2f19f1d7 -r 0a44395a25f0 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Oct 01 21:13:45 2022 +0200
+++ b/src/HOL/Divides.thy	Sat Oct 01 21:58:08 2022 +0200
@@ -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)
 
diff -r 03dd2f19f1d7 -r 0a44395a25f0 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sat Oct 01 21:13:45 2022 +0200
+++ b/src/HOL/Euclidean_Division.thy	Sat Oct 01 21:58:08 2022 +0200
@@ -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"
diff -r 03dd2f19f1d7 -r 0a44395a25f0 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Sat Oct 01 21:13:45 2022 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Sat Oct 01 21:58:08 2022 +0200
@@ -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)
diff -r 03dd2f19f1d7 -r 0a44395a25f0 src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Sat Oct 01 21:13:45 2022 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Sat Oct 01 21:58:08 2022 +0200
@@ -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>
diff -r 03dd2f19f1d7 -r 0a44395a25f0 src/HOL/Library/Signed_Division.thy
--- a/src/HOL/Library/Signed_Division.thy	Sat Oct 01 21:13:45 2022 +0200
+++ b/src/HOL/Library/Signed_Division.thy	Sat Oct 01 21:58:08 2022 +0200
@@ -7,9 +7,13 @@
   imports Main
 begin
 
-class signed_division = comm_semiring_1_cancel +
+class signed_divide =
   fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>sdiv\<close> 70)
-  and signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>smod\<close> 70)
+
+class signed_modulo =
+  fixes signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>smod\<close> 70)
+
+class signed_division = comm_semiring_1_cancel + signed_divide + signed_modulo +
   assumes sdiv_mult_smod_eq: \<open>a sdiv b * b + a smod b = a\<close>
 begin
 
diff -r 03dd2f19f1d7 -r 0a44395a25f0 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sat Oct 01 21:13:45 2022 +0200
+++ b/src/HOL/Library/Word.thy	Sat Oct 01 21:58:08 2022 +0200
@@ -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>
diff -r 03dd2f19f1d7 -r 0a44395a25f0 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Sat Oct 01 21:13:45 2022 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Sat Oct 01 21:58:08 2022 +0200
@@ -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
diff -r 03dd2f19f1d7 -r 0a44395a25f0 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Sat Oct 01 21:13:45 2022 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Sat Oct 01 21:58:08 2022 +0200
@@ -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'"
diff -r 03dd2f19f1d7 -r 0a44395a25f0 src/HOL/UNITY/Simple/Token.thy
--- a/src/HOL/UNITY/Simple/Token.thy	Sat Oct 01 21:13:45 2022 +0200
+++ b/src/HOL/UNITY/Simple/Token.thy	Sat Oct 01 21:58:08 2022 +0200
@@ -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>