|
1 (* Title: WilsonRuss.ML |
|
2 ID: $Id$ |
|
3 Author: Thomas M. Rasmussen |
|
4 Copyright 2000 University of Cambridge |
|
5 *) |
|
6 |
|
7 |
|
8 (************ Inverse **************) |
|
9 |
|
10 Goal "#1<m ==> Suc(nat(m-#2)) = nat(m-#1)"; |
|
11 by (stac (int_int_eq RS sym) 1); |
|
12 by Auto_tac; |
|
13 val lemma = result(); |
|
14 |
|
15 Goalw [inv_def] |
|
16 "[| p:zprime; #0<a; a<p |] ==> [a*(inv p a) = #1] (mod p)"; |
|
17 by (stac zcong_zmod 1); |
|
18 by (stac (zmod_zmult1_eq RS sym) 1); |
|
19 by (stac (zcong_zmod RS sym) 1); |
|
20 by (stac (power_Suc RS sym) 1); |
|
21 by (stac lemma 1); |
|
22 by (etac Little_Fermat 2); |
|
23 by (etac zdvd_not_zless 2); |
|
24 by (rewtac zprime_def); |
|
25 by Auto_tac; |
|
26 qed "inv_is_inv"; |
|
27 |
|
28 Goal "[| p:zprime; #1<a; a<p-#1 |] ==> a ~= (inv p a)"; |
|
29 by Safe_tac; |
|
30 by (cut_inst_tac [("a","a"),("p","p")] zcong_square 1); |
|
31 by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 3); |
|
32 by Auto_tac; |
|
33 by (subgoal_tac "a=#1" 1); |
|
34 by (res_inst_tac [("m","p")] zcong_zless_imp_eq 2); |
|
35 by (subgoal_tac "a=p-#1" 7); |
|
36 by (res_inst_tac [("m","p")] zcong_zless_imp_eq 8); |
|
37 by Auto_tac; |
|
38 qed "inv_distinct"; |
|
39 |
|
40 Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #0"; |
|
41 by Safe_tac; |
|
42 by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1); |
|
43 by (rewtac zcong_def); |
|
44 by Auto_tac; |
|
45 by (subgoal_tac "~p dvd #1" 1); |
|
46 by (rtac zdvd_not_zless 2); |
|
47 by (subgoal_tac "p dvd #1" 1); |
|
48 by (stac (zdvd_zminus_iff RS sym) 2); |
|
49 by Auto_tac; |
|
50 qed "inv_not_0"; |
|
51 |
|
52 Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #1"; |
|
53 by Safe_tac; |
|
54 by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1); |
|
55 by (Asm_full_simp_tac 4); |
|
56 by (subgoal_tac "a = #1" 4); |
|
57 by (rtac zcong_zless_imp_eq 5); |
|
58 by Auto_tac; |
|
59 qed "inv_not_1"; |
|
60 |
|
61 Goalw [zcong_def] "[a*(p-#1) = #1](mod p) = [a = p-#1](mod p)"; |
|
62 by (simp_tac (simpset() addsimps [zdiff_zdiff_eq,zdiff_zdiff_eq2, |
|
63 zdiff_zmult_distrib2]) 1); |
|
64 by (res_inst_tac [("s","p dvd -((a+#1)+(p*(-a)))")] trans 1); |
|
65 by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1); |
|
66 by (stac zdvd_zminus_iff 1); |
|
67 by (stac zdvd_reduce 1); |
|
68 by (res_inst_tac [("s","p dvd ((a+#1)+(p*(-#1)))")] trans 1); |
|
69 by (stac zdvd_reduce 1); |
|
70 by Auto_tac; |
|
71 val lemma = result(); |
|
72 |
|
73 Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= p-#1"; |
|
74 by Safe_tac; |
|
75 by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1); |
|
76 by Auto_tac; |
|
77 by (asm_full_simp_tac (simpset() addsimps [lemma]) 1); |
|
78 by (subgoal_tac "a = p-#1" 1); |
|
79 by (rtac zcong_zless_imp_eq 2); |
|
80 by Auto_tac; |
|
81 qed "inv_not_p_minus_1"; |
|
82 |
|
83 Goal "[| p:zprime; #1<a; a<p-#1 |] ==> #1<(inv p a)"; |
|
84 by (case_tac "#0<=(inv p a)" 1); |
|
85 by (subgoal_tac "(inv p a) ~= #1" 1); |
|
86 by (subgoal_tac "(inv p a) ~= #0" 1); |
|
87 by (rtac zle_neq_implies_zless 1); |
|
88 by (stac (zle_add1_eq_le RS sym) 1); |
|
89 by (rtac zle_neq_implies_zless 1); |
|
90 by (rtac inv_not_0 4); |
|
91 by (rtac inv_not_1 7); |
|
92 by Auto_tac; |
|
93 by (rewrite_goals_tac [inv_def,zprime_def]); |
|
94 by (asm_full_simp_tac (simpset() addsimps [pos_mod_sign]) 1); |
|
95 qed "inv_g_1"; |
|
96 |
|
97 Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a)<p-#1"; |
|
98 by (case_tac "(inv p a)<p" 1); |
|
99 by (rtac zle_neq_implies_zless 1); |
|
100 by (rtac inv_not_p_minus_1 2); |
|
101 by Auto_tac; |
|
102 by (rewrite_goals_tac [inv_def,zprime_def]); |
|
103 by (asm_full_simp_tac (simpset() addsimps [pos_mod_bound]) 1); |
|
104 qed "inv_less_p_minus_1"; |
|
105 |
|
106 Goal "#5<=p ==> nat(p-#2)*nat(p-#2) = Suc(nat(p-#1)*nat(p-#3))"; |
|
107 by (stac (int_int_eq RS sym) 1); |
|
108 by (asm_simp_tac (simpset() addsimps [zmult_int RS sym]) 1); |
|
109 by (simp_tac (simpset() addsimps [zdiff_zmult_distrib, |
|
110 zdiff_zmult_distrib2]) 1); |
|
111 val lemma = result(); |
|
112 |
|
113 Goal "[x^y = #1](mod p) --> [x^(y*z) = #1](mod p)"; |
|
114 by (induct_tac "z" 1); |
|
115 by (auto_tac (claset(),simpset() addsimps [zpower_zadd_distrib])); |
|
116 by (subgoal_tac "zcong (x^y * x^(y*n)) (#1*#1) p" 1); |
|
117 by (rtac zcong_zmult 2); |
|
118 by (ALLGOALS Asm_full_simp_tac); |
|
119 qed_spec_mp "zcong_zpower_zmult"; |
|
120 |
|
121 Goalw [inv_def] "[| p:zprime; #5<=p; #0<a; a<p |] ==> (inv p (inv p a)) = a"; |
|
122 by (stac zpower_zmod 1); |
|
123 by (stac zpower_zpower 1); |
|
124 by (rtac zcong_zless_imp_eq 1); |
|
125 by (stac zcong_zmod 5); |
|
126 by (stac mod_mod_trivial 5); |
|
127 by (stac (zcong_zmod RS sym) 5); |
|
128 by (stac lemma 5); |
|
129 by (subgoal_tac "zcong (a * a^(nat (p - #1) * nat (p - #3))) (a*#1) p" 6); |
|
130 by (rtac zcong_zmult 7); |
|
131 by (rtac zcong_zpower_zmult 8); |
|
132 by (etac Little_Fermat 8); |
|
133 by (rtac zdvd_not_zless 8); |
|
134 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [pos_mod_bound, |
|
135 pos_mod_sign]))); |
|
136 qed "inv_inv"; |
|
137 |
|
138 |
|
139 (************* wset *************) |
|
140 |
|
141 val [wset_eq] = wset.simps; |
|
142 Delsimps wset.simps; |
|
143 |
|
144 val [prem1,prem2] = |
|
145 Goal "[| !!a p. P {} a p; \ |
|
146 \ !!a p. [| #1<(a::int); P (wset (a-#1,p)) (a-#1) p |] \ |
|
147 \ ==> P (wset (a,p)) a p|] \ |
|
148 \ ==> P (wset (u,v)) u v"; |
|
149 by (rtac wset.induct 1); |
|
150 by Safe_tac; |
|
151 by (case_tac "#1<a" 2); |
|
152 by (rtac prem2 2); |
|
153 by (ALLGOALS Asm_simp_tac); |
|
154 by (ALLGOALS (asm_simp_tac (simpset() addsimps [wset_eq,prem1]))); |
|
155 qed "wset_induct"; |
|
156 |
|
157 Goal "[| #1<a; b~:(wset (a-#1,p)) |] \ |
|
158 \ ==> b:(wset (a,p)) --> b=a | b = inv p a"; |
|
159 by (stac wset_eq 1); |
|
160 by (rewtac Let_def); |
|
161 by (Asm_simp_tac 1); |
|
162 qed_spec_mp "wset_mem_imp_or"; |
|
163 |
|
164 Goal "#1<a ==> a:(wset(a,p))"; |
|
165 by (stac wset_eq 1); |
|
166 by (rewtac Let_def); |
|
167 by (Asm_simp_tac 1); |
|
168 qed "wset_mem_mem"; |
|
169 Addsimps [wset_mem_mem]; |
|
170 |
|
171 Goal "[| #1<a; b:wset(a-#1,p) |] ==> b:wset(a,p)"; |
|
172 by (stac wset_eq 1); |
|
173 by (rewtac Let_def); |
|
174 by Auto_tac; |
|
175 qed "wset_subset"; |
|
176 |
|
177 Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> #1<b"; |
|
178 by (res_inst_tac [("u","a"),("v","p")] wset_induct 1); |
|
179 by Auto_tac; |
|
180 by (case_tac "b=a" 1); |
|
181 by (case_tac "b=inv p a" 2); |
|
182 by (subgoal_tac "b=a | b = inv p a" 3); |
|
183 by (rtac wset_mem_imp_or 4); |
|
184 by (Asm_simp_tac 2); |
|
185 by (rtac inv_g_1 2); |
|
186 by Auto_tac; |
|
187 qed_spec_mp "wset_g_1"; |
|
188 |
|
189 Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> b<p-#1"; |
|
190 by (res_inst_tac [("u","a"),("v","p")] wset_induct 1); |
|
191 by Auto_tac; |
|
192 by (case_tac "b=a" 1); |
|
193 by (case_tac "b=inv p a" 2); |
|
194 by (subgoal_tac "b=a | b = inv p a" 3); |
|
195 by (rtac wset_mem_imp_or 4); |
|
196 by (Asm_simp_tac 2); |
|
197 by (rtac inv_less_p_minus_1 2); |
|
198 by Auto_tac; |
|
199 qed_spec_mp "wset_less"; |
|
200 |
|
201 Goal "p:zprime --> a<p-#1 --> #1<b --> b<=a --> b:(wset(a,p))"; |
|
202 by (res_inst_tac [("u","a"),("v","p")] wset.induct 1); |
|
203 by Auto_tac; |
|
204 by (subgoal_tac "b=a" 1); |
|
205 by (rtac zle_anti_sym 2); |
|
206 by (rtac wset_subset 4); |
|
207 by (Asm_simp_tac 1); |
|
208 by Auto_tac; |
|
209 qed_spec_mp "wset_mem"; |
|
210 |
|
211 Goal "p:zprime --> #5<=p --> a<p-#1 --> b:(wset (a,p)) \ |
|
212 \ --> (inv p b):(wset (a,p))"; |
|
213 by (res_inst_tac [("u","a"),("v","p")] wset_induct 1); |
|
214 by Auto_tac; |
|
215 by (case_tac "b=a" 1); |
|
216 by (stac wset_eq 1); |
|
217 by (rewtac Let_def); |
|
218 by (rtac wset_subset 3); |
|
219 by Auto_tac; |
|
220 by (case_tac "b = inv p a" 1); |
|
221 by (Asm_simp_tac 1); |
|
222 by (stac inv_inv 1); |
|
223 by (subgoal_tac "b=a | b = inv p a" 6); |
|
224 by (rtac wset_mem_imp_or 7); |
|
225 by Auto_tac; |
|
226 qed_spec_mp "wset_mem_inv_mem"; |
|
227 |
|
228 Goal "[| p:zprime; #5<=p; a<p-#1; #1<b; b<p-#1; (inv p b):(wset (a,p)) |] \ |
|
229 \ ==> b:(wset (a,p))"; |
|
230 by (res_inst_tac [("s","inv p (inv p b)"),("t","b")] subst 1); |
|
231 by (rtac wset_mem_inv_mem 2); |
|
232 by (rtac inv_inv 1); |
|
233 by (ALLGOALS (Asm_simp_tac)); |
|
234 qed "wset_inv_mem_mem"; |
|
235 |
|
236 Goal "finite (wset (a,p))"; |
|
237 by (res_inst_tac [("u","a"),("v","p")] wset_induct 1); |
|
238 by (stac wset_eq 2); |
|
239 by (rewtac Let_def); |
|
240 by Auto_tac; |
|
241 qed "wset_fin"; |
|
242 |
|
243 Goal "p:zprime --> #5<=p --> a<p-#1 --> [setprod (wset (a,p)) = #1](mod p)"; |
|
244 by (res_inst_tac [("u","a"),("v","p")] wset_induct 1); |
|
245 by (stac wset_eq 2); |
|
246 by (rewtac Let_def); |
|
247 by Auto_tac; |
|
248 by (stac setprod_insert 1); |
|
249 by (stac setprod_insert 3); |
|
250 by (subgoal_tac "zcong (a * (inv p a) * setprod(wset(a-#1,p))) (#1*#1) p" 5); |
|
251 by (asm_full_simp_tac (simpset() addsimps [zmult_assoc]) 5); |
|
252 by (rtac zcong_zmult 5); |
|
253 by (rtac inv_is_inv 5); |
|
254 by (Clarify_tac 4); |
|
255 by (subgoal_tac "a:wset(a-#1,p)" 4); |
|
256 by (rtac wset_inv_mem_mem 5); |
|
257 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [wset_fin]))); |
|
258 by (rtac inv_distinct 1); |
|
259 by Auto_tac; |
|
260 qed_spec_mp "wset_zcong_prod_1"; |
|
261 |
|
262 Goal "p:zprime ==> d22set(p-#2) = wset(p-#2,p)"; |
|
263 by Safe_tac; |
|
264 by (etac wset_mem 1); |
|
265 by (rtac d22set_g_1 2); |
|
266 by (rtac d22set_le 3); |
|
267 by (rtac d22set_mem 4); |
|
268 by (etac wset_g_1 4); |
|
269 by (stac (zle_add1_eq_le RS sym) 6); |
|
270 by (subgoal_tac "p-#2+#1 = p-#1" 6); |
|
271 by (Asm_simp_tac 6); |
|
272 by (etac wset_less 6); |
|
273 by Auto_tac; |
|
274 qed "d22set_eq_wset"; |
|
275 |
|
276 (********** Wilson *************) |
|
277 |
|
278 Goal "[| z-#1<=w; z-#1~=w |] ==> z<=(w::int)"; |
|
279 by (stac (zle_add1_eq_le RS sym) 1); |
|
280 by (rtac zle_neq_implies_zless 1); |
|
281 by Auto_tac; |
|
282 val lemma = result(); |
|
283 |
|
284 Goalw [zprime_def,dvd_def] "[| p : zprime; p ~= #2; p ~= #3 |] ==> #5<=p"; |
|
285 by (case_tac "p=#4" 1); |
|
286 by Auto_tac; |
|
287 by (rtac notE 1); |
|
288 by (assume_tac 2); |
|
289 by (Simp_tac 1); |
|
290 by (res_inst_tac [("x","#2")] exI 1); |
|
291 by Safe_tac; |
|
292 by (res_inst_tac [("x","#2")] exI 1); |
|
293 by Auto_tac; |
|
294 by (rtac lemma 1); |
|
295 by (rtac lemma 1); |
|
296 by (rtac lemma 1); |
|
297 by Auto_tac; |
|
298 qed "prime_g_5"; |
|
299 |
|
300 Goal "p:zprime ==> [zfact(p-#1) = #-1] (mod p)"; |
|
301 by (subgoal_tac "[(p-#1)*zfact(p-#2) = #-1*#1] (mod p)" 1); |
|
302 by (rtac zcong_zmult 2); |
|
303 by (SELECT_GOAL (rewtac zprime_def) 1); |
|
304 by (stac zfact_eq 1); |
|
305 by (res_inst_tac [("t","p-#1-#1"),("s","p-#2")] subst 1); |
|
306 by Auto_tac; |
|
307 by (SELECT_GOAL (rewtac zcong_def) 1); |
|
308 by (Asm_simp_tac 1); |
|
309 by (case_tac "p=#2" 1); |
|
310 by (asm_full_simp_tac (simpset() addsimps [zfact_eq]) 1); |
|
311 by (case_tac "p=#3" 1); |
|
312 by (asm_full_simp_tac (simpset() addsimps [zfact_eq]) 1); |
|
313 by (subgoal_tac "#5<=p" 1); |
|
314 by (etac prime_g_5 2); |
|
315 by (stac (d22set_prod_zfact RS sym) 1); |
|
316 by (stac d22set_eq_wset 1); |
|
317 by (rtac wset_zcong_prod_1 2); |
|
318 by Auto_tac; |
|
319 qed "WilsonRuss"; |