author | wenzelm |
Wed, 26 Oct 2016 15:14:17 +0200 | |
changeset 64406 | 492de9062cd2 |
parent 64282 | 261d42f0bfac |
child 65465 | 067210a08a22 |
permissions | -rw-r--r-- |
64282
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
1 |
(* Author: Jaime Mendizabal Roche *) |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
2 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
3 |
theory Euler_Criterion |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
4 |
imports Residues |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
5 |
begin |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
6 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
7 |
context |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
8 |
fixes p :: "nat" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
9 |
fixes a :: "int" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
10 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
11 |
assumes p_prime: "prime p" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
12 |
assumes p_ge_2: "2 < p" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
13 |
assumes p_a_relprime: "[a \<noteq> 0](mod p)" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
14 |
begin |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
15 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
16 |
private lemma odd_p: "odd p" using p_ge_2 p_prime prime_odd_nat by blast |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
17 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
18 |
private lemma p_minus_1_int: "int (p - 1) = int p - 1" using p_prime prime_ge_1_nat by force |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
19 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
20 |
private lemma E_1: assumes "QuadRes p a" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
21 |
shows "[a ^ ((p - 1) div 2) = 1] (mod (int p))" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
22 |
proof - |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
23 |
from assms obtain b where b: "[b ^ 2 = a] (mod p)" unfolding QuadRes_def by blast |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
24 |
hence "[a ^ ((p - 1) div 2) = b ^ (2 * ((p - 1) div 2))] (mod p)" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
25 |
by (simp add: cong_exp_int cong_sym_int power_mult) |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
26 |
hence "[a ^ ((p - 1) div 2) = b ^ (p - 1)] (mod p)" using odd_p by force |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
27 |
moreover have "~ p dvd b" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
28 |
using b cong_altdef_int[of a 0 p] cong_dvd_eq_int[of "b ^ 2" a "int p"] p_a_relprime p_prime |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
29 |
by (auto simp: prime_dvd_power_int_iff) |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
30 |
ultimately show ?thesis using fermat_theorem[of p b] p_prime |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
31 |
by (auto intro: cong_trans_int) |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
32 |
qed |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
33 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
34 |
private definition S1 :: "int set" where "S1 = {0 <.. int p - 1}" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
35 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
36 |
private definition P :: "int \<Rightarrow> int \<Rightarrow> bool" where |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
37 |
"P x y \<longleftrightarrow> [x * y = a] (mod p) \<and> y \<in> S1" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
38 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
39 |
private definition f_1 :: "int \<Rightarrow> int" where |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
40 |
"f_1 x = (THE y. P x y)" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
41 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
42 |
private definition f :: "int \<Rightarrow> int set" where |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
43 |
"f x = {x, f_1 x}" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
44 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
45 |
private definition S2 :: "int set set" where "S2 = f ` S1" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
46 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
47 |
private lemma P_lemma: assumes "x \<in> S1" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
48 |
shows "\<exists>! y. P x y" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
49 |
proof - |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
50 |
have "~ p dvd x" using assms zdvd_not_zless S1_def by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
51 |
hence co_xp: "coprime x p" using p_prime prime_imp_coprime_int[of p x] |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
52 |
by (simp add: gcd.commute) |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
53 |
then obtain y' where y': "[x * y' = 1] (mod p)" using cong_solve_coprime_int by blast |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
54 |
moreover define y where "y = y' * a mod p" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
55 |
ultimately have "[x * y = a] (mod p)" using mod_mult_right_eq[of x "y' * a" p] |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
56 |
cong_scalar_int[of "x * y'"] unfolding cong_int_def mult.assoc by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
57 |
moreover have "y \<in> {0 .. int p - 1}" unfolding y_def using p_ge_2 by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
58 |
hence "y \<in> S1" using calculation cong_altdef_int p_a_relprime S1_def by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
59 |
ultimately have "P x y" unfolding P_def by blast |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
60 |
moreover { |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
61 |
fix y1 y2 |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
62 |
assume "P x y1" "P x y2" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
63 |
moreover hence "[y1 = y2] (mod p)" unfolding P_def |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
64 |
using co_xp cong_mult_lcancel_int[of x p y1 y2] cong_sym_int cong_trans_int by blast |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
65 |
ultimately have "y1 = y2" unfolding P_def S1_def using cong_less_imp_eq_int by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
66 |
} |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
67 |
ultimately show ?thesis by blast |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
68 |
qed |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
69 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
70 |
private lemma f_1_lemma_1: assumes "x \<in> S1" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
71 |
shows "P x (f_1 x)" using assms P_lemma theI'[of "P x"] f_1_def by presburger |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
72 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
73 |
private lemma f_1_lemma_2: assumes "x \<in> S1" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
74 |
shows "f_1 (f_1 x) = x" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
75 |
using assms f_1_lemma_1[of x] f_1_def P_lemma[of "f_1 x"] P_def by (auto simp: mult.commute) |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
76 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
77 |
private lemma f_lemma_1: assumes "x \<in> S1" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
78 |
shows "f x = f (f_1 x)" using f_def f_1_lemma_2[of x] assms by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
79 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
80 |
private lemma l1: assumes "~ QuadRes p a" "x \<in> S1" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
81 |
shows "x \<noteq> f_1 x" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
82 |
using f_1_lemma_1[of x] assms unfolding P_def QuadRes_def power2_eq_square by fastforce |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
83 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
84 |
private lemma l2: assumes "~ QuadRes p a" "x \<in> S1" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
85 |
shows "[\<Prod> (f x) = a] (mod p)" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
86 |
using assms l1 f_1_lemma_1 P_def f_def by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
87 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
88 |
private lemma l3: assumes "x \<in> S2" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
89 |
shows "finite x" using assms f_def S2_def by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
90 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
91 |
private lemma l4: "S1 = \<Union> S2" using f_1_lemma_1 P_def f_def S2_def by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
92 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
93 |
private lemma l5: assumes "x \<in> S2" "y \<in> S2" "x \<noteq> y" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
94 |
shows "x \<inter> y = {}" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
95 |
proof - |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
96 |
obtain a b where ab: "x = f a" "a \<in> S1" "y = f b" "b \<in> S1" using assms S2_def by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
97 |
hence "a \<noteq> b" "a \<noteq> f_1 b" "f_1 a \<noteq> b" using assms(3) f_lemma_1 by blast+ |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
98 |
moreover hence "f_1 a \<noteq> f_1 b" using f_1_lemma_2[of a] f_1_lemma_2[of b] ab by force |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
99 |
ultimately show ?thesis using f_def ab by fastforce |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
100 |
qed |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
101 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
102 |
private lemma l6: "prod Prod S2 = \<Prod> S1" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
103 |
using prod.Union_disjoint[of S2 "\<lambda>x. x"] l3 l4 l5 unfolding comp_def by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
104 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
105 |
private lemma l7: "fact n = \<Prod> {0 <.. int n}" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
106 |
proof (induction n) |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
107 |
case (Suc n) |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
108 |
have "int (Suc n) = int n + 1" by simp |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
109 |
hence "insert (int (Suc n)) {0<..int n} = {0<..int (Suc n)}" by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
110 |
thus ?case using prod.insert[of "{0<..int n}" "int (Suc n)" "\<lambda>x. x"] Suc fact_Suc by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
111 |
qed simp |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
112 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
113 |
private lemma l8: "fact (p - 1) = \<Prod> S1" using l7[of "p - 1"] S1_def p_minus_1_int by presburger |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
114 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
115 |
private lemma l9: "[prod Prod S2 = -1] (mod p)" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
116 |
using l6 l8 wilson_theorem[of p] p_prime by presburger |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
117 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
118 |
private lemma l10: assumes "card S = n" "\<And>x. x \<in> S \<Longrightarrow> [g x = a] (mod p)" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
119 |
shows "[prod g S = a ^ n] (mod p)" using assms |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
120 |
proof (induction n arbitrary: S) |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
121 |
case 0 |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
122 |
thus ?case using card_0_eq[of S] prod.empty prod.infinite by fastforce |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
123 |
next |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
124 |
case (Suc n) |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
125 |
then obtain x where x: "x \<in> S" by force |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
126 |
define S' where "S' = S - {x}" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
127 |
hence "[prod g S' = a ^ n] (mod int p)" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
128 |
using x Suc(1)[of S'] Suc(2) Suc(3) by (simp add: card_ge_0_finite) |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
129 |
moreover have "prod g S = g x * prod g S'" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
130 |
using x S'_def Suc(2) prod.remove[of S x g] by fastforce |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
131 |
ultimately show ?case using x Suc(3) cong_mult_int by simp |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
132 |
qed |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
133 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
134 |
private lemma l11: assumes "~ QuadRes p a" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
135 |
shows "card S2 = (p - 1) div 2" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
136 |
proof - |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
137 |
have "sum card S2 = 2 * card S2" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
138 |
using sum.cong[of S2 S2 card "\<lambda>x. 2"] l1 f_def S2_def assms by fastforce |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
139 |
moreover have "p - 1 = sum card S2" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
140 |
using l4 card_UN_disjoint[of S2 "\<lambda>x. x"] l3 l5 S1_def S2_def by auto |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
141 |
ultimately show ?thesis by linarith |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
142 |
qed |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
143 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
144 |
private lemma l12: assumes "~ QuadRes p a" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
145 |
shows "[prod Prod S2 = a ^ ((p - 1) div 2)] (mod p)" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
146 |
using assms l2 l10 l11 unfolding S2_def by blast |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
147 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
148 |
private lemma E_2: assumes "~ QuadRes p a" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
149 |
shows "[a ^ ((p - 1) div 2) = -1] (mod p)" using l9 l12 cong_trans_int cong_sym_int assms by blast |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
150 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
151 |
lemma euler_criterion_aux: "[(Legendre a p) = a ^ ((p - 1) div 2)] (mod p)" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
152 |
using E_1 E_2 Legendre_def cong_sym_int p_a_relprime by presburger |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
153 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
154 |
end |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
155 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
156 |
theorem euler_criterion: assumes "prime p" "2 < p" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
157 |
shows "[(Legendre a p) = a ^ ((p - 1) div 2)] (mod p)" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
158 |
proof (cases "[a = 0] (mod p)") |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
159 |
case True |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
160 |
hence "[a ^ ((p - 1) div 2) = 0 ^ ((p - 1) div 2)] (mod p)" using cong_exp_int by blast |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
161 |
moreover have "(0::int) ^ ((p - 1) div 2) = 0" using zero_power[of "(p - 1) div 2"] assms(2) by simp |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
162 |
ultimately have "[a ^ ((p - 1) div 2) = 0] (mod p)" using cong_trans_int cong_refl_int by presburger |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
163 |
thus ?thesis unfolding Legendre_def using True cong_sym_int by presburger |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
164 |
next |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
165 |
case False |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
166 |
thus ?thesis using euler_criterion_aux assms by presburger |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
167 |
qed |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
168 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
169 |
hide_fact euler_criterion_aux |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
170 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
171 |
end |