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.32        by (simp add: algebra_simps)
    1.33    finally have "a = a div b * b + (a + c * b) mod b"
    1.34      by (simp add: add.commute [of a] add.assoc distrib_right)
    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.152      by (simp add: ac_simps)
   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.193  proof (rule add_leD2)
   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.243    by (simp add: divide_int_def)
   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