author  nipkow 
Tue, 07 Jul 2009 17:39:51 +0200  
changeset 31952  40501bb2d57c 
parent 31792  d5a6096b94ad 
permissions  rwrr 
31719  1 
(* Title: HOL/Library/Cong.thy 
2 
ID: 

3 
Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, 

4 
Thomas M. Rasmussen, Jeremy Avigad 

5 

6 

7 
Defines congruence (notation: [x = y] (mod z)) for natural numbers and 

8 
integers. 

9 

10 
This file combines and revises a number of prior developments. 

11 

12 
The original theories "GCD" and "Primes" were by Christophe Tabacznyj 

13 
and Lawrence C. Paulson, based on \cite{davenport92}. They introduced 

14 
gcd, lcm, and prime for the natural numbers. 

15 

16 
The original theory "IntPrimes" was by Thomas M. Rasmussen, and 

17 
extended gcd, lcm, primes to the integers. Amine Chaieb provided 

18 
another extension of the notions to the integers, and added a number 

19 
of results to "Primes" and "GCD". 

20 

21 
The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and 

22 
developed the congruence relations on the integers. The notion was 

23 
extended to the natural numbers by Chiaeb. Jeremy Avigad combined 

24 
these, revised and tidied them, made the development uniform for the 

25 
natural numbers and the integers, and added a number of new theorems. 

26 

27 
*) 

28 

29 

30 
header {* Congruence *} 

31 

32 
theory Cong 

33 
imports GCD 

34 
begin 

35 

36 
subsection {* Turn off One_nat_def *} 

37 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

38 
lemma induct'_nat [case_names zero plus1, induct type: nat]: 
31719  39 
"\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n" 
40 
by (erule nat_induct) (simp add:One_nat_def) 

41 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

42 
lemma cases_nat [case_names zero plus1, cases type: nat]: 
31719  43 
"P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

44 
by(metis induct'_nat) 
31719  45 

46 
lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n" 

47 
by (simp add: One_nat_def) 

48 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

49 
lemma power_eq_one_eq_nat [simp]: 
31719  50 
"((x::nat)^m = 1) = (m = 0  x = 1)" 
51 
by (induct m, auto) 

52 

53 
lemma card_insert_if' [simp]: "finite A \<Longrightarrow> 

54 
card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)" 

55 
by (auto simp add: insert_absorb) 

56 

57 
(* why wasn't card_insert_if a simp rule? *) 

58 
declare card_insert_disjoint [simp del] 

59 

60 
lemma nat_1' [simp]: "nat 1 = 1" 

61 
by simp 

62 

31792  63 
(* For those annoying moments where Suc reappears, use Suc_eq_plus1 *) 
31719  64 

65 
declare nat_1 [simp del] 

66 
declare add_2_eq_Suc [simp del] 

67 
declare add_2_eq_Suc' [simp del] 

68 

69 

70 
declare mod_pos_pos_trivial [simp] 

71 

72 

73 
subsection {* Main definitions *} 

74 

75 
class cong = 

76 

77 
fixes 

78 
cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))") 

79 

80 
begin 

81 

82 
abbreviation 

83 
notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))") 

84 
where 

85 
"notcong x y m == (~cong x y m)" 

86 

87 
end 

88 

89 
(* definitions for the natural numbers *) 

90 

91 
instantiation nat :: cong 

92 

93 
begin 

94 

95 
definition 

96 
cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" 

97 
where 

98 
"cong_nat x y m = ((x mod m) = (y mod m))" 

99 

100 
instance proof qed 

101 

102 
end 

103 

104 

105 
(* definitions for the integers *) 

106 

107 
instantiation int :: cong 

108 

109 
begin 

110 

111 
definition 

112 
cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" 

113 
where 

114 
"cong_int x y m = ((x mod m) = (y mod m))" 

115 

116 
instance proof qed 

117 

118 
end 

119 

120 

121 
subsection {* Set up Transfer *} 

122 

123 

124 
lemma transfer_nat_int_cong: 

125 
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow> 

126 
([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))" 

127 
unfolding cong_int_def cong_nat_def 

128 
apply (auto simp add: nat_mod_distrib [symmetric]) 

129 
apply (subst (asm) eq_nat_nat_iff) 

130 
apply (case_tac "m = 0", force, rule pos_mod_sign, force)+ 

131 
apply assumption 

132 
done 

133 

134 
declare TransferMorphism_nat_int[transfer add return: 

135 
transfer_nat_int_cong] 

136 

137 
lemma transfer_int_nat_cong: 

138 
"[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)" 

139 
apply (auto simp add: cong_int_def cong_nat_def) 

140 
apply (auto simp add: zmod_int [symmetric]) 

141 
done 

142 

143 
declare TransferMorphism_int_nat[transfer add return: 

144 
transfer_int_nat_cong] 

145 

146 

147 
subsection {* Congruence *} 

148 

149 
(* was zcong_0, etc. *) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

150 
lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)" 
31719  151 
by (unfold cong_nat_def, auto) 
152 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

153 
lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)" 
31719  154 
by (unfold cong_int_def, auto) 
155 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

156 
lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)" 
31719  157 
by (unfold cong_nat_def, auto) 
158 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

159 
lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)" 
31719  160 
by (unfold cong_nat_def, auto simp add: One_nat_def) 
161 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

162 
lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)" 
31719  163 
by (unfold cong_int_def, auto) 
164 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

