253 |
253 |
254 lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A" |
254 lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A" |
255 by (unfold inj_on_def, auto) |
255 by (unfold inj_on_def, auto) |
256 |
256 |
257 lemma Bnor_prod_power [rule_format]: |
257 lemma Bnor_prod_power [rule_format]: |
258 "x \<noteq> 0 ==> a < m --> setprod ((\<lambda>a. a * x) ` BnorRset (a, m)) = |
258 "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset (a, m)) = |
259 setprod (BnorRset(a, m)) * x^card (BnorRset (a, m))" |
259 \<Prod>(BnorRset(a, m)) * x^card (BnorRset (a, m))" |
260 apply (induct a m rule: BnorRset_induct) |
260 apply (induct a m rule: BnorRset_induct) |
261 prefer 2 |
261 prefer 2 |
262 apply (subst BnorRset.simps) |
262 apply (subst BnorRset.simps) |
263 apply (unfold Let_def, auto) |
263 apply (unfold Let_def, auto) |
264 apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
264 apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
271 |
271 |
272 |
272 |
273 subsection {* Fermat *} |
273 subsection {* Fermat *} |
274 |
274 |
275 lemma bijzcong_zcong_prod: |
275 lemma bijzcong_zcong_prod: |
276 "(A, B) \<in> bijR (zcongm m) ==> [setprod A = setprod B] (mod m)" |
276 "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)" |
277 apply (unfold zcongm_def) |
277 apply (unfold zcongm_def) |
278 apply (erule bijR.induct) |
278 apply (erule bijR.induct) |
279 apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B") |
279 apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B") |
280 apply (auto intro: fin_bijRl fin_bijRr zcong_zmult) |
280 apply (auto intro: fin_bijRl fin_bijRr zcong_zmult) |
281 done |
281 done |
282 |
282 |
283 lemma Bnor_prod_zgcd [rule_format]: |
283 lemma Bnor_prod_zgcd [rule_format]: |
284 "a < m --> zgcd (setprod (BnorRset (a, m)), m) = 1" |
284 "a < m --> zgcd (\<Prod>(BnorRset(a, m)), m) = 1" |
285 apply (induct a m rule: BnorRset_induct) |
285 apply (induct a m rule: BnorRset_induct) |
286 prefer 2 |
286 prefer 2 |
287 apply (subst BnorRset.simps) |
287 apply (subst BnorRset.simps) |
288 apply (unfold Let_def, auto) |
288 apply (unfold Let_def, auto) |
289 apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
289 apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
294 "0 < m ==> zgcd (x, m) = 1 ==> [x^(phi m) = 1] (mod m)" |
294 "0 < m ==> zgcd (x, m) = 1 ==> [x^(phi m) = 1] (mod m)" |
295 apply (unfold norRRset_def phi_def) |
295 apply (unfold norRRset_def phi_def) |
296 apply (case_tac "x = 0") |
296 apply (case_tac "x = 0") |
297 apply (case_tac [2] "m = 1") |
297 apply (case_tac [2] "m = 1") |
298 apply (rule_tac [3] iffD1) |
298 apply (rule_tac [3] iffD1) |
299 apply (rule_tac [3] k = "setprod (BnorRset (m - 1, m))" |
299 apply (rule_tac [3] k = "\<Prod>(BnorRset(m - 1, m))" |
300 in zcong_cancel2) |
300 in zcong_cancel2) |
301 prefer 5 |
301 prefer 5 |
302 apply (subst Bnor_prod_power [symmetric]) |
302 apply (subst Bnor_prod_power [symmetric]) |
303 apply (rule_tac [7] Bnor_prod_zgcd, simp_all) |
303 apply (rule_tac [7] Bnor_prod_zgcd, simp_all) |
304 apply (rule bijzcong_zcong_prod) |
304 apply (rule bijzcong_zcong_prod) |