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

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

author	wenzelm
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 9747	043098ba5098
child 10658	b9d43a2add79
permissions	-rw-r--r--