165 
lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)" 
31719  166 
by (unfold cong_nat_def, auto) 
167 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

168 
lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)" 
31719  169 
by (unfold cong_int_def, auto) 
170 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

171 
lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)" 
31719  172 
by (unfold cong_nat_def, auto) 
173 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

174 
lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)" 
31719  175 
by (unfold cong_int_def, auto) 
176 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

177 
lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)" 
31719  178 
by (unfold cong_nat_def, auto) 
179 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

180 
lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)" 
31719  181 
by (unfold cong_int_def, auto) 
182 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

183 
lemma cong_trans_nat [trans]: 
31719  184 
"[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)" 
185 
by (unfold cong_nat_def, auto) 

186 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

187 
lemma cong_trans_int [trans]: 
31719  188 
"[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)" 
189 
by (unfold cong_int_def, auto) 

190 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

191 
lemma cong_add_nat: 
31719  192 
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)" 
193 
apply (unfold cong_nat_def) 

194 
apply (subst (1 2) mod_add_eq) 

195 
apply simp 

196 
done 

197 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

198 
lemma cong_add_int: 
31719  199 
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)" 
200 
apply (unfold cong_int_def) 

201 
apply (subst (1 2) mod_add_left_eq) 

202 
apply (subst (1 2) mod_add_right_eq) 

203 
apply simp 

204 
done 

205 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

206 
lemma cong_diff_int: 
31719  207 
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a  c = b  d] (mod m)" 
208 
apply (unfold cong_int_def) 

209 
apply (subst (1 2) mod_diff_eq) 

210 
apply simp 

211 
done 

212 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

213 
lemma cong_diff_aux_int: 
31719  214 
"(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow> 
215 
[c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)" 

216 
apply (subst (1 2) tsub_eq) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

217 
apply (auto intro: cong_diff_int) 
31719  218 
done; 
219 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

220 
lemma cong_diff_nat: 
31719  221 
assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and 
222 
"[c = d] (mod m)" 

223 
shows "[a  c = b  d] (mod m)" 

224 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

225 
using prems by (rule cong_diff_aux_int [transferred]); 
31719  226 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

227 
lemma cong_mult_nat: 
31719  228 
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)" 
229 
apply (unfold cong_nat_def) 

230 
apply (subst (1 2) mod_mult_eq) 

231 
apply simp 

232 
done 

233 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

234 
lemma cong_mult_int: 
31719  235 
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)" 
236 
apply (unfold cong_int_def) 

237 
apply (subst (1 2) zmod_zmult1_eq) 

238 
apply (subst (1 2) mult_commute) 

239 
apply (subst (1 2) zmod_zmult1_eq) 

240 
apply simp 

241 
done 

242 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

243 
lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)" 
31719  244 
apply (induct k) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

245 
apply (auto simp add: cong_refl_nat cong_mult_nat) 
31719  246 
done 
247 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

248 
lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)" 
31719  249 
apply (induct k) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

250 
apply (auto simp add: cong_refl_int cong_mult_int) 
31719  251 
done 
252 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

253 
lemma cong_setsum_nat [rule_format]: 
31719  254 
"(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
255 
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)" 

256 
apply (case_tac "finite A") 

257 
apply (induct set: finite) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

258 
apply (auto intro: cong_add_nat) 
31719  259 
done 
260 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

261 
lemma cong_setsum_int [rule_format]: 
31719  262 
"(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
263 
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)" 

264 
apply (case_tac "finite A") 

265 
apply (induct set: finite) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

266 
apply (auto intro: cong_add_int) 
31719  267 
done 
268 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

269 
lemma cong_setprod_nat [rule_format]: 
31719  270 
"(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
271 
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)" 

272 
apply (case_tac "finite A") 

273 
apply (induct set: finite) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

274 
apply (auto intro: cong_mult_nat) 
31719  275 
done 
276 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

277 
lemma cong_setprod_int [rule_format]: 
31719  278 
"(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
279 
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)" 

280 
apply (case_tac "finite A") 

281 
apply (induct set: finite) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

282 
apply (auto intro: cong_mult_int) 
31719  283 
done 
284 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

285 
lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

286 
by (rule cong_mult_nat, simp_all) 
31719  287 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

288 
lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

289 
by (rule cong_mult_int, simp_all) 
31719  290 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

291 
lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

292 
by (rule cong_mult_nat, simp_all) 
31719  293 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

294 
lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

295 
by (rule cong_mult_int, simp_all) 
31719  296 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

297 
lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)" 
31719  298 
by (unfold cong_nat_def, auto) 
299 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

300 
lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)" 
31719  301 
by (unfold cong_int_def, auto) 
302 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

303 
lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a  b = 0] (mod m)" 
31719  304 
apply (rule iffI) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

305 
apply (erule cong_diff_int [of a b m b b, simplified]) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

306 
apply (erule cong_add_int [of "a  b" 0 m b b, simplified]) 
31719  307 
done 
308 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

309 
lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow> 
31719  310 
[(a::int) = b] (mod m) = [tsub a b = 0] (mod m)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

311 
by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int) 
31719  312 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

313 
lemma cong_eq_diff_cong_0_nat: 
31719  314 
assumes "(a::nat) >= b" 
315 
shows "[a = b] (mod m) = [a  b = 0] (mod m)" 

316 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

