src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
changeset 44766 d4d33a4d7548
parent 41541 1fa4725c4656
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Tue Sep 06 16:30:39 2011 -0700
     1.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Tue Sep 06 19:03:41 2011 -0700
     1.3 @@ -22,7 +22,7 @@
     1.4    from finite_A have "a * setsum id A = setsum (%x. a * x) A"
     1.5      by (auto simp add: setsum_const_mult id_def)
     1.6    also have "setsum (%x. a * x) = setsum (%x. x * a)"
     1.7 -    by (auto simp add: zmult_commute)
     1.8 +    by (auto simp add: mult_commute)
     1.9    also have "setsum (%x. x * a) A = setsum id B"
    1.10      by (simp add: B_def setsum_reindex_id[OF inj_on_xa_A])
    1.11    also have "... = setsum (%x. p * (x div p) + StandardRes p x) B"
    1.12 @@ -71,7 +71,7 @@
    1.13      p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E"
    1.14  proof -
    1.15    have "(a - 1) * setsum id A = a * setsum id A - setsum id A"
    1.16 -    by (auto simp add: zdiff_zmult_distrib)
    1.17 +    by (auto simp add: left_diff_distrib)
    1.18    also note QRLemma1
    1.19    also from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
    1.20       setsum id E - setsum id A =
    1.21 @@ -82,7 +82,7 @@
    1.22        p * int (card E) + 2 * setsum id E"
    1.23      by arith
    1.24    finally show ?thesis
    1.25 -    by (auto simp only: zdiff_zmult_distrib2)
    1.26 +    by (auto simp only: right_diff_distrib)
    1.27  qed
    1.28  
    1.29  lemma QRLemma4: "a \<in> zOdd ==>
    1.30 @@ -284,7 +284,7 @@
    1.31  proof -
    1.32    fix a and b
    1.33    assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2"
    1.34 -  with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
    1.35 +  with less_linear have "(p * b < q * a) | (p * b = q * a)" by auto
    1.36    moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
    1.37    ultimately show "p * b < q * a" by auto
    1.38  qed
    1.39 @@ -388,7 +388,7 @@
    1.40      by (auto simp add: int_distrib)
    1.41    then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
    1.42      apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
    1.43 -    by (auto simp add: even3, auto simp add: zmult_ac)
    1.44 +    by (auto simp add: even3, auto simp add: mult_ac)
    1.45    also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)"
    1.46      by (auto simp add: even1 even_prod_div_2)
    1.47    also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
    1.48 @@ -557,11 +557,11 @@
    1.49  
    1.50  lemma S1_carda: "int (card(S1)) =
    1.51      setsum (%j. (j * q) div p) P_set"
    1.52 -  by (auto simp add: S1_card zmult_ac)
    1.53 +  by (auto simp add: S1_card mult_ac)
    1.54  
    1.55  lemma S2_carda: "int (card(S2)) =
    1.56      setsum (%j. (j * p) div q) Q_set"
    1.57 -  by (auto simp add: S2_card zmult_ac)
    1.58 +  by (auto simp add: S2_card mult_ac)
    1.59  
    1.60  lemma pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
    1.61      (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
    1.62 @@ -610,7 +610,7 @@
    1.63      by auto
    1.64    also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) +
    1.65                     nat(setsum (%x. ((x * q) div p)) P_set))"
    1.66 -    by (auto simp add: zpower_zadd_distrib)
    1.67 +    by (auto simp add: power_add)
    1.68    also have "nat(setsum (%x. ((x * p) div q)) Q_set) +
    1.69        nat(setsum (%x. ((x * q) div p)) P_set) =
    1.70          nat((setsum (%x. ((x * p) div q)) Q_set) +