src/HOL/NumberTheory/Quadratic_Reciprocity.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14981 e73f8140af78
child 15392 290bc97038c7
permissions -rw-r--r--
import -> imports
     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 = Gauss:;
     9 
    10 (***************************************************************)
    11 (*                                                             *)
    12 (*  Lemmas leading up to the proof of theorem 3.3 in           *)
    13 (*  Niven and Zuckerman's presentation                         *)
    14 (*                                                             *)
    15 (***************************************************************)
    16 
    17 lemma (in GAUSS) QRLemma1: "a * setsum id A = 
    18   p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E";
    19 proof -;
    20   from finite_A have "a * setsum id A = setsum (%x. a * x) A"; 
    21     by (auto simp add: setsum_const_mult id_def)
    22   also have "setsum (%x. a * x) = setsum (%x. x * a)"; 
    23     by (auto simp add: zmult_commute)
    24   also; have "setsum (%x. x * a) A = setsum id B";
    25     by (auto simp add: B_def sum_prop_id finite_A inj_on_xa_A)
    26   also have "... = setsum (%x. p * (x div p) + StandardRes p x) B";
    27     apply (rule setsum_same_function)
    28     by (auto simp add: finite_B 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 sum_prop_id [THEN sym] finite_B 
    33       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     apply (rule setsum_Un_disjoint)
    38     by (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 sum_prop finite_A 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 (in GAUSS) 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 have 
    56       "... = setsum id D + setsum id F";
    57     apply (simp add: Int_commute)
    58     by (intro setsum_Un_disjoint) 
    59   also from F_def have "F = (%x. (p - x)) ` E";
    60     by auto
    61   also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) =
    62       setsum (%x. (p - x)) E";
    63     by (auto simp add: sum_prop)
    64   also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E";
    65     by (auto simp add: setsum_minus id_def)
    66   also from finite_E have "setsum (%x. p) E = p * int(card E)";
    67     by (intro setsum_const)
    68   finally show ?thesis;
    69     by arith
    70 qed;
    71 
    72 lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A = 
    73     p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E";
    74 proof -;
    75   have "(a - 1) * setsum id A = a * setsum id A - setsum id A";
    76     by (auto simp add: zdiff_zmult_distrib)  
    77   also note QRLemma1;
    78   also; from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
    79      setsum id E - setsum id A = 
    80       p * (\<Sum>x \<in> A. x * a div p) + setsum id D + 
    81       setsum id E - (p * int (card E) - setsum id E + setsum id D)";
    82     by auto
    83   also; have "... = p * (\<Sum>x \<in> A. x * a div p) - 
    84       p * int (card E) + 2 * setsum id E"; 
    85     by arith
    86   finally show ?thesis;
    87     by (auto simp only: zdiff_zmult_distrib2)
    88 qed;
    89 
    90 lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==> 
    91     (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)";
    92 proof -;
    93   assume a_odd: "a \<in> zOdd";
    94   from QRLemma3 have a: "p * (setsum (%x. ((x * a) div p)) A - int(card E)) =
    95       (a - 1) * setsum id A - 2 * setsum id E"; 
    96     by arith
    97   from a_odd have "a - 1 \<in> zEven"
    98     by (rule odd_minus_one_even)
    99   hence "(a - 1) * setsum id A \<in> zEven";
   100     by (rule even_times_either)
   101   moreover have "2 * setsum id E \<in> zEven";
   102     by (auto simp add: zEven_def)
   103   ultimately have "(a - 1) * setsum id A - 2 * setsum id E \<in> zEven"
   104     by (rule even_minus_even)
   105   with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
   106     by simp
   107   hence "p \<in> zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
   108     by (rule EvenOdd.even_product)
   109   with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
   110     by (auto simp add: odd_iff_not_even)
   111   thus ?thesis;
   112     by (auto simp only: even_diff [THEN sym])
   113 qed;
   114 
   115 lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==> 
   116    (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
   117 proof -;
   118   assume "a \<in> zOdd";
   119   from QRLemma4 have
   120     "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)";..;
   121   moreover have "0 \<le> int(card E)";
   122     by auto
   123   moreover have "0 \<le> setsum (%x. ((x * a) div p)) A";
   124     proof (intro setsum_non_neg);
   125       from finite_A show "finite A";.;
   126       next show "\<forall>x \<in> A. 0 \<le> x * a div p";
   127       proof;
   128         fix x;
   129         assume "x \<in> A";
   130         then have "0 \<le> x";
   131           by (auto simp add: A_def)
   132         with a_nonzero have "0 \<le> x * a";
   133           by (auto simp add: zero_le_mult_iff)
   134         with p_g_2 show "0 \<le> x * a div p"; 
   135           by (auto simp add: pos_imp_zdiv_nonneg_iff)
   136       qed;
   137     qed;
   138   ultimately have "(-1::int)^nat((int (card E))) =
   139       (-1)^nat(((\<Sum>x \<in> A. x * a div p)))";
   140     by (intro neg_one_power_parity, auto)
   141   also have "nat (int(card E)) = card E";
   142     by auto
   143   finally show ?thesis;.;
   144 qed;
   145 
   146 lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p));p \<in> zprime; 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 by (auto simp add: GAUSS_def)
   153 
   154 (******************************************************************)
   155 (*                                                                *)
   156 (* Stuff about S, S1 and S2...                                    *)
   157 (*                                                                *)
   158 (******************************************************************)
   159 
   160 locale QRTEMP =
   161   fixes p     :: "int"
   162   fixes q     :: "int"
   163   fixes P_set :: "int set"
   164   fixes Q_set :: "int set"
   165   fixes S     :: "(int * int) set"
   166   fixes S1    :: "(int * int) set"
   167   fixes S2    :: "(int * int) set"
   168   fixes f1    :: "int => (int * int) set"
   169   fixes f2    :: "int => (int * int) set"
   170 
   171   assumes p_prime: "p \<in> zprime"
   172   assumes p_g_2: "2 < p"
   173   assumes q_prime: "q \<in> zprime"
   174   assumes q_g_2: "2 < q"
   175   assumes p_neq_q:      "p \<noteq> q"
   176 
   177   defines P_set_def: "P_set == {x. 0 < x & x \<le> ((p - 1) div 2) }"
   178   defines Q_set_def: "Q_set == {x. 0 < x & x \<le> ((q - 1) div 2) }"
   179   defines S_def:     "S     == P_set <*> Q_set"
   180   defines S1_def:    "S1    == { (x, y). (x, y):S & ((p * y) < (q * x)) }"
   181   defines S2_def:    "S2    == { (x, y). (x, y):S & ((q * x) < (p * y)) }"
   182   defines f1_def:    "f1 j  == { (j1, y). (j1, y):S & j1 = j & 
   183                                  (y \<le> (q * j) div p) }"
   184   defines f2_def:    "f2 j  == { (x, j1). (x, j1):S & j1 = j & 
   185                                  (x \<le> (p * j) div q) }";
   186 
   187 lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2";
   188 proof -;
   189   from prems have "2 < p" by (simp add: QRTEMP_def)
   190   then have "2 \<le> p - 1" by arith
   191   then have "2 div 2 \<le> (p - 1) div 2" by (rule zdiv_mono1, auto)
   192   then show ?thesis by auto
   193 qed;
   194 
   195 lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2";
   196 proof -;
   197   from prems have "2 < q" by (simp add: QRTEMP_def)
   198   then have "2 \<le> q - 1" by arith
   199   then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto)
   200   then show ?thesis by auto
   201 qed;
   202 
   203 lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==> 
   204     (p * b \<noteq> q * a)";
   205 proof;
   206   assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2";
   207   then have "q dvd (p * b)" by (auto simp add: dvd_def)
   208   with q_prime p_g_2 have "q dvd p | q dvd b";
   209     by (auto simp add: zprime_zdvd_zmult)
   210   moreover have "~ (q dvd p)";
   211   proof;
   212     assume "q dvd p";
   213     with p_prime have "q = 1 | q = p"
   214       apply (auto simp add: zprime_def QRTEMP_def)
   215       apply (drule_tac x = q and R = False in allE)
   216       apply (simp add: QRTEMP_def)    
   217       apply (subgoal_tac "0 \<le> q", simp add: QRTEMP_def)
   218       apply (insert prems)
   219     by (auto simp add: QRTEMP_def)
   220     with q_g_2 p_neq_q show False by auto
   221   qed;
   222   ultimately have "q dvd b" by auto
   223   then have "q \<le> b";
   224   proof -;
   225     assume "q dvd b";
   226     moreover from prems have "0 < b" by auto
   227     ultimately show ?thesis by (insert zdvd_bounds [of q b], auto)
   228   qed;
   229   with prems have "q \<le> (q - 1) div 2" by auto
   230   then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
   231   then have "2 * q \<le> q - 1";
   232   proof -;
   233     assume "2 * q \<le> 2 * ((q - 1) div 2)";
   234     with prems have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
   235     with odd_minus_one_even have "(q - 1):zEven" by auto
   236     with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto
   237     with prems show ?thesis by auto
   238   qed;
   239   then have p1: "q \<le> -1" by arith
   240   with q_g_2 show False by auto
   241 qed;
   242 
   243 lemma (in QRTEMP) P_set_finite: "finite (P_set)";
   244   by (insert p_fact, auto simp add: P_set_def bdd_int_set_l_le_finite)
   245 
   246 lemma (in QRTEMP) Q_set_finite: "finite (Q_set)";
   247   by (insert q_fact, auto simp add: Q_set_def bdd_int_set_l_le_finite)
   248 
   249 lemma (in QRTEMP) S_finite: "finite S";
   250   by (auto simp add: S_def  P_set_finite Q_set_finite cartesian_product_finite)
   251 
   252 lemma (in QRTEMP) S1_finite: "finite S1";
   253 proof -;
   254   have "finite S" by (auto simp add: S_finite)
   255   moreover have "S1 \<subseteq> S" by (auto simp add: S1_def S_def)
   256   ultimately show ?thesis by (auto simp add: finite_subset)
   257 qed;
   258 
   259 lemma (in QRTEMP) S2_finite: "finite S2";
   260 proof -;
   261   have "finite S" by (auto simp add: S_finite)
   262   moreover have "S2 \<subseteq> S" by (auto simp add: S2_def S_def)
   263   ultimately show ?thesis by (auto simp add: finite_subset)
   264 qed;
   265 
   266 lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))";
   267   by (insert p_fact, auto simp add: P_set_def card_bdd_int_set_l_le)
   268 
   269 lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))";
   270   by (insert q_fact, auto simp add: Q_set_def card_bdd_int_set_l_le)
   271 
   272 lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
   273   apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
   274   apply (auto simp add: S_def zmult_int setsum_constant_nat) 
   275 done
   276 
   277 lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}";
   278   by (auto simp add: S1_def S2_def)
   279 
   280 lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2";
   281   apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
   282   proof -;
   283     fix a and b;
   284     assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2";
   285     with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
   286     moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
   287     ultimately show "p * b < q * a" by auto
   288   qed;
   289 
   290 lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) = 
   291     int(card(S1)) + int(card(S2))";
   292 proof-;
   293   have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
   294     by (auto simp add: S_card)
   295   also have "... = int( card(S1) + card(S2))";
   296     apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop)
   297     apply (drule card_Un_disjoint, auto)
   298   done
   299   also have "... = int(card(S1)) + int(card(S2))" by auto
   300   finally show ?thesis .;
   301 qed;
   302 
   303 lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2; 
   304                              0 < b; b \<le> (q - 1) div 2 |] ==>
   305                           (p * b < q * a) = (b \<le> q * a div p)";
   306 proof -;
   307   assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
   308   have "p * b < q * a ==> b \<le> q * a div p";
   309   proof -;
   310     assume "p * b < q * a";
   311     then have "p * b \<le> q * a" by auto
   312     then have "(p * b) div p \<le> (q * a) div p";
   313       by (rule zdiv_mono1, insert p_g_2, auto)
   314     then show "b \<le> (q * a) div p";
   315       apply (subgoal_tac "p \<noteq> 0")
   316       apply (frule zdiv_zmult_self2, force)
   317       by (insert p_g_2, auto)
   318   qed;
   319   moreover have "b \<le> q * a div p ==> p * b < q * a";
   320   proof -;
   321     assume "b \<le> q * a div p";
   322     then have "p * b \<le> p * ((q * a) div p)";
   323       by (insert p_g_2, auto simp add: mult_le_cancel_left)
   324     also have "... \<le> q * a";
   325       by (rule zdiv_leq_prop, insert p_g_2, auto)
   326     finally have "p * b \<le> q * a" .;
   327     then have "p * b < q * a | p * b = q * a";
   328       by (simp only: order_le_imp_less_or_eq)
   329     moreover have "p * b \<noteq> q * a";
   330       by (rule  pb_neq_qa, insert prems, auto)
   331     ultimately show ?thesis by auto
   332   qed;
   333   ultimately show ?thesis ..;
   334 qed;
   335 
   336 lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2; 
   337                              0 < b; b \<le> (q - 1) div 2 |] ==>
   338                           (q * a < p * b) = (a \<le> p * b div q)";
   339 proof -;
   340   assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2";
   341   have "q * a < p * b ==> a \<le> p * b div q";
   342   proof -;
   343     assume "q * a < p * b";
   344     then have "q * a \<le> p * b" by auto
   345     then have "(q * a) div q \<le> (p * b) div q";
   346       by (rule zdiv_mono1, insert q_g_2, auto)
   347     then show "a \<le> (p * b) div q";
   348       apply (subgoal_tac "q \<noteq> 0")
   349       apply (frule zdiv_zmult_self2, force)
   350       by (insert q_g_2, auto)
   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       by (insert q_g_2, 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: "[| p \<in> zprime; q \<in> zprime; 2 < p; 2 < q |] ==> 
   370              (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2";
   371 proof-;
   372   assume "p \<in> zprime" and "q \<in> zprime" 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     by (insert prems, 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       by (insert prems, auto simp add: f1_def S_def Q_set_def P_set_def 
   415         image_def)
   416     ultimately show ?thesis by (auto simp add: f1_def)
   417   qed;
   418   also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})";
   419   proof -;
   420     have "{y. y \<in> Q_set & y \<le> (q * j) div p} = 
   421         {y. 0 < y & y \<le> (q * j) div p}";
   422       apply (auto simp add: Q_set_def)
   423       proof -;
   424         fix x;
   425         assume "0 < x" and "x \<le> q * j div p";
   426         with j_fact P_set_def  have "j \<le> (p - 1) div 2"; by auto
   427         with q_g_2; have "q * j \<le> q * ((p - 1) div 2)";
   428           by (auto simp add: mult_le_cancel_left)
   429         with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p";
   430           by (auto simp add: zdiv_mono1)
   431         also from prems have "... \<le> (q - 1) div 2";
   432           apply simp apply (insert aux2) by (simp add: QRTEMP_def)
   433         finally show "x \<le> (q - 1) div 2" by (insert prems, auto)
   434       qed;
   435     then show ?thesis by auto
   436   qed;
   437   also have "... = (q * j) div p";
   438   proof -;
   439     from j_fact P_set_def have "0 \<le> j" by auto
   440     with q_g_2 have "q * 0 \<le> q * j" by (auto simp only: mult_left_mono)
   441     then have "0 \<le> q * j" by auto
   442     then have "0 div p \<le> (q * j) div p";
   443       apply (rule_tac a = 0 in zdiv_mono1)
   444       by (insert p_g_2, auto)
   445     also have "0 div p = 0" by auto
   446     finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
   447   qed;
   448   finally show "int (card (f1 j)) = q * j div p" .;
   449 qed;
   450 
   451 lemma (in QRTEMP) aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q";
   452 proof;
   453   fix j;
   454   assume j_fact: "j \<in> Q_set";
   455   have "int (card (f2 j)) = int (card {y. y \<in> P_set & y \<le> (p * j) div q})";
   456   proof -;
   457     have "finite (f2 j)";
   458     proof -;
   459       have "(f2 j) \<subseteq> S" by (auto simp add: f2_def)
   460       with S_finite show ?thesis by (auto simp add: finite_subset)
   461     qed;
   462     moreover have "inj_on (%(x,y). x) (f2 j)";
   463       by (auto simp add: f2_def inj_on_def)
   464     ultimately have "card ((%(x,y). x) ` (f2 j)) = card  (f2 j)";
   465       by (auto simp add: f2_def card_image)
   466     moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}";
   467       by (insert prems, auto simp add: f2_def S_def Q_set_def 
   468         P_set_def image_def)
   469     ultimately show ?thesis by (auto simp add: f2_def)
   470   qed;
   471   also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})";
   472   proof -;
   473     have "{y. y \<in> P_set & y \<le> (p * j) div q} = 
   474         {y. 0 < y & y \<le> (p * j) div q}";
   475       apply (auto simp add: P_set_def)
   476       proof -;
   477         fix x;
   478         assume "0 < x" and "x \<le> p * j div q";
   479         with j_fact Q_set_def  have "j \<le> (q - 1) div 2"; by auto
   480         with p_g_2; have "p * j \<le> p * ((q - 1) div 2)";
   481           by (auto simp add: mult_le_cancel_left)
   482         with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q";
   483           by (auto simp add: zdiv_mono1)
   484         also from prems have "... \<le> (p - 1) div 2";
   485           by (auto simp add: aux2 QRTEMP_def)
   486         finally show "x \<le> (p - 1) div 2" by (insert prems, auto)
   487       qed;
   488     then show ?thesis by auto
   489   qed;
   490   also have "... = (p * j) div q";
   491   proof -;
   492     from j_fact Q_set_def have "0 \<le> j" by auto
   493     with p_g_2 have "p * 0 \<le> p * j" by (auto simp only: mult_left_mono)
   494     then have "0 \<le> p * j" by auto
   495     then have "0 div q \<le> (p * j) div q";
   496       apply (rule_tac a = 0 in zdiv_mono1)
   497       by (insert q_g_2, auto)
   498     also have "0 div q = 0" by auto
   499     finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
   500   qed;
   501   finally show "int (card (f2 j)) = p * j div q" .;
   502 qed;
   503 
   504 lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set";
   505 proof -;
   506   have "\<forall>x \<in> P_set. finite (f1 x)";
   507   proof;
   508     fix x;
   509     have "f1 x \<subseteq> S" by (auto simp add: f1_def)
   510     with S_finite show "finite (f1 x)" by (auto simp add: finite_subset)
   511   qed;
   512   moreover have "(\<forall>x \<in> P_set. \<forall>y \<in> P_set. x \<noteq> y --> (f1 x) \<inter> (f1 y) = {})";
   513     by (auto simp add: f1_def)
   514   moreover note P_set_finite;
   515   ultimately have "int(card (UNION P_set f1)) = 
   516       setsum (%x. int(card (f1 x))) P_set";
   517     by (rule_tac A = P_set in int_card_indexed_union_disjoint_sets, auto)
   518   moreover have "S1 = UNION P_set f1";
   519     by (auto simp add: f1_def S_def S1_def S2_def P_set_def Q_set_def aux1a)
   520   ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set" 
   521     by auto
   522   also have "... = setsum (%j. q * j div p) P_set";
   523   proof -;
   524     note aux3a
   525     with  P_set_finite show ?thesis by (rule setsum_same_function)
   526   qed;
   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 (rule_tac A = Q_set in int_card_indexed_union_disjoint_sets, auto)
   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   proof -;
   551     note aux3b;
   552     with Q_set_finite show ?thesis by (rule setsum_same_function)
   553   qed;
   554   finally show ?thesis .;
   555 qed;
   556 
   557 lemma (in QRTEMP) S1_carda: "int (card(S1)) = 
   558     setsum (%j. (j * q) div p) P_set";
   559   by (auto simp add: S1_card zmult_ac)
   560 
   561 lemma (in QRTEMP) S2_carda: "int (card(S2)) = 
   562     setsum (%j. (j * p) div q) Q_set";
   563   by (auto simp add: S2_card zmult_ac)
   564 
   565 lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) + 
   566     (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)";
   567 proof -;
   568   have "(setsum (%j. (j * p) div q) Q_set) + 
   569       (setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)";
   570     by (auto simp add: S1_carda S2_carda)
   571   also have "... = int (card S1) + int (card S2)";
   572     by auto
   573   also have "... = ((p - 1) div 2) * ((q - 1) div 2)";
   574     by (auto simp add: card_sum_S1_S2)
   575   finally show ?thesis .;
   576 qed;
   577 
   578 lemma pq_prime_neq: "[| p \<in> zprime; q \<in> zprime; p \<noteq> q |] ==> (~[p = 0] (mod q))";
   579   apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
   580   apply (drule_tac x = q in allE)
   581   apply (drule_tac x = p in allE)
   582 by auto
   583 
   584 lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) = 
   585     (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
   586 proof -;
   587   from prems have "~([p = 0] (mod q))";
   588     by (auto simp add: pq_prime_neq QRTEMP_def)
   589   with prems have a1: "(Legendre p q) = (-1::int) ^ 
   590       nat(setsum (%x. ((x * p) div q)) Q_set)";
   591     apply (rule_tac p = q in  MainQRLemma)
   592     by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
   593   from prems have "~([q = 0] (mod p))";
   594     apply (rule_tac p = q and q = p in pq_prime_neq)
   595     apply (simp add: QRTEMP_def)+;
   596     by arith
   597   with prems have a2: "(Legendre q p) = 
   598       (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
   599     apply (rule_tac p = p in  MainQRLemma)
   600     by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
   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 [THEN sym]);
   614     by (auto simp add: S1_carda [THEN sym] S2_carda [THEN sym])
   615   also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))";
   616     by (auto simp add: pq_sum_prop)
   617   finally show ?thesis .;
   618 qed;
   619 
   620 theorem Quadratic_Reciprocity:
   621      "[| p \<in> zOdd; p \<in> zprime; q \<in> zOdd; q \<in> zprime; 
   622          p \<noteq> q |] 
   623       ==> (Legendre p q) * (Legendre q p) = 
   624           (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
   625   by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [THEN sym] 
   626                      QRTEMP_def)
   627 
   628 end