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