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