1 (* Title: WilsonBij.ML |
|
2 ID: $Id$ |
|
3 Author: Thomas M. Rasmussen |
|
4 Copyright 2000 University of Cambridge |
|
5 |
|
6 Wilson's Theorem using a more "abstract" approach based on |
|
7 bijections between sets. Does not use Fermat's Little Theorem |
|
8 (unlike Russinoff) |
|
9 *) |
|
10 |
|
11 |
|
12 (************ Inverse **************) |
|
13 |
|
14 Goalw [inv_def] |
|
15 "[| p:zprime; #0<a; a<p |] \ |
|
16 \ ==> #0 <= (inv p a) & (inv p a)<p & [a*(inv p a) = #1](mod p)"; |
|
17 by (Asm_simp_tac 1); |
|
18 by (rtac (zcong_lineq_unique RS ex1_implies_ex RS someI_ex) 1); |
|
19 by (etac zless_zprime_imp_zrelprime 2); |
|
20 by (rewtac zprime_def); |
|
21 by Auto_tac; |
|
22 qed "inv_correct"; |
|
23 |
|
24 bind_thm ("inv_ge",inv_correct RS conjunct1); |
|
25 bind_thm ("inv_less",(inv_correct RS conjunct2) RS conjunct1); |
|
26 bind_thm ("inv_is_inv",(inv_correct RS conjunct2) RS conjunct2); |
|
27 |
|
28 (* Same as WilsonRuss *) |
|
29 Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #0"; |
|
30 by Safe_tac; |
|
31 by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1); |
|
32 by (rewtac zcong_def); |
|
33 by Auto_tac; |
|
34 by (subgoal_tac "~p dvd #1" 1); |
|
35 by (rtac zdvd_not_zless 2); |
|
36 by (subgoal_tac "p dvd #1" 1); |
|
37 by (stac (zdvd_zminus_iff RS sym) 2); |
|
38 by Auto_tac; |
|
39 qed "inv_not_0"; |
|
40 |
|
41 (* Same as WilsonRuss *) |
|
42 Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= #1"; |
|
43 by Safe_tac; |
|
44 by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1); |
|
45 by (Asm_full_simp_tac 4); |
|
46 by (subgoal_tac "a = #1" 4); |
|
47 by (rtac zcong_zless_imp_eq 5); |
|
48 by Auto_tac; |
|
49 qed "inv_not_1"; |
|
50 |
|
51 (* Same as WilsonRuss *) |
|
52 Goalw [zcong_def] "[a*(p-#1) = #1](mod p) = [a = p-#1](mod p)"; |
|
53 by (simp_tac (simpset() addsimps [zdiff_zdiff_eq,zdiff_zdiff_eq2, |
|
54 zdiff_zmult_distrib2]) 1); |
|
55 by (res_inst_tac [("s","p dvd -((a+#1)+(p*(-a)))")] trans 1); |
|
56 by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1); |
|
57 by (stac zdvd_zminus_iff 1); |
|
58 by (stac zdvd_reduce 1); |
|
59 by (res_inst_tac [("s","p dvd (a+#1)+(p*(-#1))")] trans 1); |
|
60 by (stac zdvd_reduce 1); |
|
61 by Auto_tac; |
|
62 val lemma = result(); |
|
63 |
|
64 (* Same as WilsonRuss *) |
|
65 Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a) ~= p-#1"; |
|
66 by Safe_tac; |
|
67 by (cut_inst_tac [("a","a"),("p","p")] inv_is_inv 1); |
|
68 by Auto_tac; |
|
69 by (asm_full_simp_tac (simpset() addsimps [lemma]) 1); |
|
70 by (subgoal_tac "a = p-#1" 1); |
|
71 by (rtac zcong_zless_imp_eq 2); |
|
72 by Auto_tac; |
|
73 qed "inv_not_p_minus_1"; |
|
74 |
|
75 (* Below is slightly different as we don't expand |
|
76 inv but use 'correct'-theos *) |
|
77 Goal "[| p:zprime; #1<a; a<p-#1 |] ==> #1<(inv p a)"; |
|
78 by (subgoal_tac "(inv p a) ~= #1" 1); |
|
79 by (subgoal_tac "(inv p a) ~= #0" 1); |
|
80 by (stac order_less_le 1); |
|
81 by (stac (zle_add1_eq_le RS sym) 1); |
|
82 by (stac order_less_le 1); |
|
83 by (rtac inv_not_0 2); |
|
84 by (rtac inv_not_1 5); |
|
85 by Auto_tac; |
|
86 by (rtac inv_ge 1); |
|
87 by Auto_tac; |
|
88 qed "inv_g_1"; |
|
89 |
|
90 (* ditto *) |
|
91 Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a)<p-#1"; |
|
92 by (stac order_less_le 1); |
|
93 by (asm_full_simp_tac (simpset() addsimps [inv_not_p_minus_1, inv_less]) 1); |
|
94 qed "inv_less_p_minus_1"; |
|
95 |
|
96 (************* Bijection *******************) |
|
97 |
|
98 Goal "#1<x ==> #0<=(x::int)"; |
|
99 by Auto_tac; |
|
100 val l1 = result(); |
|
101 |
|
102 Goal "#1<x ==> #0<(x::int)"; |
|
103 by Auto_tac; |
|
104 val l2 = result(); |
|
105 |
|
106 Goal "x<=p-#2 ==> x<(p::int)"; |
|
107 by Auto_tac; |
|
108 val l3 = result(); |
|
109 |
|
110 Goal "x<=p-#2 ==> x<(p::int)-#1"; |
|
111 by Auto_tac; |
|
112 val l4 = result(); |
|
113 |
|
114 Goalw [inj_on_def] "p : zprime ==> inj_on (inv p) (d22set (p-#2))"; |
|
115 by Auto_tac; |
|
116 by (rtac zcong_zless_imp_eq 1); |
|
117 by (stac (zcong_cancel RS sym) 5); |
|
118 by (rtac zcong_trans 7); |
|
119 by (stac zcong_sym 8); |
|
120 by (etac inv_is_inv 7); |
|
121 by (Asm_simp_tac 9); |
|
122 by (etac inv_is_inv 9); |
|
123 by (rtac zless_zprime_imp_zrelprime 6); |
|
124 by (rtac inv_less 8); |
|
125 by (rtac (inv_g_1 RS l2) 7); |
|
126 by (rewtac zprime_def); |
|
127 by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l1,l2,l3,l4],simpset())); |
|
128 qed "inv_inj"; |
|
129 |
|
130 Goal "p : zprime ==> (inv p)`(d22set (p-#2)) = (d22set (p-#2))"; |
|
131 by (rtac endo_inj_surj 1); |
|
132 by (rtac d22set_fin 1); |
|
133 by (etac inv_inj 2); |
|
134 by Auto_tac; |
|
135 by (rtac d22set_mem 1); |
|
136 by (etac inv_g_1 1); |
|
137 by (subgoal_tac "inv p xa < p - #1" 3); |
|
138 by (etac inv_less_p_minus_1 4); |
|
139 by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l4],simpset())); |
|
140 qed "inv_d22set_d22set"; |
|
141 |
|
142 Goalw [reciR_def] "p:zprime \ |
|
143 \ ==> (d22set(p-#2),d22set(p-#2)) : (bijR (reciR p))"; |
|
144 by (res_inst_tac [("s","(d22set(p-#2),(inv p)`(d22set(p-#2)))")] subst 1); |
|
145 by (asm_simp_tac (simpset() addsimps [inv_d22set_d22set]) 1); |
|
146 by (rtac inj_func_bijR 1); |
|
147 by (rtac d22set_fin 3); |
|
148 by (etac inv_inj 2); |
|
149 by Auto_tac; |
|
150 by (etac inv_is_inv 1); |
|
151 by (etac inv_g_1 5); |
|
152 by (etac inv_less_p_minus_1 7); |
|
153 by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l2,l3,l4],simpset())); |
|
154 qed "d22set_d22set_bij"; |
|
155 |
|
156 Goalw [reciR_def,bijP_def] |
|
157 "p:zprime ==> bijP (reciR p) (d22set(p-#2))"; |
|
158 by Auto_tac; |
|
159 by (rtac d22set_mem 1); |
|
160 by Auto_tac; |
|
161 qed "reciP_bijP"; |
|
162 |
|
163 Goalw [reciR_def,uniqP_def] |
|
164 "p:zprime ==> uniqP (reciR p)"; |
|
165 by Auto_tac; |
|
166 by (rtac zcong_zless_imp_eq 1); |
|
167 by (stac (zcong_cancel2 RS sym) 5); |
|
168 by (rtac zcong_trans 7); |
|
169 by (stac zcong_sym 8); |
|
170 by (rtac zless_zprime_imp_zrelprime 6); |
|
171 by Auto_tac; |
|
172 by (rtac zcong_zless_imp_eq 1); |
|
173 by (stac (zcong_cancel RS sym) 5); |
|
174 by (rtac zcong_trans 7); |
|
175 by (stac zcong_sym 8); |
|
176 by (rtac zless_zprime_imp_zrelprime 6); |
|
177 by Auto_tac; |
|
178 qed "reciP_uniq"; |
|
179 |
|
180 Goalw [reciR_def,symP_def] |
|
181 "p:zprime ==> symP (reciR p)"; |
|
182 by (simp_tac (simpset() addsimps [zmult_commute]) 1); |
|
183 by Auto_tac; |
|
184 qed "reciP_sym"; |
|
185 |
|
186 Goal "p:zprime ==> d22set(p-#2) : (bijER (reciR p))"; |
|
187 by (rtac bijR_bijER 1); |
|
188 by (etac d22set_d22set_bij 1); |
|
189 by (etac reciP_bijP 1); |
|
190 by (etac reciP_uniq 1); |
|
191 by (etac reciP_sym 1); |
|
192 qed "bijER_d22set"; |
|
193 |
|
194 (*********** Wilson **************) |
|
195 |
|
196 Goalw [reciR_def] |
|
197 "[| p:zprime; A : bijER (reciR p) |] ==> [setprod A = #1](mod p)"; |
|
198 by (etac bijER.induct 1); |
|
199 by (subgoal_tac "a=#1 | a=p-#1" 2); |
|
200 by (rtac zcong_square_zless 3); |
|
201 by Auto_tac; |
|
202 by (stac setprod_insert 1); |
|
203 by (stac setprod_insert 3); |
|
204 by (auto_tac (claset(),simpset() addsimps [fin_bijER])); |
|
205 by (subgoal_tac "zcong ((a * b) * setprod A) (#1*#1) p" 1); |
|
206 by (asm_full_simp_tac (simpset() addsimps [zmult_assoc]) 1); |
|
207 by (rtac zcong_zmult 1); |
|
208 by Auto_tac; |
|
209 qed "bijER_zcong_prod_1"; |
|
210 |
|
211 Goal "p:zprime ==> [zfact(p-#1) = #-1](mod p)"; |
|
212 by (subgoal_tac "zcong ((p-#1)*zfact(p-#2)) (#-1*#1) p" 1); |
|
213 by (rtac zcong_zmult 2); |
|
214 by (full_simp_tac (simpset() addsimps [zprime_def]) 1); |
|
215 by (stac zfact_eq 1); |
|
216 by (res_inst_tac [("t","p-#1-#1"),("s","p-#2")] subst 1); |
|
217 by Auto_tac; |
|
218 by (asm_simp_tac (simpset() addsimps [zcong_def]) 1); |
|
219 by (stac (d22set_prod_zfact RS sym) 1); |
|
220 by (rtac bijER_zcong_prod_1 1); |
|
221 by (rtac bijER_d22set 2); |
|
222 by Auto_tac; |
|
223 qed "WilsonBij"; |
|