src/HOL/Divides.thy
 changeset 57514 bdc2c6b40bf2 parent 57512 cc97b347b301 child 58410 6d46ad54a2ab
```     1.1 --- a/src/HOL/Divides.thy	Sat Jul 05 10:09:01 2014 +0200
1.2 +++ b/src/HOL/Divides.thy	Sat Jul 05 11:01:53 2014 +0200
1.3 @@ -34,7 +34,7 @@
1.4
1.5  lemma mod_div_equality': "a mod b + a div b * b = a"
1.6    using mod_div_equality [of a b]
1.7 -  by (simp only: add_ac)
1.8 +  by (simp only: ac_simps)
1.9
1.10  lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
1.11    by (simp add: mod_div_equality)
1.12 @@ -228,7 +228,7 @@
1.13    have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
1.14      by (simp only: mod_div_equality)
1.15    also have "\<dots> = (a mod c + b + a div c * c) mod c"
1.16 -    by (simp only: add_ac)
1.17 +    by (simp only: ac_simps)
1.18    also have "\<dots> = (a mod c + b) mod c"
1.19      by (rule mod_mult_self1)
1.20    finally show ?thesis .
1.21 @@ -239,7 +239,7 @@
1.22    have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
1.23      by (simp only: mod_div_equality)
1.24    also have "\<dots> = (a + b mod c + b div c * c) mod c"
1.25 -    by (simp only: add_ac)
1.26 +    by (simp only: ac_simps)
1.27    also have "\<dots> = (a + b mod c) mod c"
1.28      by (rule mod_mult_self1)
1.29    finally show ?thesis .
1.30 @@ -321,7 +321,7 @@
1.31    also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
1.32      by (simp only: mod_mult_self1)
1.33    also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
1.34 -    by (simp only: add_ac mult_ac)
1.35 +    by (simp only: ac_simps ac_simps)
1.36    also have "\<dots> = a mod c"
1.37      by (simp only: mod_div_equality)
1.38    finally show ?thesis .
1.39 @@ -421,7 +421,7 @@
1.40    have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
1.41      by (simp only: mod_div_equality)
1.42    also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
1.43 -    by (simp only: minus_add_distrib minus_mult_left add_ac)
1.44 +    by (simp add: ac_simps)
1.45    also have "\<dots> = (- (a mod b)) mod b"
1.46      by (rule mod_mult_self1)
1.47    finally show ?thesis .
1.48 @@ -957,7 +957,7 @@
1.49    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
1.50
1.51    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
1.52 -    (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
1.53 +    (@{thm add_0_left} :: @{thm add_0_right} :: @{thms ac_simps}))
1.54  )
1.55  *}
1.56
1.57 @@ -1059,7 +1059,7 @@
1.58  lemma divmod_nat_rel_mult2_eq:
1.59    "divmod_nat_rel a b (q, r)
1.60     \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
1.61 -by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
1.62 +by (auto simp add: mult.commute mult.left_commute divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
1.63
1.64  lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
1.65  by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
1.66 @@ -1147,11 +1147,15 @@
1.67  lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
1.68
1.69  (*Loses information, namely we also have r<d provided d is nonzero*)
1.70 -lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
1.71 -  apply (cut_tac a = m in mod_div_equality)
1.72 -  apply (simp only: add_ac)
1.73 -  apply (blast intro: sym)
1.74 -  done
1.75 +lemma mod_eqD:
1.76 +  fixes m d r q :: nat
1.77 +  assumes "m mod d = r"
1.78 +  shows "\<exists>q. m = r + q * d"
1.79 +proof -
1.80 +  from mod_div_equality obtain q where "q * d + m mod d = m" by blast
1.81 +  with assms have "m = r + q * d" by simp
1.82 +  then show ?thesis ..
1.83 +qed
1.84
1.85  lemma split_div:
1.86   "P(n div k :: nat) =
1.87 @@ -1175,7 +1179,7 @@
1.88          with n j P show "P i" by simp
1.89        next
1.90          assume "i \<noteq> 0"
1.91 -        with not0 n j P show "P i" by(simp add:add_ac)
1.92 +        with not0 n j P show "P i" by(simp add:ac_simps)
1.93        qed
1.94      qed
1.95    qed
1.96 @@ -1209,7 +1213,7 @@
1.97  next
1.98    assume P: ?lhs
1.99    then have "divmod_nat_rel m n (q, m - n * q)"
1.100 -    unfolding divmod_nat_rel_def by (auto simp add: mult_ac)
1.101 +    unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
1.102    with divmod_nat_rel_unique divmod_nat_rel [of m n]
1.103    have "(q, m - n * q) = (m div n, m mod n)" by auto
1.104    then show ?rhs by simp
1.105 @@ -1239,7 +1243,7 @@
1.106      proof (simp, intro allI impI)
1.107        fix i j
1.108        assume "n = k*i + j" "j < k"
1.109 -      thus "P j" using not0 P by(simp add:add_ac mult_ac)
1.110 +      thus "P j" using not0 P by(simp add:ac_simps ac_simps)
1.111      qed
1.112    qed
1.113  next
1.114 @@ -1417,7 +1421,7 @@
1.115
1.116    (* Potential use of algebra : Equality modulo n*)
1.117  lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
1.119 +by (simp add: ac_simps ac_simps)
1.120
1.121  lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
1.122  proof -
1.123 @@ -1614,7 +1618,7 @@
1.124    apply (case_tac "a < b")
1.125    apply simp_all
1.126    apply (erule splitE)
1.127 -  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
1.128 +  apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
1.129    done
1.130
1.131
1.132 @@ -1644,7 +1648,7 @@
1.133    apply (case_tac "a + b < (0\<Colon>int)")
1.134    apply simp_all
1.135    apply (erule splitE)
1.136 -  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
1.137 +  apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
1.138    done
1.139
1.140
1.141 @@ -1744,7 +1748,7 @@
1.142    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
1.143
1.144    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
1.145 -    (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms add_ac}))
1.146 +    (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms ac_simps}))
1.147  )
1.148  *}
1.149
1.150 @@ -2072,7 +2076,7 @@
1.151  lemma zmult1_lemma:
1.152       "[| divmod_int_rel b c (q, r) |]
1.153        ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
1.154 -by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left mult_ac)
1.155 +by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
1.156
1.157  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
1.158  apply (case_tac "c = 0", simp)
1.159 @@ -2176,7 +2180,7 @@
1.160
1.161  lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
1.162        ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
1.163 -by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
1.164 +by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
1.165                     zero_less_mult_iff distrib_left [symmetric]
1.166                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
1.167
```