src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
author haftmann
Tue Sep 01 15:39:33 2009 +0200 (2009-09-01)
changeset 32479 521cc9bf2958
parent 30034 src/HOL/NumberTheory/Quadratic_Reciprocity.thy@60f64f112174
child 38159 e9b4835a54ee
permissions -rw-r--r--
some reorganization of number theory
     1 (*  Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     2 *)
     3 
     4 header {* The law of Quadratic reciprocity *}
     5 
     6 theory Quadratic_Reciprocity
     7 imports Gauss
     8 begin
     9 
    10 text {*
    11   Lemmas leading up to the proof of theorem 3.3 in Niven and
    12   Zuckerman's presentation.
    13 *}
    14 
    15 context GAUSS
    16 begin
    17 
    18 lemma QRLemma1: "a * setsum id A =
    19   p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E"
    20 proof -
    21   from finite_A have "a * setsum id A = setsum (%x. a * x) A"
    22     by (auto simp add: setsum_const_mult id_def)
    23   also have "setsum (%x. a * x) = setsum (%x. x * a)"
    24     by (auto simp add: zmult_commute)
    25   also have "setsum (%x. x * a) A = setsum id B"
    26     by (simp add: B_def setsum_reindex_id[OF inj_on_xa_A])
    27   also have "... = setsum (%x. p * (x div p) + StandardRes p x) B"
    28     by (auto simp add: StandardRes_def zmod_zdiv_equality)
    29   also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B"
    30     by (rule setsum_addf)
    31   also have "setsum (StandardRes p) B = setsum id C"
    32     by (auto simp add: C_def setsum_reindex_id[OF SR_B_inj])
    33   also from C_eq have "... = setsum id (D \<union> E)"
    34     by auto
    35   also from finite_D finite_E have "... = setsum id D + setsum id E"
    36     by (rule setsum_Un_disjoint) (auto simp add: D_def E_def)
    37   also have "setsum (%x. p * (x div p)) B =
    38       setsum ((%x. p * (x div p)) o (%x. (x * a))) A"
    39     by (auto simp add: B_def setsum_reindex inj_on_xa_A)
    40   also have "... = setsum (%x. p * ((x * a) div p)) A"
    41     by (auto simp add: o_def)
    42   also from finite_A have "setsum (%x. p * ((x * a) div p)) A =
    43     p * setsum (%x. ((x * a) div p)) A"
    44     by (auto simp add: setsum_const_mult)
    45   finally show ?thesis by arith
    46 qed
    47 
    48 lemma QRLemma2: "setsum id A = p * int (card E) - setsum id E +
    49   setsum id D"
    50 proof -
    51   from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)"
    52     by (simp add: Un_commute)
    53   also from F_D_disj finite_D finite_F
    54   have "... = setsum id D + setsum id F"
    55     by (auto simp add: Int_commute intro: setsum_Un_disjoint)
    56   also from F_def have "F = (%x. (p - x)) ` E"
    57     by auto
    58   also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) =
    59       setsum (%x. (p - x)) E"
    60     by (auto simp add: setsum_reindex)
    61   also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E"
    62     by (auto simp add: setsum_subtractf id_def)
    63   also from finite_E have "setsum (%x. p) E = p * int(card E)"
    64     by (intro setsum_const)
    65   finally show ?thesis
    66     by arith
    67 qed
    68 
    69 lemma QRLemma3: "(a - 1) * setsum id A =
    70     p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E"
    71 proof -
    72   have "(a - 1) * setsum id A = a * setsum id A - setsum id A"
    73     by (auto simp add: zdiff_zmult_distrib)
    74   also note QRLemma1
    75   also from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
    76      setsum id E - setsum id A =
    77       p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
    78       setsum id E - (p * int (card E) - setsum id E + setsum id D)"
    79     by auto
    80   also have "... = p * (\<Sum>x \<in> A. x * a div p) -
    81       p * int (card E) + 2 * setsum id E"
    82     by arith
    83   finally show ?thesis
    84     by (auto simp only: zdiff_zmult_distrib2)
    85 qed
    86 
    87 lemma QRLemma4: "a \<in> zOdd ==>
    88     (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)"
    89 proof -
    90   assume a_odd: "a \<in> zOdd"
    91   from QRLemma3 have a: "p * (setsum (%x. ((x * a) div p)) A - int(card E)) =
    92       (a - 1) * setsum id A - 2 * setsum id E"
    93     by arith
    94   from a_odd have "a - 1 \<in> zEven"
    95     by (rule odd_minus_one_even)
    96   hence "(a - 1) * setsum id A \<in> zEven"
    97     by (rule even_times_either)
    98   moreover have "2 * setsum id E \<in> zEven"
    99     by (auto simp add: zEven_def)
   100   ultimately have "(a - 1) * setsum id A - 2 * setsum id E \<in> zEven"
   101     by (rule even_minus_even)
   102   with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven"
   103     by simp
   104   hence "p \<in> zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven"
   105     by (rule EvenOdd.even_product)
   106   with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven"
   107     by (auto simp add: odd_iff_not_even)
   108   thus ?thesis
   109     by (auto simp only: even_diff [symmetric])
   110 qed
   111 
   112 lemma QRLemma5: "a \<in> zOdd ==>
   113    (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
   114 proof -
   115   assume "a \<in> zOdd"
   116   from QRLemma4 [OF this] have
   117     "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
   118   moreover have "0 \<le> int(card E)"
   119     by auto
   120   moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
   121     proof (intro setsum_nonneg)
   122       show "\<forall>x \<in> A. 0 \<le> x * a div p"
   123       proof
   124         fix x
   125         assume "x \<in> A"
   126         then have "0 \<le> x"
   127           by (auto simp add: A_def)
   128         with a_nonzero have "0 \<le> x * a"
   129           by (auto simp add: zero_le_mult_iff)
   130         with p_g_2 show "0 \<le> x * a div p"
   131           by (auto simp add: pos_imp_zdiv_nonneg_iff)
   132       qed
   133     qed
   134   ultimately have "(-1::int)^nat((int (card E))) =
   135       (-1)^nat(((\<Sum>x \<in> A. x * a div p)))"
   136     by (intro neg_one_power_parity, auto)
   137   also have "nat (int(card E)) = card E"
   138     by auto
   139   finally show ?thesis .
   140 qed
   141 
   142 end
   143 
   144 lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p)); zprime p; 2 < p;
   145   A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==>
   146   (Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
   147   apply (subst GAUSS.gauss_lemma)
   148   apply (auto simp add: GAUSS_def)
   149   apply (subst GAUSS.QRLemma5)
   150   apply (auto simp add: GAUSS_def)
   151   apply (simp add: GAUSS.A_def [OF GAUSS.intro] GAUSS_def)
   152   done
   153 
   154 
   155 subsection {* Stuff about S, S1 and S2 *}
   156 
   157 locale QRTEMP =
   158   fixes p     :: "int"
   159   fixes q     :: "int"
   160 
   161   assumes p_prime: "zprime p"
   162   assumes p_g_2: "2 < p"
   163   assumes q_prime: "zprime q"
   164   assumes q_g_2: "2 < q"
   165   assumes p_neq_q:      "p \<noteq> q"
   166 begin
   167 
   168 definition
   169   P_set :: "int set" where
   170   "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
   171 
   172 definition
   173   Q_set :: "int set" where
   174   "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
   175   
   176 definition
   177   S :: "(int * int) set" where
   178   "S = P_set <*> Q_set"
   179 
   180 definition
   181   S1 :: "(int * int) set" where
   182   "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
   183 
   184 definition
   185   S2 :: "(int * int) set" where
   186   "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
   187 
   188 definition
   189   f1 :: "int => (int * int) set" where
   190   "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
   191 
   192 definition
   193   f2 :: "int => (int * int) set" where
   194   "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
   195 
   196 lemma p_fact: "0 < (p - 1) div 2"
   197 proof -
   198   from p_g_2 have "2 \<le> p - 1" by arith
   199   then have "2 div 2 \<le> (p - 1) div 2" by (rule zdiv_mono1, auto)
   200   then show ?thesis by auto
   201 qed
   202 
   203 lemma q_fact: "0 < (q - 1) div 2"
   204 proof -
   205   from q_g_2 have "2 \<le> q - 1" by arith
   206   then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto)
   207   then show ?thesis by auto
   208 qed
   209 
   210 lemma pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
   211     (p * b \<noteq> q * a)"
   212 proof
   213   assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2"
   214   then have "q dvd (p * b)" by (auto simp add: dvd_def)
   215   with q_prime p_g_2 have "q dvd p | q dvd b"
   216     by (auto simp add: zprime_zdvd_zmult)
   217   moreover have "~ (q dvd p)"
   218   proof
   219     assume "q dvd p"
   220     with p_prime have "q = 1 | q = p"
   221       apply (auto simp add: zprime_def QRTEMP_def)
   222       apply (drule_tac x = q and R = False in allE)
   223       apply (simp add: QRTEMP_def)
   224       apply (subgoal_tac "0 \<le> q", simp add: QRTEMP_def)
   225       apply (insert prems)
   226       apply (auto simp add: QRTEMP_def)
   227       done
   228     with q_g_2 p_neq_q show False by auto
   229   qed
   230   ultimately have "q dvd b" by auto
   231   then have "q \<le> b"
   232   proof -
   233     assume "q dvd b"
   234     moreover from prems have "0 < b" by auto
   235     ultimately show ?thesis using zdvd_bounds [of q b] by auto
   236   qed
   237   with prems have "q \<le> (q - 1) div 2" by auto
   238   then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
   239   then have "2 * q \<le> q - 1"
   240   proof -
   241     assume "2 * q \<le> 2 * ((q - 1) div 2)"
   242     with prems have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
   243     with odd_minus_one_even have "(q - 1):zEven" by auto
   244     with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto
   245     with prems show ?thesis by auto
   246   qed
   247   then have p1: "q \<le> -1" by arith
   248   with q_g_2 show False by auto
   249 qed
   250 
   251 lemma P_set_finite: "finite (P_set)"
   252   using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)
   253 
   254 lemma Q_set_finite: "finite (Q_set)"
   255   using q_fact by (auto simp add: Q_set_def bdd_int_set_l_le_finite)
   256 
   257 lemma S_finite: "finite S"
   258   by (auto simp add: S_def  P_set_finite Q_set_finite finite_cartesian_product)
   259 
   260 lemma S1_finite: "finite S1"
   261 proof -
   262   have "finite S" by (auto simp add: S_finite)
   263   moreover have "S1 \<subseteq> S" by (auto simp add: S1_def S_def)
   264   ultimately show ?thesis by (auto simp add: finite_subset)
   265 qed
   266 
   267 lemma S2_finite: "finite S2"
   268 proof -
   269   have "finite S" by (auto simp add: S_finite)
   270   moreover have "S2 \<subseteq> S" by (auto simp add: S2_def S_def)
   271   ultimately show ?thesis by (auto simp add: finite_subset)
   272 qed
   273 
   274 lemma P_set_card: "(p - 1) div 2 = int (card (P_set))"
   275   using p_fact by (auto simp add: P_set_def card_bdd_int_set_l_le)
   276 
   277 lemma Q_set_card: "(q - 1) div 2 = int (card (Q_set))"
   278   using q_fact by (auto simp add: Q_set_def card_bdd_int_set_l_le)
   279 
   280 lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
   281   using P_set_card Q_set_card P_set_finite Q_set_finite
   282   by (auto simp add: S_def zmult_int setsum_constant)
   283 
   284 lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
   285   by (auto simp add: S1_def S2_def)
   286 
   287 lemma S1_Union_S2_prop: "S = S1 \<union> S2"
   288   apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
   289 proof -
   290   fix a and b
   291   assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2"
   292   with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
   293   moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
   294   ultimately show "p * b < q * a" by auto
   295 qed
   296 
   297 lemma card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) =
   298     int(card(S1)) + int(card(S2))"
   299 proof -
   300   have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
   301     by (auto simp add: S_card)
   302   also have "... = int( card(S1) + card(S2))"
   303     apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop)
   304     apply (drule card_Un_disjoint, auto)
   305     done
   306   also have "... = int(card(S1)) + int(card(S2))" by auto
   307   finally show ?thesis .
   308 qed
   309 
   310 lemma aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
   311                              0 < b; b \<le> (q - 1) div 2 |] ==>
   312                           (p * b < q * a) = (b \<le> q * a div p)"
   313 proof -
   314   assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
   315   have "p * b < q * a ==> b \<le> q * a div p"
   316   proof -
   317     assume "p * b < q * a"
   318     then have "p * b \<le> q * a" by auto
   319     then have "(p * b) div p \<le> (q * a) div p"
   320       by (rule zdiv_mono1) (insert p_g_2, auto)
   321     then show "b \<le> (q * a) div p"
   322       apply (subgoal_tac "p \<noteq> 0")
   323       apply (frule div_mult_self1_is_id, force)
   324       apply (insert p_g_2, auto)
   325       done
   326   qed
   327   moreover have "b \<le> q * a div p ==> p * b < q * a"
   328   proof -
   329     assume "b \<le> q * a div p"
   330     then have "p * b \<le> p * ((q * a) div p)"
   331       using p_g_2 by (auto simp add: mult_le_cancel_left)
   332     also have "... \<le> q * a"
   333       by (rule zdiv_leq_prop) (insert p_g_2, auto)
   334     finally have "p * b \<le> q * a" .
   335     then have "p * b < q * a | p * b = q * a"
   336       by (simp only: order_le_imp_less_or_eq)
   337     moreover have "p * b \<noteq> q * a"
   338       by (rule  pb_neq_qa) (insert prems, auto)
   339     ultimately show ?thesis by auto
   340   qed
   341   ultimately show ?thesis ..
   342 qed
   343 
   344 lemma aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
   345                              0 < b; b \<le> (q - 1) div 2 |] ==>
   346                           (q * a < p * b) = (a \<le> p * b div q)"
   347 proof -
   348   assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
   349   have "q * a < p * b ==> a \<le> p * b div q"
   350   proof -
   351     assume "q * a < p * b"
   352     then have "q * a \<le> p * b" by auto
   353     then have "(q * a) div q \<le> (p * b) div q"
   354       by (rule zdiv_mono1) (insert q_g_2, auto)
   355     then show "a \<le> (p * b) div q"
   356       apply (subgoal_tac "q \<noteq> 0")
   357       apply (frule div_mult_self1_is_id, force)
   358       apply (insert q_g_2, auto)
   359       done
   360   qed
   361   moreover have "a \<le> p * b div q ==> q * a < p * b"
   362   proof -
   363     assume "a \<le> p * b div q"
   364     then have "q * a \<le> q * ((p * b) div q)"
   365       using q_g_2 by (auto simp add: mult_le_cancel_left)
   366     also have "... \<le> p * b"
   367       by (rule zdiv_leq_prop) (insert q_g_2, auto)
   368     finally have "q * a \<le> p * b" .
   369     then have "q * a < p * b | q * a = p * b"
   370       by (simp only: order_le_imp_less_or_eq)
   371     moreover have "p * b \<noteq> q * a"
   372       by (rule  pb_neq_qa) (insert prems, auto)
   373     ultimately show ?thesis by auto
   374   qed
   375   ultimately show ?thesis ..
   376 qed
   377 
   378 lemma (in -) aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
   379              (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
   380 proof-
   381   assume "zprime p" and "zprime q" and "2 < p" and "2 < q"
   382   (* Set up what's even and odd *)
   383   then have "p \<in> zOdd & q \<in> zOdd"
   384     by (auto simp add:  zprime_zOdd_eq_grt_2)
   385   then have even1: "(p - 1):zEven & (q - 1):zEven"
   386     by (auto simp add: odd_minus_one_even)
   387   then have even2: "(2 * p):zEven & ((q - 1) * p):zEven"
   388     by (auto simp add: zEven_def)
   389   then have even3: "(((q - 1) * p) + (2 * p)):zEven"
   390     by (auto simp: EvenOdd.even_plus_even)
   391   (* using these prove it *)
   392   from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)"
   393     by (auto simp add: int_distrib)
   394   then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
   395     apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
   396     by (auto simp add: even3, auto simp add: zmult_ac)
   397   also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)"
   398     by (auto simp add: even1 even_prod_div_2)
   399   also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
   400     by (auto simp add: even1 even2 even_prod_div_2 even_sum_div_2)
   401   finally show ?thesis
   402     apply (rule_tac x = " q * ((p - 1) div 2)" and
   403                     y = "(q - 1) div 2" in div_prop2)
   404     using prems by auto
   405 qed
   406 
   407 lemma aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
   408 proof
   409   fix j
   410   assume j_fact: "j \<in> P_set"
   411   have "int (card (f1 j)) = int (card {y. y \<in> Q_set & y \<le> (q * j) div p})"
   412   proof -
   413     have "finite (f1 j)"
   414     proof -
   415       have "(f1 j) \<subseteq> S" by (auto simp add: f1_def)
   416       with S_finite show ?thesis by (auto simp add: finite_subset)
   417     qed
   418     moreover have "inj_on (%(x,y). y) (f1 j)"
   419       by (auto simp add: f1_def inj_on_def)
   420     ultimately have "card ((%(x,y). y) ` (f1 j)) = card  (f1 j)"
   421       by (auto simp add: f1_def card_image)
   422     moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}"
   423       using prems by (auto simp add: f1_def S_def Q_set_def P_set_def image_def)
   424     ultimately show ?thesis by (auto simp add: f1_def)
   425   qed
   426   also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})"
   427   proof -
   428     have "{y. y \<in> Q_set & y \<le> (q * j) div p} =
   429         {y. 0 < y & y \<le> (q * j) div p}"
   430       apply (auto simp add: Q_set_def)
   431     proof -
   432       fix x
   433       assume "0 < x" and "x \<le> q * j div p"
   434       with j_fact P_set_def  have "j \<le> (p - 1) div 2" by auto
   435       with q_g_2 have "q * j \<le> q * ((p - 1) div 2)"
   436         by (auto simp add: mult_le_cancel_left)
   437       with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
   438         by (auto simp add: zdiv_mono1)
   439       also from prems P_set_def have "... \<le> (q - 1) div 2"
   440         apply simp
   441         apply (insert aux2)
   442         apply (simp add: QRTEMP_def)
   443         done
   444       finally show "x \<le> (q - 1) div 2" using prems by auto
   445     qed
   446     then show ?thesis by auto
   447   qed
   448   also have "... = (q * j) div p"
   449   proof -
   450     from j_fact P_set_def have "0 \<le> j" by auto
   451     with q_g_2 have "q * 0 \<le> q * j" by (auto simp only: mult_left_mono)
   452     then have "0 \<le> q * j" by auto
   453     then have "0 div p \<le> (q * j) div p"
   454       apply (rule_tac a = 0 in zdiv_mono1)
   455       apply (insert p_g_2, auto)
   456       done
   457     also have "0 div p = 0" by auto
   458     finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
   459   qed
   460   finally show "int (card (f1 j)) = q * j div p" .
   461 qed
   462 
   463 lemma aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q"
   464 proof
   465   fix j
   466   assume j_fact: "j \<in> Q_set"
   467   have "int (card (f2 j)) = int (card {y. y \<in> P_set & y \<le> (p * j) div q})"
   468   proof -
   469     have "finite (f2 j)"
   470     proof -
   471       have "(f2 j) \<subseteq> S" by (auto simp add: f2_def)
   472       with S_finite show ?thesis by (auto simp add: finite_subset)
   473     qed
   474     moreover have "inj_on (%(x,y). x) (f2 j)"
   475       by (auto simp add: f2_def inj_on_def)
   476     ultimately have "card ((%(x,y). x) ` (f2 j)) = card  (f2 j)"
   477       by (auto simp add: f2_def card_image)
   478     moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}"
   479       using prems by (auto simp add: f2_def S_def Q_set_def P_set_def image_def)
   480     ultimately show ?thesis by (auto simp add: f2_def)
   481   qed
   482   also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})"
   483   proof -
   484     have "{y. y \<in> P_set & y \<le> (p * j) div q} =
   485         {y. 0 < y & y \<le> (p * j) div q}"
   486       apply (auto simp add: P_set_def)
   487     proof -
   488       fix x
   489       assume "0 < x" and "x \<le> p * j div q"
   490       with j_fact Q_set_def  have "j \<le> (q - 1) div 2" by auto
   491       with p_g_2 have "p * j \<le> p * ((q - 1) div 2)"
   492         by (auto simp add: mult_le_cancel_left)
   493       with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q"
   494         by (auto simp add: zdiv_mono1)
   495       also from prems have "... \<le> (p - 1) div 2"
   496         by (auto simp add: aux2 QRTEMP_def)
   497       finally show "x \<le> (p - 1) div 2" using prems by auto
   498       qed
   499     then show ?thesis by auto
   500   qed
   501   also have "... = (p * j) div q"
   502   proof -
   503     from j_fact Q_set_def have "0 \<le> j" by auto
   504     with p_g_2 have "p * 0 \<le> p * j" by (auto simp only: mult_left_mono)
   505     then have "0 \<le> p * j" by auto
   506     then have "0 div q \<le> (p * j) div q"
   507       apply (rule_tac a = 0 in zdiv_mono1)
   508       apply (insert q_g_2, auto)
   509       done
   510     also have "0 div q = 0" by auto
   511     finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
   512   qed
   513   finally show "int (card (f2 j)) = p * j div q" .
   514 qed
   515 
   516 lemma S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set"
   517 proof -
   518   have "\<forall>x \<in> P_set. finite (f1 x)"
   519   proof
   520     fix x
   521     have "f1 x \<subseteq> S" by (auto simp add: f1_def)
   522     with S_finite show "finite (f1 x)" by (auto simp add: finite_subset)
   523   qed
   524   moreover have "(\<forall>x \<in> P_set. \<forall>y \<in> P_set. x \<noteq> y --> (f1 x) \<inter> (f1 y) = {})"
   525     by (auto simp add: f1_def)
   526   moreover note P_set_finite
   527   ultimately have "int(card (UNION P_set f1)) =
   528       setsum (%x. int(card (f1 x))) P_set"
   529     by(simp add:card_UN_disjoint int_setsum o_def)
   530   moreover have "S1 = UNION P_set f1"
   531     by (auto simp add: f1_def S_def S1_def S2_def P_set_def Q_set_def aux1a)
   532   ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set"
   533     by auto
   534   also have "... = setsum (%j. q * j div p) P_set"
   535     using aux3a by(fastsimp intro: setsum_cong)
   536   finally show ?thesis .
   537 qed
   538 
   539 lemma S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set"
   540 proof -
   541   have "\<forall>x \<in> Q_set. finite (f2 x)"
   542   proof
   543     fix x
   544     have "f2 x \<subseteq> S" by (auto simp add: f2_def)
   545     with S_finite show "finite (f2 x)" by (auto simp add: finite_subset)
   546   qed
   547   moreover have "(\<forall>x \<in> Q_set. \<forall>y \<in> Q_set. x \<noteq> y -->
   548       (f2 x) \<inter> (f2 y) = {})"
   549     by (auto simp add: f2_def)
   550   moreover note Q_set_finite
   551   ultimately have "int(card (UNION Q_set f2)) =
   552       setsum (%x. int(card (f2 x))) Q_set"
   553     by(simp add:card_UN_disjoint int_setsum o_def)
   554   moreover have "S2 = UNION Q_set f2"
   555     by (auto simp add: f2_def S_def S1_def S2_def P_set_def Q_set_def aux1b)
   556   ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set"
   557     by auto
   558   also have "... = setsum (%j. p * j div q) Q_set"
   559     using aux3b by(fastsimp intro: setsum_cong)
   560   finally show ?thesis .
   561 qed
   562 
   563 lemma S1_carda: "int (card(S1)) =
   564     setsum (%j. (j * q) div p) P_set"
   565   by (auto simp add: S1_card zmult_ac)
   566 
   567 lemma S2_carda: "int (card(S2)) =
   568     setsum (%j. (j * p) div q) Q_set"
   569   by (auto simp add: S2_card zmult_ac)
   570 
   571 lemma pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
   572     (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
   573 proof -
   574   have "(setsum (%j. (j * p) div q) Q_set) +
   575       (setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)"
   576     by (auto simp add: S1_carda S2_carda)
   577   also have "... = int (card S1) + int (card S2)"
   578     by auto
   579   also have "... = ((p - 1) div 2) * ((q - 1) div 2)"
   580     by (auto simp add: card_sum_S1_S2)
   581   finally show ?thesis .
   582 qed
   583 
   584 
   585 lemma (in -) pq_prime_neq: "[| zprime p; zprime q; p \<noteq> q |] ==> (~[p = 0] (mod q))"
   586   apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
   587   apply (drule_tac x = q in allE)
   588   apply (drule_tac x = p in allE)
   589   apply auto
   590   done
   591 
   592 
   593 lemma QR_short: "(Legendre p q) * (Legendre q p) =
   594     (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
   595 proof -
   596   from prems have "~([p = 0] (mod q))"
   597     by (auto simp add: pq_prime_neq QRTEMP_def)
   598   with prems Q_set_def have a1: "(Legendre p q) = (-1::int) ^
   599       nat(setsum (%x. ((x * p) div q)) Q_set)"
   600     apply (rule_tac p = q in  MainQRLemma)
   601     apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
   602     done
   603   from prems have "~([q = 0] (mod p))"
   604     apply (rule_tac p = q and q = p in pq_prime_neq)
   605     apply (simp add: QRTEMP_def)+
   606     done
   607   with prems P_set_def have a2: "(Legendre q p) =
   608       (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
   609     apply (rule_tac p = p in  MainQRLemma)
   610     apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
   611     done
   612   from a1 a2 have "(Legendre p q) * (Legendre q p) =
   613       (-1::int) ^ nat(setsum (%x. ((x * p) div q)) Q_set) *
   614         (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
   615     by auto
   616   also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) +
   617                    nat(setsum (%x. ((x * q) div p)) P_set))"
   618     by (auto simp add: zpower_zadd_distrib)
   619   also have "nat(setsum (%x. ((x * p) div q)) Q_set) +
   620       nat(setsum (%x. ((x * q) div p)) P_set) =
   621         nat((setsum (%x. ((x * p) div q)) Q_set) +
   622           (setsum (%x. ((x * q) div p)) P_set))"
   623     apply (rule_tac z = "setsum (%x. ((x * p) div q)) Q_set" in
   624       nat_add_distrib [symmetric])
   625     apply (auto simp add: S1_carda [symmetric] S2_carda [symmetric])
   626     done
   627   also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))"
   628     by (auto simp add: pq_sum_prop)
   629   finally show ?thesis .
   630 qed
   631 
   632 end
   633 
   634 theorem Quadratic_Reciprocity:
   635      "[| p \<in> zOdd; zprime p; q \<in> zOdd; zprime q;
   636          p \<noteq> q |]
   637       ==> (Legendre p q) * (Legendre q p) =
   638           (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
   639   by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [symmetric]
   640                      QRTEMP_def)
   641 
   642 end