src/HOL/NumberTheory/Quadratic_Reciprocity.thy
changeset 13871 26e5f5e624f6
child 14353 79f9fbef9106
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Thu Mar 20 15:58:25 2003 +0100
     1.3 @@ -0,0 +1,628 @@
     1.4 +(*  Title:      HOL/Quadratic_Reciprocity/Quadratic_Reciprocity.thy
     1.5 +    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     1.6 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.7 +*)
     1.8 +
     1.9 +header {* The law of Quadratic reciprocity *}
    1.10 +
    1.11 +theory Quadratic_Reciprocity = Gauss:;
    1.12 +
    1.13 +(***************************************************************)
    1.14 +(*                                                             *)
    1.15 +(*  Lemmas leading up to the proof of theorem 3.3 in           *)
    1.16 +(*  Niven and Zuckerman's presentation                         *)
    1.17 +(*                                                             *)
    1.18 +(***************************************************************)
    1.19 +
    1.20 +lemma (in GAUSS) QRLemma1: "a * setsum id A = 
    1.21 +  p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E";
    1.22 +proof -;
    1.23 +  from finite_A have "a * setsum id A = setsum (%x. a * x) A"; 
    1.24 +    by (auto simp add: setsum_const_mult id_def)
    1.25 +  also have "setsum (%x. a * x) = setsum (%x. x * a)"; 
    1.26 +    by (auto simp add: zmult_commute)
    1.27 +  also; have "setsum (%x. x * a) A = setsum id B";
    1.28 +    by (auto simp add: B_def sum_prop_id finite_A inj_on_xa_A)
    1.29 +  also have "... = setsum (%x. p * (x div p) + StandardRes p x) B";
    1.30 +    apply (rule setsum_same_function)
    1.31 +    by (auto simp add: finite_B StandardRes_def zmod_zdiv_equality)
    1.32 +  also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B";
    1.33 +    by (rule setsum_addf)
    1.34 +  also; have "setsum (StandardRes p) B = setsum id C";
    1.35 +    by (auto simp add: C_def sum_prop_id [THEN sym] finite_B 
    1.36 +      SR_B_inj)
    1.37 +  also; from C_eq have "... = setsum id (D \<union> E)";
    1.38 +    by auto
    1.39 +  also; from finite_D finite_E have "... = setsum id D + setsum id E";
    1.40 +    apply (rule setsum_Un_disjoint)
    1.41 +    by (auto simp add: D_def E_def)
    1.42 +  also have "setsum (%x. p * (x div p)) B = 
    1.43 +      setsum ((%x. p * (x div p)) o (%x. (x * a))) A";
    1.44 +    by (auto simp add: B_def sum_prop finite_A inj_on_xa_A)
    1.45 +  also have "... = setsum (%x. p * ((x * a) div p)) A";
    1.46 +    by (auto simp add: o_def)
    1.47 +  also from finite_A have "setsum (%x. p * ((x * a) div p)) A = 
    1.48 +    p * setsum (%x. ((x * a) div p)) A";
    1.49 +    by (auto simp add: setsum_const_mult)
    1.50 +  finally show ?thesis by arith
    1.51 +qed;
    1.52 +
    1.53 +lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E + 
    1.54 +  setsum id D"; 
    1.55 +proof -;
    1.56 +  from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)";
    1.57 +    by (simp add: Un_commute)
    1.58 +  also from F_D_disj finite_D finite_F have 
    1.59 +      "... = setsum id D + setsum id F";
    1.60 +    apply (simp add: Int_commute)
    1.61 +    by (intro setsum_Un_disjoint) 
    1.62 +  also from F_def have "F = (%x. (p - x)) ` E";
    1.63 +    by auto
    1.64 +  also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) =
    1.65 +      setsum (%x. (p - x)) E";
    1.66 +    by (auto simp add: sum_prop)
    1.67 +  also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E";
    1.68 +    by (auto simp add: setsum_minus id_def)
    1.69 +  also from finite_E have "setsum (%x. p) E = p * int(card E)";
    1.70 +    by (intro setsum_const)
    1.71 +  finally show ?thesis;
    1.72 +    by arith
    1.73 +qed;
    1.74 +
    1.75 +lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A = 
    1.76 +    p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E";
    1.77 +proof -;
    1.78 +  have "(a - 1) * setsum id A = a * setsum id A - setsum id A";
    1.79 +    by (auto simp add: zdiff_zmult_distrib)  
    1.80 +  also note QRLemma1;
    1.81 +  also; from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
    1.82 +     setsum id E - setsum id A = 
    1.83 +      p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
    1.84 +      setsum id E - (p * int (card E) - setsum id E + setsum id D)";
    1.85 +    by auto
    1.86 +  also; have "... = p * (\<Sum>x \<in> A. x * a div p) - 
    1.87 +      p * int (card E) + 2 * setsum id E"; 
    1.88 +    by arith
    1.89 +  finally show ?thesis;
    1.90 +    by (auto simp only: zdiff_zmult_distrib2)
    1.91 +qed;
    1.92 +
    1.93 +lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==> 
    1.94 +    (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)";
    1.95 +proof -;
    1.96 +  assume a_odd: "a \<in> zOdd";
    1.97 +  from QRLemma3 have a: "p * (setsum (%x. ((x * a) div p)) A - int(card E)) =
    1.98 +      (a - 1) * setsum id A - 2 * setsum id E"; 
    1.99 +    by arith
   1.100 +  from a_odd have "a - 1 \<in> zEven"
   1.101 +    by (rule odd_minus_one_even)
   1.102 +  hence "(a - 1) * setsum id A \<in> zEven";
   1.103 +    by (rule even_times_either)
   1.104 +  moreover have "2 * setsum id E \<in> zEven";
   1.105 +    by (auto simp add: zEven_def)
   1.106 +  ultimately have "(a - 1) * setsum id A - 2 * setsum id E \<in> zEven"
   1.107 +    by (rule even_minus_even)
   1.108 +  with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
   1.109 +    by simp
   1.110 +  hence "p \<in> zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
   1.111 +    by (rule even_product)
   1.112 +  with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
   1.113 +    by (auto simp add: odd_iff_not_even)
   1.114 +  thus ?thesis;
   1.115 +    by (auto simp only: even_diff [THEN sym])
   1.116 +qed;
   1.117 +
   1.118 +lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==> 
   1.119 +   (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
   1.120 +proof -;
   1.121 +  assume "a \<in> zOdd";
   1.122 +  from QRLemma4 have
   1.123 +    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)";..;
   1.124 +  moreover have "0 \<le> int(card E)";
   1.125 +    by auto
   1.126 +  moreover have "0 \<le> setsum (%x. ((x * a) div p)) A";
   1.127 +    proof (intro setsum_non_neg);
   1.128 +      from finite_A show "finite A";.;
   1.129 +      next show "\<forall>x \<in> A. 0 \<le> x * a div p";
   1.130 +      proof;
   1.131 +        fix x;
   1.132 +        assume "x \<in> A";
   1.133 +        then have "0 \<le> x";
   1.134 +          by (auto simp add: A_def)
   1.135 +        with a_nonzero have "0 \<le> x * a";
   1.136 +          by (auto simp add: int_0_le_mult_iff)
   1.137 +        with p_g_2 show "0 \<le> x * a div p"; 
   1.138 +          by (auto simp add: pos_imp_zdiv_nonneg_iff)
   1.139 +      qed;
   1.140 +    qed;
   1.141 +  ultimately have "(-1::int)^nat((int (card E))) =
   1.142 +      (-1)^nat(((\<Sum>x \<in> A. x * a div p)))";
   1.143 +    by (intro neg_one_power_parity, auto)
   1.144 +  also have "nat (int(card E)) = card E";
   1.145 +    by auto
   1.146 +  finally show ?thesis;.;
   1.147 +qed;
   1.148 +
   1.149 +lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p));p \<in> zprime; 2 < p;
   1.150 +  A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==> 
   1.151 +  (Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
   1.152 +  apply (subst GAUSS.gauss_lemma)
   1.153 +  apply (auto simp add: GAUSS_def)
   1.154 +  apply (subst GAUSS.QRLemma5)
   1.155 +by (auto simp add: GAUSS_def)
   1.156 +
   1.157 +(******************************************************************)
   1.158 +(*                                                                *)
   1.159 +(* Stuff about S, S1 and S2...                                    *)
   1.160 +(*                                                                *)
   1.161 +(******************************************************************)
   1.162 +
   1.163 +locale QRTEMP =
   1.164 +  fixes p     :: "int"
   1.165 +  fixes q     :: "int"
   1.166 +  fixes P_set :: "int set"
   1.167 +  fixes Q_set :: "int set"
   1.168 +  fixes S     :: "(int * int) set"
   1.169 +  fixes S1    :: "(int * int) set"
   1.170 +  fixes S2    :: "(int * int) set"
   1.171 +  fixes f1    :: "int => (int * int) set"
   1.172 +  fixes f2    :: "int => (int * int) set"
   1.173 +
   1.174 +  assumes p_prime: "p \<in> zprime"
   1.175 +  assumes p_g_2: "2 < p"
   1.176 +  assumes q_prime: "q \<in> zprime"
   1.177 +  assumes q_g_2: "2 < q"
   1.178 +  assumes p_neq_q:      "p \<noteq> q"
   1.179 +
   1.180 +  defines P_set_def: "P_set == {x. 0 < x & x \<le> ((p - 1) div 2) }"
   1.181 +  defines Q_set_def: "Q_set == {x. 0 < x & x \<le> ((q - 1) div 2) }"
   1.182 +  defines S_def:     "S     == P_set <*> Q_set"
   1.183 +  defines S1_def:    "S1    == { (x, y). (x, y):S & ((p * y) < (q * x)) }"
   1.184 +  defines S2_def:    "S2    == { (x, y). (x, y):S & ((q * x) < (p * y)) }"
   1.185 +  defines f1_def:    "f1 j  == { (j1, y). (j1, y):S & j1 = j & 
   1.186 +                                 (y \<le> (q * j) div p) }"
   1.187 +  defines f2_def:    "f2 j  == { (x, j1). (x, j1):S & j1 = j & 
   1.188 +                                 (x \<le> (p * j) div q) }";
   1.189 +
   1.190 +lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2";
   1.191 +proof -;
   1.192 +  from prems have "2 < p" by (simp add: QRTEMP_def)
   1.193 +  then have "2 \<le> p - 1" by arith
   1.194 +  then have "2 div 2 \<le> (p - 1) div 2" by (rule zdiv_mono1, auto)
   1.195 +  then show ?thesis by auto
   1.196 +qed;
   1.197 +
   1.198 +lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2";
   1.199 +proof -;
   1.200 +  from prems have "2 < q" by (simp add: QRTEMP_def)
   1.201 +  then have "2 \<le> q - 1" by arith
   1.202 +  then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto)
   1.203 +  then show ?thesis by auto
   1.204 +qed;
   1.205 +
   1.206 +lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==> 
   1.207 +    (p * b \<noteq> q * a)";
   1.208 +proof;
   1.209 +  assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2";
   1.210 +  then have "q dvd (p * b)" by (auto simp add: dvd_def)
   1.211 +  with q_prime p_g_2 have "q dvd p | q dvd b";
   1.212 +    by (auto simp add: zprime_zdvd_zmult)
   1.213 +  moreover have "~ (q dvd p)";
   1.214 +  proof;
   1.215 +    assume "q dvd p";
   1.216 +    with p_prime have "q = 1 | q = p"
   1.217 +      apply (auto simp add: zprime_def QRTEMP_def)
   1.218 +      apply (drule_tac x = q and R = False in allE)
   1.219 +      apply (simp add: QRTEMP_def)    
   1.220 +      apply (subgoal_tac "0 \<le> q", simp add: QRTEMP_def)
   1.221 +      apply (insert prems)
   1.222 +    by (auto simp add: QRTEMP_def)
   1.223 +    with q_g_2 p_neq_q show False by auto
   1.224 +  qed;
   1.225 +  ultimately have "q dvd b" by auto
   1.226 +  then have "q \<le> b";
   1.227 +  proof -;
   1.228 +    assume "q dvd b";
   1.229 +    moreover from prems have "0 < b" by auto
   1.230 +    ultimately show ?thesis by (insert zdvd_bounds [of q b], auto)
   1.231 +  qed;
   1.232 +  with prems have "q \<le> (q - 1) div 2" by auto
   1.233 +  then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
   1.234 +  then have "2 * q \<le> q - 1";
   1.235 +  proof -;
   1.236 +    assume "2 * q \<le> 2 * ((q - 1) div 2)";
   1.237 +    with prems have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
   1.238 +    with odd_minus_one_even have "(q - 1):zEven" by auto
   1.239 +    with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto
   1.240 +    with prems show ?thesis by auto
   1.241 +  qed;
   1.242 +  then have p1: "q \<le> -1" by arith
   1.243 +  with q_g_2 show False by auto
   1.244 +qed;
   1.245 +
   1.246 +lemma (in QRTEMP) P_set_finite: "finite (P_set)";
   1.247 +  by (insert p_fact, auto simp add: P_set_def bdd_int_set_l_le_finite)
   1.248 +
   1.249 +lemma (in QRTEMP) Q_set_finite: "finite (Q_set)";
   1.250 +  by (insert q_fact, auto simp add: Q_set_def bdd_int_set_l_le_finite)
   1.251 +
   1.252 +lemma (in QRTEMP) S_finite: "finite S";
   1.253 +  by (auto simp add: S_def  P_set_finite Q_set_finite cartesian_product_finite)
   1.254 +
   1.255 +lemma (in QRTEMP) S1_finite: "finite S1";
   1.256 +proof -;
   1.257 +  have "finite S" by (auto simp add: S_finite)
   1.258 +  moreover have "S1 \<subseteq> S" by (auto simp add: S1_def S_def)
   1.259 +  ultimately show ?thesis by (auto simp add: finite_subset)
   1.260 +qed;
   1.261 +
   1.262 +lemma (in QRTEMP) S2_finite: "finite S2";
   1.263 +proof -;
   1.264 +  have "finite S" by (auto simp add: S_finite)
   1.265 +  moreover have "S2 \<subseteq> S" by (auto simp add: S2_def S_def)
   1.266 +  ultimately show ?thesis by (auto simp add: finite_subset)
   1.267 +qed;
   1.268 +
   1.269 +lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))";
   1.270 +  by (insert p_fact, auto simp add: P_set_def card_bdd_int_set_l_le)
   1.271 +
   1.272 +lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))";
   1.273 +  by (insert q_fact, auto simp add: Q_set_def card_bdd_int_set_l_le)
   1.274 +
   1.275 +lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
   1.276 +  apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
   1.277 +  apply (auto simp add: S_def zmult_int)
   1.278 +done
   1.279 +
   1.280 +lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}";
   1.281 +  by (auto simp add: S1_def S2_def)
   1.282 +
   1.283 +lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2";
   1.284 +  apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
   1.285 +  proof -;
   1.286 +    fix a and b;
   1.287 +    assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2";
   1.288 +    with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
   1.289 +    moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
   1.290 +    ultimately show "p * b < q * a" by auto
   1.291 +  qed;
   1.292 +
   1.293 +lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) = 
   1.294 +    int(card(S1)) + int(card(S2))";
   1.295 +proof-;
   1.296 +  have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
   1.297 +    by (auto simp add: S_card)
   1.298 +  also have "... = int( card(S1) + card(S2))";
   1.299 +    apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop)
   1.300 +    apply (drule card_Un_disjoint, auto)
   1.301 +  done
   1.302 +  also have "... = int(card(S1)) + int(card(S2))" by auto
   1.303 +  finally show ?thesis .;
   1.304 +qed;
   1.305 +
   1.306 +lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2; 
   1.307 +                             0 < b; b \<le> (q - 1) div 2 |] ==>
   1.308 +                          (p * b < q * a) = (b \<le> q * a div p)";
   1.309 +proof -;
   1.310 +  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
   1.311 +  have "p * b < q * a ==> b \<le> q * a div p";
   1.312 +  proof -;
   1.313 +    assume "p * b < q * a";
   1.314 +    then have "p * b \<le> q * a" by auto
   1.315 +    then have "(p * b) div p \<le> (q * a) div p";
   1.316 +      by (rule zdiv_mono1, insert p_g_2, auto)
   1.317 +    then show "b \<le> (q * a) div p";
   1.318 +      apply (subgoal_tac "p \<noteq> 0")
   1.319 +      apply (frule zdiv_zmult_self2, force)
   1.320 +      by (insert p_g_2, auto)
   1.321 +  qed;
   1.322 +  moreover have "b \<le> q * a div p ==> p * b < q * a";
   1.323 +  proof -;
   1.324 +    assume "b \<le> q * a div p";
   1.325 +    then have "p * b \<le> p * ((q * a) div p)";
   1.326 +      by (insert p_g_2, auto simp add: zmult_zle_cancel1)
   1.327 +    also have "... \<le> q * a";
   1.328 +      by (rule zdiv_leq_prop, insert p_g_2, auto)
   1.329 +    finally have "p * b \<le> q * a" .;
   1.330 +    then have "p * b < q * a | p * b = q * a";
   1.331 +      by (simp only: order_le_imp_less_or_eq)
   1.332 +    moreover have "p * b \<noteq> q * a";
   1.333 +      by (rule  pb_neq_qa, insert prems, auto)
   1.334 +    ultimately show ?thesis by auto
   1.335 +  qed;
   1.336 +  ultimately show ?thesis ..;
   1.337 +qed;
   1.338 +
   1.339 +lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2; 
   1.340 +                             0 < b; b \<le> (q - 1) div 2 |] ==>
   1.341 +                          (q * a < p * b) = (a \<le> p * b div q)";
   1.342 +proof -;
   1.343 +  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
   1.344 +  have "q * a < p * b ==> a \<le> p * b div q";
   1.345 +  proof -;
   1.346 +    assume "q * a < p * b";
   1.347 +    then have "q * a \<le> p * b" by auto
   1.348 +    then have "(q * a) div q \<le> (p * b) div q";
   1.349 +      by (rule zdiv_mono1, insert q_g_2, auto)
   1.350 +    then show "a \<le> (p * b) div q";
   1.351 +      apply (subgoal_tac "q \<noteq> 0")
   1.352 +      apply (frule zdiv_zmult_self2, force)
   1.353 +      by (insert q_g_2, auto)
   1.354 +  qed;
   1.355 +  moreover have "a \<le> p * b div q ==> q * a < p * b";
   1.356 +  proof -;
   1.357 +    assume "a \<le> p * b div q";
   1.358 +    then have "q * a \<le> q * ((p * b) div q)";
   1.359 +      by (insert q_g_2, auto simp add: zmult_zle_cancel1)
   1.360 +    also have "... \<le> p * b";
   1.361 +      by (rule zdiv_leq_prop, insert q_g_2, auto)
   1.362 +    finally have "q * a \<le> p * b" .;
   1.363 +    then have "q * a < p * b | q * a = p * b";
   1.364 +      by (simp only: order_le_imp_less_or_eq)
   1.365 +    moreover have "p * b \<noteq> q * a";
   1.366 +      by (rule  pb_neq_qa, insert prems, auto)
   1.367 +    ultimately show ?thesis by auto
   1.368 +  qed;
   1.369 +  ultimately show ?thesis ..;
   1.370 +qed;
   1.371 +
   1.372 +lemma aux2: "[| p \<in> zprime; q \<in> zprime; 2 < p; 2 < q |] ==> 
   1.373 +             (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2";
   1.374 +proof-;
   1.375 +  assume "p \<in> zprime" and "q \<in> zprime" and "2 < p" and "2 < q";
   1.376 +  (* Set up what's even and odd *)
   1.377 +  then have "p \<in> zOdd & q \<in> zOdd";
   1.378 +    by (auto simp add:  zprime_zOdd_eq_grt_2)
   1.379 +  then have even1: "(p - 1):zEven & (q - 1):zEven";
   1.380 +    by (auto simp add: odd_minus_one_even)
   1.381 +  then have even2: "(2 * p):zEven & ((q - 1) * p):zEven";
   1.382 +    by (auto simp add: zEven_def)
   1.383 +  then have even3: "(((q - 1) * p) + (2 * p)):zEven";
   1.384 +    by (auto simp: even_plus_even)
   1.385 +  (* using these prove it *)
   1.386 +  from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)";
   1.387 +    by (auto simp add: int_distrib)
   1.388 +  then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2";
   1.389 +    apply (rule_tac x = "((p - 1) * q)" in even_div_2_l);
   1.390 +    by (auto simp add: even3, auto simp add: zmult_ac)
   1.391 +  also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)";
   1.392 +    by (auto simp add: even1 even_prod_div_2)
   1.393 +  also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p";
   1.394 +    by (auto simp add: even1 even2 even_prod_div_2 even_sum_div_2)
   1.395 +  finally show ?thesis 
   1.396 +    apply (rule_tac x = " q * ((p - 1) div 2)" and 
   1.397 +                    y = "(q - 1) div 2" in div_prop2);
   1.398 +    by (insert prems, auto)
   1.399 +qed;
   1.400 +
   1.401 +lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p";
   1.402 +proof;
   1.403 +  fix j;
   1.404 +  assume j_fact: "j \<in> P_set";
   1.405 +  have "int (card (f1 j)) = int (card {y. y \<in> Q_set & y \<le> (q * j) div p})";
   1.406 +  proof -;
   1.407 +    have "finite (f1 j)";
   1.408 +    proof -;
   1.409 +      have "(f1 j) \<subseteq> S" by (auto simp add: f1_def)
   1.410 +      with S_finite show ?thesis by (auto simp add: finite_subset)
   1.411 +    qed;
   1.412 +    moreover have "inj_on (%(x,y). y) (f1 j)";
   1.413 +      by (auto simp add: f1_def inj_on_def)
   1.414 +    ultimately have "card ((%(x,y). y) ` (f1 j)) = card  (f1 j)";
   1.415 +      by (auto simp add: f1_def card_image)
   1.416 +    moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}";
   1.417 +      by (insert prems, auto simp add: f1_def S_def Q_set_def P_set_def 
   1.418 +        image_def)
   1.419 +    ultimately show ?thesis by (auto simp add: f1_def)
   1.420 +  qed;
   1.421 +  also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})";
   1.422 +  proof -;
   1.423 +    have "{y. y \<in> Q_set & y \<le> (q * j) div p} = 
   1.424 +        {y. 0 < y & y \<le> (q * j) div p}";
   1.425 +      apply (auto simp add: Q_set_def)
   1.426 +      proof -;
   1.427 +        fix x;
   1.428 +        assume "0 < x" and "x \<le> q * j div p";
   1.429 +        with j_fact P_set_def  have "j \<le> (p - 1) div 2"; by auto
   1.430 +        with q_g_2; have "q * j \<le> q * ((p - 1) div 2)";
   1.431 +          by (auto simp add: zmult_zle_cancel1)
   1.432 +        with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p";
   1.433 +          by (auto simp add: zdiv_mono1)
   1.434 +        also from prems have "... \<le> (q - 1) div 2";
   1.435 +          apply simp apply (insert aux2) by (simp add: QRTEMP_def)
   1.436 +        finally show "x \<le> (q - 1) div 2" by (insert prems, auto)
   1.437 +      qed;
   1.438 +    then show ?thesis by auto
   1.439 +  qed;
   1.440 +  also have "... = (q * j) div p";
   1.441 +  proof -;
   1.442 +    from j_fact P_set_def have "0 \<le> j" by auto
   1.443 +    with q_g_2 have "q * 0 \<le> q * j" by (auto simp only: zmult_zle_mono2)
   1.444 +    then have "0 \<le> q * j" by auto
   1.445 +    then have "0 div p \<le> (q * j) div p";
   1.446 +      apply (rule_tac a = 0 in zdiv_mono1)
   1.447 +      by (insert p_g_2, auto)
   1.448 +    also have "0 div p = 0" by auto
   1.449 +    finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
   1.450 +  qed;
   1.451 +  finally show "int (card (f1 j)) = q * j div p" .;
   1.452 +qed;
   1.453 +
   1.454 +lemma (in QRTEMP) aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q";
   1.455 +proof;
   1.456 +  fix j;
   1.457 +  assume j_fact: "j \<in> Q_set";
   1.458 +  have "int (card (f2 j)) = int (card {y. y \<in> P_set & y \<le> (p * j) div q})";
   1.459 +  proof -;
   1.460 +    have "finite (f2 j)";
   1.461 +    proof -;
   1.462 +      have "(f2 j) \<subseteq> S" by (auto simp add: f2_def)
   1.463 +      with S_finite show ?thesis by (auto simp add: finite_subset)
   1.464 +    qed;
   1.465 +    moreover have "inj_on (%(x,y). x) (f2 j)";
   1.466 +      by (auto simp add: f2_def inj_on_def)
   1.467 +    ultimately have "card ((%(x,y). x) ` (f2 j)) = card  (f2 j)";
   1.468 +      by (auto simp add: f2_def card_image)
   1.469 +    moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}";
   1.470 +      by (insert prems, auto simp add: f2_def S_def Q_set_def 
   1.471 +        P_set_def image_def)
   1.472 +    ultimately show ?thesis by (auto simp add: f2_def)
   1.473 +  qed;
   1.474 +  also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})";
   1.475 +  proof -;
   1.476 +    have "{y. y \<in> P_set & y \<le> (p * j) div q} = 
   1.477 +        {y. 0 < y & y \<le> (p * j) div q}";
   1.478 +      apply (auto simp add: P_set_def)
   1.479 +      proof -;
   1.480 +        fix x;
   1.481 +        assume "0 < x" and "x \<le> p * j div q";
   1.482 +        with j_fact Q_set_def  have "j \<le> (q - 1) div 2"; by auto
   1.483 +        with p_g_2; have "p * j \<le> p * ((q - 1) div 2)";
   1.484 +          by (auto simp add: zmult_zle_cancel1)
   1.485 +        with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q";
   1.486 +          by (auto simp add: zdiv_mono1)
   1.487 +        also from prems have "... \<le> (p - 1) div 2";
   1.488 +          by (auto simp add: aux2 QRTEMP_def)
   1.489 +        finally show "x \<le> (p - 1) div 2" by (insert prems, auto)
   1.490 +      qed;
   1.491 +    then show ?thesis by auto
   1.492 +  qed;
   1.493 +  also have "... = (p * j) div q";
   1.494 +  proof -;
   1.495 +    from j_fact Q_set_def have "0 \<le> j" by auto
   1.496 +    with p_g_2 have "p * 0 \<le> p * j" by (auto simp only: zmult_zle_mono2)
   1.497 +    then have "0 \<le> p * j" by auto
   1.498 +    then have "0 div q \<le> (p * j) div q";
   1.499 +      apply (rule_tac a = 0 in zdiv_mono1)
   1.500 +      by (insert q_g_2, auto)
   1.501 +    also have "0 div q = 0" by auto
   1.502 +    finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
   1.503 +  qed;
   1.504 +  finally show "int (card (f2 j)) = p * j div q" .;
   1.505 +qed;
   1.506 +
   1.507 +lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set";
   1.508 +proof -;
   1.509 +  have "\<forall>x \<in> P_set. finite (f1 x)";
   1.510 +  proof;
   1.511 +    fix x;
   1.512 +    have "f1 x \<subseteq> S" by (auto simp add: f1_def)
   1.513 +    with S_finite show "finite (f1 x)" by (auto simp add: finite_subset)
   1.514 +  qed;
   1.515 +  moreover have "(\<forall>x \<in> P_set. \<forall>y \<in> P_set. x \<noteq> y --> (f1 x) \<inter> (f1 y) = {})";
   1.516 +    by (auto simp add: f1_def)
   1.517 +  moreover note P_set_finite;
   1.518 +  ultimately have "int(card (UNION P_set f1)) = 
   1.519 +      setsum (%x. int(card (f1 x))) P_set";
   1.520 +    by (rule_tac A = P_set in int_card_indexed_union_disjoint_sets, auto)
   1.521 +  moreover have "S1 = UNION P_set f1";
   1.522 +    by (auto simp add: f1_def S_def S1_def S2_def P_set_def Q_set_def aux1a)
   1.523 +  ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set" 
   1.524 +    by auto
   1.525 +  also have "... = setsum (%j. q * j div p) P_set";
   1.526 +  proof -;
   1.527 +    note aux3a
   1.528 +    with  P_set_finite show ?thesis by (rule setsum_same_function)
   1.529 +  qed;
   1.530 +  finally show ?thesis .;
   1.531 +qed;
   1.532 +
   1.533 +lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set";
   1.534 +proof -;
   1.535 +  have "\<forall>x \<in> Q_set. finite (f2 x)";
   1.536 +  proof;
   1.537 +    fix x;
   1.538 +    have "f2 x \<subseteq> S" by (auto simp add: f2_def)
   1.539 +    with S_finite show "finite (f2 x)" by (auto simp add: finite_subset)
   1.540 +  qed;
   1.541 +  moreover have "(\<forall>x \<in> Q_set. \<forall>y \<in> Q_set. x \<noteq> y --> 
   1.542 +      (f2 x) \<inter> (f2 y) = {})";
   1.543 +    by (auto simp add: f2_def)
   1.544 +  moreover note Q_set_finite;
   1.545 +  ultimately have "int(card (UNION Q_set f2)) = 
   1.546 +      setsum (%x. int(card (f2 x))) Q_set";
   1.547 +    by (rule_tac A = Q_set in int_card_indexed_union_disjoint_sets, auto)
   1.548 +  moreover have "S2 = UNION Q_set f2";
   1.549 +    by (auto simp add: f2_def S_def S1_def S2_def P_set_def Q_set_def aux1b)
   1.550 +  ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set" 
   1.551 +    by auto
   1.552 +  also have "... = setsum (%j. p * j div q) Q_set";
   1.553 +  proof -;
   1.554 +    note aux3b;
   1.555 +    with Q_set_finite show ?thesis by (rule setsum_same_function)
   1.556 +  qed;
   1.557 +  finally show ?thesis .;
   1.558 +qed;
   1.559 +
   1.560 +lemma (in QRTEMP) S1_carda: "int (card(S1)) = 
   1.561 +    setsum (%j. (j * q) div p) P_set";
   1.562 +  by (auto simp add: S1_card zmult_ac)
   1.563 +
   1.564 +lemma (in QRTEMP) S2_carda: "int (card(S2)) = 
   1.565 +    setsum (%j. (j * p) div q) Q_set";
   1.566 +  by (auto simp add: S2_card zmult_ac)
   1.567 +
   1.568 +lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) + 
   1.569 +    (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)";
   1.570 +proof -;
   1.571 +  have "(setsum (%j. (j * p) div q) Q_set) + 
   1.572 +      (setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)";
   1.573 +    by (auto simp add: S1_carda S2_carda)
   1.574 +  also have "... = int (card S1) + int (card S2)";
   1.575 +    by auto
   1.576 +  also have "... = ((p - 1) div 2) * ((q - 1) div 2)";
   1.577 +    by (auto simp add: card_sum_S1_S2)
   1.578 +  finally show ?thesis .;
   1.579 +qed;
   1.580 +
   1.581 +lemma pq_prime_neq: "[| p \<in> zprime; q \<in> zprime; p \<noteq> q |] ==> (~[p = 0] (mod q))";
   1.582 +  apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
   1.583 +  apply (drule_tac x = q in allE)
   1.584 +  apply (drule_tac x = p in allE)
   1.585 +by auto
   1.586 +
   1.587 +lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) = 
   1.588 +    (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
   1.589 +proof -;
   1.590 +  from prems have "~([p = 0] (mod q))";
   1.591 +    by (auto simp add: pq_prime_neq QRTEMP_def)
   1.592 +  with prems have a1: "(Legendre p q) = (-1::int) ^ 
   1.593 +      nat(setsum (%x. ((x * p) div q)) Q_set)";
   1.594 +    apply (rule_tac p = q in  MainQRLemma)
   1.595 +    by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
   1.596 +  from prems have "~([q = 0] (mod p))";
   1.597 +    apply (rule_tac p = q and q = p in pq_prime_neq)
   1.598 +    apply (simp add: QRTEMP_def)+;
   1.599 +    by arith
   1.600 +  with prems have a2: "(Legendre q p) = 
   1.601 +      (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
   1.602 +    apply (rule_tac p = p in  MainQRLemma)
   1.603 +    by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
   1.604 +  from a1 a2 have "(Legendre p q) * (Legendre q p) = 
   1.605 +      (-1::int) ^ nat(setsum (%x. ((x * p) div q)) Q_set) *
   1.606 +        (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
   1.607 +    by auto
   1.608 +  also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) + 
   1.609 +                   nat(setsum (%x. ((x * q) div p)) P_set))";
   1.610 +    by (auto simp add: zpower_zadd_distrib)
   1.611 +  also have "nat(setsum (%x. ((x * p) div q)) Q_set) + 
   1.612 +      nat(setsum (%x. ((x * q) div p)) P_set) =
   1.613 +        nat((setsum (%x. ((x * p) div q)) Q_set) + 
   1.614 +          (setsum (%x. ((x * q) div p)) P_set))";
   1.615 +    apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in 
   1.616 +      nat_add_distrib [THEN sym]);
   1.617 +    by (auto simp add: S1_carda [THEN sym] S2_carda [THEN sym])
   1.618 +  also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))";
   1.619 +    by (auto simp add: pq_sum_prop)
   1.620 +  finally show ?thesis .;
   1.621 +qed;
   1.622 +
   1.623 +theorem Quadratic_Reciprocity:
   1.624 +     "[| p \<in> zOdd; p \<in> zprime; q \<in> zOdd; q \<in> zprime; 
   1.625 +         p \<noteq> q |] 
   1.626 +      ==> (Legendre p q) * (Legendre q p) = 
   1.627 +          (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
   1.628 +  by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [THEN sym] 
   1.629 +                     QRTEMP_def)
   1.630 +
   1.631 +end