75 definition "c = card C" |
89 definition "c = card C" |
76 definition "d = card D" |
90 definition "d = card D" |
77 definition "e = card E" |
91 definition "e = card E" |
78 definition "f = card F" |
92 definition "f = card F" |
79 |
93 |
80 lemma Gpq: "GAUSS p q" unfolding GAUSS_def |
94 lemma Gpq: "GAUSS p q" |
81 using p_prime pq_neq p_ge_2 q_prime |
95 using p_prime pq_neq p_ge_2 q_prime |
82 by (auto simp: cong_altdef_int zdvd_int [symmetric] dest: primes_dvd_imp_eq) |
96 by (auto simp: GAUSS_def cong_altdef_int zdvd_int [symmetric] dest: primes_dvd_imp_eq) |
83 |
97 |
84 lemma Gqp: "GAUSS q p" using QRqp QR.Gpq by simp |
98 lemma Gqp: "GAUSS q p" |
|
99 by (simp add: QRqp QR.Gpq) |
85 |
100 |
86 lemma QR_lemma_01: "(\<lambda>x. x mod q) ` E = GAUSS.E q p" |
101 lemma QR_lemma_01: "(\<lambda>x. x mod q) ` E = GAUSS.E q p" |
87 proof |
102 proof |
88 { |
103 have "x \<in> E \<longrightarrow> x mod int q \<in> GAUSS.E q p" if "x \<in> E" for x |
89 fix x |
104 proof - |
90 assume a1: "x \<in> E" |
105 from that obtain k where k: "x = int p * k" |
91 then obtain k where k: "x = int p * k" unfolding E_def by blast |
106 unfolding E_def by blast |
92 have "x \<in> Res_l (int p * int q)" using a1 E_def by blast |
107 from that E_def have "x \<in> Res_l (int p * int q)" |
93 hence "k \<in> GAUSS.A q" using Gqp GAUSS.A_def k qp_ineq by (simp add: zero_less_mult_iff) |
108 by blast |
94 hence "x mod q \<in> GAUSS.E q p" |
109 then have "k \<in> GAUSS.A q" |
95 using GAUSS.C_def[of q p] Gqp k GAUSS.B_def[of q p] a1 GAUSS.E_def[of q p] |
110 using Gqp GAUSS.A_def k qp_ineq by (simp add: zero_less_mult_iff) |
96 unfolding E_def by force |
111 then have "x mod q \<in> GAUSS.E q p" |
97 hence "x \<in> E \<longrightarrow> x mod int q \<in> GAUSS.E q p" by auto |
112 using GAUSS.C_def[of q p] Gqp k GAUSS.B_def[of q p] that GAUSS.E_def[of q p] |
98 } |
113 by (force simp: E_def) |
99 thus "(\<lambda>x. x mod int q) ` E \<subseteq> GAUSS.E q p" by auto |
114 then show ?thesis by auto |
100 next |
115 qed |
|
116 then show "(\<lambda>x. x mod int q) ` E \<subseteq> GAUSS.E q p" |
|
117 by auto |
101 show "GAUSS.E q p \<subseteq> (\<lambda>x. x mod q) ` E" |
118 show "GAUSS.E q p \<subseteq> (\<lambda>x. x mod q) ` E" |
102 proof |
119 proof |
103 fix x |
120 fix x |
104 assume a1: "x \<in> GAUSS.E q p" |
121 assume x: "x \<in> GAUSS.E q p" |
105 then obtain ka where ka: "ka \<in> GAUSS.A q" "x = (ka * p) mod q" |
122 then obtain ka where ka: "ka \<in> GAUSS.A q" "x = (ka * p) mod q" |
106 using Gqp GAUSS.B_def GAUSS.C_def GAUSS.E_def by auto |
123 by (auto simp: Gqp GAUSS.B_def GAUSS.C_def GAUSS.E_def) |
107 hence "ka * p \<in> Res_l (int p * int q)" |
124 then have "ka * p \<in> Res_l (int p * int q)" |
108 using GAUSS.A_def Gqp p_ge_0 qp_ineq by (simp add: Groups.mult_ac(2)) |
125 using Gqp p_ge_0 qp_ineq by (simp add: GAUSS.A_def Groups.mult_ac(2)) |
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 |
126 then show "x \<in> (\<lambda>x. x mod q) ` E" |
110 qed |
127 using ka x Gqp q_ge_0 by (force simp: E_def GAUSS.E_def) |
111 qed |
128 qed |
112 |
129 qed |
113 lemma QR_lemma_02: "e= n" |
130 |
114 proof - |
131 lemma QR_lemma_02: "e = n" |
115 { |
132 proof - |
116 fix x y |
133 have "x = y" if x: "x \<in> E" and y: "y \<in> E" and mod: "x mod q = y mod q" for x y |
117 assume a: "x \<in> E" "y \<in> E" "x mod q = y mod q" |
134 proof - |
118 obtain p_inv where p_inv: "[int p * p_inv = 1] (mod int q)" |
135 obtain p_inv where p_inv: "[int p * p_inv = 1] (mod int q)" |
119 using pq_coprime_int cong_solve_coprime_int by blast |
136 using pq_coprime_int cong_solve_coprime_int by blast |
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 |
137 from x y E_def obtain kx ky where k: "x = int p * kx" "y = int p * ky" |
121 hence "0 < x" "int p * kx \<le> (int p * int q - 1) div 2" |
138 using dvd_def[of p x] by blast |
|
139 with x y E_def have "0 < x" "int p * kx \<le> (int p * int q - 1) div 2" |
122 "0 < y" "int p * ky \<le> (int p * int q - 1) div 2" |
140 "0 < y" "int p * ky \<le> (int p * int q - 1) div 2" |
123 using E_def a greaterThanAtMost_iff mem_Collect_eq by blast+ |
141 using greaterThanAtMost_iff mem_Collect_eq by blast+ |
124 hence "0 \<le> kx" "kx < q" "0 \<le> ky" "ky < q" using qp_ineq k by (simp add: zero_less_mult_iff)+ |
142 with k have "0 \<le> kx" "kx < q" "0 \<le> ky" "ky < q" |
125 moreover have "(p_inv * (p * kx)) mod q = (p_inv * (p * ky)) mod q" |
143 using qp_ineq by (simp_all add: zero_less_mult_iff) |
126 using a(3) mod_mult_cong k by blast |
144 moreover from mod k have "(p_inv * (p * kx)) mod q = (p_inv * (p * ky)) mod q" |
127 hence "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q" by (simp add:algebra_simps) |
145 using mod_mult_cong by blast |
128 hence "kx mod q = ky mod q" |
146 then have "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q" |
129 using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] cong_int_def by auto |
147 by (simp add: algebra_simps) |
130 hence "[kx = ky] (mod q)" using cong_int_def by blast |
148 then have "kx mod q = ky mod q" |
131 ultimately have "x = y" using cong_less_imp_eq_int k by blast |
149 using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] by (auto simp: cong_int_def) |
132 } |
150 then have "[kx = ky] (mod q)" |
133 hence "inj_on (\<lambda>x. x mod q) E" unfolding inj_on_def by auto |
151 unfolding cong_int_def by blast |
134 thus ?thesis using QR_lemma_01 card_image e_def n_def by fastforce |
152 ultimately show ?thesis |
|
153 using cong_less_imp_eq_int k by blast |
|
154 qed |
|
155 then have "inj_on (\<lambda>x. x mod q) E" |
|
156 by (auto simp: inj_on_def) |
|
157 then show ?thesis |
|
158 using QR_lemma_01 card_image e_def n_def by fastforce |
135 qed |
159 qed |
136 |
160 |
137 lemma QR_lemma_03: "f = m" |
161 lemma QR_lemma_03: "f = m" |
138 proof - |
162 proof - |
139 have "F = QR.E q p" unfolding F_def pq_commute using QRqp QR.E_def[of q p] by fastforce |
163 have "F = QR.E q p" |
140 hence "f = QR.e q p" unfolding f_def using QRqp QR.e_def[of q p] by presburger |
164 unfolding F_def pq_commute using QRqp QR.E_def[of q p] by fastforce |
141 thus ?thesis using QRqp QR.QR_lemma_02 m_def QRqp QR.n_def by presburger |
165 then have "f = QR.e q p" |
142 qed |
166 unfolding f_def using QRqp QR.e_def[of q p] by presburger |
143 |
167 then show ?thesis |
144 definition f_1 :: "int \<Rightarrow> int \<times> int" where |
168 using QRqp QR.QR_lemma_02 m_def QRqp QR.n_def by presburger |
145 "f_1 x = ((x mod p), (x mod q))" |
169 qed |
146 |
170 |
147 definition P_1 :: "int \<times> int \<Rightarrow> int \<Rightarrow> bool" where |
171 definition f_1 :: "int \<Rightarrow> int \<times> int" |
148 "P_1 res x \<longleftrightarrow> x mod p = fst res & x mod q = snd res & x \<in> Res (int p * int q)" |
172 where "f_1 x = ((x mod p), (x mod q))" |
149 |
173 |
150 definition g_1 :: "int \<times> int \<Rightarrow> int" where |
174 definition P_1 :: "int \<times> int \<Rightarrow> int \<Rightarrow> bool" |
151 "g_1 res = (THE x. P_1 res x)" |
175 where "P_1 res x \<longleftrightarrow> x mod p = fst res \<and> x mod q = snd res \<and> x \<in> Res (int p * int q)" |
152 |
176 |
153 lemma P_1_lemma: assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q" |
177 definition g_1 :: "int \<times> int \<Rightarrow> int" |
154 shows "\<exists>! x. P_1 res x" |
178 where "g_1 res = (THE x. P_1 res x)" |
|
179 |
|
180 lemma P_1_lemma: |
|
181 assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q" |
|
182 shows "\<exists>!x. P_1 res x" |
155 proof - |
183 proof - |
156 obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q" |
184 obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q" |
157 using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce |
185 using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce |
158 have h1: "[y = fst res] (mod p)" "[y = snd res] (mod q)" |
186 have *: "[y = fst res] (mod p)" "[y = snd res] (mod q)" |
159 using yk(1) assms(1) cong_iff_lin_int[of "fst res"] cong_sym_int apply simp |
187 using yk(1) assms(1) cong_iff_lin_int[of "fst res"] cong_sym_int apply simp |
160 using yk(2) assms(3) cong_iff_lin_int[of "snd res"] cong_sym_int by simp |
188 using yk(2) assms(3) cong_iff_lin_int[of "snd res"] cong_sym_int by simp |
161 have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res" |
189 have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res" |
162 using h1(1) mod_mod_cancel[of "int p"] assms(1) assms(2) cong_int_def apply simp |
190 using *(1) mod_mod_cancel[of "int p"] assms(1) assms(2) cong_int_def apply simp |
163 using h1(2) mod_mod_cancel[of "int q"] assms(3) assms(4) cong_int_def by simp |
191 using *(2) mod_mod_cancel[of "int q"] assms(3) assms(4) cong_int_def by simp |
164 then obtain x where "P_1 res x" unfolding P_1_def |
192 then obtain x where "P_1 res x" |
|
193 unfolding P_1_def |
165 using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce |
194 using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce |
166 moreover { |
195 moreover have "a = b" if "P_1 res a" "P_1 res b" for a b |
167 fix a b |
196 proof - |
168 assume a: "P_1 res a" "P_1 res b" |
197 from that have "int p * int q dvd a - b" |
169 hence "int p * int q dvd a - b" |
|
170 using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int mod_eq_dvd_iff [of a _ b] |
198 using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int mod_eq_dvd_iff [of a _ b] |
171 unfolding P_1_def by force |
199 unfolding P_1_def by force |
172 hence "a = b" using dvd_imp_le_int[of "a - b"] a unfolding P_1_def by fastforce |
200 with that show ?thesis |
173 } |
201 using dvd_imp_le_int[of "a - b"] unfolding P_1_def by fastforce |
|
202 qed |
174 ultimately show ?thesis by auto |
203 ultimately show ?thesis by auto |
175 qed |
204 qed |
176 |
205 |
177 lemma g_1_lemma: assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q" |
206 lemma g_1_lemma: |
178 shows "P_1 res (g_1 res)" using assms P_1_lemma theI'[of "P_1 res"] g_1_def by presburger |
207 assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q" |
|
208 shows "P_1 res (g_1 res)" |
|
209 using assms P_1_lemma theI'[of "P_1 res"] g_1_def by presburger |
179 |
210 |
180 definition "BuC = Sets_pq Res_ge_0 Res_h Res_l" |
211 definition "BuC = Sets_pq Res_ge_0 Res_h Res_l" |
181 |
212 |
182 lemma QR_lemma_04: "card BuC = card ((Res_h p) \<times> (Res_l q))" |
213 lemma QR_lemma_04: "card BuC = card (Res_h p \<times> Res_l q)" |
183 using card_bij_eq[of f_1 "BuC" "(Res_h p) \<times> (Res_l q)" g_1] |
214 using card_bij_eq[of f_1 "BuC" "Res_h p \<times> Res_l q" g_1] |
184 proof |
215 proof |
185 { |
216 show "inj_on f_1 BuC" |
|
217 proof |
186 fix x y |
218 fix x y |
187 assume a: "x \<in> BuC" "y \<in> BuC" "f_1 x = f_1 y" |
219 assume *: "x \<in> BuC" "y \<in> BuC" "f_1 x = f_1 y" |
188 hence "int p * int q dvd x - y" |
220 then have "int p * int q dvd x - y" |
189 using f_1_def pq_coprime_int divides_mult[of "int p" "x - y" "int q"] |
221 using f_1_def pq_coprime_int divides_mult[of "int p" "x - y" "int q"] |
190 mod_eq_dvd_iff[of x _ y] by auto |
222 mod_eq_dvd_iff[of x _ y] |
191 hence "x = y" |
223 by auto |
192 using dvd_imp_le_int[of "x - y" "int p * int q"] a unfolding BuC_def by force |
224 with * show "x = y" |
193 } |
225 using dvd_imp_le_int[of "x - y" "int p * int q"] unfolding BuC_def by force |
194 thus "inj_on f_1 BuC" unfolding inj_on_def by auto |
226 qed |
195 next |
227 show "inj_on g_1 (Res_h p \<times> Res_l q)" |
196 { |
228 proof |
197 fix x y |
229 fix x y |
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" |
230 assume *: "x \<in> Res_h p \<times> Res_l q" "y \<in> Res_h p \<times> Res_l q" "g_1 x = g_1 y" |
199 hence "0 \<le> fst x" "fst x < p" "0 \<le> snd x" "snd x < q" |
231 then have "0 \<le> fst x" "fst x < p" "0 \<le> snd x" "snd x < q" |
200 "0 \<le> fst y" "fst y < p" "0 \<le> snd y" "snd y < q" |
232 "0 \<le> fst y" "fst y < p" "0 \<le> snd y" "snd y < q" |
201 using mem_Sigma_iff prod.collapse by fastforce+ |
233 using mem_Sigma_iff prod.collapse by fastforce+ |
202 hence "x = y" using g_1_lemma[of x] g_1_lemma[of y] a P_1_def by fastforce |
234 with * show "x = y" |
203 } |
235 using g_1_lemma[of x] g_1_lemma[of y] P_1_def by fastforce |
204 thus "inj_on g_1 ((Res_h p) \<times> (Res_l q))" unfolding inj_on_def by auto |
236 qed |
205 next |
237 show "g_1 ` (Res_h p \<times> Res_l q) \<subseteq> BuC" |
206 show "g_1 ` ((Res_h p) \<times> (Res_l q)) \<subseteq> BuC" |
|
207 proof |
238 proof |
208 fix y |
239 fix y |
209 assume "y \<in> g_1 ` ((Res_h p) \<times> (Res_l q))" |
240 assume "y \<in> g_1 ` (Res_h p \<times> Res_l q)" |
210 then obtain x where x: "y = g_1 x" "x \<in> ((Res_h p) \<times> (Res_l q))" by blast |
241 then obtain x where x: "y = g_1 x" "x \<in> Res_h p \<times> Res_l q" |
211 hence "P_1 x y" using g_1_lemma by fastforce |
242 by blast |
212 thus "y \<in> BuC" unfolding P_1_def BuC_def mem_Collect_eq using x SigmaE prod.sel by fastforce |
243 then have "P_1 x y" |
|
244 using g_1_lemma by fastforce |
|
245 with x show "y \<in> BuC" |
|
246 unfolding P_1_def BuC_def mem_Collect_eq using SigmaE prod.sel by fastforce |
213 qed |
247 qed |
214 qed (auto simp: BuC_def finite_subset f_1_def) |
248 qed (auto simp: BuC_def finite_subset f_1_def) |
215 |
249 |
216 lemma QR_lemma_05: "card ((Res_h p) \<times> (Res_l q)) = r" |
250 lemma QR_lemma_05: "card (Res_h p \<times> Res_l q) = r" |
217 proof - |
251 proof - |
218 have "card (Res_l q) = (q - 1) div 2" "card (Res_h p) = (p - 1) div 2" using p_eq2 by force+ |
252 have "card (Res_l q) = (q - 1) div 2" "card (Res_h p) = (p - 1) div 2" |
219 thus ?thesis unfolding r_def using card_cartesian_product[of "Res_h p" "Res_l q"] by presburger |
253 using p_eq2 by force+ |
|
254 then show ?thesis |
|
255 unfolding r_def using card_cartesian_product[of "Res_h p" "Res_l q"] by presburger |
220 qed |
256 qed |
221 |
257 |
222 lemma QR_lemma_06: "b + c = r" |
258 lemma QR_lemma_06: "b + c = r" |
223 proof - |
259 proof - |
224 have "B \<inter> C = {}" "finite B" "finite C" "B \<union> C = BuC" unfolding B_def C_def BuC_def by fastforce+ |
260 have "B \<inter> C = {}" "finite B" "finite C" "B \<union> C = BuC" |
225 thus ?thesis |
261 unfolding B_def C_def BuC_def by fastforce+ |
|
262 then show ?thesis |
226 unfolding b_def c_def using card_empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce |
263 unfolding b_def c_def using card_empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce |
227 qed |
264 qed |
228 |
265 |
229 definition f_2:: "int \<Rightarrow> int" where |
266 definition f_2:: "int \<Rightarrow> int" |
230 "f_2 x = (int p * int q) - x" |
267 where "f_2 x = (int p * int q) - x" |
231 |
268 |
232 lemma f_2_lemma_1: "\<And>x. f_2 (f_2 x) = x" unfolding f_2_def by simp |
269 lemma f_2_lemma_1: "f_2 (f_2 x) = x" |
233 |
270 by (simp add: f_2_def) |
234 lemma f_2_lemma_2: "[f_2 x = int p - x] (mod p)" unfolding f_2_def using cong_altdef_int by simp |
271 |
|
272 lemma f_2_lemma_2: "[f_2 x = int p - x] (mod p)" |
|
273 by (simp add: f_2_def cong_altdef_int) |
235 |
274 |
236 lemma f_2_lemma_3: "f_2 x \<in> S \<Longrightarrow> x \<in> f_2 ` S" |
275 lemma f_2_lemma_3: "f_2 x \<in> S \<Longrightarrow> x \<in> f_2 ` S" |
237 using f_2_lemma_1[of x] image_eqI[of x f_2 "f_2 x" S] by presburger |
276 using f_2_lemma_1[of x] image_eqI[of x f_2 "f_2 x" S] by presburger |
238 |
277 |
239 lemma QR_lemma_07: "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)" |
278 lemma QR_lemma_07: |
240 "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)" |
279 "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)" |
241 proof - |
280 "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)" |
242 have h1: "f_2 ` Res_l (int p * int q) \<subseteq> Res_h (int p * int q)" using f_2_def by force |
281 proof - |
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 |
282 have 1: "f_2 ` Res_l (int p * int q) \<subseteq> Res_h (int p * int q)" |
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 |
283 by (force simp: f_2_def) |
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 |
284 have 2: "f_2 ` Res_h (int p * int q) \<subseteq> Res_l (int p * int q)" |
246 show "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)" using h1 h3 by blast |
285 using pq_eq2 by (fastforce simp: f_2_def) |
247 show "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)" using h2 h4 by blast |
286 from 2 have 3: "Res_h (int p * int q) \<subseteq> f_2 ` Res_l (int p * int q)" |
248 qed |
287 using f_2_lemma_3 by blast |
249 |
288 from 1 have 4: "Res_l (int p * int q) \<subseteq> f_2 ` Res_h (int p * int q)" |
250 lemma QR_lemma_08: "(f_2 x mod p \<in> Res_l p) = (x mod p \<in> Res_h p)" |
289 using f_2_lemma_3 by blast |
251 "(f_2 x mod p \<in> Res_h p) = (x mod p \<in> Res_l p)" |
290 from 1 3 show "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)" |
|
291 by blast |
|
292 from 2 4 show "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)" |
|
293 by blast |
|
294 qed |
|
295 |
|
296 lemma QR_lemma_08: |
|
297 "f_2 x mod p \<in> Res_l p \<longleftrightarrow> x mod p \<in> Res_h p" |
|
298 "f_2 x mod p \<in> Res_h p \<longleftrightarrow> x mod p \<in> Res_l p" |
252 using f_2_lemma_2[of x] cong_int_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p] |
299 using f_2_lemma_2[of x] cong_int_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p] |
253 zmod_zminus1_eq_if[of x p] p_eq2 by auto |
300 zmod_zminus1_eq_if[of x p] p_eq2 |
254 |
301 by auto |
255 lemma QR_lemma_09: "(f_2 x mod q \<in> Res_l q) = (x mod q \<in> Res_h q)" |
302 |
256 "(f_2 x mod q \<in> Res_h q) = (x mod q \<in> Res_l q)" |
303 lemma QR_lemma_09: |
257 using QRqp QR.QR_lemma_08 f_2_def QR.f_2_def pq_commute by auto+ |
304 "f_2 x mod q \<in> Res_l q \<longleftrightarrow> x mod q \<in> Res_h q" |
258 |
305 "f_2 x mod q \<in> Res_h q \<longleftrightarrow> x mod q \<in> Res_l q" |
259 lemma QR_lemma_10: "a = c" unfolding a_def c_def apply (rule card_bij_eq[of f_2 A C f_2]) |
306 using QRqp QR.QR_lemma_08 f_2_def QR.f_2_def pq_commute by auto |
|
307 |
|
308 lemma QR_lemma_10: "a = c" |
|
309 unfolding a_def c_def |
|
310 apply (rule card_bij_eq[of f_2 A C f_2]) |
260 unfolding A_def C_def |
311 unfolding A_def C_def |
261 using QR_lemma_07 QR_lemma_08 QR_lemma_09 apply ((simp add: inj_on_def f_2_def),blast)+ |
312 using QR_lemma_07 QR_lemma_08 QR_lemma_09 apply ((simp add: inj_on_def f_2_def), blast)+ |
262 by fastforce+ |
313 apply fastforce+ |
|
314 done |
263 |
315 |
264 definition "BuD = Sets_pq Res_l Res_h Res_ge_0" |
316 definition "BuD = Sets_pq Res_l Res_h Res_ge_0" |
265 definition "BuDuF = Sets_pq Res_l Res_h Res" |
317 definition "BuDuF = Sets_pq Res_l Res_h Res" |
266 |
318 |
267 definition f_3 :: "int \<Rightarrow> int \<times> int" where |
319 definition f_3 :: "int \<Rightarrow> int \<times> int" |
268 "f_3 x = (x mod p, x div p + 1)" |
320 where "f_3 x = (x mod p, x div p + 1)" |
269 |
321 |
270 definition g_3 :: "int \<times> int \<Rightarrow> int" where |
322 definition g_3 :: "int \<times> int \<Rightarrow> int" |
271 "g_3 x = fst x + (snd x - 1) * p" |
323 where "g_3 x = fst x + (snd x - 1) * p" |
272 |
324 |
273 lemma QR_lemma_11: "card BuDuF = card ((Res_h p) \<times> (Res_l q))" |
325 lemma QR_lemma_11: "card BuDuF = card (Res_h p \<times> Res_l q)" |
274 using card_bij_eq[of f_3 BuDuF "(Res_h p) \<times> (Res_l q)" g_3] |
326 using card_bij_eq[of f_3 BuDuF "Res_h p \<times> Res_l q" g_3] |
275 proof |
327 proof |
276 show "f_3 ` BuDuF \<subseteq> (Res_h p) \<times> (Res_l q)" |
328 show "f_3 ` BuDuF \<subseteq> Res_h p \<times> Res_l q" |
277 proof |
329 proof |
278 fix y |
330 fix y |
279 assume "y \<in> f_3 ` BuDuF" |
331 assume "y \<in> f_3 ` BuDuF" |
280 then obtain x where x: "y = f_3 x" "x \<in> BuDuF" by blast |
332 then obtain x where x: "y = f_3 x" "x \<in> BuDuF" |
281 hence "x \<le> int p * (int q - 1) div 2 + (int p - 1) div 2" |
333 by blast |
|
334 then have "x \<le> int p * (int q - 1) div 2 + (int p - 1) div 2" |
282 unfolding BuDuF_def using p_eq2 int_distrib(4) by auto |
335 unfolding BuDuF_def using p_eq2 int_distrib(4) by auto |
283 moreover have "(int p - 1) div 2 \<le> - 1 + x mod p" using x BuDuF_def by auto |
336 moreover from x have "(int p - 1) div 2 \<le> - 1 + x mod p" |
|
337 by (auto simp: BuDuF_def) |
284 moreover have "int p * (int q - 1) div 2 = int p * ((int q - 1) div 2)" |
338 moreover have "int p * (int q - 1) div 2 = int p * ((int q - 1) div 2)" |
285 using zdiv_zmult1_eq odd_q by auto |
339 using zdiv_zmult1_eq odd_q by auto |
286 hence "p * (int q - 1) div 2 = p * ((int q + 1) div 2 - 1)" by fastforce |
340 then have "p * (int q - 1) div 2 = p * ((int q + 1) div 2 - 1)" |
287 ultimately have "x \<le> p * ((int q + 1) div 2 - 1) - 1 + x mod p" by linarith |
341 by fastforce |
288 hence "x div p < (int q + 1) div 2 - 1" |
342 ultimately have "x \<le> p * ((int q + 1) div 2 - 1) - 1 + x mod p" |
|
343 by linarith |
|
344 then have "x div p < (int q + 1) div 2 - 1" |
289 using mult.commute[of "int p" "x div p"] p_ge_0 div_mult_mod_eq[of x p] |
345 using mult.commute[of "int p" "x div p"] p_ge_0 div_mult_mod_eq[of x p] |
290 mult_less_cancel_left_pos[of p "x div p" "(int q + 1) div 2 - 1"] by linarith |
346 and mult_less_cancel_left_pos[of p "x div p" "(int q + 1) div 2 - 1"] |
291 moreover have "0 < x div p + 1" |
347 by linarith |
292 using pos_imp_zdiv_neg_iff[of p x] p_ge_0 x mem_Collect_eq BuDuF_def by auto |
348 moreover from x have "0 < x div p + 1" |
293 ultimately show "y \<in> (Res_h p) \<times> (Res_l q)" using x BuDuF_def f_3_def by auto |
349 using pos_imp_zdiv_neg_iff[of p x] p_ge_0 by (auto simp: BuDuF_def) |
294 qed |
350 ultimately show "y \<in> Res_h p \<times> Res_l q" |
295 next |
351 using x by (auto simp: BuDuF_def f_3_def) |
296 have h1: "\<And>x. x \<in> ((Res_h p) \<times> (Res_l q)) \<Longrightarrow> f_3 (g_3 x) = x" |
352 qed |
297 proof - |
353 show "inj_on g_3 (Res_h p \<times> Res_l q)" |
298 fix x |
354 proof |
299 assume a: "x \<in> ((Res_h p) \<times> (Res_l q))" |
355 have *: "f_3 (g_3 x) = x" if "x \<in> Res_h p \<times> Res_l q" for x |
300 moreover have h: "(fst x + (snd x - 1) * int p) mod int p = fst x" using a by force |
356 proof - |
301 ultimately have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x" |
357 from that have *: "(fst x + (snd x - 1) * int p) mod int p = fst x" |
302 by (auto simp: semiring_numeral_div_class.div_less) |
358 by force |
303 with h show "f_3 (g_3 x) = x" unfolding f_3_def g_3_def by simp |
359 from that have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x" |
304 qed |
360 by (auto simp: semiring_numeral_div_class.div_less) |
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]) |
361 with * show "f_3 (g_3 x) = x" |
306 proof - |
362 by (simp add: f_3_def g_3_def) |
|
363 qed |
307 fix x y |
364 fix x y |
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" |
365 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" |
309 thus "x = y" using h1[of x] h1[of y] by presburger |
366 from this *[of x] *[of y] show "x = y" |
310 qed |
367 by presburger |
311 next |
368 qed |
312 show "g_3 ` ((Res_h p) \<times> (Res_l q)) \<subseteq> BuDuF" |
369 show "g_3 ` (Res_h p \<times> Res_l q) \<subseteq> BuDuF" |
313 proof |
370 proof |
314 fix y |
371 fix y |
315 assume "y \<in> g_3 ` ((Res_h p) \<times> (Res_l q))" |
372 assume "y \<in> g_3 ` (Res_h p \<times> Res_l q)" |
316 then obtain x where x: "y = g_3 x" "x \<in> (Res_h p) \<times> (Res_l q)" by blast |
373 then obtain x where x: "x \<in> Res_h p \<times> Res_l q" and y: "y = g_3 x" |
317 hence "snd x \<le> (int q - 1) div 2" by force |
374 by blast |
|
375 then have "snd x \<le> (int q - 1) div 2" |
|
376 by force |
318 moreover have "int p * ((int q - 1) div 2) = (int p * int q - int p) div 2" |
377 moreover have "int p * ((int q - 1) div 2) = (int p * int q - int p) div 2" |
319 using int_distrib(4) zdiv_zmult1_eq[of "int p" "int q - 1" 2] odd_q by fastforce |
378 using int_distrib(4) zdiv_zmult1_eq[of "int p" "int q - 1" 2] odd_q by fastforce |
320 ultimately have "(snd x) * int p \<le> (int q * int p - int p) div 2" |
379 ultimately have "(snd x) * int p \<le> (int q * int p - int p) div 2" |
321 using mult_right_mono[of "snd x" "(int q - 1) div 2" p] mult.commute[of "(int q - 1) div 2" p] |
380 using mult_right_mono[of "snd x" "(int q - 1) div 2" p] mult.commute[of "(int q - 1) div 2" p] |
322 pq_commute by presburger |
381 pq_commute |
323 hence "(snd x - 1) * int p \<le> (int q * int p - 1) div 2 - int p" |
382 by presburger |
|
383 then have "(snd x - 1) * int p \<le> (int q * int p - 1) div 2 - int p" |
324 using p_ge_0 int_distrib(3) by auto |
384 using p_ge_0 int_distrib(3) by auto |
325 moreover have "fst x \<le> int p - 1" using x by force |
385 moreover from x have "fst x \<le> int p - 1" by force |
326 ultimately have "fst x + (snd x - 1) * int p \<le> (int p * int q - 1) div 2" |
386 ultimately have "fst x + (snd x - 1) * int p \<le> (int p * int q - 1) div 2" |
327 using pq_commute by linarith |
387 using pq_commute by linarith |
328 moreover have "0 < fst x" "0 \<le> (snd x - 1) * p" using x(2) by fastforce+ |
388 moreover from x have "0 < fst x" "0 \<le> (snd x - 1) * p" |
329 ultimately show "y \<in> BuDuF" unfolding BuDuF_def using q_ge_0 x g_3_def x(1) by auto |
389 by fastforce+ |
330 qed |
390 ultimately show "y \<in> BuDuF" |
331 next |
391 unfolding BuDuF_def using q_ge_0 x g_3_def y by auto |
|
392 qed |
332 show "finite BuDuF" unfolding BuDuF_def by fastforce |
393 show "finite BuDuF" unfolding BuDuF_def by fastforce |
333 qed (simp add: inj_on_inverseI[of BuDuF g_3] f_3_def g_3_def QR_lemma_05)+ |
394 qed (simp add: inj_on_inverseI[of BuDuF g_3] f_3_def g_3_def QR_lemma_05)+ |
334 |
395 |
335 lemma QR_lemma_12: "b + d + m = r" |
396 lemma QR_lemma_12: "b + d + m = r" |
336 proof - |
397 proof - |
337 have "B \<inter> D = {}" "finite B" "finite D" "B \<union> D = BuD" unfolding B_def D_def BuD_def by fastforce+ |
398 have "B \<inter> D = {}" "finite B" "finite D" "B \<union> D = BuD" |
338 hence "b + d = card BuD" unfolding b_def d_def using card_Un_Int by fastforce |
399 unfolding B_def D_def BuD_def by fastforce+ |
339 moreover have "BuD \<inter> F = {}" "finite BuD" "finite F" unfolding BuD_def F_def by fastforce+ |
400 then have "b + d = card BuD" |
340 moreover have "BuD \<union> F = BuDuF" unfolding BuD_def F_def BuDuF_def |
401 unfolding b_def d_def using card_Un_Int by fastforce |
|
402 moreover have "BuD \<inter> F = {}" "finite BuD" "finite F" |
|
403 unfolding BuD_def F_def by fastforce+ |
|
404 moreover have "BuD \<union> F = BuDuF" |
|
405 unfolding BuD_def F_def BuDuF_def |
341 using q_ge_0 ivl_disj_un_singleton(5)[of 0 "int q - 1"] by auto |
406 using q_ge_0 ivl_disj_un_singleton(5)[of 0 "int q - 1"] by auto |
342 ultimately show ?thesis using QR_lemma_03 QR_lemma_05 QR_lemma_11 card_Un_disjoint[of BuD F] |
407 ultimately show ?thesis |
343 unfolding b_def d_def f_def by presburger |
408 using QR_lemma_03 QR_lemma_05 QR_lemma_11 card_Un_disjoint[of BuD F] |
|
409 unfolding b_def d_def f_def |
|
410 by presburger |
344 qed |
411 qed |
345 |
412 |
346 lemma QR_lemma_13: "a + d + n = r" |
413 lemma QR_lemma_13: "a + d + n = r" |
347 proof - |
414 proof - |
348 have "A = QR.B q p" unfolding A_def pq_commute using QRqp QR.B_def[of q p] by blast |
415 have "A = QR.B q p" |
349 hence "a = QR.b q p" using a_def QRqp QR.b_def[of q p] by presburger |
416 unfolding A_def pq_commute using QRqp QR.B_def[of q p] by blast |
350 moreover have "D = QR.D q p" unfolding D_def pq_commute using QRqp QR.D_def[of q p] by blast |
417 then have "a = QR.b q p" |
351 hence "d = QR.d q p" using d_def QRqp QR.d_def[of q p] by presburger |
418 using a_def QRqp QR.b_def[of q p] by presburger |
352 moreover have "n = QR.m q p" using n_def QRqp QR.m_def[of q p] by presburger |
419 moreover have "D = QR.D q p" |
353 moreover have "r = QR.r q p" unfolding r_def using QRqp QR.r_def[of q p] by auto |
420 unfolding D_def pq_commute using QRqp QR.D_def[of q p] by blast |
354 ultimately show ?thesis using QRqp QR.QR_lemma_12 by presburger |
421 then have "d = QR.d q p" |
|
422 using d_def QRqp QR.d_def[of q p] by presburger |
|
423 moreover have "n = QR.m q p" |
|
424 using n_def QRqp QR.m_def[of q p] by presburger |
|
425 moreover have "r = QR.r q p" |
|
426 unfolding r_def using QRqp QR.r_def[of q p] by auto |
|
427 ultimately show ?thesis |
|
428 using QRqp QR.QR_lemma_12 by presburger |
355 qed |
429 qed |
356 |
430 |
357 lemma QR_lemma_14: "(-1::int) ^ (m + n) = (-1) ^ r" |
431 lemma QR_lemma_14: "(-1::int) ^ (m + n) = (-1) ^ r" |
358 proof - |
432 proof - |
359 have "m + n + 2 * d = r" using QR_lemma_06 QR_lemma_10 QR_lemma_12 QR_lemma_13 by auto |
433 have "m + n + 2 * d = r" |
360 thus ?thesis using power_add[of "-1::int" "m + n" "2 * d"] by fastforce |
434 using QR_lemma_06 QR_lemma_10 QR_lemma_12 QR_lemma_13 by auto |
|
435 then show ?thesis |
|
436 using power_add[of "-1::int" "m + n" "2 * d"] by fastforce |
361 qed |
437 qed |
362 |
438 |
363 lemma Quadratic_Reciprocity: |
439 lemma Quadratic_Reciprocity: |
364 "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))" |
440 "Legendre p q * Legendre q p = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))" |
365 using Gpq Gqp GAUSS.gauss_lemma power_add[of "-1::int" m n] QR_lemma_14 |
441 using Gpq Gqp GAUSS.gauss_lemma power_add[of "-1::int" m n] QR_lemma_14 |
366 unfolding r_def m_def n_def by auto |
442 unfolding r_def m_def n_def by auto |
367 |
443 |
368 end |
444 end |
369 |
445 |
370 theorem Quadratic_Reciprocity: assumes "prime p" "2 < p" "prime q" "2 < q" "p \<noteq> q" |
446 theorem Quadratic_Reciprocity: |
371 shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))" |
447 assumes "prime p" "2 < p" "prime q" "2 < q" "p \<noteq> q" |
|
448 shows "Legendre p q * Legendre q p = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))" |
372 using QR.Quadratic_Reciprocity QR_def assms by blast |
449 using QR.Quadratic_Reciprocity QR_def assms by blast |
373 |
450 |
374 theorem Quadratic_Reciprocity_int: assumes "prime (nat p)" "2 < p" "prime (nat q)" "2 < q" "p \<noteq> q" |
451 theorem Quadratic_Reciprocity_int: |
375 shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ (nat ((p - 1) div 2 * ((q - 1) div 2)))" |
452 assumes "prime (nat p)" "2 < p" "prime (nat q)" "2 < q" "p \<noteq> q" |
376 proof - |
453 shows "Legendre p q * Legendre q p = (-1::int) ^ (nat ((p - 1) div 2 * ((q - 1) div 2)))" |
377 have "0 \<le> (p - 1) div 2" using assms by simp |
454 proof - |
|
455 from assms have "0 \<le> (p - 1) div 2" by simp |
378 moreover have "(nat p - 1) div 2 = nat ((p - 1) div 2)" "(nat q - 1) div 2 = nat ((q - 1) div 2)" |
456 moreover have "(nat p - 1) div 2 = nat ((p - 1) div 2)" "(nat q - 1) div 2 = nat ((q - 1) div 2)" |
379 by fastforce+ |
457 by fastforce+ |
380 ultimately have "(nat p - 1) div 2 * ((nat q - 1) div 2) = nat ((p - 1) div 2 * ((q - 1) div 2))" |
458 ultimately have "(nat p - 1) div 2 * ((nat q - 1) div 2) = nat ((p - 1) div 2 * ((q - 1) div 2))" |
381 using nat_mult_distrib by presburger |
459 using nat_mult_distrib by presburger |
382 moreover have "2 < nat p" "2 < nat q" "nat p \<noteq> nat q" "int (nat p) = p" "int (nat q) = q" |
460 moreover have "2 < nat p" "2 < nat q" "nat p \<noteq> nat q" "int (nat p) = p" "int (nat q) = q" |
383 using assms by linarith+ |
461 using assms by linarith+ |
384 ultimately show ?thesis using Quadratic_Reciprocity[of "nat p" "nat q"] assms by presburger |
462 ultimately show ?thesis |
|
463 using Quadratic_Reciprocity[of "nat p" "nat q"] assms by presburger |
385 qed |
464 qed |
386 |
465 |
387 end |
466 end |