317 
using prems by (rule cong_eq_diff_cong_0_aux_int [transferred]) 
31719  318 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

319 
lemma cong_diff_cong_0'_nat: 
31719  320 
"[(x::nat) = y] (mod n) \<longleftrightarrow> 
321 
(if x <= y then [y  x = 0] (mod n) else [x  y = 0] (mod n))" 

322 
apply (case_tac "y <= x") 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

323 
apply (frule cong_eq_diff_cong_0_nat [where m = n]) 
31719  324 
apply auto [1] 
325 
apply (subgoal_tac "x <= y") 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

326 
apply (frule cong_eq_diff_cong_0_nat [where m = n]) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

327 
apply (subst cong_sym_eq_nat) 
31719  328 
apply auto 
329 
done 

330 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

331 
lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a  b))" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

332 
apply (subst cong_eq_diff_cong_0_nat, assumption) 
31719  333 
apply (unfold cong_nat_def) 
334 
apply (simp add: dvd_eq_mod_eq_0 [symmetric]) 

335 
done 

336 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

337 
lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a  b))" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

338 
apply (subst cong_eq_diff_cong_0_int) 
31719  339 
apply (unfold cong_int_def) 
340 
apply (simp add: dvd_eq_mod_eq_0 [symmetric]) 

341 
done 

342 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

343 
lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

344 
by (simp add: cong_altdef_int) 
31719  345 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

346 
lemma cong_square_int: 
31719  347 
"\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk> 
348 
\<Longrightarrow> [a = 1] (mod p) \<or> [a =  1] (mod p)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

