author | haftmann |
Fri, 20 Oct 2017 20:57:55 +0200 | |
changeset 66888 | 930abfdf8727 |
parent 66305 | 7454317f883c |
child 67051 | e7e54a0b9197 |
permissions | -rw-r--r-- |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1 |
(* Title: HOL/Number_Theory/Pocklington.thy |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
2 |
Author: Amine Chaieb |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
3 |
*) |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
4 |
|
60526 | 5 |
section \<open>Pocklington's Theorem for Primes\<close> |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
6 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
7 |
theory Pocklington |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
8 |
imports Residues |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
9 |
begin |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
10 |
|
66305 | 11 |
subsection \<open>Lemmas about previously defined terms\<close> |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
12 |
|
66305 | 13 |
lemma prime_nat_iff'': "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)" |
63633 | 14 |
unfolding prime_nat_iff |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
15 |
proof safe |
66305 | 16 |
fix m |
17 |
assume p: "p > 0" "p \<noteq> 1" |
|
18 |
and m: "m dvd p" "m \<noteq> p" |
|
19 |
and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
20 |
from p m have "m \<noteq> 0" by (intro notI) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
21 |
moreover from p m have "m < p" by (auto dest: dvd_imp_le) |
66305 | 22 |
ultimately have "coprime p m" |
23 |
using * by blast |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
24 |
with m show "m = 1" by simp |
66305 | 25 |
qed (auto simp: prime_nat_iff simp del: One_nat_def intro!: prime_imp_coprime dest: dvd_imp_le) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
26 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
27 |
lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1" |
66305 | 28 |
proof - |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
29 |
have "{ m. 0 < m \<and> m < n } = {1..<n}" by auto |
66305 | 30 |
then show ?thesis by simp |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
31 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
32 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
33 |
|
66305 | 34 |
subsection \<open>Some basic theorems about solving congruences\<close> |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
35 |
|
66305 | 36 |
lemma cong_solve: |
37 |
fixes n :: nat |
|
38 |
assumes an: "coprime a n" |
|
39 |
shows "\<exists>x. [a * x = b] (mod n)" |
|
40 |
proof (cases "a = 0") |
|
41 |
case True |
|
42 |
with an show ?thesis |
|
66888 | 43 |
by (simp add: cong_def) |
66305 | 44 |
next |
45 |
case False |
|
46 |
from bezout_add_strong_nat [OF this] |
|
47 |
obtain d x y where dxy: "d dvd a" "d dvd n" "a * x = n * y + d" by blast |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
48 |
from dxy(1,2) have d1: "d = 1" |
66305 | 49 |
by (metis assms coprime_nat) |
50 |
with dxy(3) have "a * x * b = (n * y + 1) * b" |
|
51 |
by simp |
|
52 |
then have "a * (x * b) = n * (y * b) + b" |
|
53 |
by (auto simp: algebra_simps) |
|
54 |
then have "a * (x * b) mod n = (n * (y * b) + b) mod n" |
|
55 |
by simp |
|
56 |
then have "a * (x * b) mod n = b mod n" |
|
57 |
by (simp add: mod_add_left_eq) |
|
58 |
then have "[a * (x * b) = b] (mod n)" |
|
66888 | 59 |
by (simp only: cong_def) |
66305 | 60 |
then show ?thesis by blast |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
61 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
62 |
|
66305 | 63 |
lemma cong_solve_unique: |
64 |
fixes n :: nat |
|
65 |
assumes an: "coprime a n" and nz: "n \<noteq> 0" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
66 |
shows "\<exists>!x. x < n \<and> [a * x = b] (mod n)" |
66305 | 67 |
proof - |
68 |
from cong_solve[OF an] obtain x where x: "[a * x = b] (mod n)" |
|
69 |
by blast |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
70 |
let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
71 |
let ?x = "x mod n" |
66305 | 72 |
from x have *: "[a * ?x = b] (mod n)" |
66888 | 73 |
by (simp add: cong_def mod_mult_right_eq[of a x n]) |
66305 | 74 |
from mod_less_divisor[ of n x] nz * have Px: "?P ?x" by simp |
75 |
have "y = ?x" if Py: "y < n" "[a * y = b] (mod n)" for y |
|
76 |
proof - |
|
77 |
from Py(2) * have "[a * y = a * ?x] (mod n)" |
|
66888 | 78 |
by (simp add: cong_def) |
66305 | 79 |
then have "[y = ?x] (mod n)" |
80 |
by (metis an cong_mult_lcancel_nat) |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
81 |
with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz |
66305 | 82 |
show ?thesis |
66888 | 83 |
by (simp add: cong_def) |
66305 | 84 |
qed |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
85 |
with Px show ?thesis by blast |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
86 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
87 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
88 |
lemma cong_solve_unique_nontrivial: |
66305 | 89 |
fixes p :: nat |
90 |
assumes p: "prime p" |
|
91 |
and pa: "coprime p a" |
|
92 |
and x0: "0 < x" |
|
93 |
and xp: "x < p" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
94 |
shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)" |
66305 | 95 |
proof - |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
96 |
from pa have ap: "coprime a p" |
66305 | 97 |
by (metis gcd.commute) |
98 |
have px: "coprime x p" |
|
64282
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64242
diff
changeset
|
99 |
by (metis gcd.commute p prime_nat_iff'' x0 xp) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
100 |
obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
101 |
by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px) |
66305 | 102 |
have "y \<noteq> 0" |
103 |
proof |
|
104 |
assume "y = 0" |
|
105 |
with y(2) have "p dvd a" |
|
66888 | 106 |
using cong_dvd_iff by auto |
66305 | 107 |
then show False |
108 |
by (metis gcd_nat.absorb1 not_prime_1 p pa) |
|
109 |
qed |
|
110 |
with y show ?thesis |
|
111 |
by blast |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
112 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
113 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
114 |
lemma cong_unique_inverse_prime: |
66305 | 115 |
fixes p :: nat |
116 |
assumes "prime p" and "0 < x" and "x < p" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
117 |
shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)" |
66305 | 118 |
by (rule cong_solve_unique_nontrivial) (use assms in simp_all) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
119 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
120 |
lemma chinese_remainder_coprime_unique: |
66305 | 121 |
fixes a :: nat |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
122 |
assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b \<noteq> 0" |
66305 | 123 |
and ma: "coprime m a" and nb: "coprime n b" |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
124 |
shows "\<exists>!x. coprime x (a * b) \<and> x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)" |
66305 | 125 |
proof - |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
126 |
let ?P = "\<lambda>x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
127 |
from binary_chinese_remainder_unique_nat[OF ab az bz] |
66305 | 128 |
obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" "\<forall>y. ?P y \<longrightarrow> y = x" |
129 |
by blast |
|
130 |
from ma nb x have "coprime x a" "coprime x b" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
131 |
by (metis cong_gcd_eq_nat)+ |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
132 |
then have "coprime x (a*b)" |
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62349
diff
changeset
|
133 |
by (metis coprime_mul_eq) |
66305 | 134 |
with x show ?thesis |
135 |
by blast |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
136 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
137 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
138 |
|
66305 | 139 |
subsection \<open>Lucas's theorem\<close> |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
140 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
141 |
lemma lucas_coprime_lemma: |
66305 | 142 |
fixes n :: nat |
143 |
assumes m: "m \<noteq> 0" and am: "[a^m = 1] (mod n)" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
144 |
shows "coprime a n" |
66305 | 145 |
proof - |
146 |
consider "n = 1" | "n = 0" | "n > 1" by arith |
|
147 |
then show ?thesis |
|
148 |
proof cases |
|
149 |
case 1 |
|
150 |
then show ?thesis by simp |
|
151 |
next |
|
152 |
case 2 |
|
153 |
with am m show ?thesis |
|
66888 | 154 |
by simp |
66305 | 155 |
next |
156 |
case 3 |
|
157 |
from m obtain m' where m': "m = Suc m'" by (cases m) blast+ |
|
158 |
have "d = 1" if d: "d dvd a" "d dvd n" for d |
|
159 |
proof - |
|
160 |
from am mod_less[OF \<open>n > 1\<close>] have am1: "a^m mod n = 1" |
|
66888 | 161 |
by (simp add: cong_def) |
66305 | 162 |
from dvd_mult2[OF d(1), of "a^m'"] have dam: "d dvd a^m" |
163 |
by (simp add: m') |
|
164 |
from dvd_mod_iff[OF d(2), of "a^m"] dam am1 show ?thesis |
|
165 |
by simp |
|
166 |
qed |
|
167 |
then show ?thesis by blast |
|
168 |
qed |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
169 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
170 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
171 |
lemma lucas_weak: |
66305 | 172 |
fixes n :: nat |
173 |
assumes n: "n \<ge> 2" |
|
174 |
and an: "[a ^ (n - 1) = 1] (mod n)" |
|
175 |
and nm: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
176 |
shows "prime n" |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
177 |
proof (rule totient_imp_prime) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
178 |
show "totient n = n - 1" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
179 |
proof (rule ccontr) |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
180 |
have "[a ^ totient n = 1] (mod n)" |
66305 | 181 |
by (rule euler_theorem, rule lucas_coprime_lemma [of "n - 1"]) (use n an in auto) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
182 |
moreover assume "totient n \<noteq> n - 1" |
66305 | 183 |
then have "totient n > 0" "totient n < n - 1" |
184 |
using \<open>n \<ge> 2\<close> and totient_less[of n] by simp_all |
|
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
185 |
ultimately show False |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
186 |
using nm by auto |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
187 |
qed |
66305 | 188 |
qed (use n in auto) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
189 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
190 |
lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))" |
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
191 |
by (metis ex_least_nat_le not_less0) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
192 |
|
66305 | 193 |
lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> P (Least P) \<and> (\<forall>m < (Least P). \<not> P m)" |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
194 |
(is "?lhs \<longleftrightarrow> ?rhs") |
66305 | 195 |
proof |
196 |
show ?lhs if ?rhs |
|
197 |
using that by blast |
|
198 |
show ?rhs if ?lhs |
|
199 |
proof - |
|
200 |
from \<open>?lhs\<close> obtain n where n: "P n" by blast |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
201 |
let ?x = "Least P" |
66305 | 202 |
have "\<not> P m" if "m < ?x" for m |
203 |
by (rule not_less_Least[OF that]) |
|
204 |
with LeastI_ex[OF \<open>?lhs\<close>] show ?thesis |
|
205 |
by blast |
|
206 |
qed |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
207 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
208 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
209 |
theorem lucas: |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
210 |
assumes n2: "n \<ge> 2" and an1: "[a^(n - 1) = 1] (mod n)" |
66305 | 211 |
and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> [a^((n - 1) div p) \<noteq> 1] (mod n)" |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
212 |
shows "prime n" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
213 |
proof- |
66305 | 214 |
from n2 have n01: "n \<noteq> 0" "n \<noteq> 1" "n - 1 \<noteq> 0" |
215 |
by arith+ |
|
216 |
from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" |
|
217 |
by simp |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
218 |
from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1 |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
219 |
have an: "coprime a n" "coprime (a^(n - 1)) n" |
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62349
diff
changeset
|
220 |
by (auto simp add: coprime_exp gcd.commute) |
66305 | 221 |
have False if H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m") |
222 |
proof - |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
223 |
from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where |
66305 | 224 |
m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k" |
225 |
by blast |
|
226 |
have False if nm1: "(n - 1) mod m > 0" |
|
227 |
proof - |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
228 |
from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
229 |
let ?y = "a^ ((n - 1) div m * m)" |
64242
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
63905
diff
changeset
|
230 |
note mdeq = div_mult_mod_eq[of "(n - 1)" m] |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
231 |
have yn: "coprime ?y n" |
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62349
diff
changeset
|
232 |
by (metis an(1) coprime_exp gcd.commute) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
233 |
have "?y mod n = (a^m)^((n - 1) div m) mod n" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
234 |
by (simp add: algebra_simps power_mult) |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
235 |
also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
236 |
using power_mod[of "a^m" n "(n - 1) div m"] by simp |
66888 | 237 |
also have "\<dots> = 1" using m(3)[unfolded cong_def onen] onen |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
238 |
by (metis power_one) |
66305 | 239 |
finally have *: "?y mod n = 1" . |
240 |
have **: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)" |
|
66888 | 241 |
using an1[unfolded cong_def onen] onen |
64242
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
63905
diff
changeset
|
242 |
div_mult_mod_eq[of "(n - 1)" m, symmetric] |
66888 | 243 |
by (simp add:power_add[symmetric] cong_def * del: One_nat_def) |
66305 | 244 |
have "[a ^ ((n - 1) mod m) = 1] (mod n)" |
245 |
by (metis cong_mult_rcancel_nat mult.commute ** yn) |
|
246 |
with m(4)[rule_format, OF th0] nm1 |
|
247 |
less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] show ?thesis |
|
248 |
by blast |
|
249 |
qed |
|
250 |
then have "(n - 1) mod m = 0" by auto |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
251 |
then have mn: "m dvd n - 1" by presburger |
66305 | 252 |
then obtain r where r: "n - 1 = m * r" |
253 |
unfolding dvd_def by blast |
|
254 |
from n01 r m(2) have r01: "r \<noteq> 0" "r \<noteq> 1" by auto |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
255 |
obtain p where p: "prime p" "p dvd r" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
256 |
by (metis prime_factor_nat r01(2)) |
66305 | 257 |
then have th: "prime p \<and> p dvd n - 1" |
258 |
unfolding r by (auto intro: dvd_mult) |
|
259 |
from r have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
260 |
by (simp add: power_mult) |
66305 | 261 |
also have "\<dots> = (a^(m*(r div p))) mod n" |
262 |
using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] by simp |
|
263 |
also have "\<dots> = ((a^m)^(r div p)) mod n" |
|
264 |
by (simp add: power_mult) |
|
265 |
also have "\<dots> = ((a^m mod n)^(r div p)) mod n" |
|
266 |
using power_mod .. |
|
267 |
also from m(3) onen have "\<dots> = 1" |
|
66888 | 268 |
by (simp add: cong_def) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
269 |
finally have "[(a ^ ((n - 1) div p))= 1] (mod n)" |
66888 | 270 |
using onen by (simp add: cong_def) |
66305 | 271 |
with pn th show ?thesis by blast |
272 |
qed |
|
273 |
then have "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" |
|
274 |
by blast |
|
275 |
then show ?thesis by (rule lucas_weak[OF n2 an1]) |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
276 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
277 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
278 |
|
66305 | 279 |
subsection \<open>Definition of the order of a number mod n (0 in non-coprime case)\<close> |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
280 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
281 |
definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
282 |
|
66305 | 283 |
text \<open>This has the expected properties.\<close> |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
284 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
285 |
lemma coprime_ord: |
66305 | 286 |
fixes n::nat |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
287 |
assumes "coprime n a" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
288 |
shows "ord n a > 0 \<and> [a ^(ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> [a^ m \<noteq> 1] (mod n))" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
289 |
proof- |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
290 |
let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)" |
66305 | 291 |
from bigger_prime[of a] obtain p where p: "prime p" "a < p" |
292 |
by blast |
|
293 |
from assms have o: "ord n a = Least ?P" |
|
294 |
by (simp add: ord_def) |
|
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
295 |
have ex: "\<exists>m>0. ?P m" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
296 |
proof (cases "n \<ge> 2") |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
297 |
case True |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
298 |
moreover from assms have "coprime a n" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
299 |
by (simp add: ac_simps) |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
300 |
then have "[a ^ totient n = 1] (mod n)" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
301 |
by (rule euler_theorem) |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
302 |
ultimately show ?thesis |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
303 |
by (auto intro: exI [where x = "totient n"]) |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
304 |
next |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
305 |
case False |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
306 |
then have "n = 0 \<or> n = 1" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
307 |
by auto |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
308 |
with assms show ?thesis |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
309 |
by auto |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
310 |
qed |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
311 |
from nat_exists_least_iff'[of ?P] ex assms show ?thesis |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
312 |
unfolding o[symmetric] by auto |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
313 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
314 |
|
66305 | 315 |
text \<open>With the special value \<open>0\<close> for non-coprime case, it's more convenient.\<close> |
316 |
lemma ord_works: "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> \<not> [a^ m = 1] (mod n))" |
|
317 |
for n :: nat |
|
66888 | 318 |
by (cases "coprime n a") (use coprime_ord[of n a] in \<open>auto simp add: ord_def cong_def\<close>) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
319 |
|
66305 | 320 |
lemma ord: "[a^(ord n a) = 1] (mod n)" |
321 |
for n :: nat |
|
322 |
using ord_works by blast |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
323 |
|
66305 | 324 |
lemma ord_minimal: "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> \<not> [a^m = 1] (mod n)" |
325 |
for n :: nat |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
326 |
using ord_works by blast |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
327 |
|
66305 | 328 |
lemma ord_eq_0: "ord n a = 0 \<longleftrightarrow> \<not> coprime n a" |
329 |
for n :: nat |
|
330 |
by (cases "coprime n a") (simp add: coprime_ord, simp add: ord_def) |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
331 |
|
66305 | 332 |
lemma divides_rexp: "x dvd y \<Longrightarrow> x dvd (y ^ Suc n)" |
333 |
for x y :: nat |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
334 |
by (simp add: dvd_mult2[of x y]) |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
335 |
|
66305 | 336 |
lemma ord_divides:"[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d" |
337 |
(is "?lhs \<longleftrightarrow> ?rhs") |
|
338 |
for n :: nat |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
339 |
proof |
66305 | 340 |
assume ?rhs |
341 |
then obtain k where "d = ord n a * k" |
|
342 |
unfolding dvd_def by blast |
|
343 |
then have "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)" |
|
66888 | 344 |
by (simp add : cong_def power_mult power_mod) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
345 |
also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)" |
66888 | 346 |
using ord[of a n, unfolded cong_def] |
347 |
by (simp add: cong_def power_mod) |
|
66305 | 348 |
finally show ?lhs . |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
349 |
next |
66305 | 350 |
assume ?lhs |
351 |
show ?rhs |
|
352 |
proof (cases "coprime n a") |
|
353 |
case prem: False |
|
354 |
then have o: "ord n a = 0" by (simp add: ord_def) |
|
355 |
show ?thesis |
|
356 |
proof (cases d) |
|
357 |
case 0 |
|
66888 | 358 |
with o prem show ?thesis by (simp add: cong_def) |
66305 | 359 |
next |
360 |
case (Suc d') |
|
361 |
then have d0: "d \<noteq> 0" by simp |
|
362 |
from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto |
|
363 |
from \<open>?lhs\<close> obtain q1 q2 where q12: "a ^ d + n * q1 = 1 + n * q2" |
|
364 |
by (metis prem d0 gcd.commute lucas_coprime_lemma) |
|
365 |
then have "a ^ d + n * q1 - n * q2 = 1" by simp |
|
366 |
with dvd_diff_nat [OF dvd_add [OF divides_rexp]] dvd_mult2 Suc p have "p dvd 1" |
|
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
367 |
by metis |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
368 |
with p(3) have False by simp |
66305 | 369 |
then show ?thesis .. |
370 |
qed |
|
371 |
next |
|
372 |
case H: True |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
373 |
let ?o = "ord n a" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
374 |
let ?q = "d div ord n a" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
375 |
let ?r = "d mod ord n a" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
376 |
have eqo: "[(a^?o)^?q = 1] (mod n)" |
66888 | 377 |
using cong_pow ord_works by fastforce |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
378 |
from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0) |
66305 | 379 |
then have op: "?o > 0" by simp |
380 |
from div_mult_mod_eq[of d "ord n a"] \<open>?lhs\<close> |
|
381 |
have "[a^(?o*?q + ?r) = 1] (mod n)" |
|
66888 | 382 |
by (simp add: cong_def mult.commute) |
66305 | 383 |
then have "[(a^?o)^?q * (a^?r) = 1] (mod n)" |
66888 | 384 |
by (simp add: cong_def power_mult[symmetric] power_add[symmetric]) |
66305 | 385 |
then have th: "[a^?r = 1] (mod n)" |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
386 |
using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n] |
66888 | 387 |
by (simp add: cong_def del: One_nat_def) (metis mod_mult_left_eq nat_mult_1) |
66305 | 388 |
show ?thesis |
389 |
proof (cases "?r = 0") |
|
390 |
case True |
|
391 |
then show ?thesis by (simp add: dvd_eq_mod_eq_0) |
|
392 |
next |
|
393 |
case False |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
394 |
with mod_less_divisor[OF op, of d] have r0o:"?r >0 \<and> ?r < ?o" by simp |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
395 |
from conjunct2[OF ord_works[of a n], rule_format, OF r0o] th |
66305 | 396 |
show ?thesis by blast |
397 |
qed |
|
398 |
qed |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
399 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
400 |
|
66305 | 401 |
lemma order_divides_totient: "ord n a dvd totient n" if "coprime n a" |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
402 |
by (metis euler_theorem gcd.commute ord_divides that) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
403 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
404 |
lemma order_divides_expdiff: |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
405 |
fixes n::nat and a::nat assumes na: "coprime n a" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
406 |
shows "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))" |
66305 | 407 |
proof - |
408 |
have th: "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))" |
|
409 |
if na: "coprime n a" and ed: "(e::nat) \<le> d" |
|
410 |
for n a d e :: nat |
|
411 |
proof - |
|
412 |
from na ed have "\<exists>c. d = e + c" by presburger |
|
413 |
then obtain c where c: "d = e + c" .. |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
414 |
from na have an: "coprime a n" |
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60526
diff
changeset
|
415 |
by (metis gcd.commute) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
416 |
have aen: "coprime (a^e) n" |
66305 | 417 |
by (metis coprime_exp gcd.commute na) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
418 |
have acn: "coprime (a^c) n" |
66305 | 419 |
by (metis coprime_exp gcd.commute na) |
420 |
from c have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)" |
|
421 |
by simp |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
422 |
also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add) |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
423 |
also have "\<dots> \<longleftrightarrow> [a ^ c = 1] (mod n)" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
424 |
using cong_mult_lcancel_nat [OF aen, of "a^c" "a^0"] by simp |
66305 | 425 |
also have "\<dots> \<longleftrightarrow> ord n a dvd c" |
426 |
by (simp only: ord_divides) |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
427 |
also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)" |
66888 | 428 |
by (auto simp add: cong_altdef_nat) |
66305 | 429 |
finally show ?thesis |
430 |
using c by simp |
|
431 |
qed |
|
432 |
consider "e \<le> d" | "d \<le> e" by arith |
|
433 |
then show ?thesis |
|
434 |
proof cases |
|
435 |
case 1 |
|
436 |
with na show ?thesis by (rule th) |
|
437 |
next |
|
438 |
case 2 |
|
439 |
from th[OF na this] show ?thesis |
|
66888 | 440 |
by (metis cong_sym) |
66305 | 441 |
qed |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
442 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
443 |
|
66305 | 444 |
|
445 |
subsection \<open>Another trivial primality characterization\<close> |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
446 |
|
66305 | 447 |
lemma prime_prime_factor: "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" |
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
448 |
(is "?lhs \<longleftrightarrow> ?rhs") |
66305 | 449 |
for n :: nat |
450 |
proof (cases "n = 0 \<or> n = 1") |
|
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
451 |
case True |
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
452 |
then show ?thesis |
63633 | 453 |
by (metis bigger_prime dvd_0_right not_prime_1 not_prime_0) |
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
454 |
next |
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
455 |
case False |
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
456 |
show ?thesis |
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
457 |
proof |
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
458 |
assume "prime n" |
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
459 |
then show ?rhs |
66305 | 460 |
by (metis not_prime_1 prime_nat_iff) |
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
461 |
next |
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
462 |
assume ?rhs |
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
463 |
with False show "prime n" |
63633 | 464 |
by (auto simp: prime_nat_iff) (metis One_nat_def prime_factor_nat prime_nat_iff) |
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
465 |
qed |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
466 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
467 |
|
66305 | 468 |
lemma prime_divisor_sqrt: "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)" |
469 |
for n :: nat |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
470 |
proof - |
66305 | 471 |
consider "n = 0" | "n = 1" | "n \<noteq> 0" "n \<noteq> 1" by blast |
472 |
then show ?thesis |
|
473 |
proof cases |
|
474 |
case 1 |
|
475 |
then show ?thesis by simp |
|
476 |
next |
|
477 |
case 2 |
|
478 |
then show ?thesis by simp |
|
479 |
next |
|
480 |
case n: 3 |
|
481 |
then have np: "n > 1" by arith |
|
482 |
{ |
|
483 |
fix d |
|
484 |
assume d: "d dvd n" "d\<^sup>2 \<le> n" |
|
485 |
and H: "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n" |
|
486 |
from H d have d1n: "d = 1 \<or> d = n" by blast |
|
487 |
then have "d = 1" |
|
488 |
proof |
|
489 |
assume dn: "d = n" |
|
490 |
from n have "n\<^sup>2 > n * 1" |
|
491 |
by (simp add: power2_eq_square) |
|
492 |
with dn d(2) show ?thesis by simp |
|
493 |
qed |
|
494 |
} |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
495 |
moreover |
66305 | 496 |
{ |
497 |
fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
498 |
from d n have "d \<noteq> 0" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
499 |
by (metis dvd_0_left_iff) |
66305 | 500 |
then have dp: "d > 0" by simp |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
501 |
from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
502 |
from n dp e have ep:"e > 0" by simp |
66305 | 503 |
from dp ep have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n" |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
504 |
by (auto simp add: e power2_eq_square mult_le_cancel_left) |
66305 | 505 |
then have "d = 1 \<or> d = n" |
506 |
proof |
|
507 |
assume "d\<^sup>2 \<le> n" |
|
508 |
with H[rule_format, of d] d have "d = 1" by blast |
|
509 |
then show ?thesis .. |
|
510 |
next |
|
511 |
assume h: "e\<^sup>2 \<le> n" |
|
512 |
from e have "e dvd n" by (simp add: dvd_def mult.commute) |
|
513 |
with H[rule_format, of e] h have "e = 1" by simp |
|
514 |
with e have "d = n" by simp |
|
515 |
then show ?thesis .. |
|
516 |
qed |
|
517 |
} |
|
518 |
ultimately show ?thesis |
|
519 |
unfolding prime_nat_iff using np n(2) by blast |
|
520 |
qed |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
521 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
522 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
523 |
lemma prime_prime_factor_sqrt: |
66305 | 524 |
"prime (n::nat) \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> (\<nexists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)" |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
525 |
(is "?lhs \<longleftrightarrow>?rhs") |
66305 | 526 |
proof - |
527 |
consider "n = 0" | "n = 1" | "n \<noteq> 0" "n \<noteq> 1" |
|
528 |
by blast |
|
529 |
then show ?thesis |
|
530 |
proof cases |
|
531 |
case 1 |
|
532 |
then show ?thesis by (metis not_prime_0) |
|
533 |
next |
|
534 |
case 2 |
|
535 |
then show ?thesis by (metis not_prime_1) |
|
536 |
next |
|
537 |
case n: 3 |
|
538 |
show ?thesis |
|
539 |
proof |
|
540 |
assume ?lhs |
|
541 |
from this[unfolded prime_divisor_sqrt] n show ?rhs |
|
542 |
by (metis prime_prime_factor) |
|
543 |
next |
|
544 |
assume ?rhs |
|
545 |
{ |
|
546 |
fix d |
|
547 |
assume d: "d dvd n" "d\<^sup>2 \<le> n" "d \<noteq> 1" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
548 |
then obtain p where p: "prime p" "p dvd d" |
66305 | 549 |
by (metis prime_factor_nat) |
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
550 |
from d(1) n have dp: "d > 0" |
66305 | 551 |
by (metis dvd_0_left neq0_conv) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
552 |
from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2) |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
553 |
have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith |
66305 | 554 |
with \<open>?rhs\<close> n p(1) dvd_trans[OF p(2) d(1)] have False |
555 |
by blast |
|
556 |
} |
|
557 |
with n prime_divisor_sqrt show ?lhs by auto |
|
558 |
qed |
|
559 |
qed |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
560 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
561 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
562 |
|
66305 | 563 |
subsection \<open>Pocklington theorem\<close> |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
564 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
565 |
lemma pocklington_lemma: |
66305 | 566 |
fixes p :: nat |
567 |
assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r" |
|
568 |
and an: "[a^ (n - 1) = 1] (mod n)" |
|
569 |
and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n" |
|
570 |
and pp: "prime p" and pn: "p dvd n" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
571 |
shows "[p = 1] (mod q)" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
572 |
proof - |
66305 | 573 |
have p01: "p \<noteq> 0" "p \<noteq> 1" |
574 |
using pp by (auto intro: prime_gt_0_nat) |
|
575 |
obtain k where k: "a ^ (q * r) - 1 = n * k" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
576 |
by (metis an cong_to_1_nat dvd_def nqr) |
66305 | 577 |
from pn[unfolded dvd_def] obtain l where l: "n = p * l" |
578 |
by blast |
|
579 |
have a0: "a \<noteq> 0" |
|
580 |
proof |
|
581 |
assume "a = 0" |
|
582 |
with n have "a^ (n - 1) = 0" |
|
583 |
by (simp add: power_0_left) |
|
584 |
with n an mod_less[of 1 n] show False |
|
66888 | 585 |
by (simp add: power_0_left cong_def) |
66305 | 586 |
qed |
587 |
with n nqr have aqr0: "a ^ (q * r) \<noteq> 0" |
|
588 |
by simp |
|
589 |
then have "(a ^ (q * r) - 1) + 1 = a ^ (q * r)" |
|
590 |
by simp |
|
591 |
with k l have "a ^ (q * r) = p * l * k + 1" |
|
592 |
by simp |
|
593 |
then have "a ^ (r * q) + p * 0 = 1 + p * (l * k)" |
|
594 |
by (simp add: ac_simps) |
|
595 |
then have odq: "ord p (a^r) dvd q" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
596 |
unfolding ord_divides[symmetric] power_mult[symmetric] |
66305 | 597 |
by (metis an cong_dvd_modulus_nat mult.commute nqr pn) |
598 |
from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" |
|
599 |
by blast |
|
600 |
have d1: "d = 1" |
|
601 |
proof (rule ccontr) |
|
602 |
assume d1: "d \<noteq> 1" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
603 |
obtain P where P: "prime P" "P dvd d" |
66305 | 604 |
by (metis d1 prime_factor_nat) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
605 |
from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
606 |
from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
607 |
from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast |
66305 | 608 |
from P(1) have P0: "P \<noteq> 0" |
609 |
by (metis not_prime_0) |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
610 |
from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
611 |
from d s t P0 have s': "ord p (a^r) * t = s" |
66305 | 612 |
by (metis mult.commute mult_cancel1 mult.assoc) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
613 |
have "ord p (a^r) * t*r = r * ord p (a^r) * t" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55370
diff
changeset
|
614 |
by (metis mult.assoc mult.commute) |
66305 | 615 |
then have exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t" |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
616 |
by (simp only: power_mult) |
66305 | 617 |
then have "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)" |
66888 | 618 |
by (metis cong_pow ord power_one) |
66305 | 619 |
then have pd0: "p dvd a^(ord p (a^r) * t*r) - 1" |
620 |
by (metis cong_to_1_nat exps) |
|
621 |
from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" |
|
622 |
using P0 by simp |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
623 |
with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp |
66305 | 624 |
with p01 pn pd0 coprime_common_divisor_nat show False |
625 |
by auto |
|
626 |
qed |
|
627 |
with d have o: "ord p (a^r) = q" by simp |
|
628 |
from pp totient_prime [of p] have totient_eq: "totient p = p - 1" |
|
629 |
by simp |
|
630 |
{ |
|
631 |
fix d |
|
632 |
assume d: "d dvd p" "d dvd a" "d \<noteq> 1" |
|
63633 | 633 |
from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
634 |
from n have "n \<noteq> 0" by simp |
62349
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
635 |
then have False using d dp pn |
66305 | 636 |
by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma) |
637 |
} |
|
638 |
then have cpa: "coprime p a" by auto |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
639 |
have arp: "coprime (a^r) p" |
66305 | 640 |
by (metis coprime_exp cpa gcd.commute) |
641 |
from euler_theorem [OF arp, simplified ord_divides] o totient_eq have "q dvd (p - 1)" |
|
642 |
by simp |
|
643 |
then obtain d where d:"p - 1 = q * d" |
|
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset
|
644 |
unfolding dvd_def by blast |
66305 | 645 |
have "p \<noteq> 0" |
646 |
by (metis p01(1)) |
|
647 |
with d have "p + q * 0 = 1 + q * d" by simp |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
648 |
then show ?thesis |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55370
diff
changeset
|
649 |
by (metis cong_iff_lin_nat mult.commute) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
650 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
651 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
652 |
theorem pocklington: |
66305 | 653 |
assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r" and sqr: "n \<le> q\<^sup>2" |
654 |
and an: "[a^ (n - 1) = 1] (mod n)" |
|
655 |
and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
656 |
shows "prime n" |
66305 | 657 |
unfolding prime_prime_factor_sqrt[of n] |
658 |
proof - |
|
659 |
let ?ths = "n \<noteq> 0 \<and> n \<noteq> 1 \<and> (\<nexists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)" |
|
660 |
from n have n01: "n \<noteq> 0" "n \<noteq> 1" by arith+ |
|
661 |
{ |
|
662 |
fix p |
|
663 |
assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n" |
|
664 |
from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" |
|
665 |
by (simp add: power2_eq_square) |
|
666 |
then have pq: "p \<le> q" |
|
667 |
by (metis le0 power_le_imp_le_base) |
|
668 |
from pocklington_lemma[OF n nqr an aq p(1,2)] have *: "q dvd p - 1" |
|
669 |
by (metis cong_to_1_nat) |
|
670 |
have "p - 1 \<noteq> 0" |
|
671 |
using prime_ge_2_nat [OF p(1)] by arith |
|
672 |
with pq * have False |
|
673 |
by (simp add: nat_dvd_not_less) |
|
674 |
} |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
675 |
with n01 show ?ths by blast |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
676 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
677 |
|
66305 | 678 |
text \<open>Variant for application, to separate the exponentiation.\<close> |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
679 |
lemma pocklington_alt: |
66305 | 680 |
assumes n: "n \<ge> 2" and nqr: "n - 1 = q * r" and sqr: "n \<le> q\<^sup>2" |
681 |
and an: "[a^ (n - 1) = 1] (mod n)" |
|
682 |
and aq: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> (\<exists>b. [a^((n - 1) div p) = b] (mod n) \<and> coprime (b - 1) n)" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
683 |
shows "prime n" |
66305 | 684 |
proof - |
685 |
{ |
|
686 |
fix p |
|
687 |
assume p: "prime p" "p dvd q" |
|
688 |
from aq[rule_format] p obtain b where b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n" |
|
689 |
by blast |
|
690 |
have a0: "a \<noteq> 0" |
|
691 |
proof |
|
692 |
assume a0: "a = 0" |
|
693 |
from n an have "[0 = 1] (mod n)" |
|
694 |
unfolding a0 power_0_left by auto |
|
695 |
then show False |
|
66888 | 696 |
using n by (simp add: cong_def dvd_eq_mod_eq_0[symmetric]) |
66305 | 697 |
qed |
698 |
then have a1: "a \<ge> 1" by arith |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
699 |
from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n - 1) div p)" . |
66305 | 700 |
have b0: "b \<noteq> 0" |
701 |
proof |
|
702 |
assume b0: "b = 0" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
703 |
from p(2) nqr have "(n - 1) mod p = 0" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
704 |
by (metis mod_0 mod_mod_cancel mod_mult_self1_is_0) |
64242
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
63905
diff
changeset
|
705 |
with div_mult_mod_eq[of "n - 1" p] |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
706 |
have "(n - 1) div p * p= n - 1" by auto |
66305 | 707 |
then have eq: "(a^((n - 1) div p))^p = a^(n - 1)" |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
708 |
by (simp only: power_mult[symmetric]) |
66305 | 709 |
have "p - 1 \<noteq> 0" |
710 |
using prime_ge_2_nat [OF p(1)] by arith |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
711 |
then have pS: "Suc (p - 1) = p" by arith |
66305 | 712 |
from b have d: "n dvd a^((n - 1) div p)" |
713 |
unfolding b0 by auto |
|
66888 | 714 |
from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_iff [OF an] n show False |
66305 | 715 |
by simp |
716 |
qed |
|
717 |
then have b1: "b \<ge> 1" by arith |
|
66888 | 718 |
from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym [OF b(1)] cong_refl [of 1] b1]] |
66305 | 719 |
ath b1 b nqr |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
720 |
have "coprime (a ^ ((n - 1) div p) - 1) n" |
66305 | 721 |
by simp |
722 |
} |
|
723 |
then have "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n " |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
724 |
by blast |
66305 | 725 |
then show ?thesis by (rule pocklington[OF n nqr sqr an]) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
726 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
727 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
728 |
|
66305 | 729 |
subsection \<open>Prime factorizations\<close> |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
730 |
|
55370 | 731 |
(* FIXME some overlap with material in UniqueFactorization, class unique_factorization *) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
732 |
|
66305 | 733 |
definition "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)" |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
734 |
|
66305 | 735 |
lemma primefact: |
736 |
fixes n :: nat |
|
737 |
assumes n: "n \<noteq> 0" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
738 |
shows "\<exists>ps. primefact ps n" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
739 |
proof - |
66305 | 740 |
obtain xs where xs: "mset xs = prime_factorization n" |
741 |
using ex_mset [of "prime_factorization n"] by blast |
|
742 |
from assms have "n = prod_mset (prime_factorization n)" |
|
63830 | 743 |
by (simp add: prod_mset_prime_factorization) |
744 |
also have "\<dots> = prod_mset (mset xs)" by (simp add: xs) |
|
66305 | 745 |
also have "\<dots> = foldr op * xs 1" by (induct xs) simp_all |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
746 |
finally have "foldr op * xs 1 = n" .. |
66305 | 747 |
moreover from xs have "\<forall>p\<in>#mset xs. prime p" by auto |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
748 |
ultimately have "primefact xs n" by (auto simp: primefact_def) |
66305 | 749 |
then show ?thesis .. |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
750 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
751 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
752 |
lemma primefact_contains: |
66305 | 753 |
fixes p :: nat |
754 |
assumes pf: "primefact ps n" |
|
755 |
and p: "prime p" |
|
756 |
and pn: "p dvd n" |
|
757 |
shows "p \<in> set ps" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
758 |
using pf p pn |
66305 | 759 |
proof (induct ps arbitrary: p n) |
760 |
case Nil |
|
761 |
then show ?case by (auto simp: primefact_def) |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
762 |
next |
66305 | 763 |
case (Cons q qs) |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
764 |
from Cons.prems[unfolded primefact_def] |
66305 | 765 |
have q: "prime q" "q * foldr op * qs 1 = n" "\<forall>p \<in>set qs. prime p" |
766 |
and p: "prime p" "p dvd q * foldr op * qs 1" |
|
767 |
by simp_all |
|
768 |
consider "p dvd q" | "p dvd foldr op * qs 1" |
|
769 |
by (metis p prime_dvd_mult_eq_nat) |
|
770 |
then show ?case |
|
771 |
proof cases |
|
772 |
case 1 |
|
773 |
with p(1) q(1) have "p = q" |
|
774 |
unfolding prime_nat_iff by auto |
|
775 |
then show ?thesis by simp |
|
776 |
next |
|
777 |
case prem: 2 |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
778 |
from q(3) have pqs: "primefact qs (foldr op * qs 1)" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
779 |
by (simp add: primefact_def) |
66305 | 780 |
from Cons.hyps[OF pqs p(1) prem] show ?thesis by simp |
781 |
qed |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
782 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
783 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
784 |
lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
785 |
by (auto simp add: primefact_def list_all_iff) |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
786 |
|
66305 | 787 |
text \<open>Variant of Lucas theorem.\<close> |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
788 |
lemma lucas_primefact: |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
789 |
assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)" |
66305 | 790 |
and psn: "foldr op * ps 1 = n - 1" |
791 |
and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
792 |
shows "prime n" |
66305 | 793 |
proof - |
794 |
{ |
|
795 |
fix p |
|
796 |
assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
797 |
from psn psp have psn1: "primefact ps (n - 1)" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
798 |
by (auto simp add: list_all_iff primefact_variant) |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
799 |
from p(3) primefact_contains[OF psn1 p(1,2)] psp |
66305 | 800 |
have False by (induct ps) auto |
801 |
} |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
802 |
with lucas[OF n an] show ?thesis by blast |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
803 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
804 |
|
66305 | 805 |
text \<open>Variant of Pocklington theorem.\<close> |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
806 |
lemma pocklington_primefact: |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
807 |
assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2" |
66305 | 808 |
and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q" |
809 |
and bqn: "(b^q) mod n = 1" |
|
810 |
and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
811 |
shows "prime n" |
66305 | 812 |
proof - |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
813 |
from bqn psp qrn |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
814 |
have bqn: "a ^ (n - 1) mod n = 1" |
66305 | 815 |
and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps" |
816 |
unfolding arnb[symmetric] power_mod |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
817 |
by (simp_all add: power_mult[symmetric] algebra_simps) |
66305 | 818 |
from n have n0: "n > 0" by arith |
64242
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
63905
diff
changeset
|
819 |
from div_mult_mod_eq[of "a^(n - 1)" n] |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
820 |
mod_less_divisor[OF n0, of "a^(n - 1)"] |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
821 |
have an1: "[a ^ (n - 1) = 1] (mod n)" |
66888 | 822 |
by (metis bqn cong_def mod_mod_trivial) |
66305 | 823 |
have "coprime (a ^ ((n - 1) div p) - 1) n" if p: "prime p" "p dvd q" for p |
824 |
proof - |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
825 |
from psp psq have pfpsq: "primefact ps q" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
826 |
by (auto simp add: primefact_variant list_all_iff) |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
827 |
from psp primefact_contains[OF pfpsq p] |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
828 |
have p': "coprime (a ^ (r * (q div p)) mod n - 1) n" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
829 |
by (simp add: list_all_iff) |
66305 | 830 |
from p prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p = Suc (p - 1)" |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
831 |
by auto |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
832 |
from div_mult1_eq[of r q p] p(2) |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
833 |
have eq1: "r* (q div p) = (n - 1) div p" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55370
diff
changeset
|
834 |
unfolding qrn[symmetric] dvd_eq_mod_eq_0 by (simp add: mult.commute) |
66305 | 835 |
have ath: "a \<le> b \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> 1 \<le> a \<and> 1 \<le> b" for a b :: nat |
836 |
by arith |
|
837 |
{ |
|
838 |
assume "a ^ ((n - 1) div p) mod n = 0" |
|
839 |
then obtain s where s: "a ^ ((n - 1) div p) = n * s" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
840 |
unfolding mod_eq_0_iff by blast |
66305 | 841 |
then have eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp |
842 |
from qrn[symmetric] have qn1: "q dvd n - 1" |
|
843 |
by (auto simp: dvd_def) |
|
844 |
from dvd_trans[OF p(2) qn1] have npp: "(n - 1) div p * p = n - 1" |
|
845 |
by simp |
|
846 |
with eq0 have "a ^ (n - 1) = (n * s) ^ p" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
847 |
by (simp add: power_mult[symmetric]) |
66305 | 848 |
with bqn p01 have "1 = (n * s)^(Suc (p - 1)) mod n" |
849 |
by simp |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55370
diff
changeset
|
850 |
also have "\<dots> = 0" by (simp add: mult.assoc) |
66305 | 851 |
finally have False by simp |
852 |
} |
|
853 |
then have *: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto |
|
854 |
have "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)" |
|
66888 | 855 |
by (simp add: cong_def) |
66305 | 856 |
with ath[OF mod_less_eq_dividend *] |
857 |
have "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)" |
|
66888 | 858 |
by (simp add: cong_diff_nat) |
66305 | 859 |
then show ?thesis |
860 |
by (metis cong_imp_coprime_nat eq1 p') |
|
861 |
qed |
|
862 |
with pocklington[OF n qrn[symmetric] nq2 an1] show ?thesis |
|
863 |
by blast |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
864 |
qed |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
865 |
|
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
866 |
end |