src/HOL/Number_Theory/Quadratic_Reciprocity.thy
author wenzelm
Tue Jan 17 13:59:10 2017 +0100 (2017-01-17)
changeset 64911 f0e07600de47
parent 64593 50c715579715
child 65413 cb7f9d7d35e6
permissions -rw-r--r--
isabelle update_cartouches -c -t;
eberlm@64282
     1
(* Author: Jaime Mendizabal Roche *)
eberlm@64282
     2
eberlm@64318
     3
theory Quadratic_Reciprocity
eberlm@64282
     4
imports Gauss
eberlm@64282
     5
begin
eberlm@64282
     6
wenzelm@64911
     7
text \<open>The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\<close>
eberlm@64282
     8
eberlm@64282
     9
locale QR =
eberlm@64282
    10
  fixes p :: "nat"
eberlm@64282
    11
  fixes q :: "nat"
eberlm@64282
    12
eberlm@64282
    13
  assumes p_prime: "prime p"
eberlm@64282
    14
  assumes p_ge_2: "2 < p"
eberlm@64282
    15
  assumes q_prime: "prime q"
eberlm@64282
    16
  assumes q_ge_2: "2 < q"
eberlm@64282
    17
  assumes pq_neq: "p \<noteq> q"
eberlm@64282
    18
begin
eberlm@64282
    19
eberlm@64282
    20
lemma odd_p: "odd p" using p_ge_2 p_prime prime_odd_nat by blast
eberlm@64282
    21
eberlm@64282
    22
