more standardized theorem names for facts involving the div and mod identity
authorhaftmann
Sun Oct 16 09:31:05 2016 +0200 (2016-10-16)
changeset 6424293c6f0da5c70
parent 64241 430d74089d4d
child 64243 aee949f6642d
more standardized theorem names for facts involving the div and mod identity
NEWS
src/Doc/Tutorial/Rules/Force.thy
src/Doc/Tutorial/Rules/Forward.thy
src/Doc/Tutorial/Types/Numbers.thy
src/Doc/Tutorial/document/numerics.tex
src/Doc/Tutorial/document/rules.tex
src/HOL/Data_Structures/RBT_Set.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/Hoare_Parallel/OG_Examples.thy
src/HOL/Library/Code_Target_Int.thy
src/HOL/Library/Code_Target_Nat.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/Library/Stream.thy
src/HOL/Nonstandard_Analysis/StarDef.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Old_Number_Theory/Pocklington.thy
src/HOL/Presburger.thy
src/HOL/Rings.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Word.thy
src/HOL/ex/Transfer_Ex.thy
src/HOL/ex/Word_Type.thy
     1.1 --- a/NEWS	Sun Oct 16 09:31:04 2016 +0200
     1.2 +++ b/NEWS	Sun Oct 16 09:31:05 2016 +0200
     1.3 @@ -262,6 +262,14 @@
     1.4      div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
     1.5      is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
     1.6      is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
     1.7 +    mod_div_equality ~> div_mult_mod_eq
     1.8 +    mod_div_equality2 ~> mult_div_mod_eq
     1.9 +    mod_div_equality3 ~> mod_div_mult_eq
    1.10 +    mod_div_equality4 ~> mod_mult_div_eq
    1.11 +    minus_div_eq_mod ~> minus_div_mult_eq_mod
    1.12 +    minus_div_eq_mod2 ~> minus_mult_div_eq_mod
    1.13 +    minus_mod_eq_div ~> minus_mod_eq_div_mult
    1.14 +    minus_mod_eq_div2 ~> minus_mod_eq_mult_div
    1.15  INCOMPATIBILITY.
    1.16  
    1.17  * Dedicated syntax LENGTH('a) for length of types.
     2.1 --- a/src/Doc/Tutorial/Rules/Force.thy	Sun Oct 16 09:31:04 2016 +0200
     2.2 +++ b/src/Doc/Tutorial/Rules/Force.thy	Sun Oct 16 09:31:05 2016 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  
     2.5  lemma div_mult_self_is_m: 
     2.6        "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
     2.7 -apply (insert mod_div_equality [of "m*n" n])
     2.8 +apply (insert div_mult_mod_eq [of "m*n" n])
     2.9  apply simp
    2.10  done
    2.11  
     3.1 --- a/src/Doc/Tutorial/Rules/Forward.thy	Sun Oct 16 09:31:04 2016 +0200
     3.2 +++ b/src/Doc/Tutorial/Rules/Forward.thy	Sun Oct 16 09:31:05 2016 +0200
     3.3 @@ -183,8 +183,8 @@
     3.4  
     3.5  Another example of "insert"
     3.6  
     3.7 -@{thm[display] mod_div_equality}
     3.8 -\rulename{mod_div_equality}
     3.9 +@{thm[display] div_mult_mod_eq}
    3.10 +\rulename{div_mult_mod_eq}
    3.11  *}
    3.12  
    3.13  (*MOVED to Force.thy, which now depends only on Divides.thy
     4.1 --- a/src/Doc/Tutorial/Types/Numbers.thy	Sun Oct 16 09:31:04 2016 +0200
     4.2 +++ b/src/Doc/Tutorial/Types/Numbers.thy	Sun Oct 16 09:31:05 2016 +0200
     4.3 @@ -86,8 +86,8 @@
     4.4  @{thm[display] mod_if[no_vars]}
     4.5  \rulename{mod_if}
     4.6  
     4.7 -@{thm[display] mod_div_equality[no_vars]}
     4.8 -\rulename{mod_div_equality}
     4.9 +@{thm[display] div_mult_mod_eq[no_vars]}
    4.10 +\rulename{div_mult_mod_eq}
    4.11  
    4.12  
    4.13  @{thm[display] div_mult1_eq[no_vars]}
     5.1 --- a/src/Doc/Tutorial/document/numerics.tex	Sun Oct 16 09:31:04 2016 +0200
     5.2 +++ b/src/Doc/Tutorial/document/numerics.tex	Sun Oct 16 09:31:05 2016 +0200
     5.3 @@ -143,7 +143,7 @@
     5.4  m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
     5.5  \rulename{mod_if}\isanewline
     5.6  m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
     5.7 -\rulenamedx{mod_div_equality}
     5.8 +\rulenamedx{div_mult_mod_eq}
     5.9  \end{isabelle}
    5.10  
    5.11  Many less obvious facts about quotient and remainder are also provided. 
     6.1 --- a/src/Doc/Tutorial/document/rules.tex	Sun Oct 16 09:31:04 2016 +0200
     6.2 +++ b/src/Doc/Tutorial/document/rules.tex	Sun Oct 16 09:31:05 2016 +0200
     6.3 @@ -2175,7 +2175,7 @@
     6.4  remainder obey a well-known law: 
     6.5  \begin{isabelle}
     6.6  (?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m
     6.7 -\rulename{mod_div_equality}
     6.8 +\rulename{div_mult_mod_eq}
     6.9  \end{isabelle}
    6.10  
    6.11  We refer to this law explicitly in the following proof: 
    6.12 @@ -2183,7 +2183,7 @@
    6.13  \isacommand{lemma}\ div_mult_self_is_m:\ \isanewline
    6.14  \ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m*n)\ div\ n\ =\
    6.15  (m::nat)"\isanewline
    6.16 -\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m*n"\ n])\isanewline
    6.17 +\isacommand{apply}\ (insert\ div_mult_mod_eq\ [of\ "m*n"\ n])\isanewline
    6.18  \isacommand{apply}\ (simp)\isanewline
    6.19  \isacommand{done}
    6.20  \end{isabelle}
     7.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Sun Oct 16 09:31:04 2016 +0200
     7.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Oct 16 09:31:05 2016 +0200
     7.3 @@ -419,7 +419,7 @@
     7.4  next
     7.5    case (2 h t t')
     7.6    with RB_mod obtain n where "2*n + 1 = h" 
     7.7 -    by (metis color.distinct(1) mod_div_equality2 parity) 
     7.8 +    by (metis color.distinct(1) mult_div_mod_eq parity) 
     7.9    with 2 balB_h RB_h show ?case by auto
    7.10  next
    7.11    case (3 h t t')
     8.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:04 2016 +0200
     8.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:05 2016 +0200
     8.3 @@ -4426,7 +4426,7 @@
     8.4    "n \<le> m \<longleftrightarrow> real n \<le> real m"
     8.5    "n < m \<longleftrightarrow> real n < real m"
     8.6    "n \<in> {m .. l} \<longleftrightarrow> real n \<in> {real m .. real l}"
     8.7 -  by (simp_all add: real_div_nat_eq_floor_of_divide mod_div_equality')
     8.8 +  by (simp_all add: real_div_nat_eq_floor_of_divide div_mult_mod_eq')
     8.9  
    8.10  ML_file "approximation.ML"
    8.11  
     9.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Oct 16 09:31:04 2016 +0200
     9.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sun Oct 16 09:31:05 2016 +0200
     9.3 @@ -56,7 +56,7 @@
     9.4        addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     9.5      val simpset0 =
     9.6        put_simpset HOL_basic_ss ctxt
     9.7 -      addsimps @{thms mod_div_equality' Suc_eq_plus1 simp_thms}
     9.8 +      addsimps @{thms div_mult_mod_eq' Suc_eq_plus1 simp_thms}
     9.9        |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max}
    9.10      (* Simp rules for changing (n::int) to int n *)
    9.11      val simpset1 =
    10.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Oct 16 09:31:04 2016 +0200
    10.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Oct 16 09:31:05 2016 +0200
    10.3 @@ -31,7 +31,7 @@
    10.4               @{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
    10.5  val comp_ths = distinct Thm.eq_thm (ths @ comp_arith @ @{thms simp_thms});
    10.6  
    10.7 -val mod_div_equality' = @{thm "mod_div_equality'"};
    10.8 +val div_mult_mod_eq' = @{thm "div_mult_mod_eq'"};
    10.9  val mod_add_eq = @{thm "mod_add_eq"} RS sym;
   10.10  
   10.11  fun prepare_for_mir q fm = 
   10.12 @@ -80,7 +80,7 @@
   10.13                          addsimps @{thms add.assoc add.commute add.left_commute}
   10.14                          addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
   10.15      val simpset0 = put_simpset HOL_basic_ss ctxt
   10.16 -      addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
   10.17 +      addsimps [div_mult_mod_eq', @{thm Suc_eq_plus1}]
   10.18        addsimps comp_ths
   10.19        |> fold Splitter.add_split
   10.20            [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
    11.1 --- a/src/HOL/Divides.thy	Sun Oct 16 09:31:04 2016 +0200
    11.2 +++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:05 2016 +0200
    11.3 @@ -29,16 +29,16 @@
    11.4  text \<open>@{const divide} and @{const modulo}\<close>
    11.5  
    11.6  lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
    11.7 -  by (simp add: mod_div_equality)
    11.8 +  by (simp add: div_mult_mod_eq)
    11.9  
   11.10  lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
   11.11 -  by (simp add: mod_div_equality2)
   11.12 +  by (simp add: mult_div_mod_eq)
   11.13  
   11.14  lemma mod_by_0 [simp]: "a mod 0 = a"
   11.15 -  using mod_div_equality [of a zero] by simp
   11.16 +  using div_mult_mod_eq [of a zero] by simp
   11.17  
   11.18  lemma mod_0 [simp]: "0 mod a = 0"
   11.19 -  using mod_div_equality [of zero a] div_0 by simp
   11.20 +  using div_mult_mod_eq [of zero a] div_0 by simp
   11.21  
   11.22  lemma div_mult_self2 [simp]:
   11.23    assumes "b \<noteq> 0"
   11.24 @@ -61,14 +61,14 @@
   11.25  next
   11.26    case False
   11.27    have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
   11.28 -    by (simp add: mod_div_equality)
   11.29 +    by (simp add: div_mult_mod_eq)
   11.30    also from False div_mult_self1 [of b a c] have
   11.31      "\<dots> = (c + a div b) * b + (a + c * b) mod b"
   11.32        by (simp add: algebra_simps)
   11.33    finally have "a = a div b * b + (a + c * b) mod b"
   11.34      by (simp add: add.commute [of a] add.assoc distrib_right)
   11.35    then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
   11.36 -    by (simp add: mod_div_equality)
   11.37 +    by (simp add: div_mult_mod_eq)
   11.38    then show ?thesis by simp
   11.39  qed
   11.40  
   11.41 @@ -95,7 +95,7 @@
   11.42  lemma mod_by_1 [simp]:
   11.43    "a mod 1 = 0"
   11.44  proof -
   11.45 -  from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
   11.46 +  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
   11.47    then have "a + a mod 1 = a + 0" by simp
   11.48    then show ?thesis by (rule add_left_imp_eq)
   11.49  qed
   11.50 @@ -138,7 +138,7 @@
   11.51    then show "a mod b = 0" by simp
   11.52  next
   11.53    assume "a mod b = 0"
   11.54 -  with mod_div_equality [of a b] have "a div b * b = a" by simp
   11.55 +  with div_mult_mod_eq [of a b] have "a div b * b = a" by simp
   11.56    then have "a = b * (a div b)" by (simp add: ac_simps)
   11.57    then show "b dvd a" ..
   11.58  qed
   11.59 @@ -157,7 +157,7 @@
   11.60    hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
   11.61      by (rule div_mult_self1 [symmetric])
   11.62    also have "\<dots> = a div b"
   11.63 -    by (simp only: mod_div_equality3)
   11.64 +    by (simp only: mod_div_mult_eq)
   11.65    also have "\<dots> = a div b + 0"
   11.66      by simp
   11.67    finally show ?thesis
   11.68 @@ -170,7 +170,7 @@
   11.69    have "a mod b mod b = (a mod b + a div b * b) mod b"
   11.70      by (simp only: mod_mult_self1)
   11.71    also have "\<dots> = a mod b"
   11.72 -    by (simp only: mod_div_equality3)
   11.73 +    by (simp only: mod_div_mult_eq)
   11.74    finally show ?thesis .
   11.75  qed
   11.76  
   11.77 @@ -180,7 +180,7 @@
   11.78  proof -
   11.79    from assms have "k dvd (m div n) * n + m mod n"
   11.80      by (simp only: dvd_add dvd_mult)
   11.81 -  then show ?thesis by (simp add: mod_div_equality)
   11.82 +  then show ?thesis by (simp add: div_mult_mod_eq)
   11.83  qed
   11.84  
   11.85  text \<open>Addition respects modular equivalence.\<close>
   11.86 @@ -189,7 +189,7 @@
   11.87    "(a + b) mod c = (a mod c + b) mod c"
   11.88  proof -
   11.89    have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
   11.90 -    by (simp only: mod_div_equality)
   11.91 +    by (simp only: div_mult_mod_eq)
   11.92    also have "\<dots> = (a mod c + b + a div c * c) mod c"
   11.93      by (simp only: ac_simps)
   11.94    also have "\<dots> = (a mod c + b) mod c"
   11.95 @@ -201,7 +201,7 @@
   11.96    "(a + b) mod c = (a + b mod c) mod c"
   11.97  proof -
   11.98    have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
   11.99 -    by (simp only: mod_div_equality)
  11.100 +    by (simp only: div_mult_mod_eq)
  11.101    also have "\<dots> = (a + b mod c + b div c * c) mod c"
  11.102      by (simp only: ac_simps)
  11.103    also have "\<dots> = (a + b mod c) mod c"
  11.104 @@ -230,7 +230,7 @@
  11.105    "(a * b) mod c = ((a mod c) * b) mod c"
  11.106  proof -
  11.107    have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
  11.108 -    by (simp only: mod_div_equality)
  11.109 +    by (simp only: div_mult_mod_eq)
  11.110    also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
  11.111      by (simp only: algebra_simps)
  11.112    also have "\<dots> = (a mod c * b) mod c"
  11.113 @@ -242,7 +242,7 @@
  11.114    "(a * b) mod c = (a * (b mod c)) mod c"
  11.115  proof -
  11.116    have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
  11.117 -    by (simp only: mod_div_equality)
  11.118 +    by (simp only: div_mult_mod_eq)
  11.119    also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
  11.120      by (simp only: algebra_simps)
  11.121    also have "\<dots> = (a * (b mod c)) mod c"
  11.122 @@ -287,7 +287,7 @@
  11.123    also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
  11.124      by (simp only: ac_simps)
  11.125    also have "\<dots> = a mod c"
  11.126 -    by (simp only: mod_div_equality)
  11.127 +    by (simp only: div_mult_mod_eq)
  11.128    finally show ?thesis .
  11.129  qed
  11.130  
  11.131 @@ -305,11 +305,11 @@
  11.132    case True then show ?thesis by simp
  11.133  next
  11.134    case False
  11.135 -  from mod_div_equality
  11.136 +  from div_mult_mod_eq
  11.137    have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
  11.138    with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
  11.139      = c * a + c * (a mod b)" by (simp add: algebra_simps)
  11.140 -  with mod_div_equality show ?thesis by simp
  11.141 +  with div_mult_mod_eq show ?thesis by simp
  11.142  qed
  11.143  
  11.144  lemma mod_mult_mult2:
  11.145 @@ -357,7 +357,7 @@
  11.146  lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
  11.147  proof -
  11.148    have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
  11.149 -    by (simp only: mod_div_equality)
  11.150 +    by (simp only: div_mult_mod_eq)
  11.151    also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
  11.152      by (simp add: ac_simps)
  11.153    also have "\<dots> = (- (a mod b)) mod b"
  11.154 @@ -467,7 +467,7 @@
  11.155    case True then show ?thesis by simp
  11.156  next
  11.157    case False
  11.158 -  from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
  11.159 +  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
  11.160    with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
  11.161    then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
  11.162    then have "1 div 2 = 0 \<or> 2 = 0" by simp
  11.163 @@ -502,7 +502,7 @@
  11.164  next
  11.165    fix a
  11.166    assume "a mod 2 = 1"
  11.167 -  then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
  11.168 +  then have "a = a div 2 * 2 + 1" using div_mult_mod_eq [of a 2] by simp
  11.169    then show "\<exists>b. a = b + 1" ..
  11.170  qed
  11.171  
  11.172 @@ -528,7 +528,7 @@
  11.173  
  11.174  lemma odd_two_times_div_two_succ [simp]:
  11.175    "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
  11.176 -  using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
  11.177 +  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
  11.178   
  11.179  end
  11.180  
  11.181 @@ -569,7 +569,7 @@
  11.182    "b * (a div b) = a - a mod b"
  11.183  proof -
  11.184    have "b * (a div b) + a mod b = a"
  11.185 -    using mod_div_equality [of a b] by (simp add: ac_simps)
  11.186 +    using div_mult_mod_eq [of a b] by (simp add: ac_simps)
  11.187    then have "b * (a div b) + a mod b - a mod b = a - a mod b"
  11.188      by simp
  11.189    then show ?thesis
  11.190 @@ -1107,7 +1107,7 @@
  11.191    fixes m n :: nat
  11.192    shows "m mod n \<le> m"
  11.193  proof (rule add_leD2)
  11.194 -  from mod_div_equality have "m div n * n + m mod n = m" .
  11.195 +  from div_mult_mod_eq have "m div n * n + m mod n = m" .
  11.196    then show "m div n * n + m mod n \<le> m" by auto
  11.197  qed
  11.198  
  11.199 @@ -1120,9 +1120,9 @@
  11.200  lemma mod_1 [simp]: "m mod Suc 0 = 0"
  11.201  by (induct m) (simp_all add: mod_geq)
  11.202  
  11.203 -(* a simple rearrangement of mod_div_equality: *)
  11.204 +(* a simple rearrangement of div_mult_mod_eq: *)
  11.205  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
  11.206 -  using mod_div_equality2 [of n m] by arith
  11.207 +  using mult_div_mod_eq [of n m] by arith
  11.208  
  11.209  lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
  11.210    apply (drule mod_less_divisor [where m = m])
  11.211 @@ -1279,7 +1279,7 @@
  11.212    assumes "m mod d = r"
  11.213    shows "\<exists>q. m = r + q * d"
  11.214  proof -
  11.215 -  from mod_div_equality obtain q where "q * d + m mod d = m" by blast
  11.216 +  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
  11.217    with assms have "m = r + q * d" by simp
  11.218    then show ?thesis ..
  11.219  qed
  11.220 @@ -1387,11 +1387,11 @@
  11.221    qed
  11.222  qed
  11.223  
  11.224 -theorem mod_div_equality' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n"
  11.225 -  using mod_div_equality [of m n] by arith
  11.226 +theorem div_mult_mod_eq' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n"
  11.227 +  using div_mult_mod_eq [of m n] by arith
  11.228  
  11.229  lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
  11.230 -  using mod_div_equality [of m n] by arith
  11.231 +  using div_mult_mod_eq [of m n] by arith
  11.232  (* FIXME: very similar to mult_div_cancel *)
  11.233  
  11.234  lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
  11.235 @@ -1812,7 +1812,7 @@
  11.236  text\<open>Basic laws about division and remainder\<close>
  11.237  
  11.238  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
  11.239 -  by (fact mod_div_equality2 [symmetric])
  11.240 +  by (fact mult_div_mod_eq [symmetric])
  11.241  
  11.242  lemma zdiv_int: "int (a div b) = int a div int b"
  11.243    by (simp add: divide_int_def)
  11.244 @@ -2051,7 +2051,7 @@
  11.245  
  11.246  lemma zmod_zdiv_equality' [nitpick_unfold]:
  11.247    "(m::int) mod n = m - (m div n) * n"
  11.248 -  using mod_div_equality [of m n] by arith
  11.249 +  using div_mult_mod_eq [of m n] by arith
  11.250  
  11.251  
  11.252  subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
  11.253 @@ -2282,7 +2282,7 @@
  11.254    shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
  11.255  proof -
  11.256    have "i mod k = i \<longleftrightarrow> i div k = 0"
  11.257 -    by safe (insert mod_div_equality [of i k], auto)
  11.258 +    by safe (insert div_mult_mod_eq [of i k], auto)
  11.259    with zdiv_eq_0_iff
  11.260    show ?thesis
  11.261      by simp
    12.1 --- a/src/HOL/GCD.thy	Sun Oct 16 09:31:04 2016 +0200
    12.2 +++ b/src/HOL/GCD.thy	Sun Oct 16 09:31:05 2016 +0200
    12.3 @@ -1920,7 +1920,7 @@
    12.4      apply (simp add: bezw_non_0 gcd_non_0_nat)
    12.5      apply (erule subst)
    12.6      apply (simp add: field_simps)
    12.7 -    apply (subst mod_div_equality [of m n, symmetric])
    12.8 +    apply (subst div_mult_mod_eq [of m n, symmetric])
    12.9        (* applying simp here undoes the last substitution! what is procedure cancel_div_mod? *)
   12.10      apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
   12.11      done
    13.1 --- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Sun Oct 16 09:31:04 2016 +0200
    13.2 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Sun Oct 16 09:31:05 2016 +0200
    13.3 @@ -347,10 +347,10 @@
    13.4  
    13.5  lemma mod_lemma: "\<lbrakk> (c::nat) \<le> a; a < b; b - c < n \<rbrakk> \<Longrightarrow> b mod n \<noteq> a mod n"
    13.6  apply(subgoal_tac "b=b div n*n + b mod n" )
    13.7 - prefer 2  apply (simp add: mod_div_equality [symmetric])
    13.8 + prefer 2  apply (simp add: div_mult_mod_eq [symmetric])
    13.9  apply(subgoal_tac "a=a div n*n + a mod n")
   13.10   prefer 2
   13.11 - apply(simp add: mod_div_equality [symmetric])
   13.12 + apply(simp add: div_mult_mod_eq [symmetric])
   13.13  apply(subgoal_tac "b - a \<le> b - c")
   13.14   prefer 2 apply arith
   13.15  apply(drule le_less_trans)
    14.1 --- a/src/HOL/Library/Code_Target_Int.thy	Sun Oct 16 09:31:04 2016 +0200
    14.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Sun Oct 16 09:31:05 2016 +0200
    14.3 @@ -115,7 +115,7 @@
    14.4         j = k mod 2
    14.5       in if j = 0 then l else l + 1)"
    14.6  proof -
    14.7 -  from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
    14.8 +  from div_mult_mod_eq have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
    14.9    show ?thesis
   14.10      by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
   14.11  qed
    15.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Sun Oct 16 09:31:04 2016 +0200
    15.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Oct 16 09:31:05 2016 +0200
    15.3 @@ -115,7 +115,7 @@
    15.4         m' = 2 * of_nat m
    15.5       in if q = 0 then m' else m' + 1)"
    15.6  proof -
    15.7 -  from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
    15.8 +  from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
    15.9    show ?thesis
   15.10      by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric])
   15.11        (simp add: * mult.commute of_nat_mult add.commute)
    16.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 16 09:31:04 2016 +0200
    16.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 16 09:31:05 2016 +0200
    16.3 @@ -1302,13 +1302,13 @@
    16.4  proof (cases "f div g * g = 0")
    16.5    assume "f div g * g \<noteq> 0"
    16.6    hence [simp]: "f div g \<noteq> 0" "g \<noteq> 0" by auto
    16.7 -  from mod_div_equality[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps)
    16.8 +  from div_mult_mod_eq[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps)
    16.9    also from assms have "subdegree ... = subdegree f"
   16.10      by (intro subdegree_diff_eq1) simp_all
   16.11    finally show ?thesis .
   16.12  next
   16.13    assume zero: "f div g * g = 0"
   16.14 -  from mod_div_equality[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps)
   16.15 +  from div_mult_mod_eq[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps)
   16.16    also note zero
   16.17    finally show ?thesis by simp
   16.18  qed
    17.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Sun Oct 16 09:31:04 2016 +0200
    17.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Sun Oct 16 09:31:05 2016 +0200
    17.3 @@ -1038,7 +1038,7 @@
    17.4    thus "is_unit (unit_factor_field_poly p)"
    17.5      by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
    17.6  qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
    17.7 -       euclidean_size_field_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le)
    17.8 +       euclidean_size_field_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
    17.9  
   17.10  lemma field_poly_irreducible_imp_prime:
   17.11    assumes "irreducible (p :: 'a :: field poly)"
   17.12 @@ -1356,7 +1356,7 @@
   17.13    "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
   17.14  
   17.15  instance 
   17.16 -  by standard (auto simp: euclidean_size_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le)
   17.17 +  by standard (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
   17.18  end
   17.19  
   17.20  
    18.1 --- a/src/HOL/Library/Stream.thy	Sun Oct 16 09:31:04 2016 +0200
    18.2 +++ b/src/HOL/Library/Stream.thy	Sun Oct 16 09:31:05 2016 +0200
    18.3 @@ -336,7 +336,7 @@
    18.4  
    18.5  lemma stake_cycle: "u \<noteq> [] \<Longrightarrow>
    18.6     stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u"
    18.7 -  by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto
    18.8 +  by (subst div_mult_mod_eq[of n "length u", symmetric], unfold stake_add[symmetric]) auto
    18.9  
   18.10  lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)"
   18.11    by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
    19.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 16 09:31:04 2016 +0200
    19.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 16 09:31:05 2016 +0200
    19.3 @@ -863,7 +863,7 @@
    19.4    by (intro_classes; transfer) simp_all
    19.5  
    19.6  instance star :: (semiring_div) semiring_div
    19.7 -  by (intro_classes; transfer) (simp_all add: mod_div_equality)
    19.8 +  by (intro_classes; transfer) (simp_all add: div_mult_mod_eq)
    19.9  
   19.10  instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
   19.11  instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
    20.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:04 2016 +0200
    20.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:05 2016 +0200
    20.3 @@ -27,7 +27,7 @@
    20.4  begin
    20.5  
    20.6  lemma mod_0 [simp]: "0 mod a = 0"
    20.7 -  using mod_div_equality [of 0 a] by simp
    20.8 +  using div_mult_mod_eq [of 0 a] by simp
    20.9  
   20.10  lemma dvd_mod_iff: 
   20.11    assumes "k dvd n"
   20.12 @@ -36,7 +36,7 @@
   20.13    from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" 
   20.14      by (simp add: dvd_add_right_iff)
   20.15    also have "(m div n) * n + m mod n = m"
   20.16 -    using mod_div_equality [of m n] by simp
   20.17 +    using div_mult_mod_eq [of m n] by simp
   20.18    finally show ?thesis .
   20.19  qed
   20.20  
   20.21 @@ -46,7 +46,7 @@
   20.22  proof -
   20.23    have "b dvd ((a div b) * b)" by simp
   20.24    also have "(a div b) * b = a"
   20.25 -    using mod_div_equality [of a b] by (simp add: assms)
   20.26 +    using div_mult_mod_eq [of a b] by (simp add: assms)
   20.27    finally show ?thesis .
   20.28  qed
   20.29  
   20.30 @@ -72,7 +72,7 @@
   20.31    obtains s and t where "a = s * b + t" 
   20.32      and "euclidean_size t < euclidean_size b"
   20.33  proof -
   20.34 -  from mod_div_equality [of a b] 
   20.35 +  from div_mult_mod_eq [of a b] 
   20.36       have "a = a div b * b + a mod b" by simp
   20.37    with that and assms show ?thesis by (auto simp add: mod_size_less)
   20.38  qed
   20.39 @@ -507,7 +507,7 @@
   20.40                (s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps)
   20.41        also have "s' * a + t' * b = r'" by fact
   20.42        also have "s * a + t * b = r" by fact
   20.43 -      also have "r' - r' div r * r = r' mod r" using mod_div_equality [of r' r]
   20.44 +      also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
   20.45          by (simp add: algebra_simps)
   20.46        finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
   20.47      qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')
    21.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sun Oct 16 09:31:04 2016 +0200
    21.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Sun Oct 16 09:31:05 2016 +0200
    21.3 @@ -227,7 +227,7 @@
    21.4      {assume nm1: "(n - 1) mod m > 0"
    21.5        from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast
    21.6        let ?y = "a^ ((n - 1) div m * m)"
    21.7 -      note mdeq = mod_div_equality[of "(n - 1)" m]
    21.8 +      note mdeq = div_mult_mod_eq[of "(n - 1)" m]
    21.9        have yn: "coprime ?y n"
   21.10          by (metis an(1) coprime_exp gcd.commute)
   21.11        have "?y mod n = (a^m)^((n - 1) div m) mod n"
   21.12 @@ -239,7 +239,7 @@
   21.13        finally have th3: "?y mod n = 1"  .
   21.14        have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
   21.15          using an1[unfolded cong_nat_def onen] onen
   21.16 -          mod_div_equality[of "(n - 1)" m, symmetric]
   21.17 +          div_mult_mod_eq[of "(n - 1)" m, symmetric]
   21.18          by (simp add:power_add[symmetric] cong_nat_def th3 del: One_nat_def)
   21.19        have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)"
   21.20          by (metis cong_mult_rcancel_nat mult.commute th2 yn)
   21.21 @@ -362,7 +362,7 @@
   21.22        by (metis cong_exp_nat ord power_one)
   21.23      from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
   21.24      hence op: "?o > 0" by simp
   21.25 -    from mod_div_equality[of d "ord n a"] lh
   21.26 +    from div_mult_mod_eq[of d "ord n a"] lh
   21.27      have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: cong_nat_def mult.commute)
   21.28      hence "[(a^?o)^?q * (a^?r) = 1] (mod n)"
   21.29        by (simp add: cong_nat_def power_mult[symmetric] power_add[symmetric])
   21.30 @@ -618,7 +618,7 @@
   21.31      {assume b0: "b = 0"
   21.32        from p(2) nqr have "(n - 1) mod p = 0"
   21.33          by (metis mod_0 mod_mod_cancel mod_mult_self1_is_0)
   21.34 -      with mod_div_equality[of "n - 1" p]
   21.35 +      with div_mult_mod_eq[of "n - 1" p]
   21.36        have "(n - 1) div p * p= n - 1" by auto
   21.37        hence eq: "(a^((n - 1) div p))^p = a^(n - 1)"
   21.38          by (simp only: power_mult[symmetric])
   21.39 @@ -720,7 +720,7 @@
   21.40      unfolding arnb[symmetric] power_mod 
   21.41      by (simp_all add: power_mult[symmetric] algebra_simps)
   21.42    from n  have n0: "n > 0" by arith
   21.43 -  from mod_div_equality[of "a^(n - 1)" n]
   21.44 +  from div_mult_mod_eq[of "a^(n - 1)" n]
   21.45      mod_less_divisor[OF n0, of "a^(n - 1)"]
   21.46    have an1: "[a ^ (n - 1) = 1] (mod n)"
   21.47      by (metis bqn cong_nat_def mod_mod_trivial)
    22.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Oct 16 09:31:04 2016 +0200
    22.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Oct 16 09:31:05 2016 +0200
    22.3 @@ -744,7 +744,7 @@
    22.4      {assume nm1: "(n - 1) mod m > 0"
    22.5        from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast
    22.6        let ?y = "a^ ((n - 1) div m * m)"
    22.7 -      note mdeq = mod_div_equality[of "(n - 1)" m]
    22.8 +      note mdeq = div_mult_mod_eq[of "(n - 1)" m]
    22.9        from coprime_exp[OF an(1)[unfolded coprime_commute[of a n]],
   22.10          of "(n - 1) div m * m"]
   22.11        have yn: "coprime ?y n" by (simp add: coprime_commute)
   22.12 @@ -757,7 +757,7 @@
   22.13        finally have th3: "?y mod n = 1"  .
   22.14        have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
   22.15          using an1[unfolded modeq_def onen] onen
   22.16 -          mod_div_equality[of "(n - 1)" m, symmetric]
   22.17 +          div_mult_mod_eq[of "(n - 1)" m, symmetric]
   22.18          by (simp add:power_add[symmetric] modeq_def th3 del: One_nat_def)
   22.19        from cong_mult_lcancel[of ?y n "a^((n - 1) mod m)" 1, OF yn th2]
   22.20        have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)"  .
   22.21 @@ -855,7 +855,7 @@
   22.22      have eqo: "[(a^?o)^?q = 1] (mod n)"  by (simp add: modeq_def power_Suc0)
   22.23      from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
   22.24      hence op: "?o > 0" by simp
   22.25 -    from mod_div_equality[of d "ord n a"] lh
   22.26 +    from div_mult_mod_eq[of d "ord n a"] lh
   22.27      have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: modeq_def mult.commute)
   22.28      hence "[(a^?o)^?q * (a^?r) = 1] (mod n)"
   22.29        by (simp add: modeq_def power_mult[symmetric] power_add[symmetric])
   22.30 @@ -1108,7 +1108,7 @@
   22.31      {assume b0: "b = 0"
   22.32        from p(2) nqr have "(n - 1) mod p = 0"
   22.33          apply (simp only: dvd_eq_mod_eq_0[symmetric]) by (rule dvd_mult2, simp)
   22.34 -      with mod_div_equality[of "n - 1" p]
   22.35 +      with div_mult_mod_eq[of "n - 1" p]
   22.36        have "(n - 1) div p * p= n - 1" by auto
   22.37        hence eq: "(a^((n - 1) div p))^p = a^(n - 1)"
   22.38          by (simp only: power_mult[symmetric])
   22.39 @@ -1196,7 +1196,7 @@
   22.40  
   22.41  lemma mod_le: assumes n: "n \<noteq> (0::nat)" shows "m mod n \<le> m"
   22.42  proof-
   22.43 -    from mod_div_equality[of m n]
   22.44 +    from div_mult_mod_eq[of m n]
   22.45      have "\<exists>x. x + m mod n = m" by blast
   22.46      then show ?thesis by auto
   22.47  qed
   22.48 @@ -1214,7 +1214,7 @@
   22.49      and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"  unfolding arnb[symmetric] power_mod
   22.50      by (simp_all add: power_mult[symmetric] algebra_simps)
   22.51    from n  have n0: "n > 0" by arith
   22.52 -  from mod_div_equality[of "a^(n - 1)" n]
   22.53 +  from div_mult_mod_eq[of "a^(n - 1)" n]
   22.54      mod_less_divisor[OF n0, of "a^(n - 1)"]
   22.55    have an1: "[a ^ (n - 1) = 1] (mod n)"
   22.56      unfolding nat_mod bqn
    23.1 --- a/src/HOL/Presburger.thy	Sun Oct 16 09:31:04 2016 +0200
    23.2 +++ b/src/HOL/Presburger.thy	Sun Oct 16 09:31:05 2016 +0200
    23.3 @@ -420,8 +420,8 @@
    23.4  declare mod_div_trivial [presburger]
    23.5  declare div_mod_equality2 [presburger]
    23.6  declare div_mod_equality [presburger]
    23.7 -declare mod_div_equality2 [presburger]
    23.8 -declare mod_div_equality [presburger]
    23.9 +declare mult_div_mod_eq [presburger]
   23.10 +declare div_mult_mod_eq [presburger]
   23.11  declare mod_mult_self1 [presburger]
   23.12  declare mod_mult_self2 [presburger]
   23.13  declare mod2_Suc_Suc[presburger]
    24.1 --- a/src/HOL/Rings.thy	Sun Oct 16 09:31:04 2016 +0200
    24.2 +++ b/src/HOL/Rings.thy	Sun Oct 16 09:31:05 2016 +0200
    24.3 @@ -1290,7 +1290,7 @@
    24.4  text \<open>Arbitrary quotient and remainder partitions\<close>
    24.5  
    24.6  class semiring_modulo = comm_semiring_1_cancel + divide + modulo +
    24.7 -  assumes mod_div_equality: "a div b * b + a mod b = a"
    24.8 +  assumes div_mult_mod_eq: "a div b * b + a mod b = a"
    24.9  begin
   24.10  
   24.11  lemma mod_div_decomp:
   24.12 @@ -1298,35 +1298,35 @@
   24.13    obtains q r where "q = a div b" and "r = a mod b"
   24.14      and "a = q * b + r"
   24.15  proof -
   24.16 -  from mod_div_equality have "a = a div b * b + a mod b" by simp
   24.17 +  from div_mult_mod_eq have "a = a div b * b + a mod b" by simp
   24.18    moreover have "a div b = a div b" ..
   24.19    moreover have "a mod b = a mod b" ..
   24.20    note that ultimately show thesis by blast
   24.21  qed
   24.22  
   24.23 -lemma mod_div_equality2: "b * (a div b) + a mod b = a"
   24.24 -  using mod_div_equality [of a b] by (simp add: ac_simps)
   24.25 +lemma mult_div_mod_eq: "b * (a div b) + a mod b = a"
   24.26 +  using div_mult_mod_eq [of a b] by (simp add: ac_simps)
   24.27  
   24.28 -lemma mod_div_equality3: "a mod b + a div b * b = a"
   24.29 -  using mod_div_equality [of a b] by (simp add: ac_simps)
   24.30 +lemma mod_div_mult_eq: "a mod b + a div b * b = a"
   24.31 +  using div_mult_mod_eq [of a b] by (simp add: ac_simps)
   24.32  
   24.33 -lemma mod_div_equality4: "a mod b + b * (a div b) = a"
   24.34 -  using mod_div_equality [of a b] by (simp add: ac_simps)
   24.35 +lemma mod_mult_div_eq: "a mod b + b * (a div b) = a"
   24.36 +  using div_mult_mod_eq [of a b] by (simp add: ac_simps)
   24.37  
   24.38 -lemma minus_div_eq_mod: "a - a div b * b = a mod b"
   24.39 -  by (rule add_implies_diff [symmetric]) (fact mod_div_equality3)
   24.40 +lemma minus_div_mult_eq_mod: "a - a div b * b = a mod b"
   24.41 +  by (rule add_implies_diff [symmetric]) (fact mod_div_mult_eq)
   24.42  
   24.43 -lemma minus_div_eq_mod2: "a - b * (a div b) = a mod b"
   24.44 -  by (rule add_implies_diff [symmetric]) (fact mod_div_equality4)
   24.45 +lemma minus_mult_div_eq_mod: "a - b * (a div b) = a mod b"
   24.46 +  by (rule add_implies_diff [symmetric]) (fact mod_mult_div_eq)
   24.47  
   24.48 -lemma minus_mod_eq_div: "a - a mod b = a div b * b"
   24.49 -  by (rule add_implies_diff [symmetric]) (fact mod_div_equality)
   24.50 +lemma minus_mod_eq_div_mult: "a - a mod b = a div b * b"
   24.51 +  by (rule add_implies_diff [symmetric]) (fact div_mult_mod_eq)
   24.52  
   24.53 -lemma minus_mod_eq_div2: "a - a mod b = b * (a div b)"
   24.54 -  by (rule add_implies_diff [symmetric]) (fact mod_div_equality2)
   24.55 +lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)"
   24.56 +  by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq)
   24.57  
   24.58  end
   24.59 -  
   24.60 +
   24.61  
   24.62  class ordered_semiring = semiring + ordered_comm_monoid_add +
   24.63    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    25.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sun Oct 16 09:31:04 2016 +0200
    25.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Oct 16 09:31:05 2016 +0200
    25.3 @@ -835,7 +835,7 @@
    25.4     addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
    25.5  val splits_ss =
    25.6    simpset_of (put_simpset comp_ss @{context}
    25.7 -    addsimps [@{thm "mod_div_equality'"}]
    25.8 +    addsimps [@{thm "div_mult_mod_eq'"}]
    25.9      |> fold Splitter.add_split
   25.10        [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
   25.11         @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
    26.1 --- a/src/HOL/Word/Bit_Representation.thy	Sun Oct 16 09:31:04 2016 +0200
    26.2 +++ b/src/HOL/Word/Bit_Representation.thy	Sun Oct 16 09:31:05 2016 +0200
    26.3 @@ -43,7 +43,7 @@
    26.4  lemma bin_rl_simp [simp]:
    26.5    "bin_rest w BIT bin_last w = w"
    26.6    unfolding bin_rest_def bin_last_def Bit_def
    26.7 -  using mod_div_equality [of w 2]
    26.8 +  using div_mult_mod_eq [of w 2]
    26.9    by (cases "w mod 2 = 0", simp_all)
   26.10  
   26.11  lemma bin_rest_BIT [simp]: "bin_rest (x BIT b) = x"
    27.1 --- a/src/HOL/Word/Word.thy	Sun Oct 16 09:31:04 2016 +0200
    27.2 +++ b/src/HOL/Word/Word.thy	Sun Oct 16 09:31:05 2016 +0200
    27.3 @@ -2161,7 +2161,7 @@
    27.4    apply (unfold word_less_nat_alt word_arith_nat_defs)
    27.5    apply (cut_tac y="unat b" in gt_or_eq_0)
    27.6    apply (erule disjE)
    27.7 -   apply (simp only: mod_div_equality uno_simps Word.word_unat.Rep_inverse)
    27.8 +   apply (simp only: div_mult_mod_eq uno_simps Word.word_unat.Rep_inverse)
    27.9    apply simp
   27.10    done
   27.11  
   27.12 @@ -3867,7 +3867,7 @@
   27.13     apply clarsimp
   27.14    apply (clarsimp simp add : nth_append size_rcat_lem)
   27.15    apply (simp (no_asm_use) only:  mult_Suc [symmetric] 
   27.16 -         td_gal_lt_len less_Suc_eq_le mod_div_equality')
   27.17 +         td_gal_lt_len less_Suc_eq_le div_mult_mod_eq')
   27.18    apply clarsimp
   27.19    done
   27.20  
    28.1 --- a/src/HOL/ex/Transfer_Ex.thy	Sun Oct 16 09:31:04 2016 +0200
    28.2 +++ b/src/HOL/ex/Transfer_Ex.thy	Sun Oct 16 09:31:05 2016 +0200
    28.3 @@ -16,7 +16,7 @@
    28.4    by (fact ex1 [untransferred])
    28.5  
    28.6  lemma ex2: "(a::nat) div b * b + a mod b = a"
    28.7 -  by (rule mod_div_equality)
    28.8 +  by (rule div_mult_mod_eq)
    28.9  
   28.10  lemma "0 \<le> (b::int) \<Longrightarrow> 0 \<le> (a::int) \<Longrightarrow> a div b * b + a mod b = a"
   28.11    by (fact ex2 [transferred])
    29.1 --- a/src/HOL/ex/Word_Type.thy	Sun Oct 16 09:31:04 2016 +0200
    29.2 +++ b/src/HOL/ex/Word_Type.thy	Sun Oct 16 09:31:05 2016 +0200
    29.3 @@ -33,7 +33,7 @@
    29.4      where "b = a div 2" and "c = a mod 2"
    29.5    then have a: "a = b * 2 + c" 
    29.6      and "c = 0 \<or> c = 1"
    29.7 -    by (simp_all add: mod_div_equality parity)
    29.8 +    by (simp_all add: div_mult_mod_eq parity)
    29.9    from \<open>c = 0 \<or> c = 1\<close>
   29.10    have "bitrunc (Suc n) (b * 2 + c) = bitrunc n b * 2 + c"
   29.11    proof