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