lemma p_ge_0: "0 < int p"
eberlm@64282
    23
  using p_prime not_prime_0[where 'a = nat] by fastforce+
eberlm@64282
    24
eberlm@64282
    25
lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1" using odd_p by simp
eberlm@64282
    26
eberlm@64282
    27
lemma odd_q: "odd q" using q_ge_2 q_prime prime_odd_nat by blast
eberlm@64282
    28
eberlm@64282
    29
lemma q_ge_0: "0 < int q" using q_prime not_prime_0[where 'a = nat] by fastforce+
eberlm@64282
    30
eberlm@64282
    31
lemma q_eq2: "int q = (2 * ((int q - 1) div 2)) + 1" using odd_q by simp
eberlm@64282
    32
eberlm@64282
    33
lemma pq_eq2: "int p * int q = (2 * ((int p * int q - 1) div 2)) + 1" using odd_p odd_q by simp
eberlm@64282
    34
eberlm@64282
    35
lemma pq_coprime: "coprime p q"
eberlm@64282
    36
  using pq_neq p_prime primes_coprime_nat q_prime by blast
eberlm@64282
    37
eberlm@64282
    38
lemma pq_coprime_int: "coprime (int p) (int q)"
eberlm@64282
    39
  using pq_coprime transfer_int_nat_gcd(1) by presburger
eberlm@64282
    40
eberlm@64282
    41
lemma qp_ineq: "(int p * k \<le> (int p * int q - 1) div 2) = (k \<le> (int q - 1) div 2)"
eberlm@64282
    42
proof -
eberlm@64282
    43
  have "(2 * int p * k \<le> int p * int q - 1) = (2 * k \<le> int q - 1)" using p_ge_0 by auto
eberlm@64282
    44
  thus ?thesis by auto
eberlm@64282
    45
qed
eberlm@64282
    46
eberlm@64282
    47
lemma QRqp: "QR q p" using QR_def QR_axioms by simp
eberlm@64282
    48
eberlm@64282
    49
lemma pq_commute: "int p * int q = int q * int p" by simp
eberlm@64282
    50
eberlm@64282
    51
lemma pq_ge_0: "int p * int q > 0" using p_ge_0 q_ge_0 mult_pos_pos by blast
eberlm@64282
    52
eberlm@64282
    53
definition "r = ((p - 1) div 2)*((q - 1) div 2)"
eberlm@64282
    54
definition "m = card (GAUSS.E p q)"
eberlm@64282
    55
definition "n = card (GAUSS.E q p)"
eberlm@64282
    56
eberlm@64282
    57
abbreviation "Res (k::int) \<equiv> {0 .. k - 1}"
eberlm@64282
    58
abbreviation "Res_ge_0 (k::int) \<equiv> {0 <.. k - 1}"
eberlm@64282
    59
abbreviation "Res_0 (k::int) \<equiv> {0::int}"
eberlm@64282
    60
abbreviation "Res_l (k::int) \<equiv> {0 <.. (k - 1) div 2}"
eberlm@64282
    61
abbreviation "Res_h (k::int) \<equiv> {(k - 1) div 2 <.. k - 1}"
eberlm@64282
    62
eberlm@64282
    63
abbreviation "Sets_pq r0 r1 r2 \<equiv>
eberlm@64282
    64
  {(x::int). x \<in> r0 (int p * int q) \<and> x mod p \<in> r1 (int p) \<and> x mod q \<in> r2 (int q)}"
eberlm@64282
    65
eberlm@64282
    66
definition "A = Sets_pq Res_l Res_l Res_h"
eberlm@64282
    67
definition "B = Sets_pq Res_l Res_h Res_l"
eberlm@64282
    68
definition "C = Sets_pq Res_h Res_h Res_l"
eberlm@64282
    69
definition "D = Sets_pq Res_l Res_h Res_h"
eberlm@64282
    70
definition "E = Sets_pq Res_l Res_0 Res_h"
eberlm@64282
    71
definition "F = Sets_pq Res_l Res_h Res_0"
eberlm@64282
    72
eberlm@64282
    73
definition "a = card A"
eberlm@64282
    74
definition "b = card B"
eberlm@64282
    75
definition "c = card C"
eberlm@64282
    76
definition "d = card D"
eberlm@64282
    77
definition "e = card E"
eberlm@64282
    78
definition "f = card F"
eberlm@64282
    79
eberlm@64282
    80
lemma Gpq: "GAUSS p q" unfolding GAUSS_def
eberlm@64282
    81
  using p_prime pq_neq p_ge_2 q_prime
eberlm@64282
    82
  by (auto simp: cong_altdef_int zdvd_int [symmetric] dest: primes_dvd_imp_eq) 
eberlm@64282
    83
eberlm@64282
    84
lemma Gqp: "GAUSS q p" using QRqp QR.Gpq by simp
eberlm@64282
    85
eberlm@64282
    86
lemma QR_lemma_01: "(\<lambda>x. x mod q) ` E = GAUSS.E q p"
eberlm@64282
    87
proof
eberlm@64282
    88
    {
eberlm@64282
    89
      fix x
eberlm@64282
    90
      assume a1: "x \<in> E"
eberlm@64282
    91
      then obtain k where k: "x = int p * k" unfolding E_def by blast
eberlm@64282
    92
      have "x \<in> Res_l (int p * int q)" using a1 E_def by blast
eberlm@64282
    93
      hence "k \<in> GAUSS.A q" using Gqp GAUSS.A_def k qp_ineq by (simp add: zero_less_mult_iff)
eberlm@64282
    94
      hence "x mod q \<in> GAUSS.E q p"
eberlm@64282
    95
        using GAUSS.C_def[of q p] Gqp k GAUSS.B_def[of q p] a1 GAUSS.E_def[of q p]
eberlm@64282
    96
        unfolding E_def by force
eberlm@64282
    97
      hence "x \<in> E \<longrightarrow> x mod int q \<in> GAUSS.E q p" by auto
eberlm@64282
    98
    }
eberlm@64282
    99
    thus "(\<lambda>x. x mod int q) ` E \<subseteq> GAUSS.E q p" by auto
eberlm@64282
   100
next
eberlm@64282
   101
  show "GAUSS.E q p \<subseteq> (\<lambda>x. x mod q) ` E"
eberlm@64282
   102
  proof
eberlm@64282
   103
    fix x
eberlm@64282
   104
    assume a1: "x \<in> GAUSS.E q p"
eberlm@64282
   105
    then obtain ka where ka: "ka \<in> GAUSS.A q" "x = (ka * p) mod q"
eberlm@64282
   106
      using Gqp GAUSS.B_def GAUSS.C_def GAUSS.E_def by auto
eberlm@64282
   107
    hence "ka * p \<in> Res_l (int p * int q)"
eberlm@64282
   108
      using GAUSS.A_def Gqp p_ge_0 qp_ineq by (simp add: Groups.mult_ac(2))
eberlm@64282
   109
    thus "x \<in> (\<lambda>x. x mod q) ` E" unfolding E_def using ka a1 Gqp GAUSS.E_def q_ge_0 by force
eberlm@64282
   110
  qed
eberlm@64282
   111
qed
eberlm@64282
   112
eberlm@64282
   113
lemma QR_lemma_02: "e= n"
eberlm@64282
   114
proof -
eberlm@64282
   115
  {
eberlm@64282
   116
    fix x y
eberlm@64282
   117
    assume a: "x \<in> E" "y \<in> E" "x mod q = y mod q"
eberlm@64282
   118
    obtain p_inv where p_inv: "[int p * p_inv = 1] (mod int q)"
eberlm@64282
   119
      using pq_coprime_int cong_solve_coprime_int by blast
eberlm@64282
   120
    obtain kx ky where k: "x = int p * kx" "y = int p * ky" using a E_def dvd_def[of p x] by blast
eberlm@64282
   121
    hence "0 < x" "int p * kx \<le> (int p * int q - 1) div 2"
eberlm@64282
   122
        "0 < y" "int p * ky \<le> (int p * int q - 1) div 2"
eberlm@64282
   123
      using E_def a greaterThanAtMost_iff mem_Collect_eq by blast+
eberlm@64282
   124
    hence "0 \<le> kx" "kx < q" "0 \<le> ky" "ky < q" using qp_ineq k by (simp add: zero_less_mult_iff)+
eberlm@64282
   125
    moreover have "(p_inv * (p * kx)) mod q = (p_inv * (p * ky)) mod q"
eberlm@64282
   126
      using a(3) mod_mult_cong k by blast
eberlm@64282
   127
    hence "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q" by (simp add:algebra_simps)
eberlm@64282
   128
    hence "kx mod q = ky mod q"
eberlm@64282
   129
      using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] cong_int_def by auto
eberlm@64282
   130
    hence "[kx = ky] (mod q)" using cong_int_def by blast
eberlm@64282
   131
    ultimately have "x = y" using cong_less_imp_eq_int k by blast
eberlm@64282
   132
  }
eberlm@64282
   133
  hence "inj_on (\<lambda>x. x mod q) E" unfolding inj_on_def by auto
eberlm@64282
   134
  thus ?thesis using QR_lemma_01 card_image e_def n_def by fastforce
eberlm@64282
   135
qed
eberlm@64282
   136
eberlm@64282
   137
lemma QR_lemma_03: "f = m"
eberlm@64282
   138
proof -
eberlm@64282
   139
  have "F = QR.E q p" unfolding F_def pq_commute using QRqp QR.E_def[of q p] by fastforce
eberlm@64282
   140
  hence "f = QR.e q p" unfolding f_def using QRqp QR.e_def[of q p] by presburger
eberlm@64282
   141
  thus ?thesis using QRqp QR.QR_lemma_02 m_def QRqp QR.n_def by presburger
eberlm@64282
   142
qed
eberlm@64282
   143
eberlm@64282
   144
definition f_1 :: "int \<Rightarrow> int \<times> int" where
eberlm@64282
   145
  "f_1 x = ((x mod p), (x mod q))"
eberlm@64282
   146
eberlm@64282
   147
definition P_1 :: "int \<times> int \<Rightarrow> int \<Rightarrow> bool" where
eberlm@64282
   148
  "P_1 res x \<longleftrightarrow> x mod p = fst res & x mod q = snd res & x \<in> Res (int p * int q)"
eberlm@64282
   149
eberlm@64282
   150
definition g_1 :: "int \<times> int \<Rightarrow> int" where
eberlm@64282
   151
  "g_1 res = (THE x. P_1 res x)"
eberlm@64282
   152
eberlm@64282
   153
lemma P_1_lemma: assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
eberlm@64282
   154
  shows "\<exists>! x. P_1 res x"
eberlm@64282
   155
proof -
eberlm@64282
   156
  obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q"
eberlm@64282
   157
    using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce
eberlm@64282
   158
  have h1: "[y = fst res] (mod p)" "[y = snd res] (mod q)"
eberlm@64282
   159
    using yk(1) assms(1) cong_iff_lin_int[of "fst res"] cong_sym_int apply simp
eberlm@64282
   160
    using yk(2) assms(3) cong_iff_lin_int[of "snd res"] cong_sym_int by simp
eberlm@64282
   161
  have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res"
eberlm@64282
   162
    using h1(1) mod_mod_cancel[of "int p"] assms(1) assms(2) cong_int_def apply simp
eberlm@64282
   163
    using h1(2) mod_mod_cancel[of "int q"] assms(3) assms(4) cong_int_def by simp
eberlm@64282
   164
  then obtain x where "P_1 res x" unfolding P_1_def
eberlm@64282
   165
    using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce
eberlm@64282
   166
  moreover {
eberlm@64282
   167
    fix a b
eberlm@64282
   168
    assume a: "P_1 res a" "P_1 res b"
eberlm@64282
   169
    hence "int p * int q dvd a - b"
haftmann@64593
   170
      using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int mod_eq_dvd_iff [of a _ b]
eberlm@64282
   171
      unfolding P_1_def by force
eberlm@64282
   172
    hence "a = b" using dvd_imp_le_int[of "a - b"] a unfolding P_1_def by fastforce
eberlm@64282
   173
  }
eberlm@64282
   174
  ultimately show ?thesis by auto
eberlm@64282
   175
qed
eberlm@64282
   176
eberlm@64282
   177
lemma g_1_lemma: assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q"
eberlm@64282
   178
  shows "P_1 res (g_1 res)" using assms P_1_lemma theI'[of "P_1 res"] g_1_def by presburger
eberlm@64282
   179
eberlm@64282
   180
definition "BuC = Sets_pq Res_ge_0 Res_h Res_l"
eberlm@64282
   181
eberlm@64282
   182
lemma QR_lemma_04: "card BuC = card ((Res_h p) \<times> (Res_l q))"
eberlm@64282
   183
  using card_bij_eq[of f_1 "BuC" "(Res_h p) \<times> (Res_l q)" g_1]
eberlm@64282
   184
proof
eberlm@64282
   185
  {
eberlm@64282
   186
    fix x y
eberlm@64282
   187
    assume a: "x \<in> BuC" "y \<in> BuC" "f_1 x = f_1 y"
eberlm@64282
   188
    hence "int p * int q dvd x - y"
eberlm@64282
   189
      using f_1_def pq_coprime_int divides_mult[of "int p" "x - y" "int q"] 
haftmann@64593
   190
            mod_eq_dvd_iff[of x _ y] by auto
eberlm@64282
   191
    hence "x = y"
eberlm@64282
   192
      using dvd_imp_le_int[of "x - y" "int p * int q"] a unfolding BuC_def by force
eberlm@64282
   193
  }
eberlm@64282
   194
  thus "inj_on f_1 BuC" unfolding inj_on_def by auto
eberlm@64282
   195
next
eberlm@64282
   196
  {
eberlm@64282
   197
    fix x y
eberlm@64282
   198
    assume a: "x \<in> (Res_h p) \<times> (Res_l q)" "y \<in> (Res_h p) \<times> (Res_l q)" "g_1 x = g_1 y"
eberlm@64282
   199
    hence "0 \<le> fst x" "fst x < p" "0 \<le> snd x" "snd x < q"
eberlm@64282
   200
        "0 \<le> fst y" "fst y < p" "0 \<le> snd y" "snd y < q"
eberlm@64282
   201
      using mem_Sigma_iff prod.collapse by fastforce+
eberlm@64282
   202
    hence "x = y" using g_1_lemma[of x] g_1_lemma[of y] a P_1_def by fastforce
eberlm@64282
   203
  }
eberlm@64282
   204
  thus "inj_on g_1 ((Res_h p) \<times> (Res_l q))" unfolding inj_on_def by auto
eberlm@64282
   205
next
eberlm@64282
   206
  show "g_1 ` ((Res_h p) \<times> (Res_l q)) \<subseteq> BuC"
eberlm@64282
   207
  proof
eberlm@64282
   208
    fix y
eberlm@64282
   209
    assume "y \<in> g_1 ` ((Res_h p) \<times> (Res_l q))"
eberlm@64282
   210
    then obtain x where x: "y = g_1 x" "x \<in> ((Res_h p) \<times> (Res_l q))" by blast
eberlm@64282
   211
    hence "P_1 x y" using g_1_lemma by fastforce
eberlm@64282
   212
    thus "y \<in> BuC" unfolding P_1_def BuC_def mem_Collect_eq using x SigmaE prod.sel by fastforce
eberlm@64282
   213
  qed
eberlm@64282
   214
qed (auto simp: BuC_def finite_subset f_1_def)
eberlm@64282
   215
eberlm@64282
   216
lemma QR_lemma_05: "card ((Res_h p) \<times> (Res_l q)) = r"
eberlm@64282
   217
proof -
eberlm@64282
   218
  have "card (Res_l q) = (q - 1) div 2" "card (Res_h p) = (p - 1) div 2" using p_eq2 by force+
eberlm@64282
   219
  thus ?thesis unfolding r_def using card_cartesian_product[of "Res_h p" "Res_l q"] by presburger
eberlm@64282
   220
qed
eberlm@64282
   221
eberlm@64282
   222
lemma QR_lemma_06: "b + c = r"
eberlm@64282
   223
proof -
eberlm@64282
   224
  have "B \<inter> C = {}" "finite B" "finite C" "B \<union> C = BuC" unfolding B_def C_def BuC_def by fastforce+
eberlm@64282
   225
  thus ?thesis
eberlm@64282
   226
    unfolding b_def c_def using card_empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce
eberlm@64282
   227
qed
eberlm@64282
   228
eberlm@64282
   229
definition f_2:: "int \<Rightarrow> int" where
eberlm@64282
   230
  "f_2 x = (int p * int q) - x"
eberlm@64282
   231
eberlm@64282
   232
lemma f_2_lemma_1: "\<And>x. f_2 (f_2 x) = x" unfolding f_2_def by simp
eberlm@64282
   233
eberlm@64282
   234
lemma f_2_lemma_2: "[f_2 x = int p - x] (mod p)" unfolding f_2_def using cong_altdef_int by simp
eberlm@64282
   235
eberlm@64282
   236
lemma f_2_lemma_3: "f_2 x \<in> S \<Longrightarrow> x \<in> f_2 ` S"
eberlm@64282
   237
  using f_2_lemma_1[of x] image_eqI[of x f_2 "f_2 x" S] by presburger
eberlm@64282
   238
eberlm@64282
   239
lemma QR_lemma_07: "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)"
eberlm@64282
   240
    "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)"
eberlm@64282
   241
proof -
eberlm@64282
   242
  have h1: "f_2 ` Res_l (int p * int q) \<subseteq> Res_h (int p * int q)" using f_2_def by force
eberlm@64282
   243
  have h2: "f_2 ` Res_h (int p * int q) \<subseteq> Res_l (int p * int q)" using f_2_def pq_eq2 by fastforce
eberlm@64282
   244
  have h3: "Res_h (int p * int q) \<subseteq> f_2 ` Res_l (int p * int q)" using h2 f_2_lemma_3 by blast
eberlm@64282
   245
  have h4: "Res_l (int p * int q) \<subseteq> f_2 ` Res_h (int p * int q)" using h1 f_2_lemma_3 by blast
eberlm@64282
   246
  show "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)" using h1 h3 by blast
eberlm@64282
   247
  show "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)" using h2 h4 by blast
eberlm@64282
   248
qed
eberlm@64282
   249
eberlm@64282
   250
lemma QR_lemma_08: "(f_2 x mod p \<in> Res_l p) = (x mod p \<in> Res_h p)"
eberlm@64282
   251
    "(f_2 x mod p \<in> Res_h p) = (x mod p \<in> Res_l p)"
eberlm@64282
   252
  using f_2_lemma_2[of x] cong_int_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p]
