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