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