eberlm@64282
   253
  zmod_zminus1_eq_if[of x p] p_eq2 by auto
eberlm@64282
   254
eberlm@64282
   255
lemma QR_lemma_09: "(f_2 x mod q \<in> Res_l q) = (x mod q \<in> Res_h q)"
eberlm@64282
   256
    "(f_2 x mod q \<in> Res_h q) = (x mod q \<in> Res_l q)"
eberlm@64282
   257
  using QRqp QR.QR_lemma_08 f_2_def QR.f_2_def pq_commute by auto+
eberlm@64282
   258
eberlm@64282
   259
lemma QR_lemma_10: "a = c" unfolding a_def c_def apply (rule card_bij_eq[of f_2 A C f_2])
eberlm@64282
   260
  unfolding A_def C_def
eberlm@64282
   261
  using QR_lemma_07 QR_lemma_08 QR_lemma_09 apply ((simp add: inj_on_def f_2_def),blast)+
eberlm@64282
   262
  by fastforce+
eberlm@64282
   263
eberlm@64282
   264
definition "BuD = Sets_pq Res_l Res_h Res_ge_0"
eberlm@64282
   265
definition "BuDuF = Sets_pq Res_l Res_h Res"
eberlm@64282
   266
eberlm@64282
   267
definition f_3 :: "int \<Rightarrow> int \<times> int" where
eberlm@64282
   268
  "f_3 x = (x mod p, x div p + 1)"
