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