author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10198  2b255b772585 
child 10658  b9d43a2add79 
permissions  rwrr 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

1 
(* Title: IntPrimes.ML 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

2 
ID: $Id$ 
9943  3 
Author: Thomas M. Rasmussen & L C Paulson 
9508
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 
dvd relation, GCD, Euclid's extended algorithm, primes, congruences 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

7 
(all on the Integers) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

8 

9943  9 
Comparable to Primes theory, but dvd is included here as it is not present in 
10 
IntDiv. Also includes extended GCD and congruences  not present in Primes. 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

11 
*) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

12 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

13 
eta_contract:=false; 
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 

9943  16 
Goal "(abs (z::int) = w) = (z=w & #0 <= z  z=w & z < #0)"; 
17 
by (auto_tac (claset(), simpset() addsimps [zabs_def])); 

18 
qed "zabs_eq_iff"; 

19 

20 

21 
(** gcd lemmas **) 

22 

23 
val gcd_non_0 = thm "gcd_non_0"; 

24 
val gcd_add1 = thm "gcd_add1"; 

25 
val gcd_commute = thm "gcd_commute"; 

26 

27 
Goal "gcd (m+k, k) = gcd (m+k, m)"; 

28 
by (simp_tac (simpset() addsimps [gcd_commute]) 1); 

29 
qed "gcd_add1_eq"; 

30 

10142  31 
Goal "m <= n ==> gcd (n, n  m) = gcd (n, m)"; 
9943  32 
by (subgoal_tac "n = m + (nm)" 1); 
33 
by (etac ssubst 1 THEN rtac gcd_add1_eq 1); 

34 
by (Asm_simp_tac 1); 

35 
qed "gcd_diff2"; 

36 

37 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

38 
(************************************************) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

39 
(** Divides relation 'dvd' **) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

40 
(************************************************) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

41 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

42 
Goalw [dvd_def] "(m::int) dvd #0"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

