wenzelm@11049
|
1 |
(* Title: HOL/NumberTheory/WilsonRuss.thy
|
paulson@9508
|
2 |
ID: $Id$
|
wenzelm@11049
|
3 |
Author: Thomas M. Rasmussen
|
wenzelm@11049
|
4 |
Copyright 2000 University of Cambridge
|
paulson@13833
|
5 |
|
paulson@13833
|
6 |
Changes by Jeremy Avigad, 2003/02/21:
|
paulson@13833
|
7 |
repaired proof of prime_g_5
|
paulson@9508
|
8 |
*)
|
paulson@9508
|
9 |
|
wenzelm@11049
|
10 |
header {* Wilson's Theorem according to Russinoff *}
|
wenzelm@11049
|
11 |
|
wenzelm@11049
|
12 |
theory WilsonRuss = EulerFermat:
|
wenzelm@11049
|
13 |
|
wenzelm@11049
|
14 |
text {*
|
wenzelm@11049
|
15 |
Wilson's Theorem following quite closely Russinoff's approach
|
wenzelm@11049
|
16 |
using Boyer-Moore (using finite sets instead of lists, though).
|
wenzelm@11049
|
17 |
*}
|
wenzelm@11049
|
18 |
|
wenzelm@11049
|
19 |
subsection {* Definitions and lemmas *}
|
paulson@9508
|
20 |
|
paulson@9508
|
21 |
consts
|
wenzelm@11049
|
22 |
inv :: "int => int => int"
|
wenzelm@11049
|
23 |
wset :: "int * int => int set"
|
paulson@9508
|
24 |
|
paulson@9508
|
25 |
defs
|
wenzelm@11704
|
26 |
inv_def: "inv p a == (a^(nat (p - 2))) mod p"
|
paulson@9508
|
27 |
|
wenzelm@11049
|
28 |
recdef wset
|
wenzelm@11049
|
29 |
"measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
|
wenzelm@11049
|
30 |
"wset (a, p) =
|
paulson@11868
|
31 |
(if 1 < a then
|
paulson@11868
|
32 |
let ws = wset (a - 1, p)
|
wenzelm@11049
|
33 |
in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})"
|
wenzelm@11049
|
34 |
|
wenzelm@11049
|
35 |
|
wenzelm@11049
|
36 |
text {* \medskip @{term [source] inv} *}
|
wenzelm@11049
|
37 |
|
wenzelm@13524
|
38 |
lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
|
paulson@13833
|
39 |
by (subst int_int_eq [symmetric], auto)
|
wenzelm@11049
|
40 |
|
wenzelm@11049
|
41 |
lemma inv_is_inv:
|
paulson@11868
|
42 |
"p \<in> zprime \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
|
wenzelm@11049
|
43 |
apply (unfold inv_def)
|
wenzelm@11049
|
44 |
apply (subst zcong_zmod)
|
wenzelm@11049
|
45 |
apply (subst zmod_zmult1_eq [symmetric])
|
wenzelm@11049
|
46 |
apply (subst zcong_zmod [symmetric])
|
wenzelm@11049
|
47 |
apply (subst power_Suc [symmetric])
|
wenzelm@13524
|
48 |
apply (subst inv_is_inv_aux)
|
wenzelm@11049
|
49 |
apply (erule_tac [2] Little_Fermat)
|
wenzelm@11049
|
50 |
apply (erule_tac [2] zdvd_not_zless)
|
paulson@13833
|
51 |
apply (unfold zprime_def, auto)
|
wenzelm@11049
|
52 |
done
|
wenzelm@11049
|
53 |
|
wenzelm@11049
|
54 |
lemma inv_distinct:
|
paulson@11868
|
55 |
"p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> a \<noteq> inv p a"
|
wenzelm@11049
|
56 |
apply safe
|
wenzelm@11049
|
57 |
apply (cut_tac a = a and p = p in zcong_square)
|
paulson@13833
|
58 |
apply (cut_tac [3] a = a and p = p in inv_is_inv, auto)
|
paulson@11868
|
59 |
apply (subgoal_tac "a = 1")
|
wenzelm@11049
|
60 |
apply (rule_tac [2] m = p in zcong_zless_imp_eq)
|
paulson@11868
|
61 |
apply (subgoal_tac [7] "a = p - 1")
|
paulson@13833
|
62 |
apply (rule_tac [8] m = p in zcong_zless_imp_eq, auto)
|
wenzelm@11049
|
63 |
done
|
wenzelm@11049
|
64 |
|
wenzelm@11049
|
65 |
lemma inv_not_0:
|
paulson@11868
|
66 |
"p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 0"
|
wenzelm@11049
|
67 |
apply safe
|
wenzelm@11049
|
68 |
apply (cut_tac a = a and p = p in inv_is_inv)
|
paulson@13833
|
69 |
apply (unfold zcong_def, auto)
|
paulson@11868
|
70 |
apply (subgoal_tac "\<not> p dvd 1")
|
wenzelm@11049
|
71 |
apply (rule_tac [2] zdvd_not_zless)
|
paulson@11868
|
72 |
apply (subgoal_tac "p dvd 1")
|
wenzelm@11049
|
73 |
prefer 2
|
paulson@13833
|
74 |
apply (subst zdvd_zminus_iff [symmetric], auto)
|
wenzelm@11049
|
75 |
done
|
wenzelm@11049
|
76 |
|
wenzelm@11049
|
77 |
lemma inv_not_1:
|
paulson@11868
|
78 |
"p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 1"
|
wenzelm@11049
|
79 |
apply safe
|
wenzelm@11049
|
80 |
apply (cut_tac a = a and p = p in inv_is_inv)
|
wenzelm@11049
|
81 |
prefer 4
|
wenzelm@11049
|
82 |
apply simp
|
paulson@11868
|
83 |
apply (subgoal_tac "a = 1")
|
paulson@13833
|
84 |
apply (rule_tac [2] zcong_zless_imp_eq, auto)
|
wenzelm@11049
|
85 |
done
|
wenzelm@11049
|
86 |
|
wenzelm@13524
|
87 |
lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
|
wenzelm@11049
|
88 |
apply (unfold zcong_def)
|
obua@14738
|
89 |
apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
|
paulson@11868
|
90 |
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
|
paulson@14271
|
91 |
apply (simp add: mult_commute)
|
wenzelm@11049
|
92 |
apply (subst zdvd_zminus_iff)
|
wenzelm@11049
|
93 |
apply (subst zdvd_reduce)
|
paulson@11868
|
94 |
apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
|
paulson@13833
|
95 |
apply (subst zdvd_reduce, auto)
|
wenzelm@11049
|
96 |
done
|
wenzelm@11049
|
97 |
|
wenzelm@11049
|
98 |
lemma inv_not_p_minus_1:
|
paulson@11868
|
99 |
"p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> p - 1"
|
wenzelm@11049
|
100 |
apply safe
|
paulson@13833
|
101 |
apply (cut_tac a = a and p = p in inv_is_inv, auto)
|
wenzelm@13524
|
102 |
apply (simp add: inv_not_p_minus_1_aux)
|
paulson@11868
|
103 |
apply (subgoal_tac "a = p - 1")
|
paulson@13833
|
104 |
apply (rule_tac [2] zcong_zless_imp_eq, auto)
|
wenzelm@11049
|
105 |
done
|
wenzelm@11049
|
106 |
|
wenzelm@11049
|
107 |
lemma inv_g_1:
|
paulson@11868
|
108 |
"p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> 1 < inv p a"
|
paulson@11868
|
109 |
apply (case_tac "0\<le> inv p a")
|
paulson@11868
|
110 |
apply (subgoal_tac "inv p a \<noteq> 1")
|
paulson@11868
|
111 |
apply (subgoal_tac "inv p a \<noteq> 0")
|
wenzelm@11049
|
112 |
apply (subst order_less_le)
|
wenzelm@11049
|
113 |
apply (subst zle_add1_eq_le [symmetric])
|
wenzelm@11049
|
114 |
apply (subst order_less_le)
|
wenzelm@11049
|
115 |
apply (rule_tac [2] inv_not_0)
|
paulson@13833
|
116 |
apply (rule_tac [5] inv_not_1, auto)
|
paulson@13833
|
117 |
apply (unfold inv_def zprime_def, simp)
|
wenzelm@11049
|
118 |
done
|
wenzelm@11049
|
119 |
|
wenzelm@11049
|
120 |
lemma inv_less_p_minus_1:
|
paulson@11868
|
121 |
"p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a < p - 1"
|
wenzelm@11049
|
122 |
apply (case_tac "inv p a < p")
|
wenzelm@11049
|
123 |
apply (subst order_less_le)
|
paulson@13833
|
124 |
apply (simp add: inv_not_p_minus_1, auto)
|
paulson@13833
|
125 |
apply (unfold inv_def zprime_def, simp)
|
wenzelm@11049
|
126 |
done
|
wenzelm@11049
|
127 |
|
wenzelm@13524
|
128 |
lemma inv_inv_aux: "5 \<le> p ==>
|
paulson@11868
|
129 |
nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
|
wenzelm@11049
|
130 |
apply (subst int_int_eq [symmetric])
|
wenzelm@11049
|
131 |
apply (simp add: zmult_int [symmetric])
|
wenzelm@11049
|
132 |
apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2)
|
wenzelm@11049
|
133 |
done
|
wenzelm@11049
|
134 |
|
wenzelm@11049
|
135 |
lemma zcong_zpower_zmult:
|
paulson@11868
|
136 |
"[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)"
|
wenzelm@11049
|
137 |
apply (induct z)
|
wenzelm@11049
|
138 |
apply (auto simp add: zpower_zadd_distrib)
|
paulson@11868
|
139 |
apply (subgoal_tac "zcong (x^y * x^(y * n)) (1 * 1) p")
|
paulson@13833
|
140 |
apply (rule_tac [2] zcong_zmult, simp_all)
|
wenzelm@11049
|
141 |
done
|
wenzelm@11049
|
142 |
|
wenzelm@11049
|
143 |
lemma inv_inv: "p \<in> zprime \<Longrightarrow>
|
paulson@11868
|
144 |
5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
|
wenzelm@11049
|
145 |
apply (unfold inv_def)
|
wenzelm@11049
|
146 |
apply (subst zpower_zmod)
|
wenzelm@11049
|
147 |
apply (subst zpower_zpower)
|
wenzelm@11049
|
148 |
apply (rule zcong_zless_imp_eq)
|
wenzelm@11049
|
149 |
prefer 5
|
wenzelm@11049
|
150 |
apply (subst zcong_zmod)
|
wenzelm@11049
|
151 |
apply (subst mod_mod_trivial)
|
wenzelm@11049
|
152 |
apply (subst zcong_zmod [symmetric])
|
wenzelm@13524
|
153 |
apply (subst inv_inv_aux)
|
wenzelm@11049
|
154 |
apply (subgoal_tac [2]
|
paulson@11868
|
155 |
"zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p")
|
wenzelm@11049
|
156 |
apply (rule_tac [3] zcong_zmult)
|
wenzelm@11049
|
157 |
apply (rule_tac [4] zcong_zpower_zmult)
|
wenzelm@11049
|
158 |
apply (erule_tac [4] Little_Fermat)
|
paulson@13833
|
159 |
apply (rule_tac [4] zdvd_not_zless, simp_all)
|
wenzelm@11049
|
160 |
done
|
wenzelm@11049
|
161 |
|
wenzelm@11049
|
162 |
|
wenzelm@11049
|
163 |
text {* \medskip @{term wset} *}
|
wenzelm@11049
|
164 |
|
wenzelm@11049
|
165 |
declare wset.simps [simp del]
|
wenzelm@11049
|
166 |
|
wenzelm@11049
|
167 |
lemma wset_induct:
|
wenzelm@11049
|
168 |
"(!!a p. P {} a p) \<Longrightarrow>
|
paulson@11868
|
169 |
(!!a p. 1 < (a::int) \<Longrightarrow> P (wset (a - 1, p)) (a - 1) p
|
wenzelm@11049
|
170 |
==> P (wset (a, p)) a p)
|
wenzelm@11049
|
171 |
==> P (wset (u, v)) u v"
|
wenzelm@11049
|
172 |
proof -
|
wenzelm@11549
|
173 |
case rule_context
|
wenzelm@11049
|
174 |
show ?thesis
|
paulson@13833
|
175 |
apply (rule wset.induct, safe)
|
paulson@11868
|
176 |
apply (case_tac [2] "1 < a")
|
paulson@13833
|
177 |
apply (rule_tac [2] rule_context, simp_all)
|
wenzelm@11549
|
178 |
apply (simp_all add: wset.simps rule_context)
|
wenzelm@11049
|
179 |
done
|
wenzelm@11049
|
180 |
qed
|
wenzelm@11049
|
181 |
|
wenzelm@11049
|
182 |
lemma wset_mem_imp_or [rule_format]:
|
paulson@11868
|
183 |
"1 < a \<Longrightarrow> b \<notin> wset (a - 1, p)
|
wenzelm@11049
|
184 |
==> b \<in> wset (a, p) --> b = a \<or> b = inv p a"
|
wenzelm@11049
|
185 |
apply (subst wset.simps)
|
paulson@13833
|
186 |
apply (unfold Let_def, simp)
|
wenzelm@11049
|
187 |
done
|
wenzelm@11049
|
188 |
|
paulson@11868
|
189 |
lemma wset_mem_mem [simp]: "1 < a ==> a \<in> wset (a, p)"
|
wenzelm@11049
|
190 |
apply (subst wset.simps)
|
paulson@13833
|
191 |
apply (unfold Let_def, simp)
|
wenzelm@11049
|
192 |
done
|
wenzelm@11049
|
193 |
|
paulson@11868
|
194 |
lemma wset_subset: "1 < a \<Longrightarrow> b \<in> wset (a - 1, p) ==> b \<in> wset (a, p)"
|
wenzelm@11049
|
195 |
apply (subst wset.simps)
|
paulson@13833
|
196 |
apply (unfold Let_def, auto)
|
wenzelm@11049
|
197 |
done
|
wenzelm@11049
|
198 |
|
wenzelm@11049
|
199 |
lemma wset_g_1 [rule_format]:
|
paulson@11868
|
200 |
"p \<in> zprime --> a < p - 1 --> b \<in> wset (a, p) --> 1 < b"
|
paulson@13833
|
201 |
apply (induct a p rule: wset_induct, auto)
|
wenzelm@11049
|
202 |
apply (case_tac "b = a")
|
wenzelm@11049
|
203 |
apply (case_tac [2] "b = inv p a")
|
wenzelm@11049
|
204 |
apply (subgoal_tac [3] "b = a \<or> b = inv p a")
|
wenzelm@11049
|
205 |
apply (rule_tac [4] wset_mem_imp_or)
|
wenzelm@11049
|
206 |
prefer 2
|
wenzelm@11049
|
207 |
apply simp
|
paulson@13833
|
208 |
apply (rule inv_g_1, auto)
|
wenzelm@11049
|
209 |
done
|
wenzelm@11049
|
210 |
|
wenzelm@11049
|
211 |
lemma wset_less [rule_format]:
|
paulson@11868
|
212 |
"p \<in> zprime --> a < p - 1 --> b \<in> wset (a, p) --> b < p - 1"
|
paulson@13833
|
213 |
apply (induct a p rule: wset_induct, auto)
|
wenzelm@11049
|
214 |
apply (case_tac "b = a")
|
wenzelm@11049
|
215 |
apply (case_tac [2] "b = inv p a")
|
wenzelm@11049
|
216 |
apply (subgoal_tac [3] "b = a \<or> b = inv p a")
|
wenzelm@11049
|
217 |
apply (rule_tac [4] wset_mem_imp_or)
|
wenzelm@11049
|
218 |
prefer 2
|
wenzelm@11049
|
219 |
apply simp
|
paulson@13833
|
220 |
apply (rule inv_less_p_minus_1, auto)
|
wenzelm@11049
|
221 |
done
|
wenzelm@11049
|
222 |
|
wenzelm@11049
|
223 |
lemma wset_mem [rule_format]:
|
wenzelm@11049
|
224 |
"p \<in> zprime -->
|
paulson@11868
|
225 |
a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset (a, p)"
|
paulson@13833
|
226 |
apply (induct a p rule: wset.induct, auto)
|
wenzelm@11049
|
227 |
apply (subgoal_tac "b = a")
|
wenzelm@11049
|
228 |
apply (rule_tac [2] zle_anti_sym)
|
wenzelm@11049
|
229 |
apply (rule_tac [4] wset_subset)
|
wenzelm@11049
|
230 |
apply (simp (no_asm_simp))
|
wenzelm@11049
|
231 |
apply auto
|
wenzelm@11049
|
232 |
done
|
wenzelm@11049
|
233 |
|
wenzelm@11049
|
234 |
lemma wset_mem_inv_mem [rule_format]:
|
paulson@11868
|
235 |
"p \<in> zprime --> 5 \<le> p --> a < p - 1 --> b \<in> wset (a, p)
|
wenzelm@11049
|
236 |
--> inv p b \<in> wset (a, p)"
|
paulson@13833
|
237 |
apply (induct a p rule: wset_induct, auto)
|
wenzelm@11049
|
238 |
apply (case_tac "b = a")
|
wenzelm@11049
|
239 |
apply (subst wset.simps)
|
wenzelm@11049
|
240 |
apply (unfold Let_def)
|
paulson@13833
|
241 |
apply (rule_tac [3] wset_subset, auto)
|
wenzelm@11049
|
242 |
apply (case_tac "b = inv p a")
|
wenzelm@11049
|
243 |
apply (simp (no_asm_simp))
|
wenzelm@11049
|
244 |
apply (subst inv_inv)
|
wenzelm@11049
|
245 |
apply (subgoal_tac [6] "b = a \<or> b = inv p a")
|
paulson@13833
|
246 |
apply (rule_tac [7] wset_mem_imp_or, auto)
|
wenzelm@11049
|
247 |
done
|
wenzelm@11049
|
248 |
|
wenzelm@11049
|
249 |
lemma wset_inv_mem_mem:
|
paulson@11868
|
250 |
"p \<in> zprime \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - 1 \<Longrightarrow> 1 < b \<Longrightarrow> b < p - 1
|
wenzelm@11049
|
251 |
\<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
|
wenzelm@11049
|
252 |
apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
|
wenzelm@11049
|
253 |
apply (rule_tac [2] wset_mem_inv_mem)
|
paulson@13833
|
254 |
apply (rule inv_inv, simp_all)
|
wenzelm@11049
|
255 |
done
|
wenzelm@11049
|
256 |
|
wenzelm@11049
|
257 |
lemma wset_fin: "finite (wset (a, p))"
|
wenzelm@11049
|
258 |
apply (induct a p rule: wset_induct)
|
wenzelm@11049
|
259 |
prefer 2
|
wenzelm@11049
|
260 |
apply (subst wset.simps)
|
paulson@13833
|
261 |
apply (unfold Let_def, auto)
|
wenzelm@11049
|
262 |
done
|
wenzelm@11049
|
263 |
|
wenzelm@11049
|
264 |
lemma wset_zcong_prod_1 [rule_format]:
|
wenzelm@11049
|
265 |
"p \<in> zprime -->
|
paulson@11868
|
266 |
5 \<le> p --> a < p - 1 --> [setprod (wset (a, p)) = 1] (mod p)"
|
wenzelm@11049
|
267 |
apply (induct a p rule: wset_induct)
|
wenzelm@11049
|
268 |
prefer 2
|
wenzelm@11049
|
269 |
apply (subst wset.simps)
|
paulson@13833
|
270 |
apply (unfold Let_def, auto)
|
wenzelm@11049
|
271 |
apply (subst setprod_insert)
|
wenzelm@11049
|
272 |
apply (tactic {* stac (thm "setprod_insert") 3 *})
|
wenzelm@11049
|
273 |
apply (subgoal_tac [5]
|
paulson@11868
|
274 |
"zcong (a * inv p a * setprod (wset (a - 1, p))) (1 * 1) p")
|
wenzelm@11049
|
275 |
prefer 5
|
wenzelm@11049
|
276 |
apply (simp add: zmult_assoc)
|
wenzelm@11049
|
277 |
apply (rule_tac [5] zcong_zmult)
|
wenzelm@11049
|
278 |
apply (rule_tac [5] inv_is_inv)
|
wenzelm@11049
|
279 |
apply (tactic "Clarify_tac 4")
|
paulson@11868
|
280 |
apply (subgoal_tac [4] "a \<in> wset (a - 1, p)")
|
wenzelm@11049
|
281 |
apply (rule_tac [5] wset_inv_mem_mem)
|
wenzelm@11049
|
282 |
apply (simp_all add: wset_fin)
|
paulson@13833
|
283 |
apply (rule inv_distinct, auto)
|
wenzelm@11049
|
284 |
done
|
wenzelm@11049
|
285 |
|
wenzelm@11704
|
286 |
lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - 2) = wset (p - 2, p)"
|
wenzelm@11049
|
287 |
apply safe
|
wenzelm@11049
|
288 |
apply (erule wset_mem)
|
wenzelm@11049
|
289 |
apply (rule_tac [2] d22set_g_1)
|
wenzelm@11049
|
290 |
apply (rule_tac [3] d22set_le)
|
wenzelm@11049
|
291 |
apply (rule_tac [4] d22set_mem)
|
wenzelm@11049
|
292 |
apply (erule_tac [4] wset_g_1)
|
wenzelm@11049
|
293 |
prefer 6
|
wenzelm@11049
|
294 |
apply (subst zle_add1_eq_le [symmetric])
|
paulson@11868
|
295 |
apply (subgoal_tac "p - 2 + 1 = p - 1")
|
wenzelm@11049
|
296 |
apply (simp (no_asm_simp))
|
paulson@13833
|
297 |
apply (erule wset_less, auto)
|
wenzelm@11049
|
298 |
done
|
wenzelm@11049
|
299 |
|
wenzelm@11049
|
300 |
|
wenzelm@11049
|
301 |
subsection {* Wilson *}
|
wenzelm@11049
|
302 |
|
wenzelm@11704
|
303 |
lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
|
wenzelm@11049
|
304 |
apply (unfold zprime_def dvd_def)
|
paulson@13833
|
305 |
apply (case_tac "p = 4", auto)
|
wenzelm@11049
|
306 |
apply (rule notE)
|
wenzelm@11049
|
307 |
prefer 2
|
wenzelm@11049
|
308 |
apply assumption
|
wenzelm@11049
|
309 |
apply (simp (no_asm))
|
paulson@13833
|
310 |
apply (rule_tac x = 2 in exI)
|
paulson@13833
|
311 |
apply (safe, arith)
|
paulson@13833
|
312 |
apply (rule_tac x = 2 in exI, auto)
|
wenzelm@11049
|
313 |
done
|
wenzelm@11049
|
314 |
|
wenzelm@11049
|
315 |
theorem Wilson_Russ:
|
paulson@11868
|
316 |
"p \<in> zprime ==> [zfact (p - 1) = -1] (mod p)"
|
paulson@11868
|
317 |
apply (subgoal_tac "[(p - 1) * zfact (p - 2) = -1 * 1] (mod p)")
|
wenzelm@11049
|
318 |
apply (rule_tac [2] zcong_zmult)
|
wenzelm@11049
|
319 |
apply (simp only: zprime_def)
|
wenzelm@11049
|
320 |
apply (subst zfact.simps)
|
paulson@13833
|
321 |
apply (rule_tac t = "p - 1 - 1" and s = "p - 2" in subst, auto)
|
wenzelm@11049
|
322 |
apply (simp only: zcong_def)
|
wenzelm@11049
|
323 |
apply (simp (no_asm_simp))
|
wenzelm@11704
|
324 |
apply (case_tac "p = 2")
|
wenzelm@11049
|
325 |
apply (simp add: zfact.simps)
|
wenzelm@11704
|
326 |
apply (case_tac "p = 3")
|
wenzelm@11049
|
327 |
apply (simp add: zfact.simps)
|
wenzelm@11704
|
328 |
apply (subgoal_tac "5 \<le> p")
|
wenzelm@11049
|
329 |
apply (erule_tac [2] prime_g_5)
|
wenzelm@11049
|
330 |
apply (subst d22set_prod_zfact [symmetric])
|
wenzelm@11049
|
331 |
apply (subst d22set_eq_wset)
|
paulson@13833
|
332 |
apply (rule_tac [2] wset_zcong_prod_1, auto)
|
wenzelm@11049
|
333 |
done
|
paulson@9508
|
334 |
|
paulson@9508
|
335 |
end
|