author | wenzelm |
Sun, 11 Sep 2016 00:14:37 +0200 | |
changeset 63833 | 4aaeb9427c96 |
parent 62481 | b5d8e57826df |
child 64242 | 93c6f0da5c70 |
permissions | -rw-r--r-- |
38159 | 1 |
(* Title: HOL/Old_Number_Theory/Pocklington.thy |
30488 | 2 |
Author: Amine Chaieb |
26126 | 3 |
*) |
4 |
||
61382 | 5 |
section \<open>Pocklington's Theorem for Primes\<close> |
26126 | 6 |
|
7 |
theory Pocklington |
|
38159 | 8 |
imports Primes |
26126 | 9 |
begin |
10 |
||
11 |
definition modeq:: "nat => nat => nat => bool" ("(1[_ = _] '(mod _'))") |
|
12 |
where "[a = b] (mod p) == ((a mod p) = (b mod p))" |
|
13 |
||
14 |
definition modneq:: "nat => nat => nat => bool" ("(1[_ \<noteq> _] '(mod _'))") |
|
15 |
where "[a \<noteq> b] (mod p) == ((a mod p) \<noteq> (b mod p))" |
|
16 |
||
17 |
lemma modeq_trans: |
|
18 |
"\<lbrakk> [a = b] (mod p); [b = c] (mod p) \<rbrakk> \<Longrightarrow> [a = c] (mod p)" |
|
19 |
by (simp add:modeq_def) |
|
20 |
||
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
21 |
lemma modeq_sym[sym]: |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
22 |
"[a = b] (mod p) \<Longrightarrow> [b = a] (mod p)" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
23 |
unfolding modeq_def by simp |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
24 |
|
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
25 |
lemma modneq_sym[sym]: |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
26 |
"[a \<noteq> b] (mod p) \<Longrightarrow> [b \<noteq> a] (mod p)" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
27 |
by (simp add: modneq_def) |
26126 | 28 |
|
29 |
lemma nat_mod_lemma: assumes xyn: "[x = y] (mod n)" and xy:"y \<le> x" |
|
30 |
shows "\<exists>q. x = y + n * q" |
|
27668 | 31 |
using xyn xy unfolding modeq_def using nat_mod_eq_lemma by blast |
26126 | 32 |
|
30488 | 33 |
lemma nat_mod[algebra]: "[x = y] (mod n) \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" |
27668 | 34 |
unfolding modeq_def nat_mod_eq_iff .. |
26126 | 35 |
|
36 |
(* Lemmas about previously defined terms. *) |
|
37 |
||
30488 | 38 |
lemma prime: "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p\<noteq>1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)" |
39 |
(is "?lhs \<longleftrightarrow> ?rhs") |
|
26126 | 40 |
proof- |
41 |
{assume "p=0 \<or> p=1" hence ?thesis using prime_0 prime_1 by (cases "p=0", simp_all)} |
|
42 |
moreover |
|
43 |
{assume p0: "p\<noteq>0" "p\<noteq>1" |
|
44 |
{assume H: "?lhs" |
|
45 |
{fix m assume m: "m > 0" "m < p" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
46 |
{assume "m=1" hence "coprime p m" by simp} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
47 |
moreover |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
48 |
{assume "p dvd m" hence "p \<le> m" using dvd_imp_le m by blast with m(2) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
49 |
have "coprime p m" by simp} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
50 |
ultimately have "coprime p m" using prime_coprime[OF H, of m] by blast} |
26126 | 51 |
hence ?rhs using p0 by auto} |
52 |
moreover |
|
53 |
{ assume H: "\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m" |
|
54 |
from prime_factor[OF p0(2)] obtain q where q: "prime q" "q dvd p" by blast |
|
55 |
from prime_ge_2[OF q(1)] have q0: "q > 0" by arith |
|
56 |
from dvd_imp_le[OF q(2)] p0 have qp: "q \<le> p" by arith |
|
57 |
{assume "q = p" hence ?lhs using q(1) by blast} |
|
58 |
moreover |
|
59 |
{assume "q\<noteq>p" with qp have qplt: "q < p" by arith |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
60 |
from H[rule_format, of q] qplt q0 have "coprime p q" by arith |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
61 |
with coprime_prime[of p q q] q have False by simp hence ?lhs by blast} |
26126 | 62 |
ultimately have ?lhs by blast} |
63 |
ultimately have ?thesis by blast} |
|
64 |
ultimately show ?thesis by (cases"p=0 \<or> p=1", auto) |
|
65 |
qed |
|
66 |
||
67 |
lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1" |
|
68 |
proof- |
|
69 |
have "{ m. 0 < m \<and> m < n } = {1..<n}" by auto |
|
70 |
thus ?thesis by simp |
|
71 |
qed |
|
72 |
||
73 |
lemma coprime_mod: assumes n: "n \<noteq> 0" shows "coprime (a mod n) n \<longleftrightarrow> coprime a n" |
|
74 |
using n dvd_mod_iff[of _ n a] by (auto simp add: coprime) |
|
75 |
||
76 |
(* Congruences. *) |
|
77 |
||
30488 | 78 |
lemma cong_mod_01[simp,presburger]: |
26126 | 79 |
"[x = y] (mod 0) \<longleftrightarrow> x = y" "[x = y] (mod 1)" "[x = 0] (mod n) \<longleftrightarrow> n dvd x" |
80 |
by (simp_all add: modeq_def, presburger) |
|
81 |
||
30488 | 82 |
lemma cong_sub_cases: |
26126 | 83 |
"[x = y] (mod n) \<longleftrightarrow> (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))" |
84 |
apply (auto simp add: nat_mod) |
|
85 |
apply (rule_tac x="q2" in exI) |
|
86 |
apply (rule_tac x="q1" in exI, simp) |
|
87 |
apply (rule_tac x="q2" in exI) |
|
88 |
apply (rule_tac x="q1" in exI, simp) |
|
89 |
apply (rule_tac x="q1" in exI) |
|
90 |
apply (rule_tac x="q2" in exI, simp) |
|
91 |
apply (rule_tac x="q1" in exI) |
|
92 |
apply (rule_tac x="q2" in exI, simp) |
|
93 |
done |
|
94 |
||
95 |
lemma cong_mult_lcancel: assumes an: "coprime a n" and axy:"[a * x = a * y] (mod n)" |
|
96 |
shows "[x = y] (mod n)" |
|
97 |
proof- |
|
98 |
{assume "a = 0" with an axy coprime_0'[of n] have ?thesis by (simp add: modeq_def) } |
|
99 |
moreover |
|
100 |
{assume az: "a\<noteq>0" |
|
101 |
{assume xy: "x \<le> y" hence axy': "a*x \<le> a*y" by simp |
|
102 |
with axy cong_sub_cases[of "a*x" "a*y" n] have "[a*(y - x) = 0] (mod n)" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
103 |
by (simp only: if_True diff_mult_distrib2) |
30488 | 104 |
hence th: "n dvd a*(y -x)" by simp |
26126 | 105 |
from coprime_divprod[OF th] an have "n dvd y - x" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
106 |
by (simp add: coprime_commute) |
26126 | 107 |
hence ?thesis using xy cong_sub_cases[of x y n] by simp} |
108 |
moreover |
|
30488 | 109 |
{assume H: "\<not>x \<le> y" hence xy: "y \<le> x" by arith |
26126 | 110 |
from H az have axy': "\<not> a*x \<le> a*y" by auto |
111 |
with axy H cong_sub_cases[of "a*x" "a*y" n] have "[a*(x - y) = 0] (mod n)" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
112 |
by (simp only: if_False diff_mult_distrib2) |
30488 | 113 |
hence th: "n dvd a*(x - y)" by simp |
26126 | 114 |
from coprime_divprod[OF th] an have "n dvd x - y" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
115 |
by (simp add: coprime_commute) |
26126 | 116 |
hence ?thesis using xy cong_sub_cases[of x y n] by simp} |
117 |
ultimately have ?thesis by blast} |
|
118 |
ultimately show ?thesis by blast |
|
119 |
qed |
|
120 |
||
121 |
lemma cong_mult_rcancel: assumes an: "coprime a n" and axy:"[x*a = y*a] (mod n)" |
|
122 |
shows "[x = y] (mod n)" |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
123 |
using cong_mult_lcancel[OF an axy[unfolded mult.commute[of _a]]] . |
26126 | 124 |
|
125 |
lemma cong_refl: "[x = x] (mod n)" by (simp add: modeq_def) |
|
126 |
||
127 |
lemma eq_imp_cong: "a = b \<Longrightarrow> [a = b] (mod n)" by (simp add: cong_refl) |
|
128 |
||
30488 | 129 |
lemma cong_commute: "[x = y] (mod n) \<longleftrightarrow> [y = x] (mod n)" |
26126 | 130 |
by (auto simp add: modeq_def) |
131 |
||
132 |
lemma cong_trans[trans]: "[x = y] (mod n) \<Longrightarrow> [y = z] (mod n) \<Longrightarrow> [x = z] (mod n)" |
|
133 |
by (simp add: modeq_def) |
|
134 |
||
135 |
lemma cong_add: assumes xx': "[x = x'] (mod n)" and yy':"[y = y'] (mod n)" |
|
136 |
shows "[x + y = x' + y'] (mod n)" |
|
137 |
proof- |
|
138 |
have "(x + y) mod n = (x mod n + y mod n) mod n" |
|
139 |
by (simp add: mod_add_left_eq[of x y n] mod_add_right_eq[of "x mod n" y n]) |
|
30488 | 140 |
also have "\<dots> = (x' mod n + y' mod n) mod n" using xx' yy' modeq_def by simp |
26126 | 141 |
also have "\<dots> = (x' + y') mod n" |
142 |
by (simp add: mod_add_left_eq[of x' y' n] mod_add_right_eq[of "x' mod n" y' n]) |
|
30488 | 143 |
finally show ?thesis unfolding modeq_def . |
26126 | 144 |
qed |
145 |
||
146 |
lemma cong_mult: assumes xx': "[x = x'] (mod n)" and yy':"[y = y'] (mod n)" |
|
147 |
shows "[x * y = x' * y'] (mod n)" |
|
148 |
proof- |
|
30488 | 149 |
have "(x * y) mod n = (x mod n) * (y mod n) mod n" |
30224 | 150 |
by (simp add: mod_mult_left_eq[of x y n] mod_mult_right_eq[of "x mod n" y n]) |
30488 | 151 |
also have "\<dots> = (x' mod n) * (y' mod n) mod n" using xx'[unfolded modeq_def] yy'[unfolded modeq_def] by simp |
26126 | 152 |
also have "\<dots> = (x' * y') mod n" |
30224 | 153 |
by (simp add: mod_mult_left_eq[of x' y' n] mod_mult_right_eq[of "x' mod n" y' n]) |
30488 | 154 |
finally show ?thesis unfolding modeq_def . |
26126 | 155 |
qed |
156 |
||
157 |
lemma cong_exp: "[x = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)" |
|
158 |
by (induct k, auto simp add: cong_refl cong_mult) |
|
159 |
lemma cong_sub: assumes xx': "[x = x'] (mod n)" and yy': "[y = y'] (mod n)" |
|
160 |
and yx: "y <= x" and yx': "y' <= x'" |
|
161 |
shows "[x - y = x' - y'] (mod n)" |
|
162 |
proof- |
|
30488 | 163 |
{ fix x a x' a' y b y' b' |
26126 | 164 |
have "(x::nat) + a = x' + a' \<Longrightarrow> y + b = y' + b' \<Longrightarrow> y <= x \<Longrightarrow> y' <= x' |
165 |
\<Longrightarrow> (x - y) + (a + b') = (x' - y') + (a' + b)" by arith} |
|
166 |
note th = this |
|
30488 | 167 |
from xx' yy' obtain q1 q2 q1' q2' where q12: "x + n*q1 = x'+n*q2" |
26126 | 168 |
and q12': "y + n*q1' = y'+n*q2'" unfolding nat_mod by blast+ |
169 |
from th[OF q12 q12' yx yx'] |
|
30488 | 170 |
have "(x - y) + n*(q1 + q2') = (x' - y') + n*(q2 + q1')" |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
41541
diff
changeset
|
171 |
by (simp add: distrib_left) |
26126 | 172 |
thus ?thesis unfolding nat_mod by blast |
173 |
qed |
|
174 |
||
30488 | 175 |
lemma cong_mult_lcancel_eq: assumes an: "coprime a n" |
26126 | 176 |
shows "[a * x = a * y] (mod n) \<longleftrightarrow> [x = y] (mod n)" (is "?lhs \<longleftrightarrow> ?rhs") |
177 |
proof |
|
178 |
assume H: "?rhs" from cong_mult[OF cong_refl[of a n] H] show ?lhs . |
|
179 |
next |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
180 |
assume H: "?lhs" hence H': "[x*a = y*a] (mod n)" by (simp add: mult.commute) |
26126 | 181 |
from cong_mult_rcancel[OF an H'] show ?rhs . |
182 |
qed |
|
183 |
||
30488 | 184 |
lemma cong_mult_rcancel_eq: assumes an: "coprime a n" |
26126 | 185 |
shows "[x * a = y * a] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
186 |
using cong_mult_lcancel_eq[OF an, of x y] by (simp add: mult.commute) |
26126 | 187 |
|
30488 | 188 |
lemma cong_add_lcancel_eq: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
26126 | 189 |
by (simp add: nat_mod) |
190 |
||
191 |
lemma cong_add_rcancel_eq: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
|
192 |
by (simp add: nat_mod) |
|
193 |
||
30488 | 194 |
lemma cong_add_rcancel: "[x + a = y + a] (mod n) \<Longrightarrow> [x = y] (mod n)" |
26126 | 195 |
by (simp add: nat_mod) |
196 |
||
197 |
lemma cong_add_lcancel: "[a + x = a + y] (mod n) \<Longrightarrow> [x = y] (mod n)" |
|
198 |
by (simp add: nat_mod) |
|
199 |
||
30488 | 200 |
lemma cong_add_lcancel_eq_0: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
26126 | 201 |
by (simp add: nat_mod) |
202 |
||
203 |
lemma cong_add_rcancel_eq_0: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
|
204 |
by (simp add: nat_mod) |
|
205 |
||
206 |
lemma cong_imp_eq: assumes xn: "x < n" and yn: "y < n" and xy: "[x = y] (mod n)" |
|
207 |
shows "x = y" |
|
30488 | 208 |
using xy[unfolded modeq_def mod_less[OF xn] mod_less[OF yn]] . |
26126 | 209 |
|
210 |
lemma cong_divides_modulus: "[x = y] (mod m) \<Longrightarrow> n dvd m ==> [x = y] (mod n)" |
|
211 |
apply (auto simp add: nat_mod dvd_def) |
|
212 |
apply (rule_tac x="k*q1" in exI) |
|
213 |
apply (rule_tac x="k*q2" in exI) |
|
214 |
by simp |
|
30488 | 215 |
|
26126 | 216 |
lemma cong_0_divides: "[x = 0] (mod n) \<longleftrightarrow> n dvd x" by simp |
217 |
||
218 |
lemma cong_1_divides:"[x = 1] (mod n) ==> n dvd x - 1" |
|
219 |
apply (cases "x\<le>1", simp_all) |
|
220 |
using cong_sub_cases[of x 1 n] by auto |
|
221 |
||
222 |
lemma cong_divides: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y" |
|
223 |
apply (auto simp add: nat_mod dvd_def) |
|
224 |
apply (rule_tac x="k + q1 - q2" in exI, simp add: add_mult_distrib2 diff_mult_distrib2) |
|
225 |
apply (rule_tac x="k + q2 - q1" in exI, simp add: add_mult_distrib2 diff_mult_distrib2) |
|
226 |
done |
|
227 |
||
30488 | 228 |
lemma cong_coprime: assumes xy: "[x = y] (mod n)" |
26126 | 229 |
shows "coprime n x \<longleftrightarrow> coprime n y" |
230 |
proof- |
|
231 |
{assume "n=0" hence ?thesis using xy by simp} |
|
232 |
moreover |
|
233 |
{assume nz: "n \<noteq> 0" |
|
30488 | 234 |
have "coprime n x \<longleftrightarrow> coprime (x mod n) n" |
26126 | 235 |
by (simp add: coprime_mod[OF nz, of x] coprime_commute[of n x]) |
236 |
also have "\<dots> \<longleftrightarrow> coprime (y mod n) n" using xy[unfolded modeq_def] by simp |
|
237 |
also have "\<dots> \<longleftrightarrow> coprime y n" by (simp add: coprime_mod[OF nz, of y]) |
|
238 |
finally have ?thesis by (simp add: coprime_commute) } |
|
239 |
ultimately show ?thesis by blast |
|
240 |
qed |
|
241 |
||
242 |
lemma cong_mod: "~(n = 0) \<Longrightarrow> [a mod n = a] (mod n)" by (simp add: modeq_def) |
|
243 |
||
30488 | 244 |
lemma mod_mult_cong: "~(a = 0) \<Longrightarrow> ~(b = 0) |
26126 | 245 |
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)" |
246 |
by (simp add: modeq_def mod_mult2_eq mod_add_left_eq) |
|
247 |
||
248 |
lemma cong_mod_mult: "[x = y] (mod n) \<Longrightarrow> m dvd n \<Longrightarrow> [x = y] (mod m)" |
|
249 |
apply (auto simp add: nat_mod dvd_def) |
|
250 |
apply (rule_tac x="k*q1" in exI) |
|
251 |
apply (rule_tac x="k*q2" in exI, simp) |
|
252 |
done |
|
253 |
||
254 |
(* Some things when we know more about the order. *) |
|
255 |
||
256 |
lemma cong_le: "y <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)" |
|
257 |
using nat_mod_lemma[of x y n] |
|
258 |
apply auto |
|
259 |
apply (simp add: nat_mod) |
|
260 |
apply (rule_tac x="q" in exI) |
|
261 |
apply (rule_tac x="q + q" in exI) |
|
29667 | 262 |
by (auto simp: algebra_simps) |
26126 | 263 |
|
264 |
lemma cong_to_1: "[a = 1] (mod n) \<longleftrightarrow> a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)" |
|
265 |
proof- |
|
30488 | 266 |
{assume "n = 0 \<or> n = 1\<or> a = 0 \<or> a = 1" hence ?thesis |
26126 | 267 |
apply (cases "n=0", simp_all add: cong_commute) |
268 |
apply (cases "n=1", simp_all add: cong_commute modeq_def) |
|
30488 | 269 |
apply arith |
41541 | 270 |
apply (cases "a=1") |
271 |
apply (simp_all add: modeq_def cong_commute) |
|
272 |
done } |
|
26126 | 273 |
moreover |
274 |
{assume n: "n\<noteq>0" "n\<noteq>1" and a:"a\<noteq>0" "a \<noteq> 1" hence a': "a \<ge> 1" by simp |
|
275 |
hence ?thesis using cong_le[OF a', of n] by auto } |
|
276 |
ultimately show ?thesis by auto |
|
277 |
qed |
|
278 |
||
279 |
(* Some basic theorems about solving congruences. *) |
|
280 |
||
281 |
||
282 |
lemma cong_solve: assumes an: "coprime a n" shows "\<exists>x. [a * x = b] (mod n)" |
|
283 |
proof- |
|
284 |
{assume "a=0" hence ?thesis using an by (simp add: modeq_def)} |
|
285 |
moreover |
|
286 |
{assume az: "a\<noteq>0" |
|
30488 | 287 |
from bezout_add_strong[OF az, of n] |
26126 | 288 |
obtain d x y where dxy: "d dvd a" "d dvd n" "a*x = n*y + d" by blast |
289 |
from an[unfolded coprime, rule_format, of d] dxy(1,2) have d1: "d = 1" by blast |
|
290 |
hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp |
|
291 |
hence "a*(x*b) = n*(y*b) + b" by algebra |
|
292 |
hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp |
|
293 |
hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq) |
|
294 |
hence "[a*(x*b) = b] (mod n)" unfolding modeq_def . |
|
295 |
hence ?thesis by blast} |
|
296 |
ultimately show ?thesis by blast |
|
297 |
qed |
|
298 |
||
299 |
lemma cong_solve_unique: assumes an: "coprime a n" and nz: "n \<noteq> 0" |
|
300 |
shows "\<exists>!x. x < n \<and> [a * x = b] (mod n)" |
|
301 |
proof- |
|
302 |
let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)" |
|
303 |
from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast |
|
304 |
let ?x = "x mod n" |
|
305 |
from x have th: "[a * ?x = b] (mod n)" |
|
30224 | 306 |
by (simp add: modeq_def mod_mult_right_eq[of a x n]) |
26126 | 307 |
from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp |
308 |
{fix y assume Py: "y < n" "[a * y = b] (mod n)" |
|
309 |
from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: modeq_def) |
|
310 |
hence "[y = ?x] (mod n)" by (simp add: cong_mult_lcancel_eq[OF an]) |
|
311 |
with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz |
|
312 |
have "y = ?x" by (simp add: modeq_def)} |
|
313 |
with Px show ?thesis by blast |
|
314 |
qed |
|
315 |
||
316 |
lemma cong_solve_unique_nontrivial: |
|
317 |
assumes p: "prime p" and pa: "coprime p a" and x0: "0 < x" and xp: "x < p" |
|
318 |
shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)" |
|
319 |
proof- |
|
320 |
from p have p1: "p > 1" using prime_ge_2[OF p] by arith |
|
321 |
hence p01: "p \<noteq> 0" "p \<noteq> 1" by arith+ |
|
322 |
from pa have ap: "coprime a p" by (simp add: coprime_commute) |
|
323 |
from prime_coprime[OF p, of x] dvd_imp_le[of p x] x0 xp have px:"coprime x p" |
|
324 |
by (auto simp add: coprime_commute) |
|
30488 | 325 |
from cong_solve_unique[OF px p01(1)] |
26126 | 326 |
obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y" by blast |
327 |
{assume y0: "y = 0" |
|
328 |
with y(2) have th: "p dvd a" by (simp add: cong_commute[of 0 a p]) |
|
329 |
with p coprime_prime[OF pa, of p] have False by simp} |
|
30488 | 330 |
with y show ?thesis unfolding Ex1_def using neq0_conv by blast |
26126 | 331 |
qed |
332 |
lemma cong_unique_inverse_prime: |
|
333 |
assumes p: "prime p" and x0: "0 < x" and xp: "x < p" |
|
334 |
shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)" |
|
335 |
using cong_solve_unique_nontrivial[OF p coprime_1[of p] x0 xp] . |
|
336 |
||
337 |
(* Forms of the Chinese remainder theorem. *) |
|
338 |
||
30488 | 339 |
lemma cong_chinese: |
340 |
assumes ab: "coprime a b" and xya: "[x = y] (mod a)" |
|
26126 | 341 |
and xyb: "[x = y] (mod b)" |
342 |
shows "[x = y] (mod a*b)" |
|
343 |
using ab xya xyb |
|
30488 | 344 |
by (simp add: cong_sub_cases[of x y a] cong_sub_cases[of x y b] |
345 |
cong_sub_cases[of x y "a*b"]) |
|
26126 | 346 |
(cases "x \<le> y", simp_all add: divides_mul[of a _ b]) |
347 |
||
348 |
lemma chinese_remainder_unique: |
|
349 |
assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b\<noteq>0" |
|
350 |
shows "\<exists>!x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)" |
|
351 |
proof- |
|
352 |
from az bz have abpos: "a*b > 0" by simp |
|
30488 | 353 |
from chinese_remainder[OF ab az bz] obtain x q1 q2 where |
26126 | 354 |
xq12: "x = m + q1 * a" "x = n + q2 * b" by blast |
30488 | 355 |
let ?w = "x mod (a*b)" |
26126 | 356 |
have wab: "?w < a*b" by (simp add: mod_less_divisor[OF abpos]) |
357 |
from xq12(1) have "?w mod a = ((m + q1 * a) mod (a*b)) mod a" by simp |
|
54221 | 358 |
also have "\<dots> = m mod a" by (simp add: mod_mult2_eq) |
26126 | 359 |
finally have th1: "[?w = m] (mod a)" by (simp add: modeq_def) |
360 |
from xq12(2) have "?w mod b = ((n + q2 * b) mod (a*b)) mod b" by simp |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
361 |
also have "\<dots> = ((n + q2 * b) mod (b*a)) mod b" by (simp add: mult.commute) |
54221 | 362 |
also have "\<dots> = n mod b" by (simp add: mod_mult2_eq) |
26126 | 363 |
finally have th2: "[?w = n] (mod b)" by (simp add: modeq_def) |
364 |
{fix y assume H: "y < a*b" "[y = m] (mod a)" "[y = n] (mod b)" |
|
365 |
with th1 th2 have H': "[y = ?w] (mod a)" "[y = ?w] (mod b)" |
|
366 |
by (simp_all add: modeq_def) |
|
30488 | 367 |
from cong_chinese[OF ab H'] mod_less[OF H(1)] mod_less[OF wab] |
26126 | 368 |
have "y = ?w" by (simp add: modeq_def)} |
369 |
with th1 th2 wab show ?thesis by blast |
|
370 |
qed |
|
371 |
||
372 |
lemma chinese_remainder_coprime_unique: |
|
30488 | 373 |
assumes ab: "coprime a b" and az: "a \<noteq> 0" and bz: "b \<noteq> 0" |
26126 | 374 |
and ma: "coprime m a" and nb: "coprime n b" |
375 |
shows "\<exists>!x. coprime x (a * b) \<and> x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)" |
|
376 |
proof- |
|
377 |
let ?P = "\<lambda>x. x < a * b \<and> [x = m] (mod a) \<and> [x = n] (mod b)" |
|
378 |
from chinese_remainder_unique[OF ab az bz] |
|
30488 | 379 |
obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" |
26126 | 380 |
"\<forall>y. ?P y \<longrightarrow> y = x" by blast |
381 |
from ma nb cong_coprime[OF x(2)] cong_coprime[OF x(3)] |
|
382 |
have "coprime x a" "coprime x b" by (simp_all add: coprime_commute) |
|
383 |
with coprime_mul[of x a b] have "coprime x (a*b)" by simp |
|
384 |
with x show ?thesis by blast |
|
385 |
qed |
|
386 |
||
387 |
(* Euler totient function. *) |
|
388 |
||
389 |
definition phi_def: "\<phi> n = card { m. 0 < m \<and> m <= n \<and> coprime m n }" |
|
31197
c1c163ec6c44
fine-tuned elimination of comprehensions involving x=t.
nipkow
parents:
31021
diff
changeset
|
390 |
|
26126 | 391 |
lemma phi_0[simp]: "\<phi> 0 = 0" |
31197
c1c163ec6c44
fine-tuned elimination of comprehensions involving x=t.
nipkow
parents:
31021
diff
changeset
|
392 |
unfolding phi_def by auto |
26126 | 393 |
|
394 |
lemma phi_finite[simp]: "finite ({ m. 0 < m \<and> m <= n \<and> coprime m n })" |
|
395 |
proof- |
|
396 |
have "{ m. 0 < m \<and> m <= n \<and> coprime m n } \<subseteq> {0..n}" by auto |
|
397 |
thus ?thesis by (auto intro: finite_subset) |
|
398 |
qed |
|
399 |
||
400 |
declare coprime_1[presburger] |
|
401 |
lemma phi_1[simp]: "\<phi> 1 = 1" |
|
402 |
proof- |
|
30488 | 403 |
{fix m |
26126 | 404 |
have "0 < m \<and> m <= 1 \<and> coprime m 1 \<longleftrightarrow> m = 1" by presburger } |
405 |
thus ?thesis by (simp add: phi_def) |
|
406 |
qed |
|
407 |
||
408 |
lemma [simp]: "\<phi> (Suc 0) = Suc 0" using phi_1 by simp |
|
409 |
||
410 |
lemma phi_alt: "\<phi>(n) = card { m. coprime m n \<and> m < n}" |
|
411 |
proof- |
|
412 |
{assume "n=0 \<or> n=1" hence ?thesis by (cases "n=0", simp_all)} |
|
413 |
moreover |
|
414 |
{assume n: "n\<noteq>0" "n\<noteq>1" |
|
415 |
{fix m |
|
416 |
from n have "0 < m \<and> m <= n \<and> coprime m n \<longleftrightarrow> coprime m n \<and> m < n" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
417 |
apply (cases "m = 0", simp_all) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
418 |
apply (cases "m = 1", simp_all) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
419 |
apply (cases "m = n", auto) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
420 |
done } |
26126 | 421 |
hence ?thesis unfolding phi_def by simp} |
422 |
ultimately show ?thesis by auto |
|
423 |
qed |
|
424 |
||
425 |
lemma phi_finite_lemma[simp]: "finite {m. coprime m n \<and> m < n}" (is "finite ?S") |
|
426 |
by (rule finite_subset[of "?S" "{0..n}"], auto) |
|
427 |
||
428 |
lemma phi_another: assumes n: "n\<noteq>1" |
|
429 |
shows "\<phi> n = card {m. 0 < m \<and> m < n \<and> coprime m n }" |
|
430 |
proof- |
|
30488 | 431 |
{fix m |
26126 | 432 |
from n have "0 < m \<and> m < n \<and> coprime m n \<longleftrightarrow> coprime m n \<and> m < n" |
433 |
by (cases "m=0", auto)} |
|
434 |
thus ?thesis unfolding phi_alt by auto |
|
435 |
qed |
|
436 |
||
437 |
lemma phi_limit: "\<phi> n \<le> n" |
|
438 |
proof- |
|
439 |
have "{ m. coprime m n \<and> m < n} \<subseteq> {0 ..<n}" by auto |
|
440 |
with card_mono[of "{0 ..<n}" "{ m. coprime m n \<and> m < n}"] |
|
441 |
show ?thesis unfolding phi_alt by auto |
|
442 |
qed |
|
443 |
||
444 |
lemma stupid[simp]: "{m. (0::nat) < m \<and> m < n} = {1..<n}" |
|
445 |
by auto |
|
446 |
||
30488 | 447 |
lemma phi_limit_strong: assumes n: "n\<noteq>1" |
26126 | 448 |
shows "\<phi>(n) \<le> n - 1" |
449 |
proof- |
|
450 |
show ?thesis |
|
30488 | 451 |
unfolding phi_another[OF n] finite_number_segment[of n, symmetric] |
26126 | 452 |
by (rule card_mono[of "{m. 0 < m \<and> m < n}" "{m. 0 < m \<and> m < n \<and> coprime m n}"], auto) |
453 |
qed |
|
454 |
||
455 |
lemma phi_lowerbound_1_strong: assumes n: "n \<ge> 1" |
|
456 |
shows "\<phi>(n) \<ge> 1" |
|
457 |
proof- |
|
458 |
let ?S = "{ m. 0 < m \<and> m <= n \<and> coprime m n }" |
|
30488 | 459 |
from card_0_eq[of ?S] n have "\<phi> n \<noteq> 0" unfolding phi_alt |
26126 | 460 |
apply auto |
461 |
apply (cases "n=1", simp_all) |
|
462 |
apply (rule exI[where x=1], simp) |
|
463 |
done |
|
464 |
thus ?thesis by arith |
|
465 |
qed |
|
466 |
||
467 |
lemma phi_lowerbound_1: "2 <= n ==> 1 <= \<phi>(n)" |
|
468 |
using phi_lowerbound_1_strong[of n] by auto |
|
469 |
||
470 |
lemma phi_lowerbound_2: assumes n: "3 <= n" shows "2 <= \<phi> (n)" |
|
471 |
proof- |
|
472 |
let ?S = "{ m. 0 < m \<and> m <= n \<and> coprime m n }" |
|
30488 | 473 |
have inS: "{1, n - 1} \<subseteq> ?S" using n coprime_plus1[of "n - 1"] |
26126 | 474 |
by (auto simp add: coprime_commute) |
475 |
from n have c2: "card {1, n - 1} = 2" by (auto simp add: card_insert_if) |
|
30488 | 476 |
from card_mono[of ?S "{1, n - 1}", simplified inS c2] show ?thesis |
26126 | 477 |
unfolding phi_def by auto |
478 |
qed |
|
479 |
||
480 |
lemma phi_prime: "\<phi> n = n - 1 \<and> n\<noteq>0 \<and> n\<noteq>1 \<longleftrightarrow> prime n" |
|
481 |
proof- |
|
482 |
{assume "n=0 \<or> n=1" hence ?thesis by (cases "n=1", simp_all)} |
|
483 |
moreover |
|
484 |
{assume n: "n\<noteq>0" "n\<noteq>1" |
|
485 |
let ?S = "{m. 0 < m \<and> m < n}" |
|
486 |
have fS: "finite ?S" by simp |
|
487 |
let ?S' = "{m. 0 < m \<and> m < n \<and> coprime m n}" |
|
488 |
have fS':"finite ?S'" apply (rule finite_subset[of ?S' ?S]) by auto |
|
489 |
{assume H: "\<phi> n = n - 1 \<and> n\<noteq>0 \<and> n\<noteq>1" |
|
30488 | 490 |
hence ceq: "card ?S' = card ?S" |
26126 | 491 |
using n finite_number_segment[of n] phi_another[OF n(2)] by simp |
492 |
{fix m assume m: "0 < m" "m < n" "\<not> coprime m n" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
493 |
hence mS': "m \<notin> ?S'" by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
494 |
have "insert m ?S' \<le> ?S" using m by auto |
63833 | 495 |
have "card (insert m ?S') \<le> card ?S" |
496 |
by (rule card_mono[of ?S "insert m ?S'"]) (use m in auto) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
497 |
hence False |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
498 |
unfolding card_insert_disjoint[of "?S'" m, OF fS' mS'] ceq |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
499 |
by simp } |
26126 | 500 |
hence "\<forall>m. 0 <m \<and> m < n \<longrightarrow> coprime m n" by blast |
501 |
hence "prime n" unfolding prime using n by (simp add: coprime_commute)} |
|
502 |
moreover |
|
503 |
{assume H: "prime n" |
|
30488 | 504 |
hence "?S = ?S'" unfolding prime using n |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
505 |
by (auto simp add: coprime_commute) |
26126 | 506 |
hence "card ?S = card ?S'" by simp |
507 |
hence "\<phi> n = n - 1" unfolding phi_another[OF n(2)] by simp} |
|
508 |
ultimately have ?thesis using n by blast} |
|
509 |
ultimately show ?thesis by (cases "n=0") blast+ |
|
510 |
qed |
|
511 |
||
512 |
(* Multiplicativity property. *) |
|
513 |
||
514 |
lemma phi_multiplicative: assumes ab: "coprime a b" |
|
515 |
shows "\<phi> (a * b) = \<phi> a * \<phi> b" |
|
516 |
proof- |
|
30488 | 517 |
{assume "a = 0 \<or> b = 0 \<or> a = 1 \<or> b = 1" |
26126 | 518 |
hence ?thesis |
519 |
by (cases "a=0", simp, cases "b=0", simp, cases"a=1", simp_all) } |
|
520 |
moreover |
|
521 |
{assume a: "a\<noteq>0" "a\<noteq>1" and b: "b\<noteq>0" "b\<noteq>1" |
|
522 |
hence ab0: "a*b \<noteq> 0" by simp |
|
523 |
let ?S = "\<lambda>k. {m. coprime m k \<and> m < k}" |
|
524 |
let ?f = "\<lambda>x. (x mod a, x mod b)" |
|
525 |
have eq: "?f ` (?S (a*b)) = (?S a \<times> ?S b)" |
|
526 |
proof- |
|
527 |
{fix x assume x:"x \<in> ?S (a*b)" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
528 |
hence x': "coprime x (a*b)" "x < a*b" by simp_all |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
529 |
hence xab: "coprime x a" "coprime x b" by (simp_all add: coprime_mul_eq) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
530 |
from mod_less_divisor a b have xab':"x mod a < a" "x mod b < b" by auto |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
531 |
from xab xab' have "?f x \<in> (?S a \<times> ?S b)" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
532 |
by (simp add: coprime_mod[OF a(1)] coprime_mod[OF b(1)])} |
26126 | 533 |
moreover |
534 |
{fix x y assume x: "x \<in> ?S a" and y: "y \<in> ?S b" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
535 |
hence x': "coprime x a" "x < a" and y': "coprime y b" "y < b" by simp_all |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
536 |
from chinese_remainder_coprime_unique[OF ab a(1) b(1) x'(1) y'(1)] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
537 |
obtain z where z: "coprime z (a * b)" "z < a * b" "[z = x] (mod a)" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
538 |
"[z = y] (mod b)" by blast |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
539 |
hence "(x,y) \<in> ?f ` (?S (a*b))" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
540 |
using y'(2) mod_less_divisor[of b y] x'(2) mod_less_divisor[of a x] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
541 |
by (auto simp add: image_iff modeq_def)} |
26126 | 542 |
ultimately show ?thesis by auto |
543 |
qed |
|
544 |
have finj: "inj_on ?f (?S (a*b))" |
|
545 |
unfolding inj_on_def |
|
546 |
proof(clarify) |
|
30488 | 547 |
fix x y assume H: "coprime x (a * b)" "x < a * b" "coprime y (a * b)" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
548 |
"y < a * b" "x mod a = y mod a" "x mod b = y mod b" |
30488 | 549 |
hence cp: "coprime x a" "coprime x b" "coprime y a" "coprime y b" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
550 |
by (simp_all add: coprime_mul_eq) |
26126 | 551 |
from chinese_remainder_coprime_unique[OF ab a(1) b(1) cp(3,4)] H |
552 |
show "x = y" unfolding modeq_def by blast |
|
553 |
qed |
|
554 |
from card_image[OF finj, unfolded eq] have ?thesis |
|
555 |
unfolding phi_alt by simp } |
|
556 |
ultimately show ?thesis by auto |
|
557 |
qed |
|
558 |
||
559 |
(* Fermat's Little theorem / Fermat-Euler theorem. *) |
|
560 |
||
561 |
||
562 |
lemma nproduct_mod: |
|
563 |
assumes fS: "finite S" and n0: "n \<noteq> 0" |
|
564 |
shows "[setprod (\<lambda>m. a(m) mod n) S = setprod a S] (mod n)" |
|
565 |
proof- |
|
566 |
have th1:"[1 = 1] (mod n)" by (simp add: modeq_def) |
|
567 |
from cong_mult |
|
568 |
have th3:"\<forall>x1 y1 x2 y2. |
|
569 |
[x1 = x2] (mod n) \<and> [y1 = y2] (mod n) \<longrightarrow> [x1 * y1 = x2 * y2] (mod n)" |
|
570 |
by blast |
|
571 |
have th4:"\<forall>x\<in>S. [a x mod n = a x] (mod n)" by (simp add: modeq_def) |
|
51489 | 572 |
from setprod.related [where h="(\<lambda>m. a(m) mod n)" and g=a, OF th1 th3 fS, OF th4] show ?thesis by (simp add: fS) |
26126 | 573 |
qed |
574 |
||
575 |
lemma nproduct_cmul: |
|
576 |
assumes fS:"finite S" |
|
31021 | 577 |
shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S" |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
61382
diff
changeset
|
578 |
unfolding setprod.distrib setprod_constant [of c] .. |
26126 | 579 |
|
580 |
lemma coprime_nproduct: |
|
581 |
assumes fS: "finite S" and Sn: "\<forall>x\<in>S. coprime n (a x)" |
|
582 |
shows "coprime n (setprod a S)" |
|
51489 | 583 |
using fS by (rule finite_subset_induct) |
27368 | 584 |
(insert Sn, auto simp add: coprime_mul) |
26126 | 585 |
|
586 |
lemma fermat_little: assumes an: "coprime a n" |
|
587 |
shows "[a ^ (\<phi> n) = 1] (mod n)" |
|
588 |
proof- |
|
589 |
{assume "n=0" hence ?thesis by simp} |
|
590 |
moreover |
|
591 |
{assume "n=1" hence ?thesis by (simp add: modeq_def)} |
|
592 |
moreover |
|
593 |
{assume nz: "n \<noteq> 0" and n1: "n \<noteq> 1" |
|
594 |
let ?S = "{m. coprime m n \<and> m < n}" |
|
595 |
let ?P = "\<Prod> ?S" |
|
596 |
have fS: "finite ?S" by simp |
|
597 |
have cardfS: "\<phi> n = card ?S" unfolding phi_alt .. |
|
598 |
{fix m assume m: "m \<in> ?S" |
|
599 |
hence "coprime m n" by simp |
|
30488 | 600 |
with coprime_mul[of n a m] an have "coprime (a*m) n" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
601 |
by (simp add: coprime_commute)} |
26126 | 602 |
hence Sn: "\<forall>m\<in> ?S. coprime (a*m) n " by blast |
603 |
from coprime_nproduct[OF fS, of n "\<lambda>m. m"] have nP:"coprime ?P n" |
|
604 |
by (simp add: coprime_commute) |
|
605 |
have Paphi: "[?P*a^ (\<phi> n) = ?P*1] (mod n)" |
|
606 |
proof- |
|
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
607 |
let ?h = "\<lambda>m. (a * m) mod n" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
608 |
|
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
609 |
have eq0: "(\<Prod>i\<in>?S. ?h i) = (\<Prod>i\<in>?S. i)" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
610 |
proof (rule setprod.reindex_bij_betw) |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
611 |
have "inj_on (\<lambda>i. ?h i) ?S" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
612 |
proof (rule inj_onI) |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
613 |
fix x y assume "?h x = ?h y" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
614 |
then have "[a * x = a * y] (mod n)" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
615 |
by (simp add: modeq_def) |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
616 |
moreover assume "x \<in> ?S" "y \<in> ?S" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
617 |
ultimately show "x = y" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
618 |
by (auto intro: cong_imp_eq cong_mult_lcancel an) |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
619 |
qed |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
620 |
moreover have "?h ` ?S = ?S" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
621 |
proof safe |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
622 |
fix y assume "coprime y n" then show "coprime (?h y) n" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
623 |
by (metis an nz coprime_commute coprime_mod coprime_mul_eq) |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
624 |
next |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
625 |
fix y assume y: "coprime y n" "y < n" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
626 |
from cong_solve_unique[OF an nz] obtain x where x: "x < n" "[a * x = y] (mod n)" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
627 |
by blast |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
628 |
then show "y \<in> ?h ` ?S" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
629 |
using cong_coprime[OF x(2)] coprime_mul_eq[of n a x] an y x |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
630 |
by (intro image_eqI[of _ _ x]) (auto simp add: coprime_commute modeq_def) |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
631 |
qed (insert nz, simp) |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
632 |
ultimately show "bij_betw ?h ?S ?S" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
633 |
by (simp add: bij_betw_def) |
26126 | 634 |
qed |
635 |
from nproduct_mod[OF fS nz, of "op * a"] |
|
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
636 |
have "[(\<Prod>i\<in>?S. a * i) = (\<Prod>i\<in>?S. ?h i)] (mod n)" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
637 |
by (simp add: cong_commute) |
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
638 |
also have "[(\<Prod>i\<in>?S. ?h i) = ?P] (mod n)" |
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56073
diff
changeset
|
639 |
using eq0 fS an by (simp add: setprod_def modeq_def) |
26126 | 640 |
finally show "[?P*a^ (\<phi> n) = ?P*1] (mod n)" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
641 |
unfolding cardfS mult.commute[of ?P "a^ (card ?S)"] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
642 |
nproduct_cmul[OF fS, symmetric] mult_1_right by simp |
26126 | 643 |
qed |
644 |
from cong_mult_lcancel[OF nP Paphi] have ?thesis . } |
|
645 |
ultimately show ?thesis by blast |
|
646 |
qed |
|
647 |
||
648 |
lemma fermat_little_prime: assumes p: "prime p" and ap: "coprime a p" |
|
649 |
shows "[a^ (p - 1) = 1] (mod p)" |
|
650 |
using fermat_little[OF ap] p[unfolded phi_prime[symmetric]] |
|
651 |
by simp |
|
652 |
||
653 |
||
654 |
(* Lucas's theorem. *) |
|
655 |
||
656 |
lemma lucas_coprime_lemma: |
|
657 |
assumes m: "m\<noteq>0" and am: "[a^m = 1] (mod n)" |
|
658 |
shows "coprime a n" |
|
659 |
proof- |
|
660 |
{assume "n=1" hence ?thesis by simp} |
|
661 |
moreover |
|
662 |
{assume "n = 0" hence ?thesis using am m exp_eq_1[of a m] by simp} |
|
663 |
moreover |
|
664 |
{assume n: "n\<noteq>0" "n\<noteq>1" |
|
665 |
from m obtain m' where m': "m = Suc m'" by (cases m, blast+) |
|
666 |
{fix d |
|
667 |
assume d: "d dvd a" "d dvd n" |
|
30488 | 668 |
from n have n1: "1 < n" by arith |
26126 | 669 |
from am mod_less[OF n1] have am1: "a^m mod n = 1" unfolding modeq_def by simp |
670 |
from dvd_mult2[OF d(1), of "a^m'"] have dam:"d dvd a^m" by (simp add: m') |
|
671 |
from dvd_mod_iff[OF d(2), of "a^m"] dam am1 |
|
672 |
have "d = 1" by simp } |
|
673 |
hence ?thesis unfolding coprime by auto |
|
674 |
} |
|
30488 | 675 |
ultimately show ?thesis by blast |
26126 | 676 |
qed |
677 |
||
678 |
lemma lucas_weak: |
|
30488 | 679 |
assumes n: "n \<ge> 2" and an:"[a^(n - 1) = 1] (mod n)" |
26126 | 680 |
and nm: "\<forall>m. 0 <m \<and> m < n - 1 \<longrightarrow> \<not> [a^m = 1] (mod n)" |
681 |
shows "prime n" |
|
682 |
proof- |
|
683 |
from n have n1: "n \<noteq> 1" "n\<noteq>0" "n - 1 \<noteq> 0" "n - 1 > 0" "n - 1 < n" by arith+ |
|
684 |
from lucas_coprime_lemma[OF n1(3) an] have can: "coprime a n" . |
|
685 |
from fermat_little[OF can] have afn: "[a ^ \<phi> n = 1] (mod n)" . |
|
686 |
{assume "\<phi> n \<noteq> n - 1" |
|
687 |
with phi_limit_strong[OF n1(1)] phi_lowerbound_1[OF n] |
|
688 |
have c:"\<phi> n > 0 \<and> \<phi> n < n - 1" by arith |
|
689 |
from nm[rule_format, OF c] afn have False ..} |
|
690 |
hence "\<phi> n = n - 1" by blast |
|
691 |
with phi_prime[of n] n1(1,2) show ?thesis by simp |
|
692 |
qed |
|
693 |
||
30488 | 694 |
lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))" |
26126 | 695 |
(is "?lhs \<longleftrightarrow> ?rhs") |
696 |
proof |
|
697 |
assume ?rhs thus ?lhs by blast |
|
698 |
next |
|
699 |
assume H: ?lhs then obtain n where n: "P n" by blast |
|
700 |
let ?x = "Least P" |
|
701 |
{fix m assume m: "m < ?x" |
|
702 |
from not_less_Least[OF m] have "\<not> P m" .} |
|
703 |
with LeastI_ex[OF H] show ?rhs by blast |
|
704 |
qed |
|
705 |
||
30488 | 706 |
lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))" |
26126 | 707 |
(is "?lhs \<longleftrightarrow> ?rhs") |
708 |
proof- |
|
709 |
{assume ?rhs hence ?lhs by blast} |
|
30488 | 710 |
moreover |
26126 | 711 |
{ assume H: ?lhs then obtain n where n: "P n" by blast |
712 |
let ?x = "Least P" |
|
713 |
{fix m assume m: "m < ?x" |
|
714 |
from not_less_Least[OF m] have "\<not> P m" .} |
|
715 |
with LeastI_ex[OF H] have ?rhs by blast} |
|
716 |
ultimately show ?thesis by blast |
|
717 |
qed |
|
30488 | 718 |
|
26126 | 719 |
lemma power_mod: "((x::nat) mod m)^n mod m = x^n mod m" |
720 |
proof(induct n) |
|
721 |
case 0 thus ?case by simp |
|
722 |
next |
|
30488 | 723 |
case (Suc n) |
724 |
have "(x mod m)^(Suc n) mod m = ((x mod m) * (((x mod m) ^ n) mod m)) mod m" |
|
30224 | 725 |
by (simp add: mod_mult_right_eq[symmetric]) |
26126 | 726 |
also have "\<dots> = ((x mod m) * (x^n mod m)) mod m" using Suc.hyps by simp |
727 |
also have "\<dots> = x^(Suc n) mod m" |
|
30224 | 728 |
by (simp add: mod_mult_left_eq[symmetric] mod_mult_right_eq[symmetric]) |
26126 | 729 |
finally show ?case . |
730 |
qed |
|
731 |
||
732 |
lemma lucas: |
|
30488 | 733 |
assumes n2: "n \<ge> 2" and an1: "[a^(n - 1) = 1] (mod n)" |
26126 | 734 |
and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> \<not> [a^((n - 1) div p) = 1] (mod n)" |
735 |
shows "prime n" |
|
736 |
proof- |
|
737 |
from n2 have n01: "n\<noteq>0" "n\<noteq>1" "n - 1 \<noteq> 0" by arith+ |
|
738 |
from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" by simp |
|
30488 | 739 |
from lucas_coprime_lemma[OF n01(3) an1] cong_coprime[OF an1] |
26126 | 740 |
have an: "coprime a n" "coprime (a^(n - 1)) n" by (simp_all add: coprime_commute) |
741 |
{assume H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m") |
|
30488 | 742 |
from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where |
26126 | 743 |
m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k" by blast |
30488 | 744 |
{assume nm1: "(n - 1) mod m > 0" |
745 |
from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast |
|
26126 | 746 |
let ?y = "a^ ((n - 1) div m * m)" |
747 |
note mdeq = mod_div_equality[of "(n - 1)" m] |
|
30488 | 748 |
from coprime_exp[OF an(1)[unfolded coprime_commute[of a n]], |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
749 |
of "(n - 1) div m * m"] |
30488 | 750 |
have yn: "coprime ?y n" by (simp add: coprime_commute) |
751 |
have "?y mod n = (a^m)^((n - 1) div m) mod n" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
752 |
by (simp add: algebra_simps power_mult) |
30488 | 753 |
also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
754 |
using power_mod[of "a^m" n "(n - 1) div m"] by simp |
30488 | 755 |
also have "\<dots> = 1" using m(3)[unfolded modeq_def onen] onen |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
756 |
by (simp add: power_Suc0) |
30488 | 757 |
finally have th3: "?y mod n = 1" . |
758 |
have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
759 |
using an1[unfolded modeq_def onen] onen |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
760 |
mod_div_equality[of "(n - 1)" m, symmetric] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
761 |
by (simp add:power_add[symmetric] modeq_def th3 del: One_nat_def) |
26126 | 762 |
from cong_mult_lcancel[of ?y n "a^((n - 1) mod m)" 1, OF yn th2] |
30488 | 763 |
have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)" . |
764 |
from m(4)[rule_format, OF th0] nm1 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
765 |
less_trans[OF mod_less_divisor[OF m(1), of "n - 1"] m(2)] th1 |
26126 | 766 |
have False by blast } |
767 |
hence "(n - 1) mod m = 0" by auto |
|
768 |
then have mn: "m dvd n - 1" by presburger |
|
769 |
then obtain r where r: "n - 1 = m*r" unfolding dvd_def by blast |
|
63833 | 770 |
from n01 r m(2) have r01: "r\<noteq>0" "r\<noteq>1" by auto |
26126 | 771 |
from prime_factor[OF r01(2)] obtain p where p: "prime p" "p dvd r" by blast |
772 |
hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult) |
|
773 |
have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r |
|
774 |
by (simp add: power_mult) |
|
775 |
also have "\<dots> = (a^(m*(r div p))) mod n" using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] by simp |
|
776 |
also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult) |
|
777 |
also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod[of "a^m" "n" "r div p" ] .. |
|
26158 | 778 |
also have "\<dots> = 1" using m(3) onen by (simp add: modeq_def power_Suc0) |
30488 | 779 |
finally have "[(a ^ ((n - 1) div p))= 1] (mod n)" |
26126 | 780 |
using onen by (simp add: modeq_def) |
781 |
with pn[rule_format, OF th] have False by blast} |
|
782 |
hence th: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast |
|
783 |
from lucas_weak[OF n2 an1 th] show ?thesis . |
|
784 |
qed |
|
785 |
||
786 |
(* Definition of the order of a number mod n (0 in non-coprime case). *) |
|
787 |
||
788 |
definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)" |
|
789 |
||
790 |
(* This has the expected properties. *) |
|
791 |
||
792 |
lemma coprime_ord: |
|
30488 | 793 |
assumes na: "coprime n a" |
26126 | 794 |
shows "ord n a > 0 \<and> [a ^(ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> \<not> [a^ m = 1] (mod n))" |
795 |
proof- |
|
796 |
let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)" |
|
797 |
from euclid[of a] obtain p where p: "prime p" "a < p" by blast |
|
798 |
from na have o: "ord n a = Least ?P" by (simp add: ord_def) |
|
799 |
{assume "n=0 \<or> n=1" with na have "\<exists>m>0. ?P m" apply auto apply (rule exI[where x=1]) by (simp add: modeq_def)} |
|
800 |
moreover |
|
30488 | 801 |
{assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith |
26126 | 802 |
from na have na': "coprime a n" by (simp add: coprime_commute) |
63833 | 803 |
have ex: "\<exists>m>0. ?P m" |
804 |
by (rule exI[where x="\<phi> n"]) (use phi_lowerbound_1[OF n2] fermat_little[OF na'] in auto) } |
|
26126 | 805 |
ultimately have ex: "\<exists>m>0. ?P m" by blast |
30488 | 806 |
from nat_exists_least_iff'[of ?P] ex na show ?thesis |
26126 | 807 |
unfolding o[symmetric] by auto |
808 |
qed |
|
809 |
(* With the special value 0 for non-coprime case, it's more convenient. *) |
|
810 |
lemma ord_works: |
|
811 |
"[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> ~[a^ m = 1] (mod n))" |
|
812 |
apply (cases "coprime n a") |
|
813 |
using coprime_ord[of n a] |
|
814 |
by (blast, simp add: ord_def modeq_def) |
|
815 |
||
30488 | 816 |
lemma ord: "[a^(ord n a) = 1] (mod n)" using ord_works by blast |
817 |
lemma ord_minimal: "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> ~[a^m = 1] (mod n)" |
|
26126 | 818 |
using ord_works by blast |
819 |
lemma ord_eq_0: "ord n a = 0 \<longleftrightarrow> ~coprime n a" |
|
41541 | 820 |
by (cases "coprime n a", simp add: coprime_ord, simp add: ord_def) |
26126 | 821 |
|
822 |
lemma ord_divides: |
|
823 |
"[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d" (is "?lhs \<longleftrightarrow> ?rhs") |
|
824 |
proof |
|
825 |
assume rh: ?rhs |
|
826 |
then obtain k where "d = ord n a * k" unfolding dvd_def by blast |
|
827 |
hence "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)" |
|
828 |
by (simp add : modeq_def power_mult power_mod) |
|
30488 | 829 |
also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)" |
830 |
using ord[of a n, unfolded modeq_def] |
|
26158 | 831 |
by (simp add: modeq_def power_mod power_Suc0) |
26126 | 832 |
finally show ?lhs . |
30488 | 833 |
next |
26126 | 834 |
assume lh: ?lhs |
835 |
{ assume H: "\<not> coprime n a" |
|
836 |
hence o: "ord n a = 0" by (simp add: ord_def) |
|
837 |
{assume d: "d=0" with o H have ?rhs by (simp add: modeq_def)} |
|
838 |
moreover |
|
839 |
{assume d0: "d\<noteq>0" then obtain d' where d': "d = Suc d'" by (cases d, auto) |
|
30488 | 840 |
from H[unfolded coprime] |
841 |
obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto |
|
842 |
from lh[unfolded nat_mod] |
|
26126 | 843 |
obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" by blast |
844 |
hence "a ^ d + n * q1 - n * q2 = 1" by simp |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31197
diff
changeset
|
845 |
with dvd_diff_nat [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp |
26126 | 846 |
with p(3) have False by simp |
847 |
hence ?rhs ..} |
|
848 |
ultimately have ?rhs by blast} |
|
849 |
moreover |
|
850 |
{assume H: "coprime n a" |
|
851 |
let ?o = "ord n a" |
|
852 |
let ?q = "d div ord n a" |
|
853 |
let ?r = "d mod ord n a" |
|
30488 | 854 |
from cong_exp[OF ord[of a n], of ?q] |
26158 | 855 |
have eqo: "[(a^?o)^?q = 1] (mod n)" by (simp add: modeq_def power_Suc0) |
26126 | 856 |
from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0) |
857 |
hence op: "?o > 0" by simp |
|
858 |
from mod_div_equality[of d "ord n a"] lh |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
859 |
have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: modeq_def mult.commute) |
30488 | 860 |
hence "[(a^?o)^?q * (a^?r) = 1] (mod n)" |
26126 | 861 |
by (simp add: modeq_def power_mult[symmetric] power_add[symmetric]) |
862 |
hence th: "[a^?r = 1] (mod n)" |
|
30224 | 863 |
using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n] |
26126 | 864 |
apply (simp add: modeq_def del: One_nat_def) |
30224 | 865 |
by (simp add: mod_mult_left_eq[symmetric]) |
26126 | 866 |
{assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)} |
867 |
moreover |
|
30488 | 868 |
{assume r: "?r \<noteq> 0" |
26126 | 869 |
with mod_less_divisor[OF op, of d] have r0o:"?r >0 \<and> ?r < ?o" by simp |
30488 | 870 |
from conjunct2[OF ord_works[of a n], rule_format, OF r0o] th |
26126 | 871 |
have ?rhs by blast} |
872 |
ultimately have ?rhs by blast} |
|
873 |
ultimately show ?rhs by blast |
|
874 |
qed |
|
875 |
||
876 |
lemma order_divides_phi: "coprime n a \<Longrightarrow> ord n a dvd \<phi> n" |
|
877 |
using ord_divides fermat_little coprime_commute by simp |
|
30488 | 878 |
lemma order_divides_expdiff: |
26126 | 879 |
assumes na: "coprime n a" |
880 |
shows "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))" |
|
881 |
proof- |
|
30488 | 882 |
{fix n a d e |
26126 | 883 |
assume na: "coprime n a" and ed: "(e::nat) \<le> d" |
884 |
hence "\<exists>c. d = e + c" by arith |
|
885 |
then obtain c where c: "d = e + c" by arith |
|
886 |
from na have an: "coprime a n" by (simp add: coprime_commute) |
|
30488 | 887 |
from coprime_exp[OF na, of e] |
26126 | 888 |
have aen: "coprime (a^e) n" by (simp add: coprime_commute) |
30488 | 889 |
from coprime_exp[OF na, of c] |
26126 | 890 |
have acn: "coprime (a^c) n" by (simp add: coprime_commute) |
891 |
have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)" |
|
892 |
using c by simp |
|
893 |
also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add) |
|
894 |
also have "\<dots> \<longleftrightarrow> [a ^ c = 1] (mod n)" |
|
895 |
using cong_mult_lcancel_eq[OF aen, of "a^c" "a^0"] by simp |
|
896 |
also have "\<dots> \<longleftrightarrow> ord n a dvd c" by (simp only: ord_divides) |
|
897 |
also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)" |
|
898 |
using cong_add_lcancel_eq[of e c 0 "ord n a", simplified cong_0_divides] |
|
899 |
by simp |
|
900 |
finally have "[a^d = a^e] (mod n) \<longleftrightarrow> [d = e] (mod (ord n a))" |
|
901 |
using c by simp } |
|
902 |
note th = this |
|
903 |
have "e \<le> d \<or> d \<le> e" by arith |
|
904 |
moreover |
|
905 |
{assume ed: "e \<le> d" from th[OF na ed] have ?thesis .} |
|
906 |
moreover |
|
907 |
{assume de: "d \<le> e" |
|
908 |
from th[OF na de] have ?thesis by (simp add: cong_commute) } |
|
909 |
ultimately show ?thesis by blast |
|
910 |
qed |
|
911 |
||
912 |
(* Another trivial primality characterization. *) |
|
913 |
||
914 |
lemma prime_prime_factor: |
|
915 |
"prime n \<longleftrightarrow> n \<noteq> 1\<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" |
|
916 |
proof- |
|
917 |
{assume n: "n=0 \<or> n=1" hence ?thesis using prime_0 two_is_prime by auto} |
|
918 |
moreover |
|
919 |
{assume n: "n\<noteq>0" "n\<noteq>1" |
|
920 |
{assume pn: "prime n" |
|
30488 | 921 |
|
26126 | 922 |
from pn[unfolded prime_def] have "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
923 |
using n |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
924 |
apply (cases "n = 0 \<or> n=1",simp) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
925 |
by (clarsimp, erule_tac x="p" in allE, auto)} |
26126 | 926 |
moreover |
927 |
{assume H: "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n" |
|
928 |
from n have n1: "n > 1" by arith |
|
929 |
{fix m assume m: "m dvd n" "m\<noteq>1" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
930 |
from prime_factor[OF m(2)] obtain p where |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
931 |
p: "prime p" "p dvd m" by blast |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
932 |
from dvd_trans[OF p(2) m(1)] p(1) H have "p = n" by blast |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
933 |
with p(2) have "n dvd m" by simp |
33657 | 934 |
hence "m=n" using dvd_antisym[OF m(1)] by simp } |
26126 | 935 |
with n1 have "prime n" unfolding prime_def by auto } |
30488 | 936 |
ultimately have ?thesis using n by blast} |
937 |
ultimately show ?thesis by auto |
|
26126 | 938 |
qed |
939 |
||
940 |
lemma prime_divisor_sqrt: |
|
53077 | 941 |
"prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)" |
26126 | 942 |
proof- |
30488 | 943 |
{assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1 |
26126 | 944 |
by (auto simp add: nat_power_eq_0_iff)} |
945 |
moreover |
|
946 |
{assume n: "n\<noteq>0" "n\<noteq>1" |
|
947 |
hence np: "n > 1" by arith |
|
53077 | 948 |
{fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n" |
26126 | 949 |
from H d have d1n: "d = 1 \<or> d=n" by blast |
950 |
{assume dn: "d=n" |
|
53077 | 951 |
have "n\<^sup>2 > n*1" using n by (simp add: power2_eq_square) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
952 |
with dn d(2) have "d=1" by simp} |
26126 | 953 |
with d1n have "d = 1" by blast } |
954 |
moreover |
|
53077 | 955 |
{fix d assume d: "d dvd n" and H: "\<forall>d'. d' dvd n \<and> d'\<^sup>2 \<le> n \<longrightarrow> d' = 1" |
26126 | 956 |
from d n have "d \<noteq> 0" apply - apply (rule ccontr) by simp |
957 |
hence dp: "d > 0" by simp |
|
958 |
from d[unfolded dvd_def] obtain e where e: "n= d*e" by blast |
|
959 |
from n dp e have ep:"e > 0" by simp |
|
53077 | 960 |
have "d\<^sup>2 \<le> n \<or> e\<^sup>2 \<le> n" using dp ep |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
961 |
by (auto simp add: e power2_eq_square mult_le_cancel_left) |
26126 | 962 |
moreover |
53077 | 963 |
{assume h: "d\<^sup>2 \<le> n" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
964 |
from H[rule_format, of d] h d have "d = 1" by blast} |
26126 | 965 |
moreover |
53077 | 966 |
{assume h: "e\<^sup>2 \<le> n" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
967 |
from e have "e dvd n" unfolding dvd_def by (simp add: mult.commute) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
968 |
with H[rule_format, of e] h have "e=1" by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
969 |
with e have "d = n" by simp} |
26126 | 970 |
ultimately have "d=1 \<or> d=n" by blast} |
971 |
ultimately have ?thesis unfolding prime_def using np n(2) by blast} |
|
972 |
ultimately show ?thesis by auto |
|
973 |
qed |
|
974 |
lemma prime_prime_factor_sqrt: |
|
53077 | 975 |
"prime n \<longleftrightarrow> n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)" |
26126 | 976 |
(is "?lhs \<longleftrightarrow>?rhs") |
977 |
proof- |
|
978 |
{assume "n=0 \<or> n=1" hence ?thesis using prime_0 prime_1 by auto} |
|
979 |
moreover |
|
980 |
{assume n: "n\<noteq>0" "n\<noteq>1" |
|
981 |
{assume H: ?lhs |
|
30488 | 982 |
from H[unfolded prime_divisor_sqrt] n |
41541 | 983 |
have ?rhs |
984 |
apply clarsimp |
|
985 |
apply (erule_tac x="p" in allE) |
|
986 |
apply simp |
|
987 |
done |
|
26126 | 988 |
} |
989 |
moreover |
|
990 |
{assume H: ?rhs |
|
53077 | 991 |
{fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
992 |
from prime_factor[OF d(3)] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
993 |
obtain p where p: "prime p" "p dvd d" by blast |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
994 |
from n have np: "n > 0" by arith |
63833 | 995 |
have "d \<noteq> 0" by (rule ccontr) (use d(1) n in auto) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
996 |
hence dp: "d > 0" by arith |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
997 |
from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2) |
53077 | 998 |
have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
999 |
with H n p(1) dvd_trans[OF p(2) d(1)] have False by blast} |
26126 | 1000 |
with n prime_divisor_sqrt have ?lhs by auto} |
1001 |
ultimately have ?thesis by blast } |
|
1002 |
ultimately show ?thesis by (cases "n=0 \<or> n=1", auto) |
|
1003 |
qed |
|
1004 |
(* Pocklington theorem. *) |
|
1005 |
||
1006 |
lemma pocklington_lemma: |
|
1007 |
assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)" |
|
1008 |
and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n" |
|
1009 |
and pp: "prime p" and pn: "p dvd n" |
|
1010 |
shows "[p = 1] (mod q)" |
|
1011 |
proof- |
|
1012 |
from pp prime_0 prime_1 have p01: "p \<noteq> 0" "p \<noteq> 1" by - (rule ccontr, simp)+ |
|
30488 | 1013 |
from cong_1_divides[OF an, unfolded nqr, unfolded dvd_def] |
26126 | 1014 |
obtain k where k: "a ^ (q * r) - 1 = n*k" by blast |
1015 |
from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast |
|
1016 |
{assume a0: "a = 0" |
|
1017 |
hence "a^ (n - 1) = 0" using n by (simp add: power_0_left) |
|
1018 |
with n an mod_less[of 1 n] have False by (simp add: power_0_left modeq_def)} |
|
1019 |
hence a0: "a\<noteq>0" .. |
|
41541 | 1020 |
from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp |
26126 | 1021 |
hence "(a ^ (q * r) - 1) + 1 = a ^ (q * r)" by simp |
1022 |
with k l have "a ^ (q * r) = p*l*k + 1" by simp |
|
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
1023 |
hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps) |
26126 | 1024 |
hence odq: "ord p (a^r) dvd q" |
1025 |
unfolding ord_divides[symmetric] power_mult[symmetric] nat_mod by blast |
|
1026 |
from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast |
|
30488 | 1027 |
{assume d1: "d \<noteq> 1" |
26126 | 1028 |
from prime_factor[OF d1] obtain P where P: "prime P" "P dvd d" by blast |
1029 |
from d dvd_mult[OF P(2), of "ord p (a^r)"] have Pq: "P dvd q" by simp |
|
1030 |
from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast |
|
1031 |
from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast |
|
63833 | 1032 |
have P0: "P \<noteq> 0" by (rule ccontr) (use P(1) prime_0 in simp) |
26126 | 1033 |
from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast |
1034 |
from d s t P0 have s': "ord p (a^r) * t = s" by algebra |
|
1035 |
have "ord p (a^r) * t*r = r * ord p (a^r) * t" by algebra |
|
1036 |
hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t" |
|
1037 |
by (simp only: power_mult) |
|
30488 | 1038 |
have "[((a ^ r) ^ ord p (a^r)) ^ t= 1^t] (mod p)" |
26126 | 1039 |
by (rule cong_exp, rule ord) |
30488 | 1040 |
then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)" |
26158 | 1041 |
by (simp add: power_Suc0) |
26126 | 1042 |
from cong_1_divides[OF th] exps have pd0: "p dvd a^(ord p (a^r) * t*r) - 1" by simp |
1043 |
from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp |
|
1044 |
with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp |
|
1045 |
with p01 pn pd0 have False unfolding coprime by auto} |
|
30488 | 1046 |
hence d1: "d = 1" by blast |
1047 |
hence o: "ord p (a^r) = q" using d by simp |
|
26126 | 1048 |
from pp phi_prime[of p] have phip: " \<phi> p = p - 1" by simp |
1049 |
{fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1" |
|
1050 |
from pp[unfolded prime_def] d have dp: "d = p" by blast |
|
1051 |
from n have n12:"Suc (n - 2) = n - 1" by arith |
|
1052 |
with divides_rexp[OF d(2)[unfolded dp], of "n - 2"] |
|
1053 |
have th0: "p dvd a ^ (n - 1)" by simp |
|
1054 |
from n have n0: "n \<noteq> 0" by simp |
|
63833 | 1055 |
have a0: "a \<noteq> 0" |
1056 |
by (rule ccontr) (use d(2) an n12[symmetric] in \<open>simp add: modeq_def\<close>) |
|
41541 | 1057 |
have th1: "a^ (n - 1) \<noteq> 0" using n d(2) dp a0 by auto |
30488 | 1058 |
from coprime_minus1[OF th1, unfolded coprime] |
26126 | 1059 |
dvd_trans[OF pn cong_1_divides[OF an]] th0 d(3) dp |
1060 |
have False by auto} |
|
30488 | 1061 |
hence cpa: "coprime p a" using coprime by auto |
1062 |
from coprime_exp[OF cpa, of r] coprime_commute |
|
26126 | 1063 |
have arp: "coprime (a^r) p" by blast |
1064 |
from fermat_little[OF arp, simplified ord_divides] o phip |
|
1065 |
have "q dvd (p - 1)" by simp |
|
1066 |
then obtain d where d:"p - 1 = q * d" unfolding dvd_def by blast |
|
63833 | 1067 |
have p0: "p \<noteq> 0" by (rule ccontr) (use prime_0 pp in auto) |
26126 | 1068 |
from p0 d have "p + q * 0 = 1 + q * d" by simp |
1069 |
with nat_mod[of p 1 q, symmetric] |
|
1070 |
show ?thesis by blast |
|
1071 |
qed |
|
1072 |
||
1073 |
lemma pocklington: |
|
53077 | 1074 |
assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2" |
26126 | 1075 |
and an: "[a^ (n - 1) = 1] (mod n)" |
1076 |
and aq:"\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a^ ((n - 1) div p) - 1) n" |
|
1077 |
shows "prime n" |
|
1078 |
unfolding prime_prime_factor_sqrt[of n] |
|
1079 |
proof- |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51489
diff
changeset
|
1080 |
let ?ths = "n \<noteq> 0 \<and> n \<noteq> 1 \<and> \<not> (\<exists>p. prime p \<and> p dvd n \<and> p\<^sup>2 \<le> n)" |
26126 | 1081 |
from n have n01: "n\<noteq>0" "n\<noteq>1" by arith+ |
53077 | 1082 |
{fix p assume p: "prime p" "p dvd n" "p\<^sup>2 \<le> n" |
26126 | 1083 |
from p(3) sqr have "p^(Suc 1) \<le> q^(Suc 1)" by (simp add: power2_eq_square) |
1084 |
hence pq: "p \<le> q" unfolding exp_mono_le . |
|
1085 |
from pocklington_lemma[OF n nqr an aq p(1,2)] cong_1_divides |
|
1086 |
have th: "q dvd p - 1" by blast |
|
1087 |
have "p - 1 \<noteq> 0"using prime_ge_2[OF p(1)] by arith |
|
1088 |
with divides_ge[OF th] pq have False by arith } |
|
1089 |
with n01 show ?ths by blast |
|
1090 |
qed |
|
1091 |
||
1092 |
(* Variant for application, to separate the exponentiation. *) |
|
1093 |
lemma pocklington_alt: |
|
53077 | 1094 |
assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and sqr: "n \<le> q\<^sup>2" |
26126 | 1095 |
and an: "[a^ (n - 1) = 1] (mod n)" |
1096 |
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)" |
|
1097 |
shows "prime n" |
|
1098 |
proof- |
|
1099 |
{fix p assume p: "prime p" "p dvd q" |
|
30488 | 1100 |
from aq[rule_format] p obtain b where |
26126 | 1101 |
b: "[a^((n - 1) div p) = b] (mod n)" "coprime (b - 1) n" by blast |
1102 |
{assume a0: "a=0" |
|
1103 |
from n an have "[0 = 1] (mod n)" unfolding a0 power_0_left by auto |
|
1104 |
hence False using n by (simp add: modeq_def dvd_eq_mod_eq_0[symmetric])} |
|
1105 |
hence a0: "a\<noteq> 0" .. |
|
1106 |
hence a1: "a \<ge> 1" by arith |
|
1107 |
from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n - 1) div p)" . |
|
1108 |
{assume b0: "b = 0" |
|
30488 | 1109 |
from p(2) nqr have "(n - 1) mod p = 0" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
1110 |
apply (simp only: dvd_eq_mod_eq_0[symmetric]) by (rule dvd_mult2, simp) |
30488 | 1111 |
with mod_div_equality[of "n - 1" p] |
1112 |
have "(n - 1) div p * p= n - 1" by auto |
|
26126 | 1113 |
hence eq: "(a^((n - 1) div p))^p = a^(n - 1)" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
1114 |
by (simp only: power_mult[symmetric]) |
26126 | 1115 |
from prime_ge_2[OF p(1)] have pS: "Suc (p - 1) = p" by arith |
1116 |
from b(1) have d: "n dvd a^((n - 1) div p)" unfolding b0 cong_0_divides . |
|
1117 |
from divides_rexp[OF d, of "p - 1"] pS eq cong_divides[OF an] n |
|
1118 |
have False by simp} |
|
30488 | 1119 |
then have b0: "b \<noteq> 0" .. |
1120 |
hence b1: "b \<ge> 1" by arith |
|
26126 | 1121 |
from cong_coprime[OF cong_sub[OF b(1) cong_refl[of 1] ath b1]] b(2) nqr |
1122 |
have "coprime (a ^ ((n - 1) div p) - 1) n" by (simp add: coprime_commute)} |
|
30488 | 1123 |
hence th: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n " |
26126 | 1124 |
by blast |
1125 |
from pocklington[OF n nqr sqr an th] show ?thesis . |
|
1126 |
qed |
|
1127 |
||
1128 |
(* Prime factorizations. *) |
|
1129 |
||
1130 |
definition "primefact ps n = (foldr op * ps 1 = n \<and> (\<forall>p\<in> set ps. prime p))" |
|
1131 |
||
1132 |
lemma primefact: assumes n: "n \<noteq> 0" |
|
1133 |
shows "\<exists>ps. primefact ps n" |
|
1134 |
using n |
|
1135 |
proof(induct n rule: nat_less_induct) |
|
1136 |
fix n assume H: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>ps. primefact ps m)" and n: "n\<noteq>0" |
|
1137 |
let ?ths = "\<exists>ps. primefact ps n" |
|
30488 | 1138 |
{assume "n = 1" |
26126 | 1139 |
hence "primefact [] n" by (simp add: primefact_def) |
1140 |
hence ?ths by blast } |
|
1141 |
moreover |
|
1142 |
{assume n1: "n \<noteq> 1" |
|
1143 |
with n have n2: "n \<ge> 2" by arith |
|
1144 |
from prime_factor[OF n1] obtain p where p: "prime p" "p dvd n" by blast |
|
1145 |
from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast |
|
1146 |
from n m have m0: "m > 0" "m\<noteq>0" by auto |
|
1147 |
from prime_ge_2[OF p(1)] have "1 < p" by arith |
|
1148 |
with m0 m have mn: "m < n" by auto |
|
1149 |
from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" .. |
|
1150 |
from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def) |
|
1151 |
hence ?ths by blast} |
|
1152 |
ultimately show ?ths by blast |
|
1153 |
qed |
|
1154 |
||
30488 | 1155 |
lemma primefact_contains: |
26126 | 1156 |
assumes pf: "primefact ps n" and p: "prime p" and pn: "p dvd n" |
1157 |
shows "p \<in> set ps" |
|
1158 |
using pf p pn |
|
1159 |
proof(induct ps arbitrary: p n) |
|
1160 |
case Nil thus ?case by (auto simp add: primefact_def) |
|
1161 |
next |
|
1162 |
case (Cons q qs p n) |
|
30488 | 1163 |
from Cons.prems[unfolded primefact_def] |
26126 | 1164 |
have q: "prime q" "q * foldr op * qs 1 = n" "\<forall>p \<in>set qs. prime p" and p: "prime p" "p dvd q * foldr op * qs 1" by simp_all |
1165 |
{assume "p dvd q" |
|
1166 |
with p(1) q(1) have "p = q" unfolding prime_def by auto |
|
1167 |
hence ?case by simp} |
|
1168 |
moreover |
|
1169 |
{ assume h: "p dvd foldr op * qs 1" |
|
30488 | 1170 |
from q(3) have pqs: "primefact qs (foldr op * qs 1)" |
26126 | 1171 |
by (simp add: primefact_def) |
1172 |
from Cons.hyps[OF pqs p(1) h] have ?case by simp} |
|
1173 |
ultimately show ?case using prime_divprod[OF p] by blast |
|
1174 |
qed |
|
1175 |
||
37602 | 1176 |
lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps" |
1177 |
by (auto simp add: primefact_def list_all_iff) |
|
26126 | 1178 |
|
1179 |
(* Variant of Lucas theorem. *) |
|
1180 |
||
1181 |
lemma lucas_primefact: |
|
30488 | 1182 |
assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)" |
1183 |
and psn: "foldr op * ps 1 = n - 1" |
|
26126 | 1184 |
and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps" |
1185 |
shows "prime n" |
|
1186 |
proof- |
|
1187 |
{fix p assume p: "prime p" "p dvd n - 1" "[a ^ ((n - 1) div p) = 1] (mod n)" |
|
30488 | 1188 |
from psn psp have psn1: "primefact ps (n - 1)" |
26126 | 1189 |
by (auto simp add: list_all_iff primefact_variant) |
1190 |
from p(3) primefact_contains[OF psn1 p(1,2)] psp |
|
1191 |
have False by (induct ps, auto)} |
|
1192 |
with lucas[OF n an] show ?thesis by blast |
|
1193 |
qed |
|
1194 |
||
1195 |
(* Variant of Pocklington theorem. *) |
|
1196 |
||
1197 |
lemma mod_le: assumes n: "n \<noteq> (0::nat)" shows "m mod n \<le> m" |
|
1198 |
proof- |
|
1199 |
from mod_div_equality[of m n] |
|
30488 | 1200 |
have "\<exists>x. x + m mod n = m" by blast |
26126 | 1201 |
then show ?thesis by auto |
1202 |
qed |
|
30488 | 1203 |
|
26126 | 1204 |
|
1205 |
lemma pocklington_primefact: |
|
53077 | 1206 |
assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2" |
30488 | 1207 |
and arnb: "(a^r) mod n = b" and psq: "foldr op * ps 1 = q" |
26126 | 1208 |
and bqn: "(b^q) mod n = 1" |
1209 |
and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps" |
|
1210 |
shows "prime n" |
|
1211 |
proof- |
|
1212 |
from bqn psp qrn |
|
1213 |
have bqn: "a ^ (n - 1) mod n = 1" |
|
30488 | 1214 |
and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps" unfolding arnb[symmetric] power_mod |
29667 | 1215 |
by (simp_all add: power_mult[symmetric] algebra_simps) |
26126 | 1216 |
from n have n0: "n > 0" by arith |
1217 |
from mod_div_equality[of "a^(n - 1)" n] |
|
1218 |
mod_less_divisor[OF n0, of "a^(n - 1)"] |
|
30488 | 1219 |
have an1: "[a ^ (n - 1) = 1] (mod n)" |
26126 | 1220 |
unfolding nat_mod bqn |
1221 |
apply - |
|
1222 |
apply (rule exI[where x="0"]) |
|
1223 |
apply (rule exI[where x="a^(n - 1) div n"]) |
|
29667 | 1224 |
by (simp add: algebra_simps) |
26126 | 1225 |
{fix p assume p: "prime p" "p dvd q" |
1226 |
from psp psq have pfpsq: "primefact ps q" |
|
1227 |
by (auto simp add: primefact_variant list_all_iff) |
|
30488 | 1228 |
from psp primefact_contains[OF pfpsq p] |
26126 | 1229 |
have p': "coprime (a ^ (r * (q div p)) mod n - 1) n" |
1230 |
by (simp add: list_all_iff) |
|
1231 |
from prime_ge_2[OF p(1)] have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)" by arith+ |
|
30488 | 1232 |
from div_mult1_eq[of r q p] p(2) |
26126 | 1233 |
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:
57418
diff
changeset
|
1234 |
unfolding qrn[symmetric] dvd_eq_mod_eq_0 by (simp add: mult.commute) |
26126 | 1235 |
have ath: "\<And>a (b::nat). a <= b \<Longrightarrow> a \<noteq> 0 ==> 1 <= a \<and> 1 <= b" by arith |
1236 |
from n0 have n00: "n \<noteq> 0" by arith |
|
1237 |
from mod_le[OF n00] |
|
1238 |
have th10: "a ^ ((n - 1) div p) mod n \<le> a ^ ((n - 1) div p)" . |
|
1239 |
{assume "a ^ ((n - 1) div p) mod n = 0" |
|
1240 |
then obtain s where s: "a ^ ((n - 1) div p) = n*s" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
1241 |
unfolding mod_eq_0_iff by blast |
26126 | 1242 |
hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp |
1243 |
from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto |
|
1244 |
from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n - 1" p] |
|
30488 | 1245 |
have npp: "(n - 1) div p * p = n - 1" by (simp add: dvd_eq_mod_eq_0) |
26126 | 1246 |
with eq0 have "a^ (n - 1) = (n*s)^p" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
1247 |
by (simp add: power_mult[symmetric]) |
26126 | 1248 |
hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
1249 |
also have "\<dots> = 0" by (simp add: mult.assoc) |
26126 | 1250 |
finally have False by simp } |
30488 | 1251 |
then have th11: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto |
1252 |
have th1: "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)" |
|
1253 |
unfolding modeq_def by simp |
|
26126 | 1254 |
from cong_sub[OF th1 cong_refl[of 1]] ath[OF th10 th11] |
1255 |
have th: "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)" |
|
30488 | 1256 |
by blast |
1257 |
from cong_coprime[OF th] p'[unfolded eq1] |
|
26126 | 1258 |
have "coprime (a ^ ((n - 1) div p) - 1) n" by (simp add: coprime_commute) } |
1259 |
with pocklington[OF n qrn[symmetric] nq2 an1] |
|
30488 | 1260 |
show ?thesis by blast |
26126 | 1261 |
qed |
1262 |
||
1263 |
end |