src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -388,7 +388,7 @@
     1.4      by (auto simp add: int_distrib)
     1.5    then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
     1.6      apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
     1.7 -    by (auto simp add: even3, auto simp add: mult_ac)
     1.8 +    by (auto simp add: even3, auto simp add: ac_simps)
     1.9    also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)"
    1.10      by (auto simp add: even1 even_prod_div_2)
    1.11    also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
    1.12 @@ -557,11 +557,11 @@
    1.13  
    1.14  lemma S1_carda: "int (card(S1)) =
    1.15      setsum (%j. (j * q) div p) P_set"
    1.16 -  by (auto simp add: S1_card mult_ac)
    1.17 +  by (auto simp add: S1_card ac_simps)
    1.18  
    1.19  lemma S2_carda: "int (card(S2)) =
    1.20      setsum (%j. (j * p) div q) Q_set"
    1.21 -  by (auto simp add: S2_card mult_ac)
    1.22 +  by (auto simp add: S2_card ac_simps)
    1.23  
    1.24  lemma pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
    1.25      (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"