349 
apply (simp only: cong_altdef_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

350 
apply (subst prime_dvd_mult_eq_int [symmetric], assumption) 
31719  351 
(* any way around this? *) 
352 
apply (subgoal_tac "a * a  1 = (a  1) * (a  1)") 

353 
apply (auto simp add: ring_simps) 

354 
done 

355 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

356 
lemma cong_mult_rcancel_int: 
31719  357 
"coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

358 
apply (subst (1 2) cong_altdef_int) 
31719  359 
apply (subst left_diff_distrib [symmetric]) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

360 
apply (rule coprime_dvd_mult_iff_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

361 
apply (subst gcd_commute_int, assumption) 
31719  362 
done 
363 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

364 
lemma cong_mult_rcancel_nat: 
31719  365 
assumes "coprime k (m::nat)" 
366 
shows "[a * k = b * k] (mod m) = [a = b] (mod m)" 

367 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

368 
apply (rule cong_mult_rcancel_int [transferred]) 
31719  369 
using prems apply auto 
370 
done 

371 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

372 
lemma cong_mult_lcancel_nat: 
31719  373 
"coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

374 
by (simp add: mult_commute cong_mult_rcancel_nat) 
31719  375 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

376 
lemma cong_mult_lcancel_int: 
31719  377 
"coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

378 
by (simp add: mult_commute cong_mult_rcancel_int) 
31719  379 

380 
(* was zcong_zgcd_zmult_zmod *) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

381 
lemma coprime_cong_mult_int: 
31719  382 
"[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n 
383 
\<Longrightarrow> [a = b] (mod m * n)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

384 
apply (simp only: cong_altdef_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

385 
apply (erule (2) divides_mult_int) 
31719  386 
done 
387 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

388 
lemma coprime_cong_mult_nat: 
31719  389 
assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n" 
390 
shows "[a = b] (mod m * n)" 

391 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

392 
apply (rule coprime_cong_mult_int [transferred]) 
31719  393 
using prems apply auto 
394 
done 

395 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

396 
lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow> 
31719  397 
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" 
398 
by (auto simp add: cong_nat_def mod_pos_pos_trivial) 

399 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

400 
lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow> 
31719  401 
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" 
402 
by (auto simp add: cong_int_def mod_pos_pos_trivial) 

403 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

404 
lemma cong_less_unique_nat: 
31719  405 
"0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" 
406 
apply auto 

407 
apply (rule_tac x = "a mod m" in exI) 

408 
apply (unfold cong_nat_def, auto) 

409 
done 

410 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

411 
lemma cong_less_unique_int: 
31719  412 
"0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" 
413 
apply auto 

414 
apply (rule_tac x = "a mod m" in exI) 

415 
apply (unfold cong_int_def, auto simp add: mod_pos_pos_trivial) 

416 
done 

417 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

418 
lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

419 
apply (auto simp add: cong_altdef_int dvd_def ring_simps) 
31719  420 
apply (rule_tac [!] x = "k" in exI, auto) 
421 
done 

422 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

423 
lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) = 
31719  424 
(\<exists>k1 k2. b + k1 * m = a + k2 * m)" 
425 
apply (rule iffI) 

426 
apply (case_tac "b <= a") 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

427 
apply (subst (asm) cong_altdef_nat, assumption) 
31719  428 
apply (unfold dvd_def, auto) 
429 
apply (rule_tac x = k in exI) 

430 
apply (rule_tac x = 0 in exI) 

431 
apply (auto simp add: ring_simps) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

432 
apply (subst (asm) cong_sym_eq_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

433 
apply (subst (asm) cong_altdef_nat) 
31719  434 
apply force 
435 
apply (unfold dvd_def, auto) 

436 
apply (rule_tac x = 0 in exI) 

437 
apply (rule_tac x = k in exI) 

438 
apply (auto simp add: ring_simps) 

439 
apply (unfold cong_nat_def) 

440 
apply (subgoal_tac "a mod m = (a + k2 * m) mod m") 

441 
apply (erule ssubst)back 

442 
apply (erule subst) 

443 
apply auto 

444 
done 

445 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

446 
lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

447 
apply (subst (asm) cong_iff_lin_int, auto) 
31719  448 
apply (subst add_commute) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

449 
apply (subst (2) gcd_commute_int) 
31719  450 
apply (subst mult_commute) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

451 
apply (subst gcd_add_mult_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

452 
apply (rule gcd_commute_int) 
31719  453 
done 
454 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

455 
lemma cong_gcd_eq_nat: 
31719  456 
assumes "[(a::nat) = b] (mod m)" 
457 
shows "gcd a m = gcd b m" 

458 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

459 
apply (rule cong_gcd_eq_int [transferred]) 
31719  460 
using prems apply auto 
461 
done 

462 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

463 
lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
31719  464 
coprime b m" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

465 
by (auto simp add: cong_gcd_eq_nat) 
31719  466 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

467 
lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
31719  468 
coprime b m" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

469 
by (auto simp add: cong_gcd_eq_int) 
31719  470 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

471 
lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = 
31719  472 
[a mod m = b mod m] (mod m)" 
473 
by (auto simp add: cong_nat_def) 

474 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

475 
lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = 
31719  476 
[a mod m = b mod m] (mod m)" 
477 
by (auto simp add: cong_int_def) 

478 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

479 
lemma cong_minus_int [iff]: "[(a::int) = b] (mod m) = [a = b] (mod m)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

480 
by (subst (1 2) cong_altdef_int, auto) 
31719  481 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

482 
lemma cong_zero_nat [iff]: "[(a::nat) = b] (mod 0) = (a = b)" 
31719  483 
by (auto simp add: cong_nat_def) 
484 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

485 
lemma cong_zero_int [iff]: "[(a::int) = b] (mod 0) = (a = b)" 
31719  486 
by (auto simp add: cong_int_def) 
487 

488 
(* 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

489 
lemma mod_dvd_mod_int: 
31719  490 
"0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)" 
491 
apply (unfold dvd_def, auto) 

492 
apply (rule mod_mod_cancel) 

493 
apply auto 

494 
done 

495 

496 
lemma mod_dvd_mod: 

497 
assumes "0 < (m::nat)" and "m dvd b" 

498 
shows "(a mod b mod m) = (a mod m)" 

499 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

500 
apply (rule mod_dvd_mod_int [transferred]) 
31719  501 
using prems apply auto 
502 
done 

503 
*) 

504 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

505 
lemma cong_add_lcancel_nat: 
31719  506 
"[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

507 
by (simp add: cong_iff_lin_nat) 
31719  508 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

509 
lemma cong_add_lcancel_int: 
31719  510 
"[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

511 
by (simp add: cong_iff_lin_int) 
31719  512 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

513 
lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

514 
by (simp add: cong_iff_lin_nat) 
31719  515 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

516 
lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

517 
by (simp add: cong_iff_lin_int) 
31719  518 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

519 
lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

520 
by (simp add: cong_iff_lin_nat) 
31719  521 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

522 
lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

523 
by (simp add: cong_iff_lin_int) 
31719  524 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

525 
lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

526 
by (simp add: cong_iff_lin_nat) 
31719  527 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

528 
lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

529 
by (simp add: cong_iff_lin_int) 
31719  530 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

531 
lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
31719  532 
[x = y] (mod n)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

533 
apply (auto simp add: cong_iff_lin_nat dvd_def) 
31719  534 
apply (rule_tac x="k1 * k" in exI) 
535 
apply (rule_tac x="k2 * k" in exI) 

536 
apply (simp add: ring_simps) 

537 
done 

538 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

539 
lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
31719  540 
[x = y] (mod n)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

541 
by (auto simp add: cong_altdef_int dvd_def) 
31719  542 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

543 
lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y" 
31719  544 
by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0) 
545 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

546 
lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y" 
31719  547 
by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0) 
548 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

549 
lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
31719  550 
by (simp add: cong_nat_def) 
551 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

552 
lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
31719  553 
by (simp add: cong_int_def) 
554 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

555 
lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0 
31719  556 
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)" 
557 
by (simp add: cong_nat_def mod_mult2_eq mod_add_left_eq) 

558 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

559 
lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([a = b] (mod m))" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

560 
apply (simp add: cong_altdef_int) 
31719  561 
apply (subst dvd_minus_iff [symmetric]) 
562 
apply (simp add: ring_simps) 

563 
done 

564 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

565 
lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod m))" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

566 
by (auto simp add: cong_altdef_int) 
31719  567 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

568 
lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0 
31719  569 
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)" 
570 
apply (case_tac "b > 0") 

571 
apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

572 
apply (subst (1 2) cong_modulus_neg_int) 
31719  573 
apply (unfold cong_int_def) 
574 
apply (subgoal_tac "a * b = (a * b)") 

575 
apply (erule ssubst) 

576 
apply (subst zmod_zmult2_eq) 

577 
apply (auto simp add: mod_add_left_eq) 

578 
done 

579 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

580 
lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a  1))" 
31719  581 
apply (case_tac "a = 0") 
582 
apply force 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

