author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9747  043098ba5098 
child 10658  b9d43a2add79 
permissions  rwrr 
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^(y*n)) (#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  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  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  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  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  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  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"; 