eberlm@64282
   269
eberlm@64282
   270
definition g_3 :: "int \<times> int \<Rightarrow> int" where
eberlm@64282
   271
  "g_3 x = fst x + (snd x - 1) * p"
eberlm@64282
   272
eberlm@64282
   273
lemma QR_lemma_11: "card BuDuF = card ((Res_h p) \<times> (Res_l q))"
eberlm@64282
   274
  using card_bij_eq[of f_3 BuDuF "(Res_h p) \<times> (Res_l q)" g_3]
eberlm@64282
   275
proof
eberlm@64282
   276
  show "f_3 ` BuDuF \<subseteq> (Res_h p) \<times> (Res_l q)"
eberlm@64282
   277
  proof
eberlm@64282
   278
    fix y
eberlm@64282
   279
    assume "y \<in> f_3 ` BuDuF"
eberlm@64282
   280
    then obtain x where x: "y = f_3 x" "x \<in> BuDuF" by blast
eberlm@64282
   281
    hence "x \<le> int p * (int q - 1) div 2 + (int p - 1) div 2"
eberlm@64282
   282
      unfolding BuDuF_def using p_eq2 int_distrib(4) by auto
eberlm@64282
   283
    moreover have "(int p - 1) div 2 \<le> - 1 + x mod p" using x BuDuF_def by auto
