src/HOL/Divides.thy
 changeset 64242 93c6f0da5c70 parent 64240 eabf80376aab child 64243 aee949f6642d
```     1.1 --- a/src/HOL/Divides.thy	Sun Oct 16 09:31:04 2016 +0200
1.2 +++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:05 2016 +0200
1.3 @@ -29,16 +29,16 @@
1.4  text \<open>@{const divide} and @{const modulo}\<close>
1.5
1.6  lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
1.7 -  by (simp add: mod_div_equality)
1.8 +  by (simp add: div_mult_mod_eq)
1.9
1.10  lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
1.11 -  by (simp add: mod_div_equality2)
1.12 +  by (simp add: mult_div_mod_eq)
1.13
1.14  lemma mod_by_0 [simp]: "a mod 0 = a"
1.15 -  using mod_div_equality [of a zero] by simp
1.16 +  using div_mult_mod_eq [of a zero] by simp
1.17
1.18  lemma mod_0 [simp]: "0 mod a = 0"
1.19 -  using mod_div_equality [of zero a] div_0 by simp
1.20 +  using div_mult_mod_eq [of zero a] div_0 by simp
1.21
1.22  lemma div_mult_self2 [simp]:
1.23    assumes "b \<noteq> 0"
1.24 @@ -61,14 +61,14 @@
1.25  next
1.26    case False
1.27    have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
1.28 -    by (simp add: mod_div_equality)
1.29 +    by (simp add: div_mult_mod_eq)
1.30    also from False div_mult_self1 [of b a c] have
1.31      "\<dots> = (c + a div b) * b + (a + c * b) mod b"
1.33    finally have "a = a div b * b + (a + c * b) mod b"
1.35    then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
1.36 -    by (simp add: mod_div_equality)
1.37 +    by (simp add: div_mult_mod_eq)
1.38    then show ?thesis by simp
1.39  qed
1.40
1.41 @@ -95,7 +95,7 @@
1.42  lemma mod_by_1 [simp]:
1.43    "a mod 1 = 0"
1.44  proof -
1.45 -  from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
1.46 +  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
1.47    then have "a + a mod 1 = a + 0" by simp
1.48    then show ?thesis by (rule add_left_imp_eq)
1.49  qed
1.50 @@ -138,7 +138,7 @@
1.51    then show "a mod b = 0" by simp
1.52  next
1.53    assume "a mod b = 0"
1.54 -  with mod_div_equality [of a b] have "a div b * b = a" by simp
1.55 +  with div_mult_mod_eq [of a b] have "a div b * b = a" by simp
1.56    then have "a = b * (a div b)" by (simp add: ac_simps)
1.57    then show "b dvd a" ..
1.58  qed
1.59 @@ -157,7 +157,7 @@
1.60    hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
1.61      by (rule div_mult_self1 [symmetric])
1.62    also have "\<dots> = a div b"
1.63 -    by (simp only: mod_div_equality3)
1.64 +    by (simp only: mod_div_mult_eq)
1.65    also have "\<dots> = a div b + 0"
1.66      by simp
1.67    finally show ?thesis
1.68 @@ -170,7 +170,7 @@
1.69    have "a mod b mod b = (a mod b + a div b * b) mod b"
1.70      by (simp only: mod_mult_self1)
1.71    also have "\<dots> = a mod b"
1.72 -    by (simp only: mod_div_equality3)
1.73 +    by (simp only: mod_div_mult_eq)
1.74    finally show ?thesis .
1.75  qed
1.76
1.77 @@ -180,7 +180,7 @@
1.78  proof -
1.79    from assms have "k dvd (m div n) * n + m mod n"
1.80      by (simp only: dvd_add dvd_mult)
1.81 -  then show ?thesis by (simp add: mod_div_equality)
1.82 +  then show ?thesis by (simp add: div_mult_mod_eq)
1.83  qed
1.84
1.85  text \<open>Addition respects modular equivalence.\<close>
1.86 @@ -189,7 +189,7 @@
1.87    "(a + b) mod c = (a mod c + b) mod c"
1.88  proof -
1.89    have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
1.90 -    by (simp only: mod_div_equality)
1.91 +    by (simp only: div_mult_mod_eq)
1.92    also have "\<dots> = (a mod c + b + a div c * c) mod c"
1.93      by (simp only: ac_simps)
1.94    also have "\<dots> = (a mod c + b) mod c"
1.95 @@ -201,7 +201,7 @@
1.96    "(a + b) mod c = (a + b mod c) mod c"
1.97  proof -
1.98    have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
1.99 -    by (simp only: mod_div_equality)
1.100 +    by (simp only: div_mult_mod_eq)
1.101    also have "\<dots> = (a + b mod c + b div c * c) mod c"
1.102      by (simp only: ac_simps)
1.103    also have "\<dots> = (a + b mod c) mod c"
1.104 @@ -230,7 +230,7 @@
1.105    "(a * b) mod c = ((a mod c) * b) mod c"
1.106  proof -
1.107    have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
1.108 -    by (simp only: mod_div_equality)
1.109 +    by (simp only: div_mult_mod_eq)
1.110    also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
1.111      by (simp only: algebra_simps)
1.112    also have "\<dots> = (a mod c * b) mod c"
1.113 @@ -242,7 +242,7 @@
1.114    "(a * b) mod c = (a * (b mod c)) mod c"
1.115  proof -
1.116    have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
1.117 -    by (simp only: mod_div_equality)
1.118 +    by (simp only: div_mult_mod_eq)
1.119    also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
1.120      by (simp only: algebra_simps)
1.121    also have "\<dots> = (a * (b mod c)) mod c"
1.122 @@ -287,7 +287,7 @@
1.123    also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
1.124      by (simp only: ac_simps)
1.125    also have "\<dots> = a mod c"
1.126 -    by (simp only: mod_div_equality)
1.127 +    by (simp only: div_mult_mod_eq)
1.128    finally show ?thesis .
1.129  qed
1.130
1.131 @@ -305,11 +305,11 @@
1.132    case True then show ?thesis by simp
1.133  next
1.134    case False
1.135 -  from mod_div_equality
1.136 +  from div_mult_mod_eq
1.137    have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
1.138    with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
1.139      = c * a + c * (a mod b)" by (simp add: algebra_simps)
1.140 -  with mod_div_equality show ?thesis by simp
1.141 +  with div_mult_mod_eq show ?thesis by simp
1.142  qed
1.143
1.144  lemma mod_mult_mult2:
1.145 @@ -357,7 +357,7 @@
1.146  lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
1.147  proof -
1.148    have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
1.149 -    by (simp only: mod_div_equality)
1.150 +    by (simp only: div_mult_mod_eq)
1.151    also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
1.153    also have "\<dots> = (- (a mod b)) mod b"
1.154 @@ -467,7 +467,7 @@
1.155    case True then show ?thesis by simp
1.156  next
1.157    case False
1.158 -  from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
1.159 +  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
1.160    with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
1.161    then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
1.162    then have "1 div 2 = 0 \<or> 2 = 0" by simp
1.163 @@ -502,7 +502,7 @@
1.164  next
1.165    fix a
1.166    assume "a mod 2 = 1"
1.167 -  then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
1.168 +  then have "a = a div 2 * 2 + 1" using div_mult_mod_eq [of a 2] by simp
1.169    then show "\<exists>b. a = b + 1" ..
1.170  qed
1.171
1.172 @@ -528,7 +528,7 @@
1.173
1.174  lemma odd_two_times_div_two_succ [simp]:
1.175    "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
1.176 -  using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
1.177 +  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
1.178
1.179  end
1.180
1.181 @@ -569,7 +569,7 @@
1.182    "b * (a div b) = a - a mod b"
1.183  proof -
1.184    have "b * (a div b) + a mod b = a"
1.185 -    using mod_div_equality [of a b] by (simp add: ac_simps)
1.186 +    using div_mult_mod_eq [of a b] by (simp add: ac_simps)
1.187    then have "b * (a div b) + a mod b - a mod b = a - a mod b"
1.188      by simp
1.189    then show ?thesis
1.190 @@ -1107,7 +1107,7 @@
1.191    fixes m n :: nat
1.192    shows "m mod n \<le> m"
1.194 -  from mod_div_equality have "m div n * n + m mod n = m" .
1.195 +  from div_mult_mod_eq have "m div n * n + m mod n = m" .
1.196    then show "m div n * n + m mod n \<le> m" by auto
1.197  qed
1.198
1.199 @@ -1120,9 +1120,9 @@
1.200  lemma mod_1 [simp]: "m mod Suc 0 = 0"
1.201  by (induct m) (simp_all add: mod_geq)
1.202
1.203 -(* a simple rearrangement of mod_div_equality: *)
1.204 +(* a simple rearrangement of div_mult_mod_eq: *)
1.205  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
1.206 -  using mod_div_equality2 [of n m] by arith
1.207 +  using mult_div_mod_eq [of n m] by arith
1.208
1.209  lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
1.210    apply (drule mod_less_divisor [where m = m])
1.211 @@ -1279,7 +1279,7 @@
1.212    assumes "m mod d = r"
1.213    shows "\<exists>q. m = r + q * d"
1.214  proof -
1.215 -  from mod_div_equality obtain q where "q * d + m mod d = m" by blast
1.216 +  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
1.217    with assms have "m = r + q * d" by simp
1.218    then show ?thesis ..
1.219  qed
1.220 @@ -1387,11 +1387,11 @@
1.221    qed
1.222  qed
1.223
1.224 -theorem mod_div_equality' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n"
1.225 -  using mod_div_equality [of m n] by arith
1.226 +theorem div_mult_mod_eq' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n"
1.227 +  using div_mult_mod_eq [of m n] by arith
1.228
1.229  lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
1.230 -  using mod_div_equality [of m n] by arith
1.231 +  using div_mult_mod_eq [of m n] by arith
1.232  (* FIXME: very similar to mult_div_cancel *)
1.233
1.234  lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
1.235 @@ -1812,7 +1812,7 @@
1.236  text\<open>Basic laws about division and remainder\<close>
1.237
1.238  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
1.239 -  by (fact mod_div_equality2 [symmetric])
1.240 +  by (fact mult_div_mod_eq [symmetric])
1.241
1.242  lemma zdiv_int: "int (a div b) = int a div int b"
1.244 @@ -2051,7 +2051,7 @@
1.245
1.246  lemma zmod_zdiv_equality' [nitpick_unfold]:
1.247    "(m::int) mod n = m - (m div n) * n"
1.248 -  using mod_div_equality [of m n] by arith
1.249 +  using div_mult_mod_eq [of m n] by arith
1.250
1.251
1.252  subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
1.253 @@ -2282,7 +2282,7 @@
1.254    shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
1.255  proof -
1.256    have "i mod k = i \<longleftrightarrow> i div k = 0"
1.257 -    by safe (insert mod_div_equality [of i k], auto)
1.258 +    by safe (insert div_mult_mod_eq [of i k], auto)
1.259    with zdiv_eq_0_iff
1.260    show ?thesis
1.261      by simp
```