144 moreover from mod k have "(p_inv * (p * kx)) mod q = (p_inv * (p * ky)) mod q" |
144 moreover from mod k have "(p_inv * (p * kx)) mod q = (p_inv * (p * ky)) mod q" |
145 using mod_mult_cong by blast |
145 using mod_mult_cong by blast |
146 then have "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q" |
146 then have "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q" |
147 by (simp add: algebra_simps) |
147 by (simp add: algebra_simps) |
148 then have "kx mod q = ky mod q" |
148 then have "kx mod q = ky mod q" |
149 using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] by (auto simp: cong_int_def) |
149 using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] |
|
150 by (auto simp: cong_def) |
150 then have "[kx = ky] (mod q)" |
151 then have "[kx = ky] (mod q)" |
151 unfolding cong_int_def by blast |
152 unfolding cong_def by blast |
152 ultimately show ?thesis |
153 ultimately show ?thesis |
153 using cong_less_imp_eq_int k by blast |
154 using cong_less_imp_eq_int k by blast |
154 qed |
155 qed |
155 then have "inj_on (\<lambda>x. x mod q) E" |
156 then have "inj_on (\<lambda>x. x mod q) E" |
156 by (auto simp: inj_on_def) |
157 by (auto simp: inj_on_def) |
182 assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q" |
183 assumes "0 \<le> fst res" "fst res < p" "0 \<le> snd res" "snd res < q" |
183 shows "\<exists>!x. P_1 res x" |
184 shows "\<exists>!x. P_1 res x" |
184 proof - |
185 proof - |
185 obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q" |
186 obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q" |
186 using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce |
187 using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce |
187 have *: "[y = fst res] (mod p)" "[y = snd res] (mod q)" |
188 have "fst res = int (y - k1 * p)" |
188 using yk(1) assms(1) cong_iff_lin_int[of "fst res"] cong_sym_int apply simp |
189 using \<open>0 \<le> fst res\<close> yk(1) by simp |
189 using yk(2) assms(3) cong_iff_lin_int[of "snd res"] cong_sym_int by simp |
190 moreover have "snd res = int (y - k2 * q)" |
190 have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res" |
191 using \<open>0 \<le> snd res\<close> yk(2) by simp |
191 using *(1) mod_mod_cancel[of "int p"] assms(1) assms(2) cong_int_def apply simp |
192 ultimately have res: "res = (int (y - k1 * p), int (y - k2 * q))" |
192 using *(2) mod_mod_cancel[of "int q"] assms(3) assms(4) cong_int_def by simp |
193 by (simp add: prod_eq_iff) |
|
194 have y: "k1 * p \<le> y" "k2 * q \<le> y" |
|
195 using yk by simp_all |
|
196 from y have *: "[y = nat (fst res)] (mod p)" "[y = nat (snd res)] (mod q)" |
|
197 by (auto simp add: res cong_le_nat intro: exI [of _ k1] exI [of _ k2]) |
|
198 from * have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res" |
|
199 using y apply (auto simp add: res of_nat_mult [symmetric] of_nat_mod [symmetric] mod_mod_cancel simp del: of_nat_mult) |
|
200 apply (metis \<open>fst res = int (y - k1 * p)\<close> assms(1) assms(2) cong_def mod_pos_pos_trivial nat_int of_nat_mod) |
|
201 apply (metis \<open>snd res = int (y - k2 * q)\<close> assms(3) assms(4) cong_def mod_pos_pos_trivial nat_int of_nat_mod) |
|
202 done |
193 then obtain x where "P_1 res x" |
203 then obtain x where "P_1 res x" |
194 unfolding P_1_def |
204 unfolding P_1_def |
195 using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce |
205 using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce |
196 moreover have "a = b" if "P_1 res a" "P_1 res b" for a b |
206 moreover have "a = b" if "P_1 res a" "P_1 res b" for a b |
197 proof - |
207 proof - |
318 qed |
328 qed |
319 |
329 |
320 lemma QR_lemma_08: |
330 lemma QR_lemma_08: |
321 "f_2 x mod p \<in> Res_l p \<longleftrightarrow> x mod p \<in> Res_h p" |
331 "f_2 x mod p \<in> Res_l p \<longleftrightarrow> x mod p \<in> Res_h p" |
322 "f_2 x mod p \<in> Res_h p \<longleftrightarrow> x mod p \<in> Res_l p" |
332 "f_2 x mod p \<in> Res_h p \<longleftrightarrow> x mod p \<in> Res_l p" |
323 using f_2_lemma_2[of x] cong_int_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p] |
333 using f_2_lemma_2[of x] cong_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p] |
324 zmod_zminus1_eq_if[of x p] p_eq2 |
334 zmod_zminus1_eq_if[of x p] p_eq2 |
325 by auto |
335 by auto |
326 |
336 |
327 lemma QR_lemma_09: |
337 lemma QR_lemma_09: |
328 "f_2 x mod q \<in> Res_l q \<longleftrightarrow> x mod q \<in> Res_h q" |
338 "f_2 x mod q \<in> Res_l q \<longleftrightarrow> x mod q \<in> Res_h q" |
379 have *: "f_3 (g_3 x) = x" if "x \<in> Res_h p \<times> Res_l q" for x |
389 have *: "f_3 (g_3 x) = x" if "x \<in> Res_h p \<times> Res_l q" for x |
380 proof - |
390 proof - |
381 from that have *: "(fst x + (snd x - 1) * int p) mod int p = fst x" |
391 from that have *: "(fst x + (snd x - 1) * int p) mod int p = fst x" |
382 by force |
392 by force |
383 from that have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x" |
393 from that have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x" |
384 by (auto simp: div_pos_pos_trivial) |
394 by auto |
385 with * show "f_3 (g_3 x) = x" |
395 with * show "f_3 (g_3 x) = x" |
386 by (simp add: f_3_def g_3_def) |
396 by (simp add: f_3_def g_3_def) |
387 qed |
397 qed |
388 fix x y |
398 fix x y |
389 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" |
399 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" |