eberlm@64282
   284
    moreover have "int p * (int q - 1) div 2 = int p * ((int q - 1) div 2)"
eberlm@64282
   285
      using zdiv_zmult1_eq odd_q by auto
eberlm@64282
   286
    hence "p * (int q - 1) div 2 = p * ((int q + 1) div 2 - 1)" by fastforce
eberlm@64282
   287
    ultimately have "x \<le> p * ((int q + 1) div 2 - 1) - 1 + x mod p" by linarith
eberlm@64282
   288
    hence "x div p < (int q + 1) div 2 - 1"
eberlm@64282
   289
      using mult.commute[of "int p" "x div p"] p_ge_0 div_mult_mod_eq[of x p]
eberlm@64282
   290
        mult_less_cancel_left_pos[of p "x div p" "(int q + 1) div 2 - 1"] by linarith
eberlm@64282
   291
    moreover have "0 < x div p + 1"
eberlm@64282
   292
      using pos_imp_zdiv_neg_iff[of p x] p_ge_0 x mem_Collect_eq BuDuF_def by auto
eberlm@64282
   293
    ultimately show "y \<in> (Res_h p) \<times> (Res_l q)" using x BuDuF_def f_3_def by auto
eberlm@64282
   294
  qed
eberlm@64282
   295
next
eberlm@64282
   296
  have h1: "\<And>x. x \<in> ((Res_h p) \<times> (Res_l q)) \<Longrightarrow> f_3 (g_3 x) = x"