43 
by (blast_tac (claset() addIs [zmult_0_right RS sym]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

44 
qed "zdvd_0_right"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

45 
AddIffs [zdvd_0_right]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

46 

9943  47 
Goalw [dvd_def] "(#0 dvd (m::int)) = (m = #0)"; 
9508
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 "zdvd_0_left"; 
9943  50 
AddIffs [zdvd_0_left]; 
9508
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 
Goalw [dvd_def] "#1 dvd (m::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

53 
by (Simp_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

54 
qed "zdvd_1_left"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

55 
AddIffs [zdvd_1_left]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

56 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

57 
Goalw [dvd_def] "m dvd (m::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

58 
by (blast_tac (claset() addIs [zmult_1_right RS sym]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

59 
qed "zdvd_refl"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

60 
Addsimps [zdvd_refl]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

61 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

62 
Goalw [dvd_def] "[ m dvd n; n dvd k ] ==> m dvd (k::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

63 
by (blast_tac (claset() addIs [zmult_assoc] ) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

64 
qed "zdvd_trans"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

65 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

66 
Goalw [dvd_def] "(m dvd n) = (m dvd (n::int))"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

67 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

68 
by (ALLGOALS (res_inst_tac [("x","k")] exI)); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

69 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

70 
qed "zdvd_zminus_iff"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

71 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

72 
Goalw [dvd_def] "(m dvd n) = (m dvd (n::int))"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

73 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

74 
by (ALLGOALS (res_inst_tac [("x","k")] exI)); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

75 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

76 
qed "zdvd_zminus2_iff"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

77 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

78 
Goalw [dvd_def] "[ #0<m; #0<n; m dvd n; n dvd m ] ==> m = (n::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

79 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

80 
by (asm_full_simp_tac 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

81 
(simpset() addsimps [zmult_assoc,zmult_eq_self_iff, 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

82 
int_0_less_mult_iff, zmult_eq_1_iff]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

83 
qed "zdvd_anti_sym"; 
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 
Goalw [dvd_def] "[ k dvd m; k dvd n ] ==> k dvd (m+n :: int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

86 
by (blast_tac (claset() addIs [zadd_zmult_distrib2 RS sym]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

87 
qed "zdvd_zadd"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

88 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

89 
Goalw [dvd_def] "[ k dvd m; k dvd n ] ==> k dvd (mn :: int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

90 
by (blast_tac (claset() addIs [zdiff_zmult_distrib2 RS sym]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

91 
qed "zdvd_zdiff"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

92 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

93 
Goal "[ k dvd (mn); k dvd n ] ==> k dvd (m::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

94 
by (subgoal_tac "m=n+(mn)" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

95 
by (etac ssubst 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

96 
by (blast_tac (claset() addIs [zdvd_zadd]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

97 
by (Simp_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

98 
qed "zdvd_zdiffD"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

99 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

100 
Goalw [dvd_def] "k dvd (n::int) ==> k dvd (m*n)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

101 
by (blast_tac (claset() addIs [zmult_left_commute]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

102 
qed "zdvd_zmult"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

103 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

104 
Goal "k dvd (m::int) ==> k dvd (m*n)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

105 
by (stac zmult_commute 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

106 
by (etac zdvd_zmult 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

107 
qed "zdvd_zmult2"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

108 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

109 
(* k dvd (m*k) *) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

110 
AddIffs [zdvd_refl RS zdvd_zmult, zdvd_refl RS zdvd_zmult2]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

111 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

112 
Goalw [dvd_def] "(j*k) dvd n ==> j dvd (n::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

113 
by (full_simp_tac (simpset() addsimps [zmult_assoc]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

114 
by (Blast_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

115 
qed "zdvd_zmultD2"; 
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 
Goal "(j*k) dvd n ==> k dvd (n::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

118 
by (rtac zdvd_zmultD2 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

119 
by (stac zmult_commute 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

120 
by (assume_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

121 
qed "zdvd_zmultD"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

122 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

123 
Goalw [dvd_def] "[ i dvd m; j dvd (n::int) ] ==> (i*j) dvd (m*n)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

124 
by (Clarify_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

125 
by (res_inst_tac [("x","k*ka")] exI 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

126 
by (asm_simp_tac (simpset() addsimps zmult_ac) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

127 
qed "zdvd_zmult_mono"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

128 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

129 
Goal "k dvd (n + k*m) = k dvd (n::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

130 
by (rtac iffI 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

131 
by (etac zdvd_zadd 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

132 
by (subgoal_tac "n = (n+k*m)k*m" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

133 
by (etac ssubst 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

134 
by (etac zdvd_zdiff 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

135 
by (ALLGOALS Simp_tac); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

136 
qed "zdvd_reduce"; 
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 
Goalw [dvd_def] "[ f dvd m; f dvd (n::int) ] ==> f dvd (m mod n)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

139 
by (auto_tac (claset(), simpset() addsimps [zmod_zmult_zmult1])); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

140 
qed "zdvd_zmod"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

141 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

142 
Goal "[ k dvd (m mod n); k dvd n ] ==> k dvd (m::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

143 
by (subgoal_tac "k dvd (n*(m div n) + m mod n)" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

144 
by (asm_simp_tac (simpset() addsimps [zdvd_zadd, zdvd_zmult2]) 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

145 
by (asm_full_simp_tac (simpset() addsimps [zmod_zdiv_equality RS sym]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

146 
qed "zdvd_zmod_imp_zdvd"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

147 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

148 
Goalw [dvd_def] "(k dvd n) = (n mod (k::int) = #0)"; 
10198  149 
by (auto_tac (claset(), simpset() addsimps [zmod_zmult_self2])); 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

150 
qed "zdvd_iff_zmod_eq_0"; 
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 "[ ~k<#0; k~=#0 ] ==> #0<(k::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

153 
by (arith_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

154 
val lemma = result(); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

155 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

156 
Goalw [dvd_def] "[ #0<m; m<n ] ==> ~n dvd (m::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

157 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

158 
by (subgoal_tac "#0<n" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

159 
by (blast_tac (claset() addIs [zless_trans]) 2); 
9634
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

160 
by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1); 
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

161 
by (subgoal_tac "n*k < n*#1" 1); 
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

162 
by (dtac (zmult_zless_cancel1 RS iffD1) 1); 
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

163 
by Auto_tac; 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

164 
qed "zdvd_not_zless"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

165 

9943  166 
Goal "(int m dvd z) = (m dvd nat(abs z))"; 
167 
by (auto_tac (claset(), 

168 
simpset() addsimps [dvd_def, nat_abs_mult_distrib])); 

169 
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, zabs_eq_iff])); 

170 
by (res_inst_tac [("x","(int k)")] exI 2); 

171 
by (auto_tac (claset(), simpset() addsimps [zmult_int RS sym])); 

172 
qed "int_dvd_iff"; 

173 

174 
Goal "(z dvd int m) = (nat(abs z) dvd m)"; 

175 
by (auto_tac (claset(), 

176 
simpset() addsimps [dvd_def, zabs_def, zmult_int RS sym])); 

177 
by (res_inst_tac [("x","nat k")] exI 3); 

178 
by (res_inst_tac [("x","(int k)")] exI 2); 

179 
by (res_inst_tac [("x","nat (k)")] exI 1); 

180 
by (cut_inst_tac [("k","m")] int_less_0_conv 3); 

181 
by (cut_inst_tac [("k","m")] int_less_0_conv 1); 

182 
by (auto_tac (claset(), 

183 
simpset() addsimps [int_0_le_mult_iff, zmult_less_0_iff, 

184 
nat_mult_distrib RS sym, nat_eq_iff2])); 

185 
qed "dvd_int_iff"; 

186 

187 
Goal "(nat z dvd m) = (if #0 <= z then (z dvd int m) else m=0)"; 

188 
by (auto_tac (claset(), simpset() addsimps [dvd_def, zmult_int RS sym])); 

189 
by (res_inst_tac [("x","nat k")] exI 1); 

190 
by (cut_inst_tac [("k","m")] int_less_0_conv 1); 

191 
by (auto_tac (claset(), 

192 
simpset() addsimps [int_0_le_mult_iff, zmult_less_0_iff, 

193 
nat_mult_distrib RS sym, nat_eq_iff2])); 

194 
qed "nat_dvd_iff"; 

195 

196 
Goal "(z dvd w) = (z dvd (w::int))"; 

197 
by (auto_tac (claset(), simpset() addsimps [dvd_def])); 

198 
by (ALLGOALS (res_inst_tac [("x","k")] exI)); 

199 
by Auto_tac; 

200 
qed "zminus_dvd_iff"; 

201 

202 
Goal "(z dvd w) = (z dvd (w::int))"; 

203 
by (auto_tac (claset(), simpset() addsimps [dvd_def])); 

204 
by (dtac (zminus_equation RS iffD1) 1); 

205 
by (ALLGOALS (res_inst_tac [("x","k")] exI)); 

206 
by Auto_tac; 

207 
qed "dvd_zminus_iff"; 

208 
AddIffs [zminus_dvd_iff, dvd_zminus_iff]; 

209 

9508
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 
(************************************************) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

212 
(** Euclid's Algorithm and GCD **) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

213 
(************************************************) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

214 

9943  215 
Goal "zgcd(m,#0) = abs m"; 
216 
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

217 
qed "zgcd_0"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

218 
Addsimps [zgcd_0]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

219 

9943  220 
Goal"zgcd(#0,m) = abs m"; 
221 
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

222 
qed "zgcd_0_left"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

223 
Addsimps [zgcd_0_left]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

224 

9943  225 
Goal "zgcd(m,n) = zgcd(m,n)"; 
226 
by (simp_tac (simpset() addsimps [zgcd_def]) 1); 

227 
qed "zgcd_zminus"; 

228 
Addsimps [zgcd_zminus]; 

229 

230 
Goal "zgcd(m,n) = zgcd(m,n)"; 

231 
by (simp_tac (simpset() addsimps [zgcd_def]) 1); 

232 
qed "zgcd_zminus2"; 

233 
Addsimps [zgcd_zminus2]; 

234 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

235 
Goal "#0<n ==> zgcd(m,n) = zgcd (n, m mod n)"; 
9943  236 
by (forw_inst_tac [("b","n"), ("a","m")] pos_mod_sign 1); 
237 
by (asm_simp_tac (simpset() addsimps [zgcd_def, zabs_def, nat_mod_distrib]) 1); 

238 
by (cut_inst_tac [("a","m"),("b","n")] zmod_zminus1_eq_if 1); 

239 
by (auto_tac (claset(), 

240 
simpset() addsimps [gcd_non_0, nat_mod_distrib RS sym, 

241 
zmod_zminus1_eq_if])); 

242 
by (forw_inst_tac [("a","m")] pos_mod_bound 1); 

243 
by (asm_simp_tac (simpset() addsimps [nat_diff_distrib]) 1); 

244 
by (rtac gcd_diff2 1); 

245 
by (asm_full_simp_tac (simpset() addsimps [nat_le_eq_zle]) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

246 
qed "zgcd_non_0"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

247 

9943  248 
Goal "zgcd(m,n) = zgcd (n, m mod n)"; 
249 
by (zdiv_undefined_case_tac "n = #0" 1); 

250 
by (auto_tac 

251 
(claset(), 

252 
simpset() addsimps [linorder_neq_iff, zgcd_non_0])); 

253 
by (cut_inst_tac [("m","m"),("n","n")] zgcd_non_0 1); 

254 
by Auto_tac; 

255 
qed "zgcd_eq"; 

256 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

257 
Goal "zgcd(m,#1) = #1"; 
9943  258 
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

259 
qed "zgcd_1"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

260 
Addsimps [zgcd_1]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

261 

9943  262 
Goal "(zgcd(#0,m) = #1) = (abs m = #1)"; 
263 
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

264 
qed "zgcd_0_1_iff"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

265 
Addsimps [zgcd_0_1_iff]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

266 

9943  267 
Goal "zgcd(m,n) dvd m"; 
268 
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff]) 1); 

269 
qed "zgcd_zdvd1"; 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

270 

9943  271 
Goal "zgcd(m,n) dvd n"; 
272 
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff]) 1); 

273 
qed "zgcd_zdvd2"; 

274 
AddIffs [zgcd_zdvd1, zgcd_zdvd2]; 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

275 

9943  276 
Goal "k dvd zgcd(m,n) = (k dvd m & k dvd n)"; 
277 
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff, 

278 
dvd_int_iff, nat_dvd_iff]) 1); 

279 
qed "zgcd_greatest_iff"; 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

280 

9943  281 
Goal "zgcd(m,n) = zgcd(n,m)"; 
282 
by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_commute"]) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

283 
qed "zgcd_commute"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

284 

9943  285 
Goal "zgcd(#1,m) = #1"; 
286 
by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_1_left"]) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

287 
qed "zgcd_1_left"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

288 
Addsimps [zgcd_1_left]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

289 

9943  290 
Goal "zgcd(zgcd(k,m),n) = zgcd(k,zgcd(m,n))"; 
291 
by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_assoc"]) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

292 
qed "zgcd_assoc"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

293 

9943  294 
Goal "zgcd(k,zgcd(m,n)) = zgcd(m,zgcd(k,n))"; 
295 
by (rtac (zgcd_commute RS trans) 1); 

296 
by (rtac (zgcd_assoc RS trans) 1); 

297 
by (rtac (zgcd_commute RS arg_cong) 1); 

298 
qed "zgcd_left_commute"; 

299 

300 
(*Addition is an ACoperator*) 

301 
bind_thms ("zgcd_ac", [zgcd_assoc, zgcd_commute, zgcd_left_commute]); 

302 

303 
val gcd_mult_distrib2 = thm"gcd_mult_distrib2"; 

304 

305 
Goal "#0<=k ==> k * zgcd(m,n) = zgcd(k*m, k*n)"; 

306 
by (asm_simp_tac 

307 
(simpset() delsimps [zmult_zminus_right] 

308 
addsimps [zmult_zminus_right RS sym, 

309 
nat_mult_distrib, zgcd_def, zabs_def, 

310 
zmult_less_0_iff, gcd_mult_distrib2 RS sym, 

311 
zmult_int RS sym]) 1); 

312 
qed "zgcd_zmult_distrib2"; 

313 

314 
Goal "zgcd(k*m, k*n) = abs k * zgcd(m,n)"; 

315 
by (simp_tac (simpset() addsimps [zabs_def, zgcd_zmult_distrib2]) 1); 

316 
qed "zgcd_zmult_distrib2_abs"; 

317 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

318 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

319 
Goal "#0<=m ==> zgcd(m,m) = m"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

320 
by (cut_inst_tac [("k","m"),("m","#1"),("n","#1")] zgcd_zmult_distrib2 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

321 
by (ALLGOALS Asm_full_simp_tac); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

322 
qed "zgcd_self"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

323 
Addsimps [zgcd_self]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

324 

9943  325 
Goal "#0<=k ==> zgcd(k, k*n) = k"; 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

326 
by (cut_inst_tac [("k","k"),("m","#1"),("n","n")] zgcd_zmult_distrib2 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

327 
by (ALLGOALS Asm_full_simp_tac); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

328 
qed "zgcd_zmult_eq_self"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

329 
Addsimps [zgcd_zmult_eq_self]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

330 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

331 
Goal "#0<=k ==> zgcd(k*n, k) = k"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

332 
by (cut_inst_tac [("k","k"),("m","n"),("n","#1")] zgcd_zmult_distrib2 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

333 
by (ALLGOALS Asm_full_simp_tac); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

334 
qed "zgcd_zmult_eq_self2"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

335 
Addsimps [zgcd_zmult_eq_self2]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

336 

9943  337 
Goal "[ zgcd(n,k)=#1; k dvd (m*n); #0 <= m ] ==> k dvd m"; 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

338 
by (subgoal_tac "m = zgcd(m*n, m*k)" 1); 
9943  339 
by (etac ssubst 1 THEN rtac (zgcd_greatest_iff RS iffD2) 1); 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

340 
by (ALLGOALS (asm_simp_tac (simpset() 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

341 
addsimps [zgcd_zmult_distrib2 RS sym,int_0_le_mult_iff]))); 
9943  342 
val lemma = result(); 
343 

344 
Goal "[ zgcd(n,k)=#1; k dvd (m*n) ] ==> k dvd m"; 

345 
by (case_tac "#0 <= m" 1); 

346 
by (blast_tac (claset() addIs [lemma]) 1); 

347 
by (subgoal_tac "k dvd m" 1); 

348 
by (rtac lemma 2); 

349 
by Auto_tac; 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

350 
qed "zrelprime_zdvd_zmult"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

351 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

352 
Goalw [zprime_def] "[ p:zprime; ~p dvd n ] ==> zgcd(n,p) = #1"; 
9943  353 
by Auto_tac; 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

354 
qed "zprime_imp_zrelprime"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

355 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

356 
Goal "[ p:zprime; #0<n; n<p ] ==> zgcd(n,p) = #1"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

357 
by (etac zprime_imp_zrelprime 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

358 
by (etac zdvd_not_zless 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

359 
by (assume_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

360 
qed "zless_zprime_imp_zrelprime"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

361 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

362 
Goal "[ #0<=(m::int); p:zprime; p dvd (m*n) ] ==> p dvd m  p dvd n"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

363 
by Safe_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

364 
by (rtac zrelprime_zdvd_zmult 1); 
9943  365 
by (rtac zprime_imp_zrelprime 1); 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

366 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

367 
qed "zprime_zdvd_zmult"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

368 

9943  369 
val gcd_add_mult = thm "gcd_add_mult"; 
370 

371 
Goal "zgcd(m + n*k, n) = zgcd(m,n)"; 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

372 
by (rtac (zgcd_eq RS trans) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

373 
by (simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
9943  374 
by (rtac (zgcd_eq RS sym) 1); 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

375 
qed "zgcd_zadd_zmult"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

376 
Addsimps [zgcd_zadd_zmult]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

377 

9943  378 

379 
Goal "zgcd(m,n) dvd zgcd(k*m,n)"; 

380 
by (simp_tac (simpset() addsimps [zgcd_greatest_iff]) 1); 

381 
by (blast_tac (claset() addIs [zdvd_trans]) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

382 
qed "zgcd_zdvd_zgcd_zmult"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

383 

9943  384 
Goal "zgcd(k,n) = #1 ==> zgcd(k*m,n) dvd zgcd(m,n)"; 
385 
by (simp_tac (simpset() addsimps [zgcd_greatest_iff]) 1); 

386 
by (res_inst_tac [("n","k")] zrelprime_zdvd_zmult 1); 

387 
by (simp_tac (simpset() addsimps [zmult_commute]) 2); 

388 
by (subgoal_tac "zgcd (k, zgcd (k * m, n)) = zgcd (k * m, zgcd (k, n))" 1); 

389 
by (Asm_full_simp_tac 1); 

390 
by (simp_tac (simpset() addsimps zgcd_ac) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

391 
qed "zgcd_zmult_zdvd_zgcd"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

392 

9943  393 
val gcd_mult_cancel = thm "gcd_mult_cancel"; 
394 

395 
Goal "zgcd(k,n) = #1 ==> zgcd(k*m, n) = zgcd(m,n)"; 

396 
by (asm_full_simp_tac (simpset() addsimps [zgcd_def, 

397 
nat_abs_mult_distrib, gcd_mult_cancel]) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

398 
qed "zgcd_zmult_cancel"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

399 

9943  400 
Goal "[ zgcd(k,m) = #1; zgcd(n,m) = #1 ] ==> zgcd(k*n,m) = #1"; 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

401 
by (asm_simp_tac (simpset() addsimps [zgcd_zmult_cancel]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

402 
qed "zgcd_zgcd_zmult"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

403 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

404 
Goal "#0<m ==> (m dvd n) = (zgcd(n,m) = m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

405 
by Safe_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

406 
by (res_inst_tac [("n","zgcd(n,m)")] zdvd_trans 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

407 
by (rtac zgcd_zdvd1 3); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

408 
by (ALLGOALS Asm_simp_tac); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

409 
by (rewtac dvd_def); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

410 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

411 
qed "zdvd_iff_zgcd"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

412 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

413 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

414 
(************************************************) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

415 
(** Congruences **) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

416 
(************************************************) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

417 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

418 
Goalw [zcong_def] "[a=b](mod #1)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

419 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

420 
qed "zcong_1"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

421 
Addsimps [zcong_1]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

422 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

423 
Goalw [zcong_def] "[k = k] (mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

424 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

425 
qed "zcong_refl"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

426 
Addsimps [zcong_refl]; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

427 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

428 
Goalw [zcong_def,dvd_def] "[a = b](mod m) = [b = a](mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

429 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

430 
by (ALLGOALS (res_inst_tac [("x","k")] exI)); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

431 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

432 
qed "zcong_sym"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

433 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

434 
Goalw [zcong_def] 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

435 
"[ [a = b] (mod m); [c = d] (mod m) ] ==> [a+c = b+d](mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

436 
by (res_inst_tac [("s","(ab)+(cd)")] subst 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

437 
by (rtac zdvd_zadd 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

438 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

439 
qed "zcong_zadd"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

440 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

441 
Goalw [zcong_def] 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

442 
"[ [a = b] (mod m); [c = d] (mod m) ] ==> [ac = bd](mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

443 
by (res_inst_tac [("s","(ab)(cd)")] subst 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

444 
by (rtac zdvd_zdiff 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

445 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

446 
qed "zcong_zdiff"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

447 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

448 
Goalw [zcong_def,dvd_def] 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

449 
"[ [a = b](mod m); [b = c](mod m) ] ==> [a = c](mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

450 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

451 
by (res_inst_tac [("x","k+ka")] exI 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

452 
by (asm_full_simp_tac (simpset() addsimps zadd_ac@[zadd_zmult_distrib2]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

453 
qed "zcong_trans"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

454 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

455 
Goal "[ [a = b] (mod m); [c = d] (mod m) ] ==> [a*c = b*d](mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

456 
by (res_inst_tac [("b","b*c")] zcong_trans 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

457 
by (rewtac zcong_def); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

458 
by (res_inst_tac [("s","c*(ab)")] subst 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

459 
by (res_inst_tac [("s","b*(cd)")] subst 3); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

460 
by (blast_tac (claset() addIs [zdvd_zmult]) 4); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

461 
by (blast_tac (claset() addIs [zdvd_zmult]) 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

462 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2, 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

463 
zmult_commute]))); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

464 
qed "zcong_zmult"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

465 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

466 
Goal "[a = b] (mod m) ==> [a*k = b*k](mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

467 
by (rtac zcong_zmult 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

468 
by (ALLGOALS Asm_simp_tac); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

469 
qed "zcong_scalar"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

470 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

471 
Goal "[a = b] (mod m) ==> [k*a = k*b](mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

472 
by (rtac zcong_zmult 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

473 
by (ALLGOALS Asm_simp_tac); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

474 
qed "zcong_scalar2"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

475 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

476 
Goalw [zcong_def] "[a*m = b*m](mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

477 
by (rtac zdvd_zdiff 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

478 
by (ALLGOALS Simp_tac); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

479 
qed "zcong_zmult_self"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

480 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

481 
Goalw [zcong_def] 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

482 
"[ p:zprime; #0<a; [a*a = #1](mod p) ] \ 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

483 
\ ==> [a=#1](mod p)  [a = p#1](mod p)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

484 
by (rtac zprime_zdvd_zmult 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

485 
by (res_inst_tac [("s","a*a  #1 + p*(#1a)")] subst 3); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

486 
by (simp_tac (simpset() addsimps [zdvd_reduce]) 4); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

487 
by (ALLGOALS (asm_simp_tac (simpset() 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

488 
addsimps [zdiff_zmult_distrib,zmult_commute,zdiff_zmult_distrib2]))); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

489 
qed "zcong_square"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

490 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

491 
Goal "[ #0<=m; zgcd(k,m) = #1 ] ==> [a*k = b*k](mod m) = [a = b](mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

492 
by Safe_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

493 
by (blast_tac (claset() addIs [zcong_scalar]) 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

494 
by (case_tac "b<a" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

495 
by (stac zcong_sym 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

496 
by (rewrite_goals_tac [zcong_def]); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

497 
by (ALLGOALS (rtac zrelprime_zdvd_zmult)); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

498 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib]))); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

499 
by (subgoal_tac "m dvd ((a*k  b*k))" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

500 
by (asm_full_simp_tac (simpset() addsimps [zminus_zdiff_eq]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

501 
by (stac zdvd_zminus_iff 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

502 
by (assume_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

503 
qed "zcong_cancel"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

504 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

505 
Goal "[ #0<=m; zgcd(k,m) = #1 ] ==> [k*a = k*b](mod m) = [a = b](mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

506 
by (asm_simp_tac (simpset() addsimps [zmult_commute,zcong_cancel]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

507 
qed "zcong_cancel2"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

508 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

509 
Goalw [zcong_def,dvd_def] 
9943  510 
"[ [a = b] (mod m); [a = b] (mod n); zgcd(m,n) = #1 ] \ 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

511 
\ ==> [a=b](mod m*n)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

512 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

513 
by (subgoal_tac "m dvd (n*ka)" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

514 
by (subgoal_tac "m dvd ka" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

515 
by (case_tac "#0<=ka" 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

516 
by (stac (zdvd_zminus_iff RS sym) 3); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

517 
by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2); 
9943  518 
by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 2); 
519 
by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 2); 

520 
by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2); 

521 
by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 2); 

522 
by (asm_full_simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 2); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

523 
by (rewtac dvd_def); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

524 
by Safe_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

525 
by (res_inst_tac [("x","kc")] exI 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

526 
by (res_inst_tac [("x","k")] exI 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

527 
by (simp_tac (simpset() addsimps zmult_ac) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

528 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

529 
qed "zcong_zgcd_zmult_zmod"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

530 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

531 
Goalw [zcong_def,dvd_def] 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

532 
"[ #0<=a; a<m; #0<=b; b<m; [a = b] (mod m) ] ==> a = b"; 
9634
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

533 
by Auto_tac; 
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

534 
by (dres_inst_tac [("f", "%z. z mod m")] arg_cong 1); 
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

535 
by (cut_inst_tac [("z","a"),("w","b")] zless_linear 1); 
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

536 
by Auto_tac; 
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

537 
by (subgoal_tac "(a  b) mod m = ab" 2); 
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

538 
by (rtac mod_pos_pos_trivial 3); 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

539 
by Auto_tac; 
9634
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

540 
by (subgoal_tac "(m + (a  b)) mod m = m + (a  b)" 1); 
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

541 
by (rtac mod_pos_pos_trivial 2); 
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

542 
by Auto_tac; 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

543 
qed "zcong_zless_imp_eq"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

544 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

545 
Goal "[ p:zprime; #0<a; a<p; [a*a = #1](mod p) ] ==> a = #1  a = p#1"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

546 
by (cut_inst_tac [("p","p"),("a","a")] zcong_square 1); 
10198  547 
by (full_simp_tac (simpset() addsimps [zprime_def]) 1); 
548 
by (auto_tac (claset() addIs [zcong_zless_imp_eq], simpset())); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

549 
qed "zcong_square_zless"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

550 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

551 
Goalw [zcong_def] "[ #0<a; a<m; #0<b; b<a ] ==> ~[a = b] (mod m) "; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

552 
by (rtac zdvd_not_zless 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

553 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

554 
qed "zcong_not"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

555 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

556 
Goalw [zcong_def,dvd_def] "[ #0<=a; a<m; [a=#0](mod m) ] ==> a = #0"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

557 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

558 
by (subgoal_tac "#0<m" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

559 
by (rotate_tac ~1 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

560 
by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

561 
by (subgoal_tac "m*k<m*#1" 1); 
9634
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset

562 
by (dtac (zmult_zless_cancel1 RS iffD1) 1); 
9969  563 
by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff])); 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

564 
qed "zcong_zless_0"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

565 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

566 
Goal "#0<m ==> (EX! b. #0<=b & b<m & [a = b] (mod m))"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

567 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

568 
by (subgoal_tac "[b = y] (mod m)" 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

569 
by (case_tac "b=#0" 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

570 
by (case_tac "y=#0" 3); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

571 
by (auto_tac (claset() addIs [zcong_trans,zcong_zless_0, 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

572 
zcong_zless_imp_eq,zle_neq_implies_zless], 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

573 
simpset() addsimps [zcong_sym])); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

574 
by (rewrite_goals_tac [zcong_def,dvd_def]); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

575 
by (res_inst_tac [("x","a mod m")] exI 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

576 
by (auto_tac (claset(),simpset() addsimps [pos_mod_sign,pos_mod_bound])); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

577 
by (res_inst_tac [("x","(a div m)")] exI 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

578 
by (cut_inst_tac [("a","a"),("b","m")] zmod_zdiv_equality 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

579 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

580 
qed "zcong_zless_unique"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

581 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

582 
Goalw [zcong_def,dvd_def] "([a = b] (mod m)) = (EX k. b = a + m*k)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

583 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

584 
by (ALLGOALS (res_inst_tac [("x","k")] exI)); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

585 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

586 
qed "zcong_iff_lin"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

587 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

588 
Goal "[ #0<m; zgcd(a,m) = #1; [a = b] (mod m) ] ==> zgcd(b,m) = #1"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

589 
by (auto_tac (claset(),simpset() addsimps [zcong_iff_lin])); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

590 
qed "zgcd_zcong_zgcd"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

591 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

592 
Goal "[ a=c; b=d ] ==> ab = c(d::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

593 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

594 
val lemma = result(); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

595 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

596 
Goal "a  b = (m::int) * (a div m  b div m) + (a mod m  b mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

597 
by (res_inst_tac [("s","(m * (a div m) + a mod m)  \ 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

598 
\ (m * (b div m) + b mod m)")] trans 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

599 
by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

600 
by (rtac lemma 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

601 
by (ALLGOALS (rtac zmod_zdiv_equality)); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

602 
val lemma = result(); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

603 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

604 
Goalw [zcong_def] "[a = b] (mod m) = [a mod m = b mod m](mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

605 
by (res_inst_tac [("t","ab")] ssubst 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

606 
by (res_inst_tac [("m","m")] lemma 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

607 
by (rtac trans 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

608 
by (res_inst_tac [("k","m"),("m","a div m  b div m")] zdvd_reduce 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

609 
by (simp_tac (simpset() addsimps [zadd_commute]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

610 
qed "zcong_zmod"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

611 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

612 
Goal "#0<m ==> [a = b] (mod m) = (a mod m = b mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

613 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

614 
by (res_inst_tac [("m","m")] zcong_zless_imp_eq 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

615 
by (stac (zcong_zmod RS sym) 5); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

616 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_bound,pos_mod_sign]))); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

617 
by (rewrite_goals_tac [zcong_def,dvd_def]); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

618 
by (res_inst_tac [("x","a div m  b div m")] exI 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

619 
by (res_inst_tac [("m1","m")] (lemma RS trans) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

620 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

621 
qed "zcong_zmod_eq"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

622 

9943  623 
Goal "[a = b] (mod m) = [a = b] (mod m)"; 
624 
by (auto_tac (claset(), simpset() addsimps [zcong_def])); 

625 
qed "zcong_zminus"; 

626 
AddIffs [zcong_zminus]; 

627 

628 
Goal "[a = b] (mod #0) = (a = b)"; 

629 
by (auto_tac (claset(), simpset() addsimps [zcong_def])); 

630 
qed "zcong_zero"; 

631 
AddIffs [zcong_zero]; 

632 

633 
Goal "[a = b] (mod m) = (a mod m = b mod m)"; 

634 
by (zdiv_undefined_case_tac "m = #0" 1); 

635 
by (case_tac "#0<m" 1); 

636 
by (asm_simp_tac (simpset() addsimps [zcong_zmod_eq]) 1); 

637 
by (res_inst_tac [("t","m")] (zminus_zminus RS subst) 1); 

638 
by (stac zcong_zminus 1); 

639 
by (stac zcong_zmod_eq 1); 

640 
by (arith_tac 1); 

641 
(*FIXME: finish this proof?*) 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

642 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

643 
(************************************************) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

644 
(** Modulo **) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

645 
(************************************************) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

646 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

647 
Goalw [dvd_def] "[ #0<(m::int); m dvd b ] ==> (a mod b mod m) = (a mod m)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

648 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

649 
by (stac (zcong_zmod_eq RS sym) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

650 
by (stac zcong_iff_lin 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

651 
by (res_inst_tac [("x","k*(a div (m*k))")] exI 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

652 
by (stac zadd_commute 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

653 
by (stac (zmult_assoc RS sym) 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

654 
by (rtac zmod_zdiv_equality 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

655 
by (assume_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

656 
qed "zmod_zdvd_zmod"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

657 

9943  658 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

659 
(************************************************) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

660 
(** Extended GCD **) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

661 
(************************************************) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

662 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

663 
val [xzgcda_eq] = xzgcda.simps; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

664 
Delsimps xzgcda.simps; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

665 

10142  666 
Goal "zgcd(r',r) = k > #0 < r > \ 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

667 
\ (EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn))"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

668 
by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"), 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

669 
("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

670 
xzgcda.induct 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

671 
by (stac zgcd_eq 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

672 
by (stac xzgcda_eq 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

673 
by Auto_tac; 
9943  674 
by (case_tac "r' mod r = #0" 1); 
675 
by (forw_inst_tac [("a","r'")] pos_mod_sign 2); 

676 
by Auto_tac; 

677 
by (arith_tac 2); 

678 
by (rtac exI 1); 

679 
by (rtac exI 1); 

680 
by (stac xzgcda_eq 1); 

681 
by Auto_tac; 

682 
by (asm_full_simp_tac (simpset() addsimps [zabs_def]) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

683 
val lemma1 = result(); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

684 

10142  685 
Goal "(EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn)) > #0 < r > \ 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

686 
\ zgcd(r',r) = k"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

687 
by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"), 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

688 
("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

689 
xzgcda.induct 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

690 
by (stac zgcd_eq 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

691 
by (stac xzgcda_eq 1); 
9943  692 
by (auto_tac (claset(), simpset() addsimps [linorder_not_le])); 
693 
by (case_tac "r' mod r = #0" 1); 

694 
by (forw_inst_tac [("a","r'")] pos_mod_sign 2); 

695 
by Auto_tac; 

696 
by (arith_tac 2); 

697 
by (eres_inst_tac [("P","xzgcda ?u = ?v")] rev_mp 1); 

698 
by (stac xzgcda_eq 1); 

699 
by Auto_tac; 

700 
by (asm_full_simp_tac (simpset() addsimps [zabs_def]) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

701 
val lemma2 = result(); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

702 

10142  703 
Goalw [xzgcd_def] "#0 < n ==> (zgcd(m,n) = k) = (EX s t. xzgcd m n = (k,s,t))"; 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

704 
by (rtac iffI 1); 
9943  705 
by (rtac (lemma2 RS mp RS mp) 2); 
706 
by (rtac (lemma1 RS mp RS mp) 1); 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

707 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

708 
qed "xzgcd_correct"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

709 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

710 
(* xzgcd linear *) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

711 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

712 
Goal "(ar*b)*m + (cr*d)*(n::int) = (a*m + c*n)  r*(b*m + d*n)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

713 
by (simp_tac (simpset() addsimps [zdiff_zmult_distrib,zadd_zmult_distrib2, 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

714 
zmult_assoc]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

715 
val lemma = result(); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

716 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

717 
Goal "[ r' = s'*m + t'*n; r = s*m + t*n ] \ 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

718 
\ ==> (r' mod r) = (s'  (r' div r)*s)*m + (t'  (r' div r)*t)*(n::int)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

719 
by (rtac trans 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

720 
by (rtac (lemma RS sym) 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

721 
by (Asm_simp_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

722 
by (stac eq_zdiff_eq 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

723 
by (rtac (trans RS sym) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

724 
by (res_inst_tac [("b","s*m + t*n")] zmod_zdiv_equality 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

725 
by (simp_tac (simpset() addsimps [zmult_commute]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

726 
val lemma = result(); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

727 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

728 
Goal "#0<r > xzgcda(m,n,r',r,s',s,t',t) = (rn,sn,tn) \ 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

729 
\ > r' = s'*m + t'*n > r = s*m + t*n > rn = sn*m + tn*n"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

730 
by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"), 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

731 
("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

732 
xzgcda.induct 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

733 
by (stac xzgcda_eq 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

734 
by (Simp_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

735 
by (REPEAT (rtac impI 1)); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

736 
by (case_tac "r' mod r = #0" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

737 
by (asm_full_simp_tac (simpset() addsimps [xzgcda_eq]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

738 
by (SELECT_GOAL Safe_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

739 
by (subgoal_tac "#0 < r' mod r" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

740 
by (rtac zle_neq_implies_zless 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

741 
by (rtac pos_mod_sign 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

742 
by (cut_inst_tac [("m","m"),("n","n"),("r'","r'"),("r","r"), 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

743 
("s'","s'"),("s","s"),("t'","t'"),("t","t")] 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

744 
lemma 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

745 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

746 
qed_spec_mp "xzgcda_linear"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

747 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

748 
Goalw [xzgcd_def] "[ #0<n; xzgcd m n = (r,s,t) ] ==> r = s*m + t*n"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

749 
by (etac xzgcda_linear 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

750 
by (assume_tac 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

751 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

752 
qed "xzgcd_linear"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

753 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

754 
Goal "[ #0<n; zgcd(m,n) = k ] ==> (EX s t. k = s*m + t*n)"; 
9943  755 
by (asm_full_simp_tac (simpset() addsimps [xzgcd_correct]) 1); 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

756 
by Safe_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

757 
by (REPEAT (rtac exI 1)); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

758 
by (etac xzgcd_linear 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

759 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

760 
qed "zgcd_ex_linear"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

761 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

762 
Goal "[ #0<n; zgcd(a,n) = #1 ] ==> EX x. [a*x = #1](mod n)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

763 
by (cut_inst_tac [("m","a"),("n","n"),("k","#1")] zgcd_ex_linear 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

764 
by Safe_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

765 
by (res_inst_tac [("x","s")] exI 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

766 
by (res_inst_tac [("b","s*a+t*n")] zcong_trans 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

767 
by (Asm_simp_tac 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

768 
by (rewtac zcong_def); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

769 
by (simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

770 
qed "zcong_lineq_ex"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

771 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

772 
Goal "[ #0<n; zgcd(a,n) = #1 ] ==> EX! x. #0<=x & x<n & [a*x = b](mod n)"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

773 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

774 
by (rtac zcong_zless_imp_eq 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

775 
by (stac (zcong_cancel2 RS sym) 6); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

776 
by (rtac zcong_trans 8); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

777 
by (ALLGOALS Asm_simp_tac); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

778 
by (asm_full_simp_tac (simpset() addsimps [zcong_sym]) 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

779 
by (cut_inst_tac [("a","a"),("n","n")] zcong_lineq_ex 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

780 
by Auto_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

781 
by (res_inst_tac [("x","x*b mod n")] exI 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

782 
by Safe_tac; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

783 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_bound,pos_mod_sign]))); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

784 
by (stac zcong_zmod 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

785 
by (stac (zmod_zmult1_eq RS sym) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

786 
by (stac (zcong_zmod RS sym) 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

787 
by (subgoal_tac "[a*x*b = #1*b](mod n)" 1); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

788 
by (rtac zcong_zmult 2); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

789 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_assoc]))); 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

790 
qed "zcong_lineq_unique"; 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

791 