5 |
5 |
6 header {*Integers: Divisibility and Congruences*} |
6 header {*Integers: Divisibility and Congruences*} |
7 |
7 |
8 theory Int2 imports Finite2 WilsonRuss begin |
8 theory Int2 imports Finite2 WilsonRuss begin |
9 |
9 |
10 text{*Note. This theory is being revised. See the web page |
10 definition |
11 \url{http://www.andrew.cmu.edu/~avigad/isabelle}.*} |
11 MultInv :: "int => int => int" |
12 |
12 "MultInv p x = x ^ nat (p - 2)" |
13 constdefs |
13 |
14 MultInv :: "int => int => int" |
14 |
15 "MultInv p x == x ^ nat (p - 2)" |
15 subsection {* Useful lemmas about dvd and powers *} |
16 |
|
17 (*****************************************************************) |
|
18 (* *) |
|
19 (* Useful lemmas about dvd and powers *) |
|
20 (* *) |
|
21 (*****************************************************************) |
|
22 |
16 |
23 lemma zpower_zdvd_prop1: |
17 lemma zpower_zdvd_prop1: |
24 "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)" |
18 "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)" |
25 by (induct n) (auto simp add: zdvd_zmult zdvd_zmult2 [of p y]) |
19 by (induct n) (auto simp add: zdvd_zmult zdvd_zmult2 [of p y]) |
26 |
20 |
99 by (auto simp add: zcong_refl zcong_zadd) |
90 by (auto simp add: zcong_refl zcong_zadd) |
100 |
91 |
101 lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)" |
92 lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)" |
102 by (induct z) (auto simp add: zcong_zmult) |
93 by (induct z) (auto simp add: zcong_zmult) |
103 |
94 |
104 lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> |
95 lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> |
105 [a = d](mod m)" |
96 [a = d](mod m)" |
106 apply (erule zcong_trans) |
97 apply (erule zcong_trans) |
107 apply simp |
98 apply simp |
108 done |
99 done |
109 |
100 |
110 lemma aux1: "a - b = (c::int) ==> a = c + b" |
101 lemma aux1: "a - b = (c::int) ==> a = c + b" |
111 by auto |
102 by auto |
112 |
103 |
113 lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = |
104 lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = |
114 [c = b * d] (mod m))" |
105 [c = b * d] (mod m))" |
115 apply (auto simp add: zcong_def dvd_def) |
106 apply (auto simp add: zcong_def dvd_def) |
116 apply (rule_tac x = "ka + k * d" in exI) |
107 apply (rule_tac x = "ka + k * d" in exI) |
117 apply (drule aux1)+ |
108 apply (drule aux1)+ |
118 apply (auto simp add: int_distrib) |
109 apply (auto simp add: int_distrib) |
119 apply (rule_tac x = "ka - k * d" in exI) |
110 apply (rule_tac x = "ka - k * d" in exI) |
120 apply (drule aux1)+ |
111 apply (drule aux1)+ |
121 apply (auto simp add: int_distrib) |
112 apply (auto simp add: int_distrib) |
122 done |
113 done |
123 |
114 |
124 lemma zcong_zmult_prop2: "[a = b](mod m) ==> |
115 lemma zcong_zmult_prop2: "[a = b](mod m) ==> |
125 ([c = d * a](mod m) = [c = d * b] (mod m))" |
116 ([c = d * a](mod m) = [c = d * b] (mod m))" |
126 by (auto simp add: zmult_ac zcong_zmult_prop1) |
117 by (auto simp add: zmult_ac zcong_zmult_prop1) |
127 |
118 |
128 lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p); |
119 lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p); |
129 ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)" |
120 ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)" |
130 apply (auto simp add: zcong_def) |
121 apply (auto simp add: zcong_def) |
131 apply (drule zprime_zdvd_zmult_better, auto) |
122 apply (drule zprime_zdvd_zmult_better, auto) |
132 done |
123 done |
133 |
124 |
134 lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); |
125 lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); |
135 x < m; y < m |] ==> x = y" |
126 x < m; y < m |] ==> x = y" |
136 apply (simp add: zcong_zmod_eq) |
127 apply (simp add: zcong_zmod_eq) |
137 apply (subgoal_tac "(x mod m) = x") |
128 apply (subgoal_tac "(x mod m) = x") |
138 apply (subgoal_tac "(y mod m) = y") |
129 apply (subgoal_tac "(y mod m) = y") |
139 apply simp |
130 apply simp |
140 apply (rule_tac [1-2] mod_pos_pos_trivial) |
131 apply (rule_tac [1-2] mod_pos_pos_trivial) |
141 apply auto |
132 apply auto |
142 done |
133 done |
143 |
134 |
144 lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> |
135 lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> |
145 ~([x = 1] (mod p))" |
136 ~([x = 1] (mod p))" |
146 proof |
137 proof |
147 assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)" |
138 assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)" |
148 then have "[1 = -1] (mod p)" |
139 then have "[1 = -1] (mod p)" |
149 apply (auto simp add: zcong_sym) |
140 apply (auto simp add: zcong_sym) |
160 qed |
151 qed |
161 |
152 |
162 lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)" |
153 lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)" |
163 by (auto simp add: zcong_def) |
154 by (auto simp add: zcong_def) |
164 |
155 |
165 lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==> |
156 lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==> |
166 [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)" |
157 [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)" |
167 by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult) |
158 by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult) |
168 |
159 |
169 lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==> |
160 lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==> |
170 ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)" |
161 ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)" |
171 apply auto |
162 apply auto |
172 apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero) |
163 apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero) |
173 apply auto |
164 apply auto |
174 done |
165 done |
175 |
166 |
176 lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)" |
167 lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)" |
177 by (auto simp add: zcong_zero_equiv_div zdvd_not_zless) |
168 by (auto simp add: zcong_zero_equiv_div zdvd_not_zless) |
178 |
169 |
179 lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0" |
170 lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0" |
180 apply (drule order_le_imp_less_or_eq, auto) |
171 apply (drule order_le_imp_less_or_eq, auto) |
181 apply (frule_tac m = m in zcong_not_zero) |
172 apply (frule_tac m = m in zcong_not_zero) |
184 |
175 |
185 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |] |
176 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |] |
186 ==> zgcd (setprod id A,y) = 1" |
177 ==> zgcd (setprod id A,y) = 1" |
187 by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult) |
178 by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult) |
188 |
179 |
189 (*****************************************************************) |
180 |
190 (* *) |
181 subsection {* Some properties of MultInv *} |
191 (* Some properties of MultInv *) |
182 |
192 (* *) |
183 lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> |
193 (*****************************************************************) |
|
194 |
|
195 lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> |
|
196 [(MultInv p x) = (MultInv p y)] (mod p)" |
184 [(MultInv p x) = (MultInv p y)] (mod p)" |
197 by (auto simp add: MultInv_def zcong_zpower) |
185 by (auto simp add: MultInv_def zcong_zpower) |
198 |
186 |
199 lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
187 lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
200 [(x * (MultInv p x)) = 1] (mod p)" |
188 [(x * (MultInv p x)) = 1] (mod p)" |
201 proof (simp add: MultInv_def zcong_eq_zdvd_prop) |
189 proof (simp add: MultInv_def zcong_eq_zdvd_prop) |
202 assume "2 < p" and "zprime p" and "~ p dvd x" |
190 assume "2 < p" and "zprime p" and "~ p dvd x" |
203 have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)" |
191 have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)" |
204 by auto |
192 by auto |
206 by (simp only: nat_add_distrib, auto) |
194 by (simp only: nat_add_distrib, auto) |
207 also have "p - 2 + 1 = p - 1" by arith |
195 also have "p - 2 + 1 = p - 1" by arith |
208 finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)" |
196 finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)" |
209 by (rule ssubst, auto) |
197 by (rule ssubst, auto) |
210 also from prems have "[x ^ nat (p - 1) = 1] (mod p)" |
198 also from prems have "[x ^ nat (p - 1) = 1] (mod p)" |
211 by (auto simp add: Little_Fermat) |
199 by (auto simp add: Little_Fermat) |
212 finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" . |
200 finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" . |
213 qed |
201 qed |
214 |
202 |
215 lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
203 lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
216 [(MultInv p x) * x = 1] (mod p)" |
204 [(MultInv p x) * x = 1] (mod p)" |
217 by (auto simp add: MultInv_prop2 zmult_ac) |
205 by (auto simp add: MultInv_prop2 zmult_ac) |
218 |
206 |
219 lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))" |
207 lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))" |
220 by (simp add: nat_diff_distrib) |
208 by (simp add: nat_diff_distrib) |
221 |
209 |
222 lemma aux_2: "2 < p ==> 0 < nat (p - 2)" |
210 lemma aux_2: "2 < p ==> 0 < nat (p - 2)" |
223 by auto |
211 by auto |
224 |
212 |
225 lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
213 lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
226 ~([MultInv p x = 0](mod p))" |
214 ~([MultInv p x = 0](mod p))" |
227 apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1) |
215 apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1) |
228 apply (drule aux_2) |
216 apply (drule aux_2) |
229 apply (drule zpower_zdvd_prop2, auto) |
217 apply (drule zpower_zdvd_prop2, auto) |
230 done |
218 done |
231 |
219 |
232 lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> |
220 lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> |
233 [(MultInv p (MultInv p x)) = (x * (MultInv p x) * |
221 [(MultInv p (MultInv p x)) = (x * (MultInv p x) * |
234 (MultInv p (MultInv p x)))] (mod p)" |
222 (MultInv p (MultInv p x)))] (mod p)" |
235 apply (drule MultInv_prop2, auto) |
223 apply (drule MultInv_prop2, auto) |
236 apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto) |
224 apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto) |
237 apply (auto simp add: zcong_sym) |
225 apply (auto simp add: zcong_sym) |
238 done |
226 done |
244 apply (drule MultInv_prop2, auto) |
232 apply (drule MultInv_prop2, auto) |
245 apply (drule_tac k = x in zcong_scalar2, auto) |
233 apply (drule_tac k = x in zcong_scalar2, auto) |
246 apply (auto simp add: zmult_ac) |
234 apply (auto simp add: zmult_ac) |
247 done |
235 done |
248 |
236 |
249 lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
237 lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
250 [(MultInv p (MultInv p x)) = x] (mod p)" |
238 [(MultInv p (MultInv p x)) = x] (mod p)" |
251 apply (frule aux__1, auto) |
239 apply (frule aux__1, auto) |
252 apply (drule aux__2, auto) |
240 apply (drule aux__2, auto) |
253 apply (drule zcong_trans, auto) |
241 apply (drule zcong_trans, auto) |
254 done |
242 done |
255 |
243 |
256 lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p)); |
244 lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p)); |
257 ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> |
245 ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> |
258 [x = y] (mod p)" |
246 [x = y] (mod p)" |
259 apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and |
247 apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and |
260 m = p and k = x in zcong_scalar) |
248 m = p and k = x in zcong_scalar) |
261 apply (insert MultInv_prop2 [of p x], simp) |
249 apply (insert MultInv_prop2 [of p x], simp) |
262 apply (auto simp only: zcong_sym [of "MultInv p x * x"]) |
250 apply (auto simp only: zcong_sym [of "MultInv p x * x"]) |
263 apply (auto simp add: zmult_ac) |
251 apply (auto simp add: zmult_ac) |
264 apply (drule zcong_trans, auto) |
252 apply (drule zcong_trans, auto) |
266 apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac) |
254 apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac) |
267 apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x]) |
255 apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x]) |
268 apply (auto simp add: zcong_sym) |
256 apply (auto simp add: zcong_sym) |
269 done |
257 done |
270 |
258 |
271 lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> |
259 lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> |
272 [a * MultInv p j = a * MultInv p k] (mod p)" |
260 [a * MultInv p j = a * MultInv p k] (mod p)" |
273 by (drule MultInv_prop1, auto simp add: zcong_scalar2) |
261 by (drule MultInv_prop1, auto simp add: zcong_scalar2) |
274 |
262 |
275 lemma aux___1: "[j = a * MultInv p k] (mod p) ==> |
263 lemma aux___1: "[j = a * MultInv p k] (mod p) ==> |
276 [j * k = a * MultInv p k * k] (mod p)" |
264 [j * k = a * MultInv p k * k] (mod p)" |
277 by (auto simp add: zcong_scalar) |
265 by (auto simp add: zcong_scalar) |
278 |
266 |
279 lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p)); |
267 lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p)); |
280 [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)" |
268 [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)" |
281 apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 |
269 apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 |
282 [of "MultInv p k * k" 1 p "j * k" a]) |
270 [of "MultInv p k * k" 1 p "j * k" a]) |
283 apply (auto simp add: zmult_ac) |
271 apply (auto simp add: zmult_ac) |
284 done |
272 done |
285 |
273 |
286 lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = |
274 lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = |
287 (MultInv p j) * a] (mod p)" |
275 (MultInv p j) * a] (mod p)" |
288 by (auto simp add: zmult_assoc zcong_scalar2) |
276 by (auto simp add: zmult_assoc zcong_scalar2) |
289 |
277 |
290 lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p)); |
278 lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p)); |
291 [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |] |
279 [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |] |
292 ==> [k = a * (MultInv p j)] (mod p)" |
280 ==> [k = a * (MultInv p j)] (mod p)" |
293 apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 |
281 apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 |
294 [of "MultInv p j * j" 1 p "MultInv p j * a" k]) |
282 [of "MultInv p j * j" 1 p "MultInv p j * a" k]) |
295 apply (auto simp add: zmult_ac zcong_sym) |
283 apply (auto simp add: zmult_ac zcong_sym) |
296 done |
284 done |
297 |
285 |
298 lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p)); |
286 lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p)); |
299 ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> |
287 ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> |
300 [k = a * MultInv p j] (mod p)" |
288 [k = a * MultInv p j] (mod p)" |
301 apply (drule aux___1) |
289 apply (drule aux___1) |
302 apply (frule aux___2, auto) |
290 apply (frule aux___2, auto) |
303 by (drule aux___3, drule aux___4, auto) |
291 by (drule aux___3, drule aux___4, auto) |
304 |
292 |
305 lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p)); |
293 lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p)); |
306 ~([k = 0](mod p)); ~([j = 0](mod p)); |
294 ~([k = 0](mod p)); ~([j = 0](mod p)); |
307 [a * MultInv p j = a * MultInv p k] (mod p) |] ==> |
295 [a * MultInv p j = a * MultInv p k] (mod p) |] ==> |
308 [j = k] (mod p)" |
296 [j = k] (mod p)" |
309 apply (auto simp add: zcong_eq_zdvd_prop [of a p]) |
297 apply (auto simp add: zcong_eq_zdvd_prop [of a p]) |
310 apply (frule zprime_imp_zrelprime, auto) |
298 apply (frule zprime_imp_zrelprime, auto) |
311 apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto) |
299 apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto) |
312 apply (drule MultInv_prop5, auto) |
300 apply (drule MultInv_prop5, auto) |