eberlm@64282
   297
  proof -
eberlm@64282
   298
    fix x
eberlm@64282
   299
    assume a: "x \<in> ((Res_h p) \<times> (Res_l q))"
eberlm@64282
   300
    moreover have h: "(fst x + (snd x - 1) * int p) mod int p = fst x" using a by force
eberlm@64282
   301
    ultimately have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x"
eberlm@64282
   302
      by (auto simp: semiring_numeral_div_class.div_less)
eberlm@64282
   303
    with h show "f_3 (g_3 x) = x" unfolding f_3_def g_3_def by simp
eberlm@64282
   304
  qed
eberlm@64282
   305
  show "inj_on g_3 ((Res_h p) \<times> (Res_l q))" apply (rule inj_onI[of "(Res_h p) \<times> (Res_l q)" g_3])
eberlm@64282
   306
  proof -
eberlm@64282
   307
    fix x y
eberlm@64282
   308
    assume "x \<in> ((Res_h p) \<times> (Res_l q))" "y \<in> ((Res_h p) \<times> (Res_l q))" "g_3 x = g_3 y"
eberlm@64282
   309
    thus "x = y" using h1[of x] h1[of y] by presburger
eberlm@64282
   310
  qed
eberlm@64282
   311
next
eberlm@64282
   312
  show "g_3 ` ((Res_h p) \<times> (Res_l q)) \<subseteq> BuDuF"