583 
apply (subst (asm) cong_altdef_nat) 
31719  584 
apply auto 
585 
done 

586 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

587 
lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)" 
31719  588 
by (unfold cong_nat_def, auto) 
589 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

590 
lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1)  (n = 1))" 
31719  591 
by (unfold cong_int_def, auto simp add: zmult_eq_1_iff) 
592 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

593 
lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow> 
31719  594 
a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)" 
595 
apply (case_tac "n = 1") 

596 
apply auto [1] 

597 
apply (drule_tac x = "a  1" in spec) 

598 
apply force 

599 
apply (case_tac "a = 0") 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

600 
apply (auto simp add: cong_0_1_nat) [1] 
31719  601 
apply (rule iffI) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

602 
apply (drule cong_to_1_nat) 
31719  603 
apply (unfold dvd_def) 
604 
apply auto [1] 

605 
apply (rule_tac x = k in exI) 

606 
apply (auto simp add: ring_simps) [1] 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

607 
apply (subst cong_altdef_nat) 
31719  608 
apply (auto simp add: dvd_def) 
609 
done 

610 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

611 
lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

612 
apply (subst cong_altdef_nat) 
31719  613 
apply assumption 
614 
apply (unfold dvd_def, auto simp add: ring_simps) 

615 
apply (rule_tac x = k in exI) 

616 
apply auto 

617 
done 

618 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

619 
lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)" 
31719  620 
apply (case_tac "n = 0") 
621 
apply force 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

622 
apply (frule bezout_nat [of a n], auto) 
31719  623 
apply (rule exI, erule ssubst) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

