18 consts |
18 consts |
19 inv :: "int => int => int" |
19 inv :: "int => int => int" |
20 wset :: "int * int => int set" |
20 wset :: "int * int => int set" |
21 |
21 |
22 defs |
22 defs |
23 inv_def: "inv p a == (a^(nat (p - #2))) mod p" |
23 inv_def: "inv p a == (a^(nat (p - # 2))) mod p" |
24 |
24 |
25 recdef wset |
25 recdef wset |
26 "measure ((\<lambda>(a, p). nat a) :: int * int => nat)" |
26 "measure ((\<lambda>(a, p). nat a) :: int * int => nat)" |
27 "wset (a, p) = |
27 "wset (a, p) = |
28 (if #1 < a then |
28 (if Numeral1 < a then |
29 let ws = wset (a - #1, p) |
29 let ws = wset (a - Numeral1, p) |
30 in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})" |
30 in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})" |
31 |
31 |
32 |
32 |
33 text {* \medskip @{term [source] inv} *} |
33 text {* \medskip @{term [source] inv} *} |
34 |
34 |
35 lemma aux: "#1 < m ==> Suc (nat (m - #2)) = nat (m - #1)" |
35 lemma aux: "Numeral1 < m ==> Suc (nat (m - # 2)) = nat (m - Numeral1)" |
36 apply (subst int_int_eq [symmetric]) |
36 apply (subst int_int_eq [symmetric]) |
37 apply auto |
37 apply auto |
38 done |
38 done |
39 |
39 |
40 lemma inv_is_inv: |
40 lemma inv_is_inv: |
41 "p \<in> zprime \<Longrightarrow> #0 < a \<Longrightarrow> a < p ==> [a * inv p a = #1] (mod p)" |
41 "p \<in> zprime \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> [a * inv p a = Numeral1] (mod p)" |
42 apply (unfold inv_def) |
42 apply (unfold inv_def) |
43 apply (subst zcong_zmod) |
43 apply (subst zcong_zmod) |
44 apply (subst zmod_zmult1_eq [symmetric]) |
44 apply (subst zmod_zmult1_eq [symmetric]) |
45 apply (subst zcong_zmod [symmetric]) |
45 apply (subst zcong_zmod [symmetric]) |
46 apply (subst power_Suc [symmetric]) |
46 apply (subst power_Suc [symmetric]) |
50 apply (unfold zprime_def) |
50 apply (unfold zprime_def) |
51 apply auto |
51 apply auto |
52 done |
52 done |
53 |
53 |
54 lemma inv_distinct: |
54 lemma inv_distinct: |
55 "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> a \<noteq> inv p a" |
55 "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> a \<noteq> inv p a" |
56 apply safe |
56 apply safe |
57 apply (cut_tac a = a and p = p in zcong_square) |
57 apply (cut_tac a = a and p = p in zcong_square) |
58 apply (cut_tac [3] a = a and p = p in inv_is_inv) |
58 apply (cut_tac [3] a = a and p = p in inv_is_inv) |
59 apply auto |
59 apply auto |
60 apply (subgoal_tac "a = #1") |
60 apply (subgoal_tac "a = Numeral1") |
61 apply (rule_tac [2] m = p in zcong_zless_imp_eq) |
61 apply (rule_tac [2] m = p in zcong_zless_imp_eq) |
62 apply (subgoal_tac [7] "a = p - #1") |
62 apply (subgoal_tac [7] "a = p - Numeral1") |
63 apply (rule_tac [8] m = p in zcong_zless_imp_eq) |
63 apply (rule_tac [8] m = p in zcong_zless_imp_eq) |
64 apply auto |
64 apply auto |
65 done |
65 done |
66 |
66 |
67 lemma inv_not_0: |
67 lemma inv_not_0: |
68 "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> #0" |
68 "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> inv p a \<noteq> Numeral0" |
69 apply safe |
69 apply safe |
70 apply (cut_tac a = a and p = p in inv_is_inv) |
70 apply (cut_tac a = a and p = p in inv_is_inv) |
71 apply (unfold zcong_def) |
71 apply (unfold zcong_def) |
72 apply auto |
72 apply auto |
73 apply (subgoal_tac "\<not> p dvd #1") |
73 apply (subgoal_tac "\<not> p dvd Numeral1") |
74 apply (rule_tac [2] zdvd_not_zless) |
74 apply (rule_tac [2] zdvd_not_zless) |
75 apply (subgoal_tac "p dvd #1") |
75 apply (subgoal_tac "p dvd Numeral1") |
76 prefer 2 |
76 prefer 2 |
77 apply (subst zdvd_zminus_iff [symmetric]) |
77 apply (subst zdvd_zminus_iff [symmetric]) |
78 apply auto |
78 apply auto |
79 done |
79 done |
80 |
80 |
81 lemma inv_not_1: |
81 lemma inv_not_1: |
82 "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> #1" |
82 "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> inv p a \<noteq> Numeral1" |
83 apply safe |
83 apply safe |
84 apply (cut_tac a = a and p = p in inv_is_inv) |
84 apply (cut_tac a = a and p = p in inv_is_inv) |
85 prefer 4 |
85 prefer 4 |
86 apply simp |
86 apply simp |
87 apply (subgoal_tac "a = #1") |
87 apply (subgoal_tac "a = Numeral1") |
88 apply (rule_tac [2] zcong_zless_imp_eq) |
88 apply (rule_tac [2] zcong_zless_imp_eq) |
89 apply auto |
89 apply auto |
90 done |
90 done |
91 |
91 |
92 lemma aux: "[a * (p - #1) = #1] (mod p) = [a = p - #1] (mod p)" |
92 lemma aux: "[a * (p - Numeral1) = Numeral1] (mod p) = [a = p - Numeral1] (mod p)" |
93 apply (unfold zcong_def) |
93 apply (unfold zcong_def) |
94 apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2) |
94 apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2) |
95 apply (rule_tac s = "p dvd -((a + #1) + (p * -a))" in trans) |
95 apply (rule_tac s = "p dvd -((a + Numeral1) + (p * -a))" in trans) |
96 apply (simp add: zmult_commute zminus_zdiff_eq) |
96 apply (simp add: zmult_commute zminus_zdiff_eq) |
97 apply (subst zdvd_zminus_iff) |
97 apply (subst zdvd_zminus_iff) |
98 apply (subst zdvd_reduce) |
98 apply (subst zdvd_reduce) |
99 apply (rule_tac s = "p dvd (a + #1) + (p * -#1)" in trans) |
99 apply (rule_tac s = "p dvd (a + Numeral1) + (p * -Numeral1)" in trans) |
100 apply (subst zdvd_reduce) |
100 apply (subst zdvd_reduce) |
101 apply auto |
101 apply auto |
102 done |
102 done |
103 |
103 |
104 lemma inv_not_p_minus_1: |
104 lemma inv_not_p_minus_1: |
105 "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a \<noteq> p - #1" |
105 "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> inv p a \<noteq> p - Numeral1" |
106 apply safe |
106 apply safe |
107 apply (cut_tac a = a and p = p in inv_is_inv) |
107 apply (cut_tac a = a and p = p in inv_is_inv) |
108 apply auto |
108 apply auto |
109 apply (simp add: aux) |
109 apply (simp add: aux) |
110 apply (subgoal_tac "a = p - #1") |
110 apply (subgoal_tac "a = p - Numeral1") |
111 apply (rule_tac [2] zcong_zless_imp_eq) |
111 apply (rule_tac [2] zcong_zless_imp_eq) |
112 apply auto |
112 apply auto |
113 done |
113 done |
114 |
114 |
115 lemma inv_g_1: |
115 lemma inv_g_1: |
116 "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> #1 < inv p a" |
116 "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> Numeral1 < inv p a" |
117 apply (case_tac "#0\<le> inv p a") |
117 apply (case_tac "Numeral0\<le> inv p a") |
118 apply (subgoal_tac "inv p a \<noteq> #1") |
118 apply (subgoal_tac "inv p a \<noteq> Numeral1") |
119 apply (subgoal_tac "inv p a \<noteq> #0") |
119 apply (subgoal_tac "inv p a \<noteq> Numeral0") |
120 apply (subst order_less_le) |
120 apply (subst order_less_le) |
121 apply (subst zle_add1_eq_le [symmetric]) |
121 apply (subst zle_add1_eq_le [symmetric]) |
122 apply (subst order_less_le) |
122 apply (subst order_less_le) |
123 apply (rule_tac [2] inv_not_0) |
123 apply (rule_tac [2] inv_not_0) |
124 apply (rule_tac [5] inv_not_1) |
124 apply (rule_tac [5] inv_not_1) |
126 apply (unfold inv_def zprime_def) |
126 apply (unfold inv_def zprime_def) |
127 apply (simp add: pos_mod_sign) |
127 apply (simp add: pos_mod_sign) |
128 done |
128 done |
129 |
129 |
130 lemma inv_less_p_minus_1: |
130 lemma inv_less_p_minus_1: |
131 "p \<in> zprime \<Longrightarrow> #1 < a \<Longrightarrow> a < p - #1 ==> inv p a < p - #1" |
131 "p \<in> zprime \<Longrightarrow> Numeral1 < a \<Longrightarrow> a < p - Numeral1 ==> inv p a < p - Numeral1" |
132 apply (case_tac "inv p a < p") |
132 apply (case_tac "inv p a < p") |
133 apply (subst order_less_le) |
133 apply (subst order_less_le) |
134 apply (simp add: inv_not_p_minus_1) |
134 apply (simp add: inv_not_p_minus_1) |
135 apply auto |
135 apply auto |
136 apply (unfold inv_def zprime_def) |
136 apply (unfold inv_def zprime_def) |
137 apply (simp add: pos_mod_bound) |
137 apply (simp add: pos_mod_bound) |
138 done |
138 done |
139 |
139 |
140 lemma aux: "#5 \<le> p ==> |
140 lemma aux: "# 5 \<le> p ==> |
141 nat (p - #2) * nat (p - #2) = Suc (nat (p - #1) * nat (p - #3))" |
141 nat (p - # 2) * nat (p - # 2) = Suc (nat (p - Numeral1) * nat (p - # 3))" |
142 apply (subst int_int_eq [symmetric]) |
142 apply (subst int_int_eq [symmetric]) |
143 apply (simp add: zmult_int [symmetric]) |
143 apply (simp add: zmult_int [symmetric]) |
144 apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2) |
144 apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2) |
145 done |
145 done |
146 |
146 |
147 lemma zcong_zpower_zmult: |
147 lemma zcong_zpower_zmult: |
148 "[x^y = #1] (mod p) \<Longrightarrow> [x^(y * z) = #1] (mod p)" |
148 "[x^y = Numeral1] (mod p) \<Longrightarrow> [x^(y * z) = Numeral1] (mod p)" |
149 apply (induct z) |
149 apply (induct z) |
150 apply (auto simp add: zpower_zadd_distrib) |
150 apply (auto simp add: zpower_zadd_distrib) |
151 apply (subgoal_tac "zcong (x^y * x^(y * n)) (#1 * #1) p") |
151 apply (subgoal_tac "zcong (x^y * x^(y * n)) (Numeral1 * Numeral1) p") |
152 apply (rule_tac [2] zcong_zmult) |
152 apply (rule_tac [2] zcong_zmult) |
153 apply simp_all |
153 apply simp_all |
154 done |
154 done |
155 |
155 |
156 lemma inv_inv: "p \<in> zprime \<Longrightarrow> |
156 lemma inv_inv: "p \<in> zprime \<Longrightarrow> |
157 #5 \<le> p \<Longrightarrow> #0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a" |
157 # 5 \<le> p \<Longrightarrow> Numeral0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a" |
158 apply (unfold inv_def) |
158 apply (unfold inv_def) |
159 apply (subst zpower_zmod) |
159 apply (subst zpower_zmod) |
160 apply (subst zpower_zpower) |
160 apply (subst zpower_zpower) |
161 apply (rule zcong_zless_imp_eq) |
161 apply (rule zcong_zless_imp_eq) |
162 prefer 5 |
162 prefer 5 |
163 apply (subst zcong_zmod) |
163 apply (subst zcong_zmod) |
164 apply (subst mod_mod_trivial) |
164 apply (subst mod_mod_trivial) |
165 apply (subst zcong_zmod [symmetric]) |
165 apply (subst zcong_zmod [symmetric]) |
166 apply (subst aux) |
166 apply (subst aux) |
167 apply (subgoal_tac [2] |
167 apply (subgoal_tac [2] |
168 "zcong (a * a^(nat (p - #1) * nat (p - #3))) (a * #1) p") |
168 "zcong (a * a^(nat (p - Numeral1) * nat (p - # 3))) (a * Numeral1) p") |
169 apply (rule_tac [3] zcong_zmult) |
169 apply (rule_tac [3] zcong_zmult) |
170 apply (rule_tac [4] zcong_zpower_zmult) |
170 apply (rule_tac [4] zcong_zpower_zmult) |
171 apply (erule_tac [4] Little_Fermat) |
171 apply (erule_tac [4] Little_Fermat) |
172 apply (rule_tac [4] zdvd_not_zless) |
172 apply (rule_tac [4] zdvd_not_zless) |
173 apply (simp_all add: pos_mod_bound pos_mod_sign) |
173 apply (simp_all add: pos_mod_bound pos_mod_sign) |
178 |
178 |
179 declare wset.simps [simp del] |
179 declare wset.simps [simp del] |
180 |
180 |
181 lemma wset_induct: |
181 lemma wset_induct: |
182 "(!!a p. P {} a p) \<Longrightarrow> |
182 "(!!a p. P {} a p) \<Longrightarrow> |
183 (!!a p. #1 < (a::int) \<Longrightarrow> P (wset (a - #1, p)) (a - #1) p |
183 (!!a p. Numeral1 < (a::int) \<Longrightarrow> P (wset (a - Numeral1, p)) (a - Numeral1) p |
184 ==> P (wset (a, p)) a p) |
184 ==> P (wset (a, p)) a p) |
185 ==> P (wset (u, v)) u v" |
185 ==> P (wset (u, v)) u v" |
186 proof - |
186 proof - |
187 case rule_context |
187 case rule_context |
188 show ?thesis |
188 show ?thesis |
189 apply (rule wset.induct) |
189 apply (rule wset.induct) |
190 apply safe |
190 apply safe |
191 apply (case_tac [2] "#1 < a") |
191 apply (case_tac [2] "Numeral1 < a") |
192 apply (rule_tac [2] rule_context) |
192 apply (rule_tac [2] rule_context) |
193 apply simp_all |
193 apply simp_all |
194 apply (simp_all add: wset.simps rule_context) |
194 apply (simp_all add: wset.simps rule_context) |
195 done |
195 done |
196 qed |
196 qed |
197 |
197 |
198 lemma wset_mem_imp_or [rule_format]: |
198 lemma wset_mem_imp_or [rule_format]: |
199 "#1 < a \<Longrightarrow> b \<notin> wset (a - #1, p) |
199 "Numeral1 < a \<Longrightarrow> b \<notin> wset (a - Numeral1, p) |
200 ==> b \<in> wset (a, p) --> b = a \<or> b = inv p a" |
200 ==> b \<in> wset (a, p) --> b = a \<or> b = inv p a" |
201 apply (subst wset.simps) |
201 apply (subst wset.simps) |
202 apply (unfold Let_def) |
202 apply (unfold Let_def) |
203 apply simp |
203 apply simp |
204 done |
204 done |
205 |
205 |
206 lemma wset_mem_mem [simp]: "#1 < a ==> a \<in> wset (a, p)" |
206 lemma wset_mem_mem [simp]: "Numeral1 < a ==> a \<in> wset (a, p)" |
207 apply (subst wset.simps) |
207 apply (subst wset.simps) |
208 apply (unfold Let_def) |
208 apply (unfold Let_def) |
209 apply simp |
209 apply simp |
210 done |
210 done |
211 |
211 |
212 lemma wset_subset: "#1 < a \<Longrightarrow> b \<in> wset (a - #1, p) ==> b \<in> wset (a, p)" |
212 lemma wset_subset: "Numeral1 < a \<Longrightarrow> b \<in> wset (a - Numeral1, p) ==> b \<in> wset (a, p)" |
213 apply (subst wset.simps) |
213 apply (subst wset.simps) |
214 apply (unfold Let_def) |
214 apply (unfold Let_def) |
215 apply auto |
215 apply auto |
216 done |
216 done |
217 |
217 |
218 lemma wset_g_1 [rule_format]: |
218 lemma wset_g_1 [rule_format]: |
219 "p \<in> zprime --> a < p - #1 --> b \<in> wset (a, p) --> #1 < b" |
219 "p \<in> zprime --> a < p - Numeral1 --> b \<in> wset (a, p) --> Numeral1 < b" |
220 apply (induct a p rule: wset_induct) |
220 apply (induct a p rule: wset_induct) |
221 apply auto |
221 apply auto |
222 apply (case_tac "b = a") |
222 apply (case_tac "b = a") |
223 apply (case_tac [2] "b = inv p a") |
223 apply (case_tac [2] "b = inv p a") |
224 apply (subgoal_tac [3] "b = a \<or> b = inv p a") |
224 apply (subgoal_tac [3] "b = a \<or> b = inv p a") |
243 apply auto |
243 apply auto |
244 done |
244 done |
245 |
245 |
246 lemma wset_mem [rule_format]: |
246 lemma wset_mem [rule_format]: |
247 "p \<in> zprime --> |
247 "p \<in> zprime --> |
248 a < p - #1 --> #1 < b --> b \<le> a --> b \<in> wset (a, p)" |
248 a < p - Numeral1 --> Numeral1 < b --> b \<le> a --> b \<in> wset (a, p)" |
249 apply (induct a p rule: wset.induct) |
249 apply (induct a p rule: wset.induct) |
250 apply auto |
250 apply auto |
251 apply (subgoal_tac "b = a") |
251 apply (subgoal_tac "b = a") |
252 apply (rule_tac [2] zle_anti_sym) |
252 apply (rule_tac [2] zle_anti_sym) |
253 apply (rule_tac [4] wset_subset) |
253 apply (rule_tac [4] wset_subset) |
254 apply (simp (no_asm_simp)) |
254 apply (simp (no_asm_simp)) |
255 apply auto |
255 apply auto |
256 done |
256 done |
257 |
257 |
258 lemma wset_mem_inv_mem [rule_format]: |
258 lemma wset_mem_inv_mem [rule_format]: |
259 "p \<in> zprime --> #5 \<le> p --> a < p - #1 --> b \<in> wset (a, p) |
259 "p \<in> zprime --> # 5 \<le> p --> a < p - Numeral1 --> b \<in> wset (a, p) |
260 --> inv p b \<in> wset (a, p)" |
260 --> inv p b \<in> wset (a, p)" |
261 apply (induct a p rule: wset_induct) |
261 apply (induct a p rule: wset_induct) |
262 apply auto |
262 apply auto |
263 apply (case_tac "b = a") |
263 apply (case_tac "b = a") |
264 apply (subst wset.simps) |
264 apply (subst wset.simps) |
290 apply auto |
290 apply auto |
291 done |
291 done |
292 |
292 |
293 lemma wset_zcong_prod_1 [rule_format]: |
293 lemma wset_zcong_prod_1 [rule_format]: |
294 "p \<in> zprime --> |
294 "p \<in> zprime --> |
295 #5 \<le> p --> a < p - #1 --> [setprod (wset (a, p)) = #1] (mod p)" |
295 # 5 \<le> p --> a < p - Numeral1 --> [setprod (wset (a, p)) = Numeral1] (mod p)" |
296 apply (induct a p rule: wset_induct) |
296 apply (induct a p rule: wset_induct) |
297 prefer 2 |
297 prefer 2 |
298 apply (subst wset.simps) |
298 apply (subst wset.simps) |
299 apply (unfold Let_def) |
299 apply (unfold Let_def) |
300 apply auto |
300 apply auto |
301 apply (subst setprod_insert) |
301 apply (subst setprod_insert) |
302 apply (tactic {* stac (thm "setprod_insert") 3 *}) |
302 apply (tactic {* stac (thm "setprod_insert") 3 *}) |
303 apply (subgoal_tac [5] |
303 apply (subgoal_tac [5] |
304 "zcong (a * inv p a * setprod (wset (a - #1, p))) (#1 * #1) p") |
304 "zcong (a * inv p a * setprod (wset (a - Numeral1, p))) (Numeral1 * Numeral1) p") |
305 prefer 5 |
305 prefer 5 |
306 apply (simp add: zmult_assoc) |
306 apply (simp add: zmult_assoc) |
307 apply (rule_tac [5] zcong_zmult) |
307 apply (rule_tac [5] zcong_zmult) |
308 apply (rule_tac [5] inv_is_inv) |
308 apply (rule_tac [5] inv_is_inv) |
309 apply (tactic "Clarify_tac 4") |
309 apply (tactic "Clarify_tac 4") |
310 apply (subgoal_tac [4] "a \<in> wset (a - #1, p)") |
310 apply (subgoal_tac [4] "a \<in> wset (a - Numeral1, p)") |
311 apply (rule_tac [5] wset_inv_mem_mem) |
311 apply (rule_tac [5] wset_inv_mem_mem) |
312 apply (simp_all add: wset_fin) |
312 apply (simp_all add: wset_fin) |
313 apply (rule inv_distinct) |
313 apply (rule inv_distinct) |
314 apply auto |
314 apply auto |
315 done |
315 done |
316 |
316 |
317 lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - #2) = wset (p - #2, p)" |
317 lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - # 2) = wset (p - # 2, p)" |
318 apply safe |
318 apply safe |
319 apply (erule wset_mem) |
319 apply (erule wset_mem) |
320 apply (rule_tac [2] d22set_g_1) |
320 apply (rule_tac [2] d22set_g_1) |
321 apply (rule_tac [3] d22set_le) |
321 apply (rule_tac [3] d22set_le) |
322 apply (rule_tac [4] d22set_mem) |
322 apply (rule_tac [4] d22set_mem) |
323 apply (erule_tac [4] wset_g_1) |
323 apply (erule_tac [4] wset_g_1) |
324 prefer 6 |
324 prefer 6 |
325 apply (subst zle_add1_eq_le [symmetric]) |
325 apply (subst zle_add1_eq_le [symmetric]) |
326 apply (subgoal_tac "p - #2 + #1 = p - #1") |
326 apply (subgoal_tac "p - # 2 + Numeral1 = p - Numeral1") |
327 apply (simp (no_asm_simp)) |
327 apply (simp (no_asm_simp)) |
328 apply (erule wset_less) |
328 apply (erule wset_less) |
329 apply auto |
329 apply auto |
330 done |
330 done |
331 |
331 |
332 |
332 |
333 subsection {* Wilson *} |
333 subsection {* Wilson *} |
334 |
334 |
335 lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> #2 \<Longrightarrow> p \<noteq> #3 ==> #5 \<le> p" |
335 lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> # 2 \<Longrightarrow> p \<noteq> # 3 ==> # 5 \<le> p" |
336 apply (unfold zprime_def dvd_def) |
336 apply (unfold zprime_def dvd_def) |
337 apply (case_tac "p = #4") |
337 apply (case_tac "p = # 4") |
338 apply auto |
338 apply auto |
339 apply (rule notE) |
339 apply (rule notE) |
340 prefer 2 |
340 prefer 2 |
341 apply assumption |
341 apply assumption |
342 apply (simp (no_asm)) |
342 apply (simp (no_asm)) |
343 apply (rule_tac x = "#2" in exI) |
343 apply (rule_tac x = "# 2" in exI) |
344 apply safe |
344 apply safe |
345 apply (rule_tac x = "#2" in exI) |
345 apply (rule_tac x = "# 2" in exI) |
346 apply auto |
346 apply auto |
347 apply arith |
347 apply arith |
348 done |
348 done |
349 |
349 |
350 theorem Wilson_Russ: |
350 theorem Wilson_Russ: |
351 "p \<in> zprime ==> [zfact (p - #1) = #-1] (mod p)" |
351 "p \<in> zprime ==> [zfact (p - Numeral1) = # -1] (mod p)" |
352 apply (subgoal_tac "[(p - #1) * zfact (p - #2) = #-1 * #1] (mod p)") |
352 apply (subgoal_tac "[(p - Numeral1) * zfact (p - # 2) = # -1 * Numeral1] (mod p)") |
353 apply (rule_tac [2] zcong_zmult) |
353 apply (rule_tac [2] zcong_zmult) |
354 apply (simp only: zprime_def) |
354 apply (simp only: zprime_def) |
355 apply (subst zfact.simps) |
355 apply (subst zfact.simps) |
356 apply (rule_tac t = "p - #1 - #1" and s = "p - #2" in subst) |
356 apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - # 2" in subst) |
357 apply auto |
357 apply auto |
358 apply (simp only: zcong_def) |
358 apply (simp only: zcong_def) |
359 apply (simp (no_asm_simp)) |
359 apply (simp (no_asm_simp)) |
360 apply (case_tac "p = #2") |
360 apply (case_tac "p = # 2") |
361 apply (simp add: zfact.simps) |
361 apply (simp add: zfact.simps) |
362 apply (case_tac "p = #3") |
362 apply (case_tac "p = # 3") |
363 apply (simp add: zfact.simps) |
363 apply (simp add: zfact.simps) |
364 apply (subgoal_tac "#5 \<le> p") |
364 apply (subgoal_tac "# 5 \<le> p") |
365 apply (erule_tac [2] prime_g_5) |
365 apply (erule_tac [2] prime_g_5) |
366 apply (subst d22set_prod_zfact [symmetric]) |
366 apply (subst d22set_prod_zfact [symmetric]) |
367 apply (subst d22set_eq_wset) |
367 apply (subst d22set_eq_wset) |
368 apply (rule_tac [2] wset_zcong_prod_1) |
368 apply (rule_tac [2] wset_zcong_prod_1) |
369 apply auto |
369 apply auto |