eberlm@64282
   313
  proof
eberlm@64282
   314
    fix y
eberlm@64282
   315
    assume "y \<in> g_3 ` ((Res_h p) \<times> (Res_l q))"
eberlm@64282
   316
    then obtain x where x: "y = g_3 x" "x \<in> (Res_h p) \<times> (Res_l q)" by blast
eberlm@64282
   317
    hence "snd x \<le> (int q - 1) div 2" by force
eberlm@64282
   318
    moreover have "int p * ((int q - 1) div 2) = (int p * int q - int p) div 2"
eberlm@64282
   319
      using int_distrib(4) zdiv_zmult1_eq[of "int p" "int q - 1" 2] odd_q by fastforce
eberlm@64282
   320
    ultimately have "(snd x) * int p \<le> (int q * int p - int p) div 2"
eberlm@64282
   321
      using mult_right_mono[of "snd x" "(int q - 1) div 2" p] mult.commute[of "(int q - 1) div 2" p]
eberlm@64282
   322
        pq_commute by presburger
eberlm@64282
   323
    hence "(snd x - 1) * int p \<le> (int q * int p - 1) div 2 - int p"
eberlm@64282
   324
      using p_ge_0 int_distrib(3) by auto
eberlm@64282
   325
    moreover have "fst x \<le> int p - 1" using x by force
eberlm@64282
   326
    ultimately have "fst x + (snd x - 1) * int p \<le> (int p * int q - 1) div 2"
eberlm@64282
   327
      using pq_commute by linarith
eberlm@64282
   328
    moreover have "0 < fst x" "0 \<le> (snd x - 1) * p" using x(2) by fastforce+
eberlm@64282
   329
    ultimately show "y \<in> BuDuF" unfolding BuDuF_def using q_ge_0 x g_3_def x(1) by auto
eberlm@64282
   330
  qed
eberlm@64282
   331
next
eberlm@64282
   332
  show "finite BuDuF" unfolding BuDuF_def by fastforce
eberlm@64282
   333
qed (simp add: inj_on_inverseI[of BuDuF g_3] f_3_def g_3_def QR_lemma_05)+
eberlm@64282
   334
eberlm@64282
   335
lemma QR_lemma_12: "b + d + m = r"
eberlm@64282
   336
proof -
eberlm@64282
   337
  have "B \<inter> D = {}" "finite B" "finite D" "B \<union> D = BuD" unfolding B_def D_def BuD_def by fastforce+
eberlm@64282
   338
  hence "b + d = card BuD" unfolding b_def d_def using card_Un_Int by fastforce
eberlm@64282
   339
  moreover have "BuD \<inter> F = {}" "finite BuD" "finite F" unfolding BuD_def F_def by fastforce+
eberlm@64282
   340
  moreover have "BuD \<union> F = BuDuF" unfolding BuD_def F_def BuDuF_def
