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.118 -by (simp add: mult_ac add_ac)
   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