624 
apply (rule cong_trans_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

625 
apply (rule cong_add_nat) 
31719  626 
apply (subst mult_commute) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

627 
apply (rule cong_mult_self_nat) 
31719  628 
prefer 2 
629 
apply simp 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

630 
apply (rule cong_refl_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

631 
apply (rule cong_refl_nat) 
31719  632 
done 
633 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

634 
lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)" 
31719  635 
apply (case_tac "n = 0") 
636 
apply (case_tac "a \<ge> 0") 

637 
apply auto 

638 
apply (rule_tac x = "1" in exI) 

639 
apply auto 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

640 
apply (insert bezout_int [of a n], auto) 
31719  641 
apply (rule exI) 
642 
apply (erule subst) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

643 
apply (rule cong_trans_int) 
31719  644 
prefer 2 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

645 
apply (rule cong_add_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

646 
apply (rule cong_refl_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

647 
apply (rule cong_sym_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

648 
apply (rule cong_mult_self_int) 
31719  649 
apply simp 
650 
apply (subst mult_commute) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

651 
apply (rule cong_refl_int) 
31719  652 
done 
653 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

654 
lemma cong_solve_dvd_nat: 
31719  655 
assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d" 
656 
shows "EX x. [a * x = d] (mod n)" 

657 
proof  

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

658 
from cong_solve_nat [OF a] obtain x where 
31719  659 
"[a * x = gcd a n](mod n)" 
660 
by auto 

661 
hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

662 
by (elim cong_scalar2_nat) 
31719  663 
also from b have "(d div gcd a n) * gcd a n = d" 
664 
by (rule dvd_div_mult_self) 

665 
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" 

666 
by auto 

667 
finally show ?thesis 

668 
by auto 

669 
qed 

670 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

671 
lemma cong_solve_dvd_int: 
31719  672 
assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d" 
673 
shows "EX x. [a * x = d] (mod n)" 

674 
proof  

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

675 
from cong_solve_int [OF a] obtain x where 
31719  676 
"[a * x = gcd a n](mod n)" 
677 
by auto 

678 
hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

679 
by (elim cong_scalar2_int) 
31719  680 
also from b have "(d div gcd a n) * gcd a n = d" 
681 
by (rule dvd_div_mult_self) 

682 
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" 

683 
by auto 

684 
finally show ?thesis 

685 
by auto 

686 
qed 

687 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

688 
lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> 
31719  689 
EX x. [a * x = 1] (mod n)" 
690 
apply (case_tac "a = 0") 

691 
apply force 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

692 
apply (frule cong_solve_nat [of a n]) 
31719  693 
apply auto 
694 
done 

695 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

696 
lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> 
31719  697 
EX x. [a * x = 1] (mod n)" 
698 
apply (case_tac "a = 0") 

699 
apply auto 

700 
apply (case_tac "n \<ge> 0") 

701 
apply auto 

702 
apply (subst cong_int_def, auto) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

703 
apply (frule cong_solve_int [of a n]) 
31719  704 
apply auto 
705 
done 

706 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

707 
lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = 
31719  708 
(EX x. [a * x = 1] (mod m))" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

709 
apply (auto intro: cong_solve_coprime_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

710 
apply (unfold cong_nat_def, auto intro: invertible_coprime_nat) 
31719  711 
done 
712 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

713 
lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = 
31719  714 
(EX x. [a * x = 1] (mod m))" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

715 
apply (auto intro: cong_solve_coprime_int) 
31719  716 
apply (unfold cong_int_def) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

717 
apply (auto intro: invertible_coprime_int) 
31719  718 
done 
719 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

720 
lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m = 
31719  721 
(EX x. 0 <= x & x < m & [a * x = 1] (mod m))" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

722 
apply (subst coprime_iff_invertible_int) 
31719  723 
apply auto 
724 
apply (auto simp add: cong_int_def) 

725 
apply (rule_tac x = "x mod m" in exI) 

726 
apply (auto simp add: mod_mult_right_eq [symmetric]) 

727 
done 

728 

729 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

730 
lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow> 
31719  731 
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" 
732 
apply (case_tac "y \<le> x") 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

733 
apply (auto simp add: cong_altdef_nat lcm_least_nat) [1] 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

734 
apply (rule cong_sym_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

735 
apply (subst (asm) (1 2) cong_sym_eq_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

736 
apply (auto simp add: cong_altdef_nat lcm_least_nat) 
31719  737 
done 
738 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

739 
lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow> 
31719  740 
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

741 
by (auto simp add: cong_altdef_int lcm_least_int) [1] 
31719  742 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

743 
lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow> 
31719  744 
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

745 
apply (frule (1) cong_cong_lcm_nat)back 
31719  746 
apply (simp add: lcm_nat_def) 
747 
done 

748 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

749 
lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow> 
31719  750 
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

751 
apply (frule (1) cong_cong_lcm_int)back 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

752 
apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric]) 
31719  753 
done 
754 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

755 
lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow> 
31719  756 
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> 
757 
(ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow> 

758 
[x = y] (mod (PROD i:A. m i))" 

759 
apply (induct set: finite) 

760 
apply auto 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

761 
apply (rule cong_cong_coprime_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

762 
apply (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

763 
apply (rule setprod_coprime_nat) 
31719  764 
apply auto 
765 
done 

766 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

767 
lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow> 
31719  768 
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> 
769 
(ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow> 

770 
[x = y] (mod (PROD i:A. m i))" 

771 
apply (induct set: finite) 

772 
apply auto 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

773 
apply (rule cong_cong_coprime_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

774 
apply (subst gcd_commute_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

775 
apply (rule setprod_coprime_int) 
31719  776 
apply auto 
777 
done 

778 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

779 
lemma binary_chinese_remainder_aux_nat: 
31719  780 
assumes a: "coprime (m1::nat) m2" 
781 
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> 

782 
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" 

783 
proof  

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

784 
from cong_solve_coprime_nat [OF a] 
31719  785 
obtain x1 where one: "[m1 * x1 = 1] (mod m2)" 
786 
by auto 

787 
from a have b: "coprime m2 m1" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

788 
by (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

789 
from cong_solve_coprime_nat [OF b] 
31719  790 
obtain x2 where two: "[m2 * x2 = 1] (mod m1)" 
791 
by auto 

792 
have "[m1 * x1 = 0] (mod m1)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

793 
by (subst mult_commute, rule cong_mult_self_nat) 
31719  794 
moreover have "[m2 * x2 = 0] (mod m2)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

795 
by (subst mult_commute, rule cong_mult_self_nat) 
31719  796 
moreover note one two 
797 
ultimately show ?thesis by blast 

798 
qed 

799 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

800 
lemma binary_chinese_remainder_aux_int: 
31719  801 
assumes a: "coprime (m1::int) m2" 
802 
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> 

803 
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" 

804 
proof  

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

805 
from cong_solve_coprime_int [OF a] 
31719  806 
obtain x1 where one: "[m1 * x1 = 1] (mod m2)" 
807 
by auto 

808 
from a have b: "coprime m2 m1" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

809 
by (subst gcd_commute_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

810 
from cong_solve_coprime_int [OF b] 
31719  811 
obtain x2 where two: "[m2 * x2 = 1] (mod m1)" 
812 
by auto 

813 
have "[m1 * x1 = 0] (mod m1)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

814 
by (subst mult_commute, rule cong_mult_self_int) 
31719  815 
moreover have "[m2 * x2 = 0] (mod m2)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

816 
by (subst mult_commute, rule cong_mult_self_int) 
31719  817 
moreover note one two 
818 
ultimately show ?thesis by blast 

819 
qed 

820 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

821 
lemma binary_chinese_remainder_nat: 
31719  822 
assumes a: "coprime (m1::nat) m2" 
823 
shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" 

824 
proof  

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

825 
from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2 
31719  826 
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and 
827 
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" 

828 
by blast 

829 
let ?x = "u1 * b1 + u2 * b2" 

830 
have "[?x = u1 * 1 + u2 * 0] (mod m1)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

831 
apply (rule cong_add_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

832 
apply (rule cong_scalar2_nat) 
31719  833 
apply (rule `[b1 = 1] (mod m1)`) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

834 
apply (rule cong_scalar2_nat) 
31719  835 
apply (rule `[b2 = 0] (mod m1)`) 
836 
done 

837 
hence "[?x = u1] (mod m1)" by simp 

838 
have "[?x = u1 * 0 + u2 * 1] (mod m2)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

839 
apply (rule cong_add_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

840 
apply (rule cong_scalar2_nat) 
31719  841 
apply (rule `[b1 = 0] (mod m2)`) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

842 
apply (rule cong_scalar2_nat) 
31719  843 
apply (rule `[b2 = 1] (mod m2)`) 
844 
done 

845 
hence "[?x = u2] (mod m2)" by simp 

846 
with `[?x = u1] (mod m1)` show ?thesis by blast 

847 
qed 

848 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

849 
lemma binary_chinese_remainder_int: 
31719  850 
assumes a: "coprime (m1::int) m2" 
851 
shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" 

852 
proof  

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

853 
from binary_chinese_remainder_aux_int [OF a] obtain b1 b2 
31719  854 
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and 
855 
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" 

856 
by blast 

857 
let ?x = "u1 * b1 + u2 * b2" 

858 
have "[?x = u1 * 1 + u2 * 0] (mod m1)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

859 
apply (rule cong_add_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

860 
apply (rule cong_scalar2_int) 
31719  861 
apply (rule `[b1 = 1] (mod m1)`) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

862 
apply (rule cong_scalar2_int) 
31719  863 
apply (rule `[b2 = 0] (mod m1)`) 
864 
done 

865 
hence "[?x = u1] (mod m1)" by simp 

866 
have "[?x = u1 * 0 + u2 * 1] (mod m2)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

867 
apply (rule cong_add_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

868 
apply (rule cong_scalar2_int) 
31719  869 
apply (rule `[b1 = 0] (mod m2)`) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

870 
apply (rule cong_scalar2_int) 
31719  871 
apply (rule `[b2 = 1] (mod m2)`) 
872 
done 

873 
hence "[?x = u2] (mod m2)" by simp 

874 
with `[?x = u1] (mod m1)` show ?thesis by blast 

875 
qed 

876 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

877 
lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow> 
31719  878 
[x = y] (mod m)" 
879 
apply (case_tac "y \<le> x") 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

880 
apply (simp add: cong_altdef_nat) 
31719  881 
apply (erule dvd_mult_left) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

882 
apply (rule cong_sym_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

883 
apply (subst (asm) cong_sym_eq_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

884 
apply (simp add: cong_altdef_nat) 
31719  885 
apply (erule dvd_mult_left) 
886 
done 

887 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

888 
lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow> 
31719  889 
[x = y] (mod m)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

890 
apply (simp add: cong_altdef_int) 
31719  891 
apply (erule dvd_mult_left) 
892 
done 

893 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

894 
lemma cong_less_modulus_unique_nat: 
31719  895 
"[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y" 
896 
by (simp add: cong_nat_def) 

897 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

898 
lemma binary_chinese_remainder_unique_nat: 
31719  899 
assumes a: "coprime (m1::nat) m2" and 
900 
nz: "m1 \<noteq> 0" "m2 \<noteq> 0" 

901 
shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)" 

902 
proof  

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

903 
from binary_chinese_remainder_nat [OF a] obtain y where 
31719  904 
"[y = u1] (mod m1)" and "[y = u2] (mod m2)" 
905 
by blast 

906 
let ?x = "y mod (m1 * m2)" 

907 
from nz have less: "?x < m1 * m2" 

908 
by auto 

909 
have one: "[?x = u1] (mod m1)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

910 
apply (rule cong_trans_nat) 
31719  911 
prefer 2 
912 
apply (rule `[y = u1] (mod m1)`) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

913 
apply (rule cong_modulus_mult_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

914 
apply (rule cong_mod_nat) 
31719  915 
using nz apply auto 
916 
done 

917 
have two: "[?x = u2] (mod m2)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

918 
apply (rule cong_trans_nat) 
31719  919 
prefer 2 
920 
apply (rule `[y = u2] (mod m2)`) 

921 
apply (subst mult_commute) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

922 
apply (rule cong_modulus_mult_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

923 
apply (rule cong_mod_nat) 
31719  924 
using nz apply auto 
925 
done 

926 
have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> 

927 
z = ?x" 

928 
proof (clarify) 

929 
fix z 

930 
assume "z < m1 * m2" 

931 
assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)" 

932 
have "[?x = z] (mod m1)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

933 
apply (rule cong_trans_nat) 
31719  934 
apply (rule `[?x = u1] (mod m1)`) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

935 
apply (rule cong_sym_nat) 
31719  936 
apply (rule `[z = u1] (mod m1)`) 
937 
done 

938 
moreover have "[?x = z] (mod m2)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

939 
apply (rule cong_trans_nat) 
31719  940 
apply (rule `[?x = u2] (mod m2)`) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

941 
apply (rule cong_sym_nat) 
31719  942 
apply (rule `[z = u2] (mod m2)`) 
943 
done 

944 
ultimately have "[?x = z] (mod m1 * m2)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

945 
by (auto intro: coprime_cong_mult_nat a) 
31719  946 
with `z < m1 * m2` `?x < m1 * m2` show "z = ?x" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

947 
apply (intro cong_less_modulus_unique_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

948 
apply (auto, erule cong_sym_nat) 
31719  949 
done 
950 
qed 

951 
with less one two show ?thesis 

952 
by auto 

953 
qed 

954 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

955 
lemma chinese_remainder_aux_nat: 
31719  956 
fixes A :: "'a set" and 
957 
m :: "'a \<Rightarrow> nat" 

958 
assumes fin: "finite A" and 

959 
cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" 

960 
shows "EX b. (ALL i : A. 

961 
[b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A  {i}. m j)))" 

962 
proof (rule finite_set_choice, rule fin, rule ballI) 

963 
fix i 

964 
assume "i : A" 

965 
with cop have "coprime (PROD j : A  {i}. m j) (m i)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

966 
by (intro setprod_coprime_nat, auto) 
31719  967 
hence "EX x. [(PROD j : A  {i}. m j) * x = 1] (mod m i)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

968 
by (elim cong_solve_coprime_nat) 
31719  969 
then obtain x where "[(PROD j : A  {i}. m j) * x = 1] (mod m i)" 
970 
by auto 

971 
moreover have "[(PROD j : A  {i}. m j) * x = 0] 

972 
(mod (PROD j : A  {i}. m j))" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

973 
by (subst mult_commute, rule cong_mult_self_nat) 
31719  974 
ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] 
975 
(mod setprod m (A  {i}))" 

976 
by blast 

977 
qed 

978 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

979 
lemma chinese_remainder_nat: 
31719  980 
fixes A :: "'a set" and 
981 
m :: "'a \<Rightarrow> nat" and 

982 
u :: "'a \<Rightarrow> nat" 

983 
assumes 

984 
fin: "finite A" and 

985 
cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" 

986 
shows "EX x. (ALL i:A. [x = u i] (mod m i))" 

987 
proof  

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

988 
from chinese_remainder_aux_nat [OF fin cop] obtain b where 
31719  989 
bprop: "ALL i:A. [b i = 1] (mod m i) \<and> 
990 
[b i = 0] (mod (PROD j : A  {i}. m j))" 

991 
by blast 

992 
let ?x = "SUM i:A. (u i) * (b i)" 

993 
show "?thesis" 

994 
proof (rule exI, clarify) 

995 
fix i 

996 
assume a: "i : A" 

997 
show "[?x = u i] (mod m i)" 

998 
proof  

999 
from fin a have "?x = (SUM j:{i}. u j * b j) + 

1000 
(SUM j:A{i}. u j * b j)" 

1001 
by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong) 

1002 
hence "[?x = u i * b i + (SUM j:A{i}. u j * b j)] (mod m i)" 

1003 
by auto 

1004 
also have "[u i * b i + (SUM j:A{i}. u j * b j) = 

1005 
u i * 1 + (SUM j:A{i}. u j * 0)] (mod m i)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1006 
apply (rule cong_add_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1007 
apply (rule cong_scalar2_nat) 
31719  1008 
using bprop a apply blast 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1009 
apply (rule cong_setsum_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1010 
apply (rule cong_scalar2_nat) 
31719  1011 
using bprop apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1012 
apply (rule cong_dvd_modulus_nat) 
31719  1013 
apply (drule (1) bspec) 
1014 
apply (erule conjE) 

1015 
apply assumption 

1016 
apply (rule dvd_setprod) 

1017 
using fin a apply auto 

1018 
done 

1019 
finally show ?thesis 

1020 
by simp 

1021 
qed 

1022 
qed 

1023 
qed 

1024 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1025 
lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow> 
31719  1026 
(ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> 
1027 
(ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow> 

1028 
[x = y] (mod (PROD i:A. m i))" 

1029 
apply (induct set: finite) 

1030 
apply auto 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1031 
apply (erule (1) coprime_cong_mult_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1032 
apply (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1033 
apply (rule setprod_coprime_nat) 
31719  1034 
apply auto 
1035 
done 

1036 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1037 
lemma chinese_remainder_unique_nat: 
31719  1038 
fixes A :: "'a set" and 
1039 
m :: "'a \<Rightarrow> nat" and 

1040 
u :: "'a \<Rightarrow> nat" 

1041 
assumes 

1042 
fin: "finite A" and 

1043 
nz: "ALL i:A. m i \<noteq> 0" and 

1044 
cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" 

1045 
shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))" 

1046 
proof  

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1047 
from chinese_remainder_nat [OF fin cop] obtain y where 
31719  1048 
one: "(ALL i:A. [y = u i] (mod m i))" 
1049 
by blast 

1050 
let ?x = "y mod (PROD i:A. m i)" 

1051 
from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0" 

1052 
by auto 

1053 
hence less: "?x < (PROD i:A. m i)" 

1054 
by auto 

1055 
have cong: "ALL i:A. [?x = u i] (mod m i)" 

1056 
apply auto 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1057 
apply (rule cong_trans_nat) 
31719  1058 
prefer 2 
1059 
using one apply auto 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1060 
apply (rule cong_dvd_modulus_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1061 
apply (rule cong_mod_nat) 
31719  1062 
using prodnz apply auto 
1063 
apply (rule dvd_setprod) 

1064 
apply (rule fin) 

1065 
apply assumption 

1066 
done 

1067 
have unique: "ALL z. z < (PROD i:A. m i) \<and> 

1068 
(ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x" 

1069 
proof (clarify) 

1070 
fix z 

1071 
assume zless: "z < (PROD i:A. m i)" 

1072 
assume zcong: "(ALL i:A. [z = u i] (mod m i))" 

1073 
have "ALL i:A. [?x = z] (mod m i)" 

1074 
apply clarify 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1075 
apply (rule cong_trans_nat) 
31719  1076 
using cong apply (erule bspec) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1077 
apply (rule cong_sym_nat) 
31719  1078 
using zcong apply auto 
1079 
done 

1080 
with fin cop have "[?x = z] (mod (PROD i:A. m i))" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1081 
by (intro coprime_cong_prod_nat, auto) 
31719  1082 
with zless less show "z = ?x" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1083 
apply (intro cong_less_modulus_unique_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

1084 
apply (auto, erule cong_sym_nat) 
31719  1085 
done 
1086 
qed 

1087 
from less cong unique show ?thesis 

1088 
by blast 

1089 
qed 

1090 

1091 
end 