eberlm@64282
   341
    using q_ge_0 ivl_disj_un_singleton(5)[of 0 "int q - 1"] by auto
eberlm@64282
   342
  ultimately show ?thesis using QR_lemma_03 QR_lemma_05 QR_lemma_11 card_Un_disjoint[of BuD F]
eberlm@64282
   343
    unfolding b_def d_def f_def by presburger
eberlm@64282
   344
qed
eberlm@64282
   345
eberlm@64282
   346
lemma QR_lemma_13: "a + d + n = r"
eberlm@64282
   347
proof -
eberlm@64282
   348
  have "A = QR.B q p" unfolding A_def pq_commute using QRqp QR.B_def[of q p] by blast
eberlm@64282
   349
  hence "a = QR.b q p" using a_def QRqp QR.b_def[of q p] by presburger
eberlm@64282
   350
  moreover have "D = QR.D q p" unfolding D_def pq_commute using QRqp QR.D_def[of q p] by blast
eberlm@64282
   351
    hence "d = QR.d q p" using d_def  QRqp QR.d_def[of q p] by presburger
eberlm@64282
   352
  moreover have "n = QR.m q p" using n_def QRqp QR.m_def[of q p] by presburger
eberlm@64282
   353
  moreover have "r = QR.r q p" unfolding r_def using QRqp QR.r_def[of q p] by auto
eberlm@64282
   354
  ultimately show ?thesis using QRqp QR.QR_lemma_12 by presburger
eberlm@64282
   355
qed
eberlm@64282
   356
eberlm@64282
   357
lemma QR_lemma_14: "(-1::int) ^ (m + n) = (-1) ^ r"
eberlm@64282
   358
proof -
eberlm@64282
   359
  have "m + n + 2 * d = r" using QR_lemma_06 QR_lemma_10 QR_lemma_12 QR_lemma_13 by auto
eberlm@64282
   360
  thus ?thesis using power_add[of "-1::int" "m + n" "2 * d"] by fastforce
eberlm@64282
   361
qed
eberlm@64282
   362
eberlm@64282
   363
lemma Quadratic_Reciprocity:
eberlm@64282
   364
    "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))"
eberlm@64282
   365
  using Gpq Gqp GAUSS.gauss_lemma power_add[of "-1::int" m n] QR_lemma_14
eberlm@64282
   366
  unfolding r_def m_def n_def by auto
eberlm@64282
   367
eberlm@64282
   368
end
eberlm@64282
   369
eberlm@64282
   370
theorem Quadratic_Reciprocity: assumes "prime p" "2 < p" "prime q" "2 < q" "p \<noteq> q"
eberlm@64282
   371
  shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))"
eberlm@64282
   372
  using QR.Quadratic_Reciprocity QR_def assms by blast
eberlm@64282
   373
eberlm@64282
   374
theorem Quadratic_Reciprocity_int: assumes "prime (nat p)" "2 < p" "prime (nat q)" "2 < q" "p \<noteq> q"
eberlm@64282
   375
  shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ (nat ((p - 1) div 2 * ((q - 1) div 2)))"
eberlm@64282
   376
proof -
eberlm@64282
   377
  have "0 \<le> (p - 1) div 2" using assms by simp
eberlm@64282
   378
  moreover have "(nat p - 1) div 2 = nat ((p - 1) div 2)" "(nat q - 1) div 2 = nat ((q - 1) div 2)"
eberlm@64282
   379
    by fastforce+
eberlm@64282
   380
  ultimately have "(nat p - 1) div 2 * ((nat q - 1) div 2) = nat ((p - 1) div 2 * ((q - 1) div 2))"
eberlm@64282
   381
    using nat_mult_distrib by presburger
eberlm@64282
   382
  moreover have "2 < nat p" "2 < nat q" "nat p \<noteq> nat q" "int (nat p) = p" "int (nat q) = q"
eberlm@64282
   383
    using assms by linarith+
eberlm@64282
   384
  ultimately show ?thesis using Quadratic_Reciprocity[of "nat p" "nat q"] assms by presburger
eberlm@64282
   385
qed
eberlm@64282
   386
eberlm@64318
   387
end