isabelle: src/HOL/NumberTheory/EulerFermat.ML@50be659d4222 (annotated)

9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	1	(* Title: EulerFermat.ML
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	2	ID: $Id$
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	3	Author: Thomas M. Rasmussen
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	4	Copyright 2000 University of Cambridge
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	5
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	6	Fermat's Little Theorem extended to Euler's Totient function.
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	7	More abstract approach than Boyer-Moore (which seems necessary
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	8	to achieve the extended version)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	9	*)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	10
9943 55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	11	(LCP: not sure why this lemma is needed now)
55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	12	Goal "(abs z = (#1::int)) = (z = #1 \| z = #-1)";
55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	13	by (auto_tac (claset(), simpset() addsimps [zabs_def]));
55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	14	qed "abs_eq_1_iff";
55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	15	AddIffs [abs_eq_1_iff];
55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	16
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	17
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	18	(* norRRset *)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	19
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	20	Addsimps [RsetR.empty];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	21
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	22	val [BnorRset_eq] = BnorRset.simps;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	23	Delsimps BnorRset.simps;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	24
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	25	val [prem1,prem2] =
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	26	Goal "[\| !! a m. P {} a m; \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	27	\ (!!a m. [\| #0 < (a::int); P (BnorRset(a-#1,m::int)) (a-#1) m \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	28	\ ==> P (BnorRset(a,m)) a m) \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	29	\ ==> P (BnorRset(u,v)) u v";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	30	by (rtac BnorRset.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	31	by Safe_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	32	by (case_tac "#0<a" 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	33	by (rtac prem2 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	34	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	35	by (ALLGOALS (asm_simp_tac (simpset() addsimps [BnorRset_eq,prem1])));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	36	qed "BnorRset_induct";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	37
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	38	Goal "b:BnorRset(a,m) --> b<=a";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9634 diff changeset	39	by (induct_thm_tac BnorRset_induct "a m" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	40	by (stac BnorRset_eq 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	41	by (rewtac Let_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	42	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	43	qed_spec_mp "Bnor_mem_zle";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	44
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	45	Goal "a<b ==> b~:BnorRset(a,m)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	46	by (res_inst_tac [("Pa","b<=a")] swap 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	47	by (rtac Bnor_mem_zle 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	48	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	49	qed "Bnor_mem_zle_swap";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	50
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	51	Goal "b:BnorRset(a,m) --> #0<b";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9634 diff changeset	52	by (induct_thm_tac BnorRset_induct "a m" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	53	by (stac BnorRset_eq 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	54	by (rewtac Let_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	55	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	56	qed_spec_mp "Bnor_mem_zg";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	57
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	58	Goal "zgcd(b,m) = #1 --> #0<b --> b<=a --> b:BnorRset(a,m)";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9634 diff changeset	59	by (induct_thm_tac BnorRset.induct "a m" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	60	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	61	by (case_tac "a=b" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	62	by (asm_full_simp_tac (simpset() addsimps [zle_neq_implies_zless]) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	63	by (Asm_simp_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	64	by (ALLGOALS (stac BnorRset_eq));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	65	by (rewtac Let_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	66	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	67	qed_spec_mp "Bnor_mem_if";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	68
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	69	Goal "a<m --> BnorRset (a,m) : RsetR m";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9634 diff changeset	70	by (induct_thm_tac BnorRset_induct "a m" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	71	by (Simp_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	72	by (stac BnorRset_eq 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	73	by (rewtac Let_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	74	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	75	by (rtac RsetR.insert 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	76	by (rtac allI 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	77	by (rtac impI 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	78	by (rtac zcong_not 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	79	by (subgoal_tac "a' <= a-#1" 6);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	80	by (rtac Bnor_mem_zle 7);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	81	by (rtac Bnor_mem_zg 5);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	82	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	83	qed_spec_mp "Bnor_in_RsetR";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	84
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	85	Goal "finite (BnorRset (a,m))";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9634 diff changeset	86	by (induct_thm_tac BnorRset_induct "a m" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	87	by (stac BnorRset_eq 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	88	by (rewtac Let_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	89	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	90	qed "Bnor_fin";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	91
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	92	Goal "a <= b - #1 ==> a < (b::int)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	93	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	94	val lemma = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	95
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	96	Goalw [norRRset_def]
9572 bfee45ac5d38 tidied paulson parents: 9508 diff changeset	97	"[\| #1<m; zgcd(a,m) = #1 \|] ==> (EX! b. [a = b](mod m) & b:(norRRset m))";
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	98	by (cut_inst_tac [("a","a"),("m","m")] zcong_zless_unique 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	99	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	100	by (res_inst_tac [("m","m")] zcong_zless_imp_eq 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	101	by (auto_tac (claset() addIs [Bnor_mem_zle,Bnor_mem_zg,zcong_trans,
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	102	zless_imp_zle,lemma],
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	103	simpset() addsimps [zcong_sym]));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	104	by (res_inst_tac [("x","b")] exI 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	105	by Safe_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	106	by (rtac Bnor_mem_if 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	107	by (case_tac "b=#0" 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	108	by (auto_tac (claset() addIs [zle_neq_implies_zless], simpset()));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	109	by (SELECT_GOAL (rewtac zcong_def) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	110	by (subgoal_tac "zgcd(a,m) = m" 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	111	by (stac (zdvd_iff_zgcd RS sym) 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	112	by (rtac zgcd_zcong_zgcd 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	113	by (ALLGOALS (asm_full_simp_tac (simpset()
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	114	addsimps [zdvd_zminus_iff,zcong_sym])));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	115	qed "norR_mem_unique";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	116
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	117
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	118	(* noXRRset *)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	119
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	120	Goalw [is_RRset_def]
9943 55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	121	"is_RRset A m ==> a:A --> zgcd (a,m) = #1";
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	122	by (rtac RsetR.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	123	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	124	qed_spec_mp "RRset_gcd";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	125
9943 55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	126	Goal "[\| A : RsetR m; #0<m; zgcd(x, m) = #1 \|] ==> (%a. a*x)``A : RsetR m";
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	127	by (etac RsetR.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	128	by (ALLGOALS Simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	129	by (rtac RsetR.insert 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	130	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	131	by (asm_full_simp_tac (simpset() addsimps [zcong_cancel]) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	132	by (blast_tac (claset() addIs [zgcd_zgcd_zmult]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	133	qed "RsetR_zmult_mono";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	134
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	135	Goalw [norRRset_def,noXRRset_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	136	"[\| #0<m; zgcd(x,m) = #1 \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	137	\ ==> card (noXRRset m x) = card (norRRset m)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	138	by (rtac card_image 1);
9634 61b57cc1cb5a modified proofs: better rules for cancellation of common factors across comparisons paulson parents: 9572 diff changeset	139	by (auto_tac (claset(),simpset() addsimps [inj_on_def, Bnor_fin]));
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	140	by (asm_full_simp_tac (simpset() addsimps [BnorRset_eq]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	141	qed "card_nor_eq_noX";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	142
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	143	Goalw [is_RRset_def,phi_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	144	"[\| #0<m; zgcd(x,m) = #1 \|] ==> is_RRset (noXRRset m x) m";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	145	by (auto_tac (claset(),simpset() addsimps [card_nor_eq_noX]));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	146	by (rewrite_goals_tac [noXRRset_def,norRRset_def]);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	147	by (rtac RsetR_zmult_mono 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	148	by (rtac Bnor_in_RsetR 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	149	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	150	qed "noX_is_RRset";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	151
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	152	Goal "[\| #1<m; is_RRset A m; a:A \|] \
9943 55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	153	\ ==> zcong a (@ b. [a = b](mod m) & b : norRRset m) m & \
55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	154	\ (@ b. [a = b](mod m) & b : norRRset m) : norRRset m";
9572 bfee45ac5d38 tidied paulson parents: 9508 diff changeset	155	by (rtac (norR_mem_unique RS ex1_implies_ex RS ex_someI) 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	156	by (rtac RRset_gcd 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	157	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	158	val lemma_some = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	159
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	160	Goalw [RRset2norRR_def]
9943 55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	161	"[\| #1<m; is_RRset A m; a:A \|] \
55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	162	\ ==> [a = RRset2norRR A m a] (mod m) & (RRset2norRR A m a):(norRRset m)";
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	163	by (Asm_simp_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	164	by (rtac lemma_some 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	165	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	166	qed "RRset2norRR_correct";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	167
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	168	bind_thm ("RRset2norRR_correct1", RRset2norRR_correct RS conjunct1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	169	bind_thm ("RRset2norRR_correct2", RRset2norRR_correct RS conjunct2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	170
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	171	Goal "A : (RsetR m) ==> finite A";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	172	by (etac RsetR.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	173	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	174	qed "RsetR_fin";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	175
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	176	Goalw [is_RRset_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	177	"[\| #1<m; is_RRset A m; [a = b](mod m) \|] ==> a:A --> b:A --> a = b";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	178	by (rtac RsetR.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	179	by (auto_tac (claset(), simpset() addsimps [zcong_sym]));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	180	qed_spec_mp "RRset_zcong_eq";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	181
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	182	Goal "[\| P (@ a. P a); Q (@ a. Q a); (@ a. P a) = (@ a. Q a) \|] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	183	\ ==> (EX a. P a & Q a)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	184	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	185	val lemma = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	186
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	187	Goalw [RRset2norRR_def,inj_on_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	188	"[\| #1<m; is_RRset A m \|] ==> inj_on (RRset2norRR A m) A";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	189	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	190	by (subgoal_tac "(EX b. ([x = b](mod m) & b : norRRset m) & \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	191	\ ([y = b](mod m) & b : norRRset m))" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	192	by (rtac lemma 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	193	by (rtac lemma_some 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	194	by (rtac lemma_some 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	195	by (rtac RRset_zcong_eq 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	196	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	197	by (res_inst_tac [("b","b")] zcong_trans 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	198	by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zcong_sym])));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	199	qed "RRset2norRR_inj";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	200
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	201	Goal "[\| #1<m; is_RRset A m \|] ==> (RRset2norRR A m)``A = (norRRset m)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	202	by (rtac card_seteq 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	203	by (stac card_image 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	204	by (rtac RRset2norRR_inj 4);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	205	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	206	by (rtac RRset2norRR_correct2 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	207	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	208	by (rewrite_goals_tac [is_RRset_def,phi_def,norRRset_def]);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	209	by (auto_tac (claset(),simpset() addsimps [RsetR_fin,Bnor_fin]));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	210	qed "RRset2norRR_eq_norR";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	211
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	212	Goalw [inj_on_def] "[\| a ~: A ; inj f \|] ==> (f a) ~: f``A";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	213	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	214	val lemma = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	215
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	216	Goal "x~=#0 ==> a<m --> setprod ((%a. a*x) `` BnorRset(a,m)) = \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	217	\ setprod (BnorRset(a,m)) * x^card(BnorRset(a,m))";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9634 diff changeset	218	by (induct_thm_tac BnorRset_induct "a m" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	219	by (stac BnorRset_eq 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	220	by (rewtac Let_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	221	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	222	by (asm_simp_tac (simpset() addsimps [Bnor_fin,Bnor_mem_zle_swap]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	223	by (stac setprod_insert 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	224	by (rtac lemma 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	225	by (rewtac inj_on_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	226	by (ALLGOALS (asm_full_simp_tac (simpset()
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	227	addsimps zmult_ac@[Bnor_fin,finite_imageI,Bnor_mem_zle_swap])));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	228	qed_spec_mp "Bnor_prod_power";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	229
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	230
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	231	(* Fermat *)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	232
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	233	Goalw [zcongm_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	234	"(A,B) : bijR (zcongm m) ==> [setprod A = setprod B](mod m)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	235	by (etac bijR.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	236	by (subgoal_tac "a~:A & b~:B & finite A & finite B" 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	237	by (auto_tac (claset() addIs [fin_bijRl,fin_bijRr,zcong_zmult],
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	238	simpset()));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	239	qed "bijzcong_zcong_prod";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	240
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	241	Goalw [norRRset_def,phi_def]
9943 55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	242	"a<m --> zgcd (setprod (BnorRset (a,m)),m) = #1";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9634 diff changeset	243	by (induct_thm_tac BnorRset_induct "a m" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	244	by (stac BnorRset_eq 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	245	by (rewtac Let_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	246	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	247	by (asm_simp_tac (simpset() addsimps [Bnor_fin,Bnor_mem_zle_swap]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	248	by (blast_tac (claset() addIs [zgcd_zgcd_zmult]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	249	qed_spec_mp "Bnor_prod_zgcd";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	250
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	251	Goalw [norRRset_def,phi_def]
9943 55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	252	"[\| #0<m; zgcd(x,m) = #1 \|] ==> [x^phi(m) = #1] (mod m)";
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	253	by (case_tac "x=#0" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	254	by (case_tac "m=#1" 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	255	by (rtac iffD1 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	256	by (res_inst_tac [("k","setprod (BnorRset (m-#1,m))")] zcong_cancel2 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	257	by (stac (Bnor_prod_power RS sym) 5);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	258	by (rtac Bnor_prod_zgcd 4);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	259	by (ALLGOALS Asm_full_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	260	by (rtac bijzcong_zcong_prod 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	261	by (fold_goals_tac [norRRset_def,noXRRset_def]);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	262	by (stac (RRset2norRR_eq_norR RS sym) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	263	by (rtac inj_func_bijR 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	264	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	265	by (rewtac zcongm_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	266	by (rtac RRset2norRR_correct1 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	267	by (rtac RRset2norRR_inj 6);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	268	by (auto_tac (claset() addIs [zle_neq_implies_zless],
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	269	simpset() addsimps [noX_is_RRset]));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	270	by (rewrite_goals_tac [noXRRset_def,norRRset_def]);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	271	by (rtac finite_imageI 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	272	by (rtac Bnor_fin 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	273	qed "EulerFermatTheorem";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	274
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	275	Goalw [zprime_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	276	"p:zprime ==> a<p --> (ALL b. #0<b & b<=a --> zgcd(b,p) = #1) \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	277	\ --> card (BnorRset(a, p)) = nat a";
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 9634 diff changeset	278	by (induct_thm_tac BnorRset.induct "a p" 1);
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	279	by (stac BnorRset_eq 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	280	by (rewtac Let_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	281	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	282	qed_spec_mp "Bnor_prime";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	283
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	284	Goalw [phi_def,norRRset_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	285	"p:zprime ==> phi(p) = nat (p-#1)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	286	by (rtac Bnor_prime 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	287	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	288	by (etac zless_zprime_imp_zrelprime 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	289	by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	290	qed "phi_prime";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	291
9943 55c82decf3f4 zgcd now works for negative integers paulson parents: 9747 diff changeset	292	Goal "[\| p:zprime; ~p dvd x \|] ==> [x^(nat (p-#1)) = #1] (mod p)";
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	293	by (stac (phi_prime RS sym) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	294	by (rtac EulerFermatTheorem 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	295	by (etac zprime_imp_zrelprime 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	296	by (rewtac zprime_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	297	by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	298	qed "Little_Fermat";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	299

author	wenzelm
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 9943	55c82decf3f4
child 10175	76646fc8b1bf
permissions	-rw-r--r--