reoriented congruence rules in non-explosive direction
authorhaftmann
Sat Dec 17 15:22:14 2016 +0100 (2016-12-17)
changeset 6459350c715579715
parent 64592 7759f1766189
child 64594 4719f13989df
reoriented congruence rules in non-explosive direction
NEWS
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Divides.thy
src/HOL/Groebner_Basis.thy
src/HOL/IMP/Abs_Int1_parity.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Omega_Words_Fun.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
src/HOL/SPARK/Manual/Proc1.thy
src/HOL/SPARK/Manual/Proc2.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Bits_Int.thy
src/HOL/Word/Misc_Numeric.thy
src/HOL/Word/Word.thy
src/HOL/Word/Word_Miscellaneous.thy
src/HOL/ex/Word_Type.thy
     1.1 --- a/NEWS	Sat Dec 17 15:22:14 2016 +0100
     1.2 +++ b/NEWS	Sat Dec 17 15:22:14 2016 +0100
     1.3 @@ -6,6 +6,24 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Swapped orientation of congruence rules mod_add_left_eq,
    1.10 +mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
    1.11 +mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
    1.12 +mod_diff_eq.  INCOMPATIBILITY.
    1.13 +
    1.14 +* Generalized some facts:
    1.15 +    zminus_zmod ~> mod_minus_eq
    1.16 +    zdiff_zmod_left ~> mod_diff_left_eq
    1.17 +    zdiff_zmod_right ~> mod_diff_right_eq
    1.18 +    zmod_eq_dvd_iff ~> mod_eq_dvd_iff
    1.19 +INCOMPATIBILITY.
    1.20 +
    1.21 +* Named collection mod_simps covers various congruence rules
    1.22 +concerning mod, replacing former zmod_simps.
    1.23 +INCOMPATIBILITY.
    1.24 +
    1.25  * (Co)datatype package:
    1.26    - The 'size_gen_o_map' lemma is no longer generated for datatypes
    1.27      with type class annotations. As a result, the tactic that derives
    1.28 @@ -74,7 +92,6 @@
    1.29  * Solve direct: option "solve_direct_strict_warnings" gives explicit
    1.30  warnings for lemma statements with trivial proofs.
    1.31  
    1.32 -
    1.33  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.34  
    1.35  * More aggressive flushing of machine-generated input, according to
     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sat Dec 17 15:22:14 2016 +0100
     2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sat Dec 17 15:22:14 2016 +0100
     2.3 @@ -3206,7 +3206,7 @@
     2.4        using of_int_eq_iff apply fastforce
     2.5        by (metis of_int_add of_int_mult of_int_of_nat_eq)
     2.6      also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
     2.7 -      by (auto simp: zmod_eq_dvd_iff dvd_def algebra_simps)
     2.8 +      by (auto simp: mod_eq_dvd_iff dvd_def algebra_simps)
     2.9      also have "... \<longleftrightarrow> j mod n = k mod n"
    2.10        by (metis of_nat_eq_iff zmod_int)
    2.11      finally have "(\<exists>z. \<i> * (of_nat j * (of_real pi * 2)) =
     3.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 17 15:22:14 2016 +0100
     3.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 17 15:22:14 2016 +0100
     3.3 @@ -45,8 +45,8 @@
     3.4      (* Some simpsets for dealing with mod div abs and nat*)
     3.5      val mod_div_simpset =
     3.6        put_simpset HOL_basic_ss ctxt
     3.7 -      addsimps @{thms refl mod_add_eq [symmetric] mod_add_left_eq [symmetric]
     3.8 -          mod_add_right_eq [symmetric]
     3.9 +      addsimps @{thms refl mod_add_eq mod_add_left_eq
    3.10 +          mod_add_right_eq
    3.11            div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
    3.12            mod_self
    3.13            div_by_0 mod_by_0 div_0 mod_0
     4.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Dec 17 15:22:14 2016 +0100
     4.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Dec 17 15:22:14 2016 +0100
     4.3 @@ -31,8 +31,6 @@
     4.4               @{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
     4.5  val comp_ths = distinct Thm.eq_thm (ths @ comp_arith @ @{thms simp_thms});
     4.6  
     4.7 -val mod_add_eq = @{thm "mod_add_eq"} RS sym;
     4.8 -
     4.9  fun prepare_for_mir q fm = 
    4.10    let
    4.11      val ps = Logic.strip_params fm
    4.12 @@ -71,7 +69,7 @@
    4.13      val (t,np,nh) = prepare_for_mir q g
    4.14      (* Some simpsets for dealing with mod div abs and nat*)
    4.15      val mod_div_simpset = put_simpset HOL_basic_ss ctxt
    4.16 -                        addsimps [refl, mod_add_eq, 
    4.17 +                        addsimps [refl, @{thm mod_add_eq}, 
    4.18                                    @{thm mod_self},
    4.19                                    @{thm div_0}, @{thm mod_0},
    4.20                                    @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
     5.1 --- a/src/HOL/Divides.thy	Sat Dec 17 15:22:14 2016 +0100
     5.2 +++ b/src/HOL/Divides.thy	Sat Dec 17 15:22:14 2016 +0100
     5.3 @@ -189,97 +189,6 @@
     5.4    finally show ?thesis .
     5.5  qed
     5.6  
     5.7 -text \<open>Addition respects modular equivalence.\<close>
     5.8 -
     5.9 -lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close>
    5.10 -  "(a + b) mod c = (a mod c + b) mod c"
    5.11 -proof -
    5.12 -  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
    5.13 -    by (simp only: div_mult_mod_eq)
    5.14 -  also have "\<dots> = (a mod c + b + a div c * c) mod c"
    5.15 -    by (simp only: ac_simps)
    5.16 -  also have "\<dots> = (a mod c + b) mod c"
    5.17 -    by (rule mod_mult_self1)
    5.18 -  finally show ?thesis .
    5.19 -qed
    5.20 -
    5.21 -lemma mod_add_right_eq: \<comment> \<open>FIXME reorient\<close>
    5.22 -  "(a + b) mod c = (a + b mod c) mod c"
    5.23 -proof -
    5.24 -  have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
    5.25 -    by (simp only: div_mult_mod_eq)
    5.26 -  also have "\<dots> = (a + b mod c + b div c * c) mod c"
    5.27 -    by (simp only: ac_simps)
    5.28 -  also have "\<dots> = (a + b mod c) mod c"
    5.29 -    by (rule mod_mult_self1)
    5.30 -  finally show ?thesis .
    5.31 -qed
    5.32 -
    5.33 -lemma mod_add_eq: \<comment> \<open>FIXME reorient\<close>
    5.34 -  "(a + b) mod c = (a mod c + b mod c) mod c"
    5.35 -by (rule trans [OF mod_add_left_eq mod_add_right_eq])
    5.36 -
    5.37 -lemma mod_add_cong:
    5.38 -  assumes "a mod c = a' mod c"
    5.39 -  assumes "b mod c = b' mod c"
    5.40 -  shows "(a + b) mod c = (a' + b') mod c"
    5.41 -proof -
    5.42 -  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
    5.43 -    unfolding assms ..
    5.44 -  thus ?thesis
    5.45 -    by (simp only: mod_add_eq [symmetric])
    5.46 -qed
    5.47 -
    5.48 -text \<open>Multiplication respects modular equivalence.\<close>
    5.49 -
    5.50 -lemma mod_mult_left_eq: \<comment> \<open>FIXME reorient\<close>
    5.51 -  "(a * b) mod c = ((a mod c) * b) mod c"
    5.52 -proof -
    5.53 -  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
    5.54 -    by (simp only: div_mult_mod_eq)
    5.55 -  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
    5.56 -    by (simp only: algebra_simps)
    5.57 -  also have "\<dots> = (a mod c * b) mod c"
    5.58 -    by (rule mod_mult_self1)
    5.59 -  finally show ?thesis .
    5.60 -qed
    5.61 -
    5.62 -lemma mod_mult_right_eq: \<comment> \<open>FIXME reorient\<close>
    5.63 -  "(a * b) mod c = (a * (b mod c)) mod c"
    5.64 -proof -
    5.65 -  have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
    5.66 -    by (simp only: div_mult_mod_eq)
    5.67 -  also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
    5.68 -    by (simp only: algebra_simps)
    5.69 -  also have "\<dots> = (a * (b mod c)) mod c"
    5.70 -    by (rule mod_mult_self1)
    5.71 -  finally show ?thesis .
    5.72 -qed
    5.73 -
    5.74 -lemma mod_mult_eq: \<comment> \<open>FIXME reorient\<close>
    5.75 -  "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
    5.76 -by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
    5.77 -
    5.78 -lemma mod_mult_cong:
    5.79 -  assumes "a mod c = a' mod c"
    5.80 -  assumes "b mod c = b' mod c"
    5.81 -  shows "(a * b) mod c = (a' * b') mod c"
    5.82 -proof -
    5.83 -  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
    5.84 -    unfolding assms ..
    5.85 -  thus ?thesis
    5.86 -    by (simp only: mod_mult_eq [symmetric])
    5.87 -qed
    5.88 -
    5.89 -text \<open>Exponentiation respects modular equivalence.\<close>
    5.90 -
    5.91 -lemma power_mod: "(a mod b) ^ n mod b = a ^ n mod b"
    5.92 -apply (induct n, simp_all)
    5.93 -apply (rule mod_mult_right_eq [THEN trans])
    5.94 -apply (simp (no_asm_simp))
    5.95 -apply (rule mod_mult_eq [symmetric])
    5.96 -done
    5.97 -
    5.98  lemma mod_mod_cancel:
    5.99    assumes "c dvd b"
   5.100    shows "a mod b mod c = a mod c"
   5.101 @@ -331,6 +240,121 @@
   5.102  lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   5.103    unfolding dvd_def by (auto simp add: mod_mult_mult1)
   5.104  
   5.105 +named_theorems mod_simps
   5.106 +
   5.107 +text \<open>Addition respects modular equivalence.\<close>
   5.108 +
   5.109 +lemma mod_add_left_eq [mod_simps]:
   5.110 +  "(a mod c + b) mod c = (a + b) mod c"
   5.111 +proof -
   5.112 +  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
   5.113 +    by (simp only: div_mult_mod_eq)
   5.114 +  also have "\<dots> = (a mod c + b + a div c * c) mod c"
   5.115 +    by (simp only: ac_simps)
   5.116 +  also have "\<dots> = (a mod c + b) mod c"
   5.117 +    by (rule mod_mult_self1)
   5.118 +  finally show ?thesis
   5.119 +    by (rule sym)
   5.120 +qed
   5.121 +
   5.122 +lemma mod_add_right_eq [mod_simps]:
   5.123 +  "(a + b mod c) mod c = (a + b) mod c"
   5.124 +  using mod_add_left_eq [of b c a] by (simp add: ac_simps)
   5.125 +
   5.126 +lemma mod_add_eq:
   5.127 +  "(a mod c + b mod c) mod c = (a + b) mod c"
   5.128 +  by (simp add: mod_add_left_eq mod_add_right_eq)
   5.129 +
   5.130 +lemma mod_sum_eq [mod_simps]:
   5.131 +  "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
   5.132 +proof (induct A rule: infinite_finite_induct)
   5.133 +  case (insert i A)
   5.134 +  then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
   5.135 +    = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
   5.136 +    by simp
   5.137 +  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
   5.138 +    by (simp add: mod_simps)
   5.139 +  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
   5.140 +    by (simp add: insert.hyps)
   5.141 +  finally show ?case
   5.142 +    by (simp add: insert.hyps mod_simps)
   5.143 +qed simp_all
   5.144 +
   5.145 +lemma mod_add_cong:
   5.146 +  assumes "a mod c = a' mod c"
   5.147 +  assumes "b mod c = b' mod c"
   5.148 +  shows "(a + b) mod c = (a' + b') mod c"
   5.149 +proof -
   5.150 +  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
   5.151 +    unfolding assms ..
   5.152 +  then show ?thesis
   5.153 +    by (simp add: mod_add_eq)
   5.154 +qed
   5.155 +
   5.156 +text \<open>Multiplication respects modular equivalence.\<close>
   5.157 +
   5.158 +lemma mod_mult_left_eq [mod_simps]:
   5.159 +  "((a mod c) * b) mod c = (a * b) mod c"
   5.160 +proof -
   5.161 +  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
   5.162 +    by (simp only: div_mult_mod_eq)
   5.163 +  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
   5.164 +    by (simp only: algebra_simps)
   5.165 +  also have "\<dots> = (a mod c * b) mod c"
   5.166 +    by (rule mod_mult_self1)
   5.167 +  finally show ?thesis
   5.168 +    by (rule sym)
   5.169 +qed
   5.170 +
   5.171 +lemma mod_mult_right_eq [mod_simps]:
   5.172 +  "(a * (b mod c)) mod c = (a * b) mod c"
   5.173 +  using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
   5.174 +
   5.175 +lemma mod_mult_eq:
   5.176 +  "((a mod c) * (b mod c)) mod c = (a * b) mod c"
   5.177 +  by (simp add: mod_mult_left_eq mod_mult_right_eq)
   5.178 +
   5.179 +lemma mod_prod_eq [mod_simps]:
   5.180 +  "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
   5.181 +proof (induct A rule: infinite_finite_induct)
   5.182 +  case (insert i A)
   5.183 +  then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
   5.184 +    = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
   5.185 +    by simp
   5.186 +  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
   5.187 +    by (simp add: mod_simps)
   5.188 +  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
   5.189 +    by (simp add: insert.hyps)
   5.190 +  finally show ?case
   5.191 +    by (simp add: insert.hyps mod_simps)
   5.192 +qed simp_all
   5.193 +
   5.194 +lemma mod_mult_cong:
   5.195 +  assumes "a mod c = a' mod c"
   5.196 +  assumes "b mod c = b' mod c"
   5.197 +  shows "(a * b) mod c = (a' * b') mod c"
   5.198 +proof -
   5.199 +  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
   5.200 +    unfolding assms ..
   5.201 +  then show ?thesis
   5.202 +    by (simp add: mod_mult_eq)
   5.203 +qed
   5.204 +
   5.205 +text \<open>Exponentiation respects modular equivalence.\<close>
   5.206 +
   5.207 +lemma power_mod [mod_simps]: 
   5.208 +  "((a mod b) ^ n) mod b = (a ^ n) mod b"
   5.209 +proof (induct n)
   5.210 +  case 0
   5.211 +  then show ?case by simp
   5.212 +next
   5.213 +  case (Suc n)
   5.214 +  have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
   5.215 +    by (simp add: mod_mult_right_eq)
   5.216 +  with Suc show ?case
   5.217 +    by (simp add: mod_mult_left_eq mod_mult_right_eq)
   5.218 +qed
   5.219 +
   5.220  end
   5.221  
   5.222  class ring_div = comm_ring_1 + semiring_div
   5.223 @@ -338,9 +362,28 @@
   5.224  
   5.225  subclass idom_divide ..
   5.226  
   5.227 +lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
   5.228 +  using div_mult_mult1 [of "- 1" a b] by simp
   5.229 +
   5.230 +lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
   5.231 +  using mod_mult_mult1 [of "- 1" a b] by simp
   5.232 +
   5.233 +lemma div_minus_right: "a div (- b) = (- a) div b"
   5.234 +  using div_minus_minus [of "- a" b] by simp
   5.235 +
   5.236 +lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
   5.237 +  using mod_minus_minus [of "- a" b] by simp
   5.238 +
   5.239 +lemma div_minus1_right [simp]: "a div (- 1) = - a"
   5.240 +  using div_minus_right [of a 1] by simp
   5.241 +
   5.242 +lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
   5.243 +  using mod_minus_right [of a 1] by simp
   5.244 +
   5.245  text \<open>Negation respects modular equivalence.\<close>
   5.246  
   5.247 -lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
   5.248 +lemma mod_minus_eq [mod_simps]:
   5.249 +  "(- (a mod b)) mod b = (- a) mod b"
   5.250  proof -
   5.251    have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
   5.252      by (simp only: div_mult_mod_eq)
   5.253 @@ -348,7 +391,8 @@
   5.254      by (simp add: ac_simps)
   5.255    also have "\<dots> = (- (a mod b)) mod b"
   5.256      by (rule mod_mult_self1)
   5.257 -  finally show ?thesis .
   5.258 +  finally show ?thesis
   5.259 +    by (rule sym)
   5.260  qed
   5.261  
   5.262  lemma mod_minus_cong:
   5.263 @@ -357,51 +401,37 @@
   5.264  proof -
   5.265    have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
   5.266      unfolding assms ..
   5.267 -  thus ?thesis
   5.268 -    by (simp only: mod_minus_eq [symmetric])
   5.269 +  then show ?thesis
   5.270 +    by (simp add: mod_minus_eq)
   5.271  qed
   5.272  
   5.273  text \<open>Subtraction respects modular equivalence.\<close>
   5.274  
   5.275 -lemma mod_diff_left_eq:
   5.276 -  "(a - b) mod c = (a mod c - b) mod c"
   5.277 -  using mod_add_cong [of a c "a mod c" "- b" "- b"] by simp
   5.278 -
   5.279 -lemma mod_diff_right_eq:
   5.280 -  "(a - b) mod c = (a - b mod c) mod c"
   5.281 -  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
   5.282 +lemma mod_diff_left_eq [mod_simps]:
   5.283 +  "(a mod c - b) mod c = (a - b) mod c"
   5.284 +  using mod_add_cong [of a c "a mod c" "- b" "- b"]
   5.285 +  by simp
   5.286 +
   5.287 +lemma mod_diff_right_eq [mod_simps]:
   5.288 +  "(a - b mod c) mod c = (a - b) mod c"
   5.289 +  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   5.290 +  by simp
   5.291  
   5.292  lemma mod_diff_eq:
   5.293 -  "(a - b) mod c = (a mod c - b mod c) mod c"
   5.294 -  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
   5.295 +  "(a mod c - b mod c) mod c = (a - b) mod c"
   5.296 +  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   5.297 +  by simp
   5.298  
   5.299  lemma mod_diff_cong:
   5.300    assumes "a mod c = a' mod c"
   5.301    assumes "b mod c = b' mod c"
   5.302    shows "(a - b) mod c = (a' - b') mod c"
   5.303 -  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
   5.304 -
   5.305 -lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
   5.306 -  using div_mult_mult1 [of "- 1" a b]
   5.307 -  unfolding neg_equal_0_iff_equal by simp
   5.308 -
   5.309 -lemma mod_minus_minus [simp]: "(-a) mod (-b) = - (a mod b)"
   5.310 -  using mod_mult_mult1 [of "- 1" a b] by simp
   5.311 -
   5.312 -lemma div_minus_right: "a div (-b) = (-a) div b"
   5.313 -  using div_minus_minus [of "-a" b] by simp
   5.314 -
   5.315 -lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"
   5.316 -  using mod_minus_minus [of "-a" b] by simp
   5.317 -
   5.318 -lemma div_minus1_right [simp]: "a div (-1) = -a"
   5.319 -  using div_minus_right [of a 1] by simp
   5.320 -
   5.321 -lemma mod_minus1_right [simp]: "a mod (-1) = 0"
   5.322 -  using mod_minus_right [of a 1] by simp
   5.323 +  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
   5.324 +  by simp
   5.325  
   5.326  lemma minus_mod_self2 [simp]:
   5.327    "(a - b) mod b = a mod b"
   5.328 +  using mod_diff_right_eq [of a b b]
   5.329    by (simp add: mod_diff_right_eq)
   5.330  
   5.331  lemma minus_mod_self1 [simp]:
   5.332 @@ -455,18 +485,21 @@
   5.333    assume "a mod 2 = 1"
   5.334    moreover assume "b mod 2 = 1"
   5.335    ultimately show "(a + b) mod 2 = 0"
   5.336 -    using mod_add_eq [of a b 2] by simp
   5.337 +    using mod_add_eq [of a 2 b] by simp
   5.338  next
   5.339    fix a b
   5.340    assume "(a * b) mod 2 = 0"
   5.341 +  then have "(a mod 2) * (b mod 2) mod 2 = 0"
   5.342 +    by (simp add: mod_mult_eq)
   5.343    then have "(a mod 2) * (b mod 2) = 0"
   5.344 -    by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
   5.345 +    by (cases "a mod 2 = 0") simp_all
   5.346    then show "a mod 2 = 0 \<or> b mod 2 = 0"
   5.347      by (rule divisors_zero)
   5.348  next
   5.349    fix a
   5.350    assume "a mod 2 = 1"
   5.351 -  then have "a = a div 2 * 2 + 1" using div_mult_mod_eq [of a 2] by simp
   5.352 +  then have "a = a div 2 * 2 + 1"
   5.353 +    using div_mult_mod_eq [of a 2] by simp
   5.354    then show "\<exists>b. a = b + 1" ..
   5.355  qed
   5.356  
   5.357 @@ -1052,6 +1085,24 @@
   5.358      let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   5.359    by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
   5.360  
   5.361 +lemma mod_Suc_eq [mod_simps]:
   5.362 +  "Suc (m mod n) mod n = Suc m mod n"
   5.363 +proof -
   5.364 +  have "(m mod n + 1) mod n = (m + 1) mod n"
   5.365 +    by (simp only: mod_simps)
   5.366 +  then show ?thesis
   5.367 +    by simp
   5.368 +qed
   5.369 +
   5.370 +lemma mod_Suc_Suc_eq [mod_simps]:
   5.371 +  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
   5.372 +proof -
   5.373 +  have "(m mod n + 2) mod n = (m + 2) mod n"
   5.374 +    by (simp only: mod_simps)
   5.375 +  then show ?thesis
   5.376 +    by simp
   5.377 +qed
   5.378 +
   5.379  
   5.380  subsubsection \<open>Quotient\<close>
   5.381  
   5.382 @@ -1860,12 +1911,12 @@
   5.383  apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
   5.384  done
   5.385  
   5.386 -lemma zmod_zminus1_not_zero: -- \<open>FIXME generalize\<close>
   5.387 +lemma zmod_zminus1_not_zero:
   5.388    fixes k l :: int
   5.389    shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   5.390    by (simp add: mod_eq_0_iff_dvd)
   5.391  
   5.392 -lemma zmod_zminus2_not_zero: -- \<open>FIXME generalize\<close>
   5.393 +lemma zmod_zminus2_not_zero:
   5.394    fixes k l :: int
   5.395    shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   5.396    by (simp add: mod_eq_0_iff_dvd)
   5.397 @@ -2094,7 +2145,7 @@
   5.398      P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
   5.399  apply (rule iffI, clarify)
   5.400   apply (erule_tac P="P x y" for x y in rev_mp)
   5.401 - apply (subst mod_add_eq)
   5.402 + apply (subst mod_add_eq [symmetric])
   5.403   apply (subst zdiv_zadd1_eq)
   5.404   apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
   5.405  txt\<open>converse direction\<close>
   5.406 @@ -2107,7 +2158,7 @@
   5.407      P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
   5.408  apply (rule iffI, clarify)
   5.409   apply (erule_tac P="P x y" for x y in rev_mp)
   5.410 - apply (subst mod_add_eq)
   5.411 + apply (subst mod_add_eq [symmetric])
   5.412   apply (subst zdiv_zadd1_eq)
   5.413   apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
   5.414  txt\<open>converse direction\<close>
   5.415 @@ -2427,24 +2478,6 @@
   5.416   apply simp_all
   5.417  done
   5.418  
   5.419 -text \<open>by Brian Huffman\<close>
   5.420 -lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
   5.421 -by (rule mod_minus_eq [symmetric])
   5.422 -
   5.423 -lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
   5.424 -by (rule mod_diff_left_eq [symmetric])
   5.425 -
   5.426 -lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
   5.427 -by (rule mod_diff_right_eq [symmetric])
   5.428 -
   5.429 -lemmas zmod_simps =
   5.430 -  mod_add_left_eq  [symmetric]
   5.431 -  mod_add_right_eq [symmetric]
   5.432 -  mod_mult_right_eq[symmetric]
   5.433 -  mod_mult_left_eq [symmetric]
   5.434 -  power_mod
   5.435 -  zminus_zmod zdiff_zmod_left zdiff_zmod_right
   5.436 -
   5.437  text \<open>Distributive laws for function \<open>nat\<close>.\<close>
   5.438  
   5.439  lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
   5.440 @@ -2504,28 +2537,29 @@
   5.441  apply (rule Divides.div_less_dividend, simp_all)
   5.442  done
   5.443  
   5.444 -lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
   5.445 +lemma (in ring_div) mod_eq_dvd_iff:
   5.446 +  "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
   5.447  proof
   5.448 -  assume H: "x mod n = y mod n"
   5.449 -  hence "x mod n - y mod n = 0" by simp
   5.450 -  hence "(x mod n - y mod n) mod n = 0" by simp
   5.451 -  hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
   5.452 -  thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
   5.453 +  assume ?P
   5.454 +  then have "(a mod c - b mod c) mod c = 0"
   5.455 +    by simp
   5.456 +  then show ?Q
   5.457 +    by (simp add: dvd_eq_mod_eq_0 mod_simps)
   5.458  next
   5.459 -  assume H: "n dvd x - y"
   5.460 -  then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
   5.461 -  hence "x = n*k + y" by simp
   5.462 -  hence "x mod n = (n*k + y) mod n" by simp
   5.463 -  thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
   5.464 +  assume ?Q
   5.465 +  then obtain d where d: "a - b = c * d" ..
   5.466 +  then have "a = c * d + b"
   5.467 +    by (simp add: algebra_simps)
   5.468 +  then show ?P by simp
   5.469  qed
   5.470  
   5.471 -lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"
   5.472 +lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
   5.473    shows "\<exists>q. x = y + n * q"
   5.474  proof-
   5.475    from xy have th: "int x - int y = int (x - y)" by simp
   5.476    from xyn have "int x mod int n = int y mod int n"
   5.477      by (simp add: zmod_int [symmetric])
   5.478 -  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])
   5.479 +  hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
   5.480    hence "n dvd x - y" by (simp add: th zdvd_int)
   5.481    then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
   5.482  qed
     6.1 --- a/src/HOL/Groebner_Basis.thy	Sat Dec 17 15:22:14 2016 +0100
     6.2 +++ b/src/HOL/Groebner_Basis.thy	Sat Dec 17 15:22:14 2016 +0100
     6.3 @@ -72,7 +72,7 @@
     6.4  declare zmod_eq_0_iff[algebra]
     6.5  declare dvd_0_left_iff[algebra]
     6.6  declare zdvd1_eq[algebra]
     6.7 -declare zmod_eq_dvd_iff[algebra]
     6.8 +declare mod_eq_dvd_iff[algebra]
     6.9  declare nat_mod_eq_iff[algebra]
    6.10  
    6.11  context semiring_parity
     7.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Sat Dec 17 15:22:14 2016 +0100
     7.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Sat Dec 17 15:22:14 2016 +0100
     7.3 @@ -112,7 +112,8 @@
     7.4    case 3 show ?case by auto
     7.5  next
     7.6    case (4 _ a1 _ a2) thus ?case
     7.7 -    by (induction a1 a2 rule: plus_parity.induct) (auto simp add:mod_add_eq)
     7.8 +    by (induction a1 a2 rule: plus_parity.induct)
     7.9 +      (auto simp add: mod_add_eq [symmetric])
    7.10  qed
    7.11  
    7.12  text{* In case 4 we needed to refer to particular variables.
     8.1 --- a/src/HOL/Library/Numeral_Type.thy	Sat Dec 17 15:22:14 2016 +0100
     8.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sat Dec 17 15:22:14 2016 +0100
     8.3 @@ -133,7 +133,7 @@
     8.4  
     8.5  lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
     8.6  apply (intro_classes, unfold definitions)
     8.7 -apply (simp_all add: Rep_simps zmod_simps field_simps)
     8.8 +apply (simp_all add: Rep_simps mod_simps field_simps)
     8.9  done
    8.10  
    8.11  end
    8.12 @@ -147,12 +147,12 @@
    8.13  lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
    8.14  apply (induct k)
    8.15  apply (simp add: zero_def)
    8.16 -apply (simp add: Rep_simps add_def one_def zmod_simps ac_simps)
    8.17 +apply (simp add: Rep_simps add_def one_def mod_simps ac_simps)
    8.18  done
    8.19  
    8.20  lemma of_int_eq: "of_int z = Abs (z mod n)"
    8.21  apply (cases z rule: int_diff_cases)
    8.22 -apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
    8.23 +apply (simp add: Rep_simps of_nat_eq diff_def mod_simps)
    8.24  done
    8.25  
    8.26  lemma Rep_numeral:
     9.1 --- a/src/HOL/Library/Omega_Words_Fun.thy	Sat Dec 17 15:22:14 2016 +0100
     9.2 +++ b/src/HOL/Library/Omega_Words_Fun.thy	Sat Dec 17 15:22:14 2016 +0100
     9.3 @@ -626,7 +626,7 @@
     9.4        by (auto simp add: set_conv_nth)
     9.5      \<comment> "the following bound is terrible, but it simplifies the proof"
     9.6      from nempty k have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
     9.7 -      by (simp add: mod_add_left_eq)
     9.8 +      by (simp add: mod_add_left_eq [symmetric])
     9.9      moreover
    9.10      \<comment> "why is the following so hard to prove??"
    9.11      have "\<forall>m. m < (Suc m)*(length w) + k"
    10.1 --- a/src/HOL/Number_Theory/Cong.thy	Sat Dec 17 15:22:14 2016 +0100
    10.2 +++ b/src/HOL/Number_Theory/Cong.thy	Sat Dec 17 15:22:14 2016 +0100
    10.3 @@ -251,7 +251,7 @@
    10.4    done
    10.5  
    10.6  lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
    10.7 -  by (metis cong_int_def zmod_eq_dvd_iff)
    10.8 +  by (metis cong_int_def mod_eq_dvd_iff)
    10.9  
   10.10  lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
   10.11    by (simp add: cong_altdef_int)
   10.12 @@ -429,7 +429,7 @@
   10.13    by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
   10.14  
   10.15  lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
   10.16 -  by (metis cong_int_def minus_minus zminus_zmod)
   10.17 +  by (metis cong_int_def minus_minus mod_minus_cong)
   10.18  
   10.19  lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
   10.20    by (auto simp add: cong_altdef_int)
    11.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sat Dec 17 15:22:14 2016 +0100
    11.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Sat Dec 17 15:22:14 2016 +0100
    11.3 @@ -369,7 +369,7 @@
    11.4      hence th: "[a^?r = 1] (mod n)"
    11.5        using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
    11.6        apply (simp add: cong_nat_def del: One_nat_def)
    11.7 -      by (simp add: mod_mult_left_eq[symmetric])
    11.8 +      by (metis mod_mult_left_eq nat_mult_1)
    11.9      {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
   11.10      moreover
   11.11      {assume r: "?r \<noteq> 0"
    12.1 --- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sat Dec 17 15:22:14 2016 +0100
    12.2 +++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sat Dec 17 15:22:14 2016 +0100
    12.3 @@ -167,7 +167,7 @@
    12.4      fix a b
    12.5      assume a: "P_1 res a" "P_1 res b"
    12.6      hence "int p * int q dvd a - b"
    12.7 -      using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int zmod_eq_dvd_iff[of a _ b]
    12.8 +      using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int mod_eq_dvd_iff [of a _ b]
    12.9        unfolding P_1_def by force
   12.10      hence "a = b" using dvd_imp_le_int[of "a - b"] a unfolding P_1_def by fastforce
   12.11    }
   12.12 @@ -187,7 +187,7 @@
   12.13      assume a: "x \<in> BuC" "y \<in> BuC" "f_1 x = f_1 y"
   12.14      hence "int p * int q dvd x - y"
   12.15        using f_1_def pq_coprime_int divides_mult[of "int p" "x - y" "int q"] 
   12.16 -            zmod_eq_dvd_iff[of x _ y] by auto
   12.17 +            mod_eq_dvd_iff[of x _ y] by auto
   12.18      hence "x = y"
   12.19        using dvd_imp_le_int[of "x - y" "int p * int q"] a unfolding BuC_def by force
   12.20    }
    13.1 --- a/src/HOL/Number_Theory/Residues.thy	Sat Dec 17 15:22:14 2016 +0100
    13.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sat Dec 17 15:22:14 2016 +0100
    13.3 @@ -40,7 +40,7 @@
    13.4    apply (insert m_gt_one)
    13.5    apply (rule abelian_groupI)
    13.6    apply (unfold R_def residue_ring_def)
    13.7 -  apply (auto simp add: mod_add_right_eq [symmetric] ac_simps)
    13.8 +  apply (auto simp add: mod_add_right_eq ac_simps)
    13.9    apply (case_tac "x = 0")
   13.10    apply force
   13.11    apply (subgoal_tac "(x + (m - x)) mod m = 0")
   13.12 @@ -55,7 +55,7 @@
   13.13    apply auto
   13.14    apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
   13.15    apply (erule ssubst)
   13.16 -  apply (subst mod_mult_right_eq [symmetric])+
   13.17 +  apply (subst mod_mult_right_eq)+
   13.18    apply (simp_all only: ac_simps)
   13.19    done
   13.20  
   13.21 @@ -64,9 +64,9 @@
   13.22    apply (rule abelian_group)
   13.23    apply (rule comm_monoid)
   13.24    apply (unfold R_def residue_ring_def, auto)
   13.25 -  apply (subst mod_add_eq [symmetric])
   13.26 +  apply (subst mod_add_eq)
   13.27    apply (subst mult.commute)
   13.28 -  apply (subst mod_mult_right_eq [symmetric])
   13.29 +  apply (subst mod_mult_right_eq)
   13.30    apply (simp add: field_simps)
   13.31    done
   13.32  
   13.33 @@ -116,9 +116,9 @@
   13.34    apply auto
   13.35    apply (rule the_equality)
   13.36    apply auto
   13.37 -  apply (subst mod_add_right_eq [symmetric])
   13.38 +  apply (subst mod_add_right_eq)
   13.39    apply auto
   13.40 -  apply (subst mod_add_left_eq [symmetric])
   13.41 +  apply (subst mod_add_left_eq)
   13.42    apply auto
   13.43    apply (subgoal_tac "y mod m = - x mod m")
   13.44    apply simp
   13.45 @@ -143,13 +143,11 @@
   13.46  
   13.47  lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
   13.48    unfolding R_def residue_ring_def
   13.49 -  apply auto
   13.50 -  apply presburger
   13.51 -  done
   13.52 +  by (auto simp add: mod_simps)
   13.53  
   13.54  lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
   13.55    unfolding R_def residue_ring_def
   13.56 -  by auto (metis mod_mult_eq)
   13.57 +  by (auto simp add: mod_simps)
   13.58  
   13.59  lemma zero_cong: "\<zero> = 0"
   13.60    unfolding R_def residue_ring_def by auto
    14.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Dec 17 15:22:14 2016 +0100
    14.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Dec 17 15:22:14 2016 +0100
    14.3 @@ -456,7 +456,7 @@
    14.4      unfolding round_def
    14.5      unfolding steps_to_steps'
    14.6      unfolding H1[symmetric]
    14.7 -    by (simp add: uint_word_ariths(1) rdmods
    14.8 +    by (simp add: uint_word_ariths(1) mod_simps
    14.9        uint_word_of_int_id)
   14.10  qed
   14.11  
    15.1 --- a/src/HOL/SPARK/Manual/Proc1.thy	Sat Dec 17 15:22:14 2016 +0100
    15.2 +++ b/src/HOL/SPARK/Manual/Proc1.thy	Sat Dec 17 15:22:14 2016 +0100
    15.3 @@ -5,10 +5,10 @@
    15.4  spark_open "loop_invariant/proc1"
    15.5  
    15.6  spark_vc procedure_proc1_5
    15.7 -  by (simp add: ring_distribs pull_mods)
    15.8 +  by (simp add: ring_distribs mod_simps)
    15.9  
   15.10  spark_vc procedure_proc1_8
   15.11 -  by (simp add: ring_distribs pull_mods)
   15.12 +  by (simp add: ring_distribs mod_simps)
   15.13  
   15.14  spark_end
   15.15  
    16.1 --- a/src/HOL/SPARK/Manual/Proc2.thy	Sat Dec 17 15:22:14 2016 +0100
    16.2 +++ b/src/HOL/SPARK/Manual/Proc2.thy	Sat Dec 17 15:22:14 2016 +0100
    16.3 @@ -5,7 +5,7 @@
    16.4  spark_open "loop_invariant/proc2"
    16.5  
    16.6  spark_vc procedure_proc2_7
    16.7 -  by (simp add: ring_distribs pull_mods)
    16.8 +  by (simp add: ring_distribs mod_simps)
    16.9  
   16.10  spark_end
   16.11  
    17.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 17 15:22:14 2016 +0100
    17.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 17 15:22:14 2016 +0100
    17.3 @@ -824,8 +824,8 @@
    17.4  val div_mod_ss =
    17.5    simpset_of (put_simpset HOL_basic_ss @{context}
    17.6      addsimps @{thms simp_thms
    17.7 -      mod_eq_0_iff_dvd mod_add_left_eq [symmetric] mod_add_right_eq [symmetric]
    17.8 -      mod_add_eq [symmetric] div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
    17.9 +      mod_eq_0_iff_dvd mod_add_left_eq mod_add_right_eq
   17.10 +      mod_add_eq div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
   17.11        mod_self mod_by_0 div_by_0
   17.12        div_0 mod_0 div_by_1 mod_by_1
   17.13        div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1
    18.1 --- a/src/HOL/Word/Bit_Representation.thy	Sat Dec 17 15:22:14 2016 +0100
    18.2 +++ b/src/HOL/Word/Bit_Representation.thy	Sat Dec 17 15:22:14 2016 +0100
    18.3 @@ -308,17 +308,12 @@
    18.4  
    18.5  lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n"
    18.6    apply (induct n arbitrary: w)
    18.7 -   apply simp
    18.8 -   apply (subst mod_add_left_eq)
    18.9 -   apply (simp add: bin_last_def)
   18.10 -   apply arith
   18.11 -  apply (simp add: bin_last_def bin_rest_def Bit_def)
   18.12 -  apply (clarsimp simp: mod_mult_mult1 [symmetric] 
   18.13 -         mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
   18.14 -  apply (rule trans [symmetric, OF _ emep1])
   18.15 -  apply auto
   18.16 +   apply (auto simp add: bin_last_odd bin_rest_def Bit_def elim!: evenE oddE)
   18.17 +   apply (smt pos_zmod_mult_2 zle2p)
   18.18 +  apply (simp add: mult_mod_right)
   18.19    done
   18.20  
   18.21 +
   18.22  subsection "Simplifications for (s)bintrunc"
   18.23  
   18.24  lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
   18.25 @@ -647,28 +642,6 @@
   18.26    "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
   18.27    unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
   18.28  
   18.29 -lemmas zmod_uminus' = zminus_zmod [where m=c] for c
   18.30 -lemmas zpower_zmod' = power_mod [where b=c and n=k] for c k
   18.31 -
   18.32 -lemmas brdmod1s' [symmetric] =
   18.33 -  mod_add_left_eq mod_add_right_eq
   18.34 -  mod_diff_left_eq mod_diff_right_eq
   18.35 -  mod_mult_left_eq mod_mult_right_eq
   18.36 -
   18.37 -lemmas brdmods' [symmetric] = 
   18.38 -  zpower_zmod' [symmetric]
   18.39 -  trans [OF mod_add_left_eq mod_add_right_eq] 
   18.40 -  trans [OF mod_diff_left_eq mod_diff_right_eq] 
   18.41 -  trans [OF mod_mult_right_eq mod_mult_left_eq] 
   18.42 -  zmod_uminus' [symmetric]
   18.43 -  mod_add_left_eq [where b = "1::int"]
   18.44 -  mod_diff_left_eq [where b = "1::int"]
   18.45 -
   18.46 -lemmas bintr_arith1s =
   18.47 -  brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n
   18.48 -lemmas bintr_ariths =
   18.49 -  brdmods' [where c="2^n::int", folded bintrunc_mod2p] for n
   18.50 -
   18.51  lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
   18.52  
   18.53  lemma bintr_ge0: "0 \<le> bintrunc n w"
    19.1 --- a/src/HOL/Word/Bits_Int.thy	Sat Dec 17 15:22:14 2016 +0100
    19.2 +++ b/src/HOL/Word/Bits_Int.thy	Sat Dec 17 15:22:14 2016 +0100
    19.3 @@ -643,14 +643,14 @@
    19.4  lemma mod_BIT:
    19.5    "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
    19.6  proof -
    19.7 -  have "bin mod 2 ^ n < 2 ^ n" by simp
    19.8 -  then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
    19.9 -  then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
   19.10 -    by (rule mult_left_mono) simp
   19.11 -  then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
   19.12 -  then show ?thesis
   19.13 -    by (auto simp add: Bit_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
   19.14 -      mod_pos_pos_trivial)
   19.15 +  have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
   19.16 +    by (simp add: mod_mult_mult1)
   19.17 +  also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
   19.18 +    by (simp add: ac_simps p1mod22k')
   19.19 +  also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
   19.20 +    by (simp only: mod_simps)
   19.21 +  finally show ?thesis
   19.22 +    by (auto simp add: Bit_def)
   19.23  qed
   19.24  
   19.25  lemma AND_mod:
    20.1 --- a/src/HOL/Word/Misc_Numeric.thy	Sat Dec 17 15:22:14 2016 +0100
    20.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Sat Dec 17 15:22:14 2016 +0100
    20.3 @@ -8,6 +8,10 @@
    20.4  imports Main
    20.5  begin
    20.6  
    20.7 +lemma one_mod_exp_eq_one [simp]:
    20.8 +  "1 mod (2 * 2 ^ n) = (1::int)"
    20.9 +  by (smt mod_pos_pos_trivial zero_less_power)
   20.10 +
   20.11  lemma mod_2_neq_1_eq_eq_0:
   20.12    fixes k :: int
   20.13    shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
    21.1 --- a/src/HOL/Word/Word.thy	Sat Dec 17 15:22:14 2016 +0100
    21.2 +++ b/src/HOL/Word/Word.thy	Sat Dec 17 15:22:14 2016 +0100
    21.3 @@ -282,10 +282,10 @@
    21.4  subsection \<open>Arithmetic operations\<close>
    21.5  
    21.6  lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"
    21.7 -  by (metis bintr_ariths(6))
    21.8 +  by (auto simp add: bintrunc_mod2p intro: mod_add_cong)
    21.9  
   21.10  lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x - 1"
   21.11 -  by (metis bintr_ariths(7))
   21.12 +  by (auto simp add: bintrunc_mod2p intro: mod_diff_cong)
   21.13  
   21.14  instantiation word :: (len0) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}"
   21.15  begin
   21.16 @@ -295,16 +295,16 @@
   21.17  lift_definition one_word :: "'a word" is "1" .
   21.18  
   21.19  lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op +"
   21.20 -  by (metis bintr_ariths(2))
   21.21 +  by (auto simp add: bintrunc_mod2p intro: mod_add_cong)
   21.22  
   21.23  lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op -"
   21.24 -  by (metis bintr_ariths(3))
   21.25 +  by (auto simp add: bintrunc_mod2p intro: mod_diff_cong)
   21.26  
   21.27  lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus
   21.28 -  by (metis bintr_ariths(5))
   21.29 +  by (auto simp add: bintrunc_mod2p intro: mod_minus_cong)
   21.30  
   21.31  lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op *"
   21.32 -  by (metis bintr_ariths(4))
   21.33 +  by (auto simp add: bintrunc_mod2p intro: mod_mult_cong)
   21.34  
   21.35  definition
   21.36    word_div_def: "a div b = word_of_int (uint a div uint b)"
   21.37 @@ -332,9 +332,6 @@
   21.38    unfolding word_succ_def word_pred_def zero_word_def one_word_def
   21.39    by simp_all
   21.40  
   21.41 -lemmas arths = 
   21.42 -  bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1], folded word_ubin.eq_norm]
   21.43 -
   21.44  lemma wi_homs: 
   21.45    shows
   21.46    wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
   21.47 @@ -1340,10 +1337,11 @@
   21.48      and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)"
   21.49      and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0"
   21.50      and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1"
   21.51 -  by (simp_all add: uint_word_arith_bintrs
   21.52 -    [THEN uint_sint [symmetric, THEN trans],
   21.53 -    unfolded uint_sint bintr_arith1s bintr_ariths 
   21.54 -      len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep])
   21.55 +         apply (simp_all only: word_sbin.inverse_norm [symmetric])
   21.56 +         apply (simp_all add: wi_hom_syms)
   21.57 +   apply transfer apply simp
   21.58 +  apply transfer apply simp
   21.59 +  done
   21.60  
   21.61  lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
   21.62  lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
   21.63 @@ -1443,7 +1441,7 @@
   21.64    with \<open>1 \<le> uint w\<close> have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
   21.65      by auto
   21.66    then show ?thesis
   21.67 -    by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq [symmetric])
   21.68 +    by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq)
   21.69  qed
   21.70  
   21.71  lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
   21.72 @@ -2699,7 +2697,7 @@
   21.73  lemma nth_w2p:
   21.74    "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a::len)"
   21.75    unfolding test_bit_2p [symmetric] word_of_int [symmetric]
   21.76 -  by (simp add:  of_int_power)
   21.77 +  by simp
   21.78  
   21.79  lemma uint_2p: 
   21.80    "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
   21.81 @@ -2723,16 +2721,7 @@
   21.82    done
   21.83  
   21.84  lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
   21.85 -  apply (unfold word_arith_power_alt)
   21.86 -  apply (case_tac "len_of TYPE ('a)")
   21.87 -   apply clarsimp
   21.88 -  apply (case_tac "nat")
   21.89 -   apply (rule word_ubin.norm_eq_iff [THEN iffD1]) 
   21.90 -   apply (rule box_equals) 
   21.91 -     apply (rule_tac [2] bintr_ariths (1))+ 
   21.92 -   apply simp
   21.93 -  apply simp
   21.94 -  done
   21.95 +  by (induct n) (simp_all add: wi_hom_syms)
   21.96  
   21.97  lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)" 
   21.98    apply (rule xtr3) 
   21.99 @@ -3244,6 +3233,9 @@
  21.100  lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
  21.101    by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
  21.102  
  21.103 +lemma and_mask_wi': "word_of_int i AND mask n = (word_of_int (bintrunc (min LENGTH('a) n) i) :: 'a::len word)"
  21.104 +  by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
  21.105 +
  21.106  lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
  21.107    unfolding word_numeral_alt by (rule and_mask_wi)
  21.108  
  21.109 @@ -3342,12 +3334,12 @@
  21.110    "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
  21.111    "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
  21.112    using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
  21.113 -  by (auto simp: and_mask_wi bintr_ariths bintr_arith1s word_of_int_homs)
  21.114 +  by (auto simp add: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
  21.115  
  21.116  lemma mask_power_eq:
  21.117    "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
  21.118    using word_of_int_Ex [where x=x]
  21.119 -  by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
  21.120 +  by (auto simp add: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
  21.121  
  21.122  
  21.123  subsubsection \<open>Revcast\<close>
  21.124 @@ -4242,7 +4234,7 @@
  21.125    apply (simp add: word_size nat_mod_distrib)
  21.126    apply (rule of_nat_eq_0_iff [THEN iffD1])
  21.127    apply (auto simp add: not_le mod_eq_0_iff_dvd zdvd_int nat_add_distrib [symmetric])
  21.128 -  using mod_mod_trivial zmod_eq_dvd_iff
  21.129 +  using mod_mod_trivial mod_eq_dvd_iff
  21.130    apply blast
  21.131    done
  21.132  
  21.133 @@ -4579,9 +4571,9 @@
  21.134    shows "(x + y) mod b = z' mod b'"
  21.135  proof -
  21.136    from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
  21.137 -    by (simp add: mod_add_eq[symmetric])
  21.138 +    by (simp add: mod_add_eq)
  21.139    also have "\<dots> = (x' + y') mod b'"
  21.140 -    by (simp add: mod_add_eq[symmetric])
  21.141 +    by (simp add: mod_add_eq)
  21.142    finally show ?thesis by (simp add: 4)
  21.143  qed
  21.144  
  21.145 @@ -4591,11 +4583,8 @@
  21.146        and 3: "y mod b' = y' mod b'"
  21.147        and 4: "x' - y' = z'"
  21.148    shows "(x - y) mod b = z' mod b'"
  21.149 -  using assms
  21.150 -  apply (subst mod_diff_left_eq)
  21.151 -  apply (subst mod_diff_right_eq)
  21.152 -  apply (simp add: mod_diff_left_eq [symmetric] mod_diff_right_eq [symmetric])
  21.153 -  done
  21.154 +  using 1 2 3 4 [symmetric]
  21.155 +  by (auto intro: mod_diff_cong)
  21.156  
  21.157  lemma word_induct_less: 
  21.158    "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
    22.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Sat Dec 17 15:22:14 2016 +0100
    22.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Sat Dec 17 15:22:14 2016 +0100
    22.3 @@ -201,10 +201,6 @@
    22.4  
    22.5  lemmas push_mods = push_mods' [THEN eq_reflection]
    22.6  lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection]
    22.7 -lemmas mod_simps = 
    22.8 -  mod_mult_self2_is_0 [THEN eq_reflection]
    22.9 -  mod_mult_self1_is_0 [THEN eq_reflection]
   22.10 -  mod_mod_trivial [THEN eq_reflection]
   22.11  
   22.12  lemma nat_mod_eq:
   22.13    "!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)" 
    23.1 --- a/src/HOL/ex/Word_Type.thy	Sat Dec 17 15:22:14 2016 +0100
    23.2 +++ b/src/HOL/ex/Word_Type.thy	Sat Dec 17 15:22:14 2016 +0100
    23.3 @@ -57,7 +57,7 @@
    23.4  
    23.5  lemma bitrunc_plus:
    23.6    "bitrunc n (bitrunc n a + bitrunc n b) = bitrunc n (a + b)"
    23.7 -  by (simp add: bitrunc_eq_mod mod_add_eq [symmetric])
    23.8 +  by (simp add: bitrunc_eq_mod mod_add_eq)
    23.9  
   23.10  lemma bitrunc_of_1_eq_0_iff [simp]:
   23.11    "bitrunc n 1 = 0 \<longleftrightarrow> n = 0"
   23.12 @@ -74,12 +74,12 @@
   23.13  lemma bitrunc_uminus:
   23.14    fixes k :: int
   23.15    shows "bitrunc n (- (bitrunc n k)) = bitrunc n (- k)"
   23.16 -  by (simp add: bitrunc_eq_mod mod_minus_eq [symmetric])
   23.17 +  by (simp add: bitrunc_eq_mod mod_minus_eq)
   23.18  
   23.19  lemma bitrunc_minus:
   23.20    fixes k l :: int
   23.21    shows "bitrunc n (bitrunc n k - bitrunc n l) = bitrunc n (k - l)"
   23.22 -  by (simp add: bitrunc_eq_mod mod_diff_eq [symmetric])
   23.23 +  by (simp add: bitrunc_eq_mod mod_diff_eq)
   23.24  
   23.25  lemma bitrunc_nonnegative [simp]:
   23.26    fixes k :: int
   23.27 @@ -279,7 +279,7 @@
   23.28  
   23.29  lemma of_int_signed [simp]:
   23.30    "of_int (signed a) = a"
   23.31 -  by transfer (simp add: signed_bitrunc_eq_bitrunc bitrunc_eq_mod zdiff_zmod_left)
   23.32 +  by transfer (simp add: signed_bitrunc_eq_bitrunc bitrunc_eq_mod mod_simps)
   23.33  
   23.34  
   23.35  subsubsection \<open>Properties\<close>