author  haftmann 
Sun, 09 Nov 2014 10:03:18 +0100  
changeset 58954  18750e86d5b8 
parent 58937  49e8115f70d8 
child 59010  ec2b4270a502 
permissions  rwrr 
41959  1 
(* Title: HOL/Number_Theory/Cong.thy 
31719  2 
Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, 
3 
Thomas M. Rasmussen, Jeremy Avigad 

4 

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

6 
integers. 

7 

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

9 

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

58623  11 
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced 
31719  12 
gcd, lcm, and prime for the natural numbers. 
13 

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

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

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

44872  17 
of results to "Primes" and "GCD". 
31719  18 

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

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

33718  21 
extended to the natural numbers by Chaieb. Jeremy Avigad combined 
31719  22 
these, revised and tidied them, made the development uniform for the 
23 
natural numbers and the integers, and added a number of new theorems. 

24 
*) 

25 

58889  26 
section {* Congruence *} 
31719  27 

28 
theory Cong 

37293  29 
imports Primes 
31719  30 
begin 
31 

44872  32 
subsection {* Turn off @{text One_nat_def} *} 
31719  33 

44872  34 
lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0  x = 1)" 
35 
by (induct m) auto 

31719  36 

37 
declare mod_pos_pos_trivial [simp] 

38 

39 

40 
subsection {* Main definitions *} 

41 

42 
class cong = 

58937  43 
fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(()mod _'))") 
31719  44 
begin 
45 

58937  46 
abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(()mod _'))") 
44872  47 
where "notcong x y m \<equiv> \<not> cong x y m" 
31719  48 

49 
end 

50 

51 
(* definitions for the natural numbers *) 

52 

53 
instantiation nat :: cong 

44872  54 
begin 
31719  55 

44872  56 
definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" 
57 
where "cong_nat x y m = ((x mod m) = (y mod m))" 

31719  58 

44872  59 
instance .. 
31719  60 

61 
end 

62 

63 

64 
(* definitions for the integers *) 

65 

66 
instantiation int :: cong 

44872  67 
begin 
31719  68 

44872  69 
definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" 
70 
where "cong_int x y m = ((x mod m) = (y mod m))" 

31719  71 

44872  72 
instance .. 
31719  73 

74 
end 

75 

76 

77 
subsection {* Set up Transfer *} 

78 

79 

80 
lemma transfer_nat_int_cong: 

44872  81 
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow> 
31719  82 
([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))" 
44872  83 
unfolding cong_int_def cong_nat_def 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

84 
by (metis Divides.transfer_int_nat_functions(2) nat_0_le nat_mod_distrib) 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

85 

31719  86 

44872  87 
declare transfer_morphism_nat_int[transfer add return: 
31719  88 
transfer_nat_int_cong] 
89 

90 
lemma transfer_int_nat_cong: 

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

92 
apply (auto simp add: cong_int_def cong_nat_def) 

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

44872  94 
done 
31719  95 

44872  96 
declare transfer_morphism_int_nat[transfer add return: 
31719  97 
transfer_int_nat_cong] 
98 

99 

100 
subsection {* Congruence *} 

101 

102 
(* was zcong_0, etc. *) 

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

103 
lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)" 
44872  104 
unfolding cong_nat_def by auto 
31719  105 

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

106 
lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)" 
44872  107 
unfolding cong_int_def by auto 
31719  108 

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

109 
lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)" 
44872  110 
unfolding cong_nat_def by auto 
31719  111 

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

112 
lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

113 
unfolding cong_nat_def by auto 
31719  114 

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

115 
lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)" 
44872  116 
unfolding cong_int_def by auto 
31719  117 

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

118 
lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)" 
44872  119 
unfolding cong_nat_def by auto 
31719  120 

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

121 
lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)" 
44872  122 
unfolding cong_int_def by auto 
31719  123 

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

124 
lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)" 
44872  125 
unfolding cong_nat_def by auto 
31719  126 

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

127 
lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)" 
44872  128 
unfolding cong_int_def by auto 
31719  129 

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

130 
lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)" 
44872  131 
unfolding cong_nat_def by auto 
31719  132 

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

133 
lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)" 
44872  134 
unfolding cong_int_def by auto 
31719  135 

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

136 
lemma cong_trans_nat [trans]: 
31719  137 
"[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)" 
44872  138 
unfolding cong_nat_def by auto 
31719  139 

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

140 
lemma cong_trans_int [trans]: 
31719  141 
"[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)" 
44872  142 
unfolding cong_int_def by auto 
31719  143 

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

144 
lemma cong_add_nat: 
31719  145 
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

146 
unfolding cong_nat_def by (metis mod_add_cong) 
31719  147 

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

148 
lemma cong_add_int: 
31719  149 
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

150 
unfolding cong_int_def by (metis mod_add_cong) 
31719  151 

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

152 
lemma cong_diff_int: 
31719  153 
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a  c = b  d] (mod m)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

154 
unfolding cong_int_def by (metis mod_diff_cong) 
31719  155 

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

156 
lemma cong_diff_aux_int: 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

157 
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

158 
(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [tsub a c = tsub b d] (mod m)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

159 
by (metis cong_diff_int tsub_eq) 
31719  160 

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

161 
lemma cong_diff_nat: 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

162 
assumes"[a = b] (mod m)" "[c = d] (mod m)" "(a::nat) >= c" "b >= d" 
31719  163 
shows "[a  c = b  d] (mod m)" 
58860  164 
using assms by (rule cong_diff_aux_int [transferred]) 
31719  165 

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

166 
lemma cong_mult_nat: 
31719  167 
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

168 
unfolding cong_nat_def by (metis mod_mult_cong) 
31719  169 

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

170 
lemma cong_mult_int: 
31719  171 
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

172 
unfolding cong_int_def by (metis mod_mult_cong) 
31719  173 

44872  174 
lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)" 
175 
by (induct k) (auto simp add: cong_mult_nat) 

176 

177 
lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)" 

178 
by (induct k) (auto simp add: cong_mult_int) 

179 

180 
lemma cong_setsum_nat [rule_format]: 

181 
"(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 

31719  182 
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)" 
44872  183 
apply (cases "finite A") 
31719  184 
apply (induct set: finite) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

185 
apply (auto intro: cong_add_nat) 
44872  186 
done 
31719  187 

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

188 
lemma cong_setsum_int [rule_format]: 
44872  189 
"(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
31719  190 
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)" 
44872  191 
apply (cases "finite A") 
31719  192 
apply (induct set: finite) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

193 
apply (auto intro: cong_add_int) 
44872  194 
done 
31719  195 

44872  196 
lemma cong_setprod_nat [rule_format]: 
197 
"(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 

31719  198 
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)" 
44872  199 
apply (cases "finite A") 
31719  200 
apply (induct set: finite) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

201 
apply (auto intro: cong_mult_nat) 
44872  202 
done 
31719  203 

44872  204 
lemma cong_setprod_int [rule_format]: 
205 
"(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 

31719  206 
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)" 
44872  207 
apply (cases "finite A") 
31719  208 
apply (induct set: finite) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

209 
apply (auto intro: cong_mult_int) 
44872  210 
done 
31719  211 

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

212 
lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)" 
44872  213 
by (rule cong_mult_nat) simp_all 
31719  214 

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

215 
lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)" 
44872  216 
by (rule cong_mult_int) simp_all 
31719  217 

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

218 
lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)" 
44872  219 
by (rule cong_mult_nat) simp_all 
31719  220 

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

221 
lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)" 
44872  222 
by (rule cong_mult_int) simp_all 
31719  223 

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

224 
lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)" 
44872  225 
unfolding cong_nat_def by auto 
31719  226 

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

227 
lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)" 
44872  228 
unfolding cong_int_def by auto 
31719  229 

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

230 
lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a  b = 0] (mod m)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

231 
by (metis cong_add_int cong_diff_int cong_refl_int diff_add_cancel diff_self) 
31719  232 

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

233 
lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow> 
31719  234 
[(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

235 
by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int) 
31719  236 

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

237 
lemma cong_eq_diff_cong_0_nat: 
31719  238 
assumes "(a::nat) >= b" 
239 
shows "[a = b] (mod m) = [a  b = 0] (mod m)" 

41541  240 
using assms by (rule cong_eq_diff_cong_0_aux_int [transferred]) 
31719  241 

44872  242 
lemma cong_diff_cong_0'_nat: 
243 
"[(x::nat) = y] (mod n) \<longleftrightarrow> 

31719  244 
(if x <= y then [y  x = 0] (mod n) else [x  y = 0] (mod n))" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

245 
by (metis cong_eq_diff_cong_0_nat cong_sym_nat nat_le_linear) 
31719  246 

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

247 
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

248 
apply (subst cong_eq_diff_cong_0_nat, assumption) 
31719  249 
apply (unfold cong_nat_def) 
250 
apply (simp add: dvd_eq_mod_eq_0 [symmetric]) 

44872  251 
done 
31719  252 

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

253 
lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a  b))" 
55371  254 
by (metis cong_int_def zmod_eq_dvd_iff) 
31719  255 

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

256 
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

257 
by (simp add: cong_altdef_int) 
31719  258 

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

259 
lemma cong_square_int: 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55161
diff
changeset

260 
fixes a::int 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55161
diff
changeset

261 
shows "\<lbrakk> prime p; 0 < a; [a * a = 1] (mod p) \<rbrakk> 
31719  262 
\<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

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

264 
apply (subst prime_dvd_mult_eq_int [symmetric], assumption) 
36350  265 
apply (auto simp add: field_simps) 
44872  266 
done 
31719  267 

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

268 
lemma cong_mult_rcancel_int: 
44872  269 
"coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)" 
55371  270 
by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd_int.commute) 
31719  271 

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

272 
lemma cong_mult_rcancel_nat: 
55371  273 
"coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)" 
274 
by (metis cong_mult_rcancel_int [transferred]) 

31719  275 

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

276 
lemma cong_mult_lcancel_nat: 
44872  277 
"coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

278 
by (simp add: mult.commute cong_mult_rcancel_nat) 
31719  279 

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

280 
lemma cong_mult_lcancel_int: 
44872  281 
"coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

282 
by (simp add: mult.commute cong_mult_rcancel_int) 
31719  283 

284 
(* was zcong_zgcd_zmult_zmod *) 

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

285 
lemma coprime_cong_mult_int: 
31719  286 
"[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n 
287 
\<Longrightarrow> [a = b] (mod m * n)" 

55371  288 
by (metis divides_mult_int cong_altdef_int) 
31719  289 

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

290 
lemma coprime_cong_mult_nat: 
31719  291 
assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n" 
292 
shows "[a = b] (mod m * n)" 

55371  293 
by (metis assms coprime_cong_mult_int [transferred]) 
31719  294 

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

295 
lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow> 
31719  296 
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" 
41541  297 
by (auto simp add: cong_nat_def) 
31719  298 

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

299 
lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow> 
31719  300 
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" 
41541  301 
by (auto simp add: cong_int_def) 
31719  302 

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

303 
lemma cong_less_unique_nat: 
31719  304 
"0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" 
55371  305 
by (auto simp: cong_nat_def) (metis mod_less_divisor mod_mod_trivial) 
31719  306 

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

307 
lemma cong_less_unique_int: 
31719  308 
"0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" 
55371  309 
by (auto simp: cong_int_def) (metis mod_mod_trivial pos_mod_conj) 
31719  310 

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

311 
lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)" 
55371  312 
apply (auto simp add: cong_altdef_int dvd_def) 
31719  313 
apply (rule_tac [!] x = "k" in exI, auto) 
44872  314 
done 
31719  315 

55371  316 
lemma cong_iff_lin_nat: 
317 
"([(a::nat) = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)" (is "?lhs = ?rhs") 

318 
proof (rule iffI) 

319 
assume eqm: ?lhs 

320 
show ?rhs 

321 
proof (cases "b \<le> a") 

322 
case True 

323 
then show ?rhs using eqm 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

324 
by (metis cong_altdef_nat dvd_def le_add_diff_inverse add_0_right mult_0 mult.commute) 
55371  325 
next 
326 
case False 

327 
then show ?rhs using eqm 

328 
apply (subst (asm) cong_sym_eq_nat) 

329 
apply (auto simp: cong_altdef_nat) 

330 
apply (metis add_0_right add_diff_inverse dvd_div_mult_self less_or_eq_imp_le mult_0) 

331 
done 

332 
qed 

333 
next 

334 
assume ?rhs 

335 
then show ?lhs 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

336 
by (metis cong_nat_def mod_mult_self2 mult.commute) 
55371  337 
qed 
31719  338 

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

339 
lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m" 
55371  340 
by (metis cong_int_def gcd_red_int) 
31719  341 

44872  342 
lemma cong_gcd_eq_nat: 
55371  343 
"[(a::nat) = b] (mod m) \<Longrightarrow>gcd a m = gcd b m" 
344 
by (metis assms cong_gcd_eq_int [transferred]) 

31719  345 

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

347 
by (auto simp add: cong_gcd_eq_nat) 
31719  348 

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

350 
by (auto simp add: cong_gcd_eq_int) 
31719  351 

44872  352 
lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = [a mod m = b mod m] (mod m)" 
31719  353 
by (auto simp add: cong_nat_def) 
354 

44872  355 
lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = [a mod m = b mod m] (mod m)" 
31719  356 
by (auto simp add: cong_int_def) 
357 

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

358 
lemma cong_minus_int [iff]: "[(a::int) = b] (mod m) = [a = b] (mod m)" 
55371  359 
by (metis cong_iff_lin_int minus_equation_iff mult_minus_left mult_minus_right) 
31719  360 

361 
(* 

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

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

365 
apply (rule mod_mod_cancel) 

366 
apply auto 

44872  367 
done 
31719  368 

369 
lemma mod_dvd_mod: 

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

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

372 

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

373 
apply (rule mod_dvd_mod_int [transferred]) 
41541  374 
using assms apply auto 
375 
done 

31719  376 
*) 
377 

44872  378 
lemma cong_add_lcancel_nat: 
379 
"[(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

380 
by (simp add: cong_iff_lin_nat) 
31719  381 

44872  382 
lemma cong_add_lcancel_int: 
383 
"[(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

384 
by (simp add: cong_iff_lin_int) 
31719  385 

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

386 
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

387 
by (simp add: cong_iff_lin_nat) 
31719  388 

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

389 
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

390 
by (simp add: cong_iff_lin_int) 
31719  391 

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

393 
by (simp add: cong_iff_lin_nat) 
31719  394 

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

396 
by (simp add: cong_iff_lin_int) 
31719  397 

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

399 
by (simp add: cong_iff_lin_nat) 
31719  400 

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

402 
by (simp add: cong_iff_lin_int) 
31719  403 

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

406 
apply (auto simp add: cong_iff_lin_nat dvd_def) 
31719  407 
apply (rule_tac x="k1 * k" in exI) 
408 
apply (rule_tac x="k2 * k" in exI) 

36350  409 
apply (simp add: field_simps) 
44872  410 
done 
31719  411 

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

413 
by (auto simp add: cong_altdef_int dvd_def) 
31719  414 

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

415 
lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y" 
44872  416 
unfolding cong_nat_def by (auto simp add: dvd_eq_mod_eq_0) 
31719  417 

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

418 
lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y" 
44872  419 
unfolding cong_int_def by (auto simp add: dvd_eq_mod_eq_0) 
31719  420 

44872  421 
lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
31719  422 
by (simp add: cong_nat_def) 
423 

44872  424 
lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
31719  425 
by (simp add: cong_int_def) 
426 

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

430 

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

431 
lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([a = b] (mod m))" 
55371  432 
by (metis cong_int_def minus_minus zminus_zmod) 
31719  433 

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

434 
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

435 
by (auto simp add: cong_altdef_int) 
31719  436 

44872  437 
lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0 
31719  438 
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)" 
55371  439 
apply (cases "b > 0", 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

440 
apply (subst (1 2) cong_modulus_neg_int) 
31719  441 
apply (unfold cong_int_def) 
442 
apply (subgoal_tac "a * b = (a * b)") 

443 
apply (erule ssubst) 

444 
apply (subst zmod_zmult2_eq) 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47163
diff
changeset

445 
apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47163
diff
changeset

446 
apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 semiring_numeral_div_class.diff_zero)+ 
44872  447 
done 
31719  448 

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

449 
lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a  1))" 
55371  450 
apply (cases "a = 0", force) 
451 
by (metis cong_altdef_nat leI less_one) 

31719  452 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

453 
lemma cong_0_1_nat': "[(0::nat) = Suc 0] (mod n) = (n = Suc 0)" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

454 
unfolding cong_nat_def by auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset

455 

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

456 
lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)" 
44872  457 
unfolding cong_nat_def by auto 
31719  458 

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

459 
lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1)  (n = 1))" 
44872  460 
unfolding cong_int_def by (auto simp add: zmult_eq_1_iff) 
31719  461 

44872  462 
lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow> 
31719  463 
a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)" 
44872  464 
apply (cases "n = 1") 
31719  465 
apply auto [1] 
466 
apply (drule_tac x = "a  1" in spec) 

467 
apply force 

55371  468 
apply (cases "a = 0", simp add: cong_0_1_nat) 
31719  469 
apply (rule iffI) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

470 
apply (metis cong_to_1_nat dvd_def monoid_mult_class.mult.right_neutral mult.commute mult_eq_if) 
55371  471 
apply (metis cong_add_lcancel_0_nat cong_mult_self_nat) 
44872  472 
done 
31719  473 

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

474 
lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

475 
by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def mult.commute) 
31719  476 

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

477 
lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)" 
44872  478 
apply (cases "n = 0") 
31719  479 
apply force 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

480 
apply (frule bezout_nat [of a n], auto) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

481 
by (metis cong_add_rcancel_0_nat cong_mult_self_nat mult.commute) 
31719  482 

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

483 
lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)" 
44872  484 
apply (cases "n = 0") 
485 
apply (cases "a \<ge> 0") 

31719  486 
apply auto 
487 
apply (rule_tac x = "1" in exI) 

488 
apply auto 

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

489 
apply (insert bezout_int [of a n], auto) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

490 
by (metis cong_iff_lin_int mult.commute) 
44872  491 

492 
lemma cong_solve_dvd_nat: 

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

495 
proof  

44872  496 
from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)" 
31719  497 
by auto 
44872  498 
then have "[(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

499 
by (elim cong_scalar2_nat) 
31719  500 
also from b have "(d div gcd a n) * gcd a n = d" 
501 
by (rule dvd_div_mult_self) 

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

503 
by auto 

504 
finally show ?thesis 

505 
by auto 

506 
qed 

507 

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

511 
proof  

44872  512 
from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)" 
31719  513 
by auto 
44872  514 
then have "[(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

515 
by (elim cong_scalar2_int) 
31719  516 
also from b have "(d div gcd a n) * gcd a n = d" 
517 
by (rule dvd_div_mult_self) 

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

519 
by auto 

520 
finally show ?thesis 

521 
by auto 

522 
qed 

523 

44872  524 
lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)" 
525 
apply (cases "a = 0") 

31719  526 
apply force 
55161  527 
apply (metis cong_solve_nat) 
44872  528 
done 
31719  529 

44872  530 
lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)" 
531 
apply (cases "a = 0") 

31719  532 
apply auto 
44872  533 
apply (cases "n \<ge> 0") 
31719  534 
apply auto 
55161  535 
apply (metis cong_solve_int) 
536 
done 

537 

538 
lemma coprime_iff_invertible_nat: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))" 

55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55321
diff
changeset

539 
apply (auto intro: cong_solve_coprime_nat simp: One_nat_def) 
55161  540 
apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral) 
541 
apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat 

542 
gcd_lcm_complete_lattice_nat.inf_bot_right gcd_nat.commute) 

44872  543 
done 
31719  544 

55161  545 
lemma coprime_iff_invertible_int: "m > (0::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))" 
546 
apply (auto intro: cong_solve_coprime_int) 

547 
apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd_int.commute gcd_red_int) 

44872  548 
done 
31719  549 

55161  550 
lemma coprime_iff_invertible'_nat: "m > 0 \<Longrightarrow> coprime a m = 
551 
(EX x. 0 \<le> x & x < m & [a * x = Suc 0] (mod m))" 

552 
apply (subst coprime_iff_invertible_nat) 

553 
apply auto 

554 
apply (auto simp add: cong_nat_def) 

555 
apply (metis mod_less_divisor mod_mult_right_eq) 

44872  556 
done 
31719  557 

55161  558 
lemma coprime_iff_invertible'_int: "m > (0::int) \<Longrightarrow> coprime a m = 
31719  559 
(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

560 
apply (subst coprime_iff_invertible_int) 
31719  561 
apply (auto simp add: cong_int_def) 
55371  562 
apply (metis mod_mult_right_eq pos_mod_conj) 
44872  563 
done 
31719  564 

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

565 
lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow> 
31719  566 
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" 
44872  567 
apply (cases "y \<le> x") 
55371  568 
apply (metis cong_altdef_nat lcm_least_nat) 
569 
apply (metis cong_altdef_nat cong_diff_cong_0'_nat lcm_semilattice_nat.sup.bounded_iff le0 minus_nat.diff_0) 

44872  570 
done 
31719  571 

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

572 
lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow> 
31719  573 
[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

574 
by (auto simp add: cong_altdef_int lcm_least_int) [1] 
31719  575 

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

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

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

580 
apply (induct set: finite) 

581 
apply auto 

55371  582 
apply (metis coprime_cong_mult_nat gcd_semilattice_nat.inf_commute setprod_coprime_nat) 
44872  583 
done 
31719  584 

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

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

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

589 
apply (induct set: finite) 

590 
apply auto 

55371  591 
apply (metis coprime_cong_mult_int gcd_int.commute setprod_coprime_int) 
44872  592 
done 
31719  593 

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

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

598 
proof  

44872  599 
from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)" 
31719  600 
by auto 
44872  601 
from a have b: "coprime m2 m1" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

602 
by (subst gcd_commute_nat) 
44872  603 
from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)" 
31719  604 
by auto 
605 
have "[m1 * x1 = 0] (mod m1)" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

606 
by (subst mult.commute, rule cong_mult_self_nat) 
31719  607 
moreover have "[m2 * x2 = 0] (mod m2)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

608 
by (subst mult.commute, rule cong_mult_self_nat) 
31719  609 
moreover note one two 
610 
ultimately show ?thesis by blast 

611 
qed 

612 

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

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

617 
proof  

44872  618 
from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)" 
31719  619 
by auto 
44872  620 
from a have b: "coprime m2 m1" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

621 
by (subst gcd_commute_int) 
44872  622 
from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)" 
31719  623 
by auto 
624 
have "[m1 * x1 = 0] (mod m1)" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

625 
by (subst mult.commute, rule cong_mult_self_int) 
31719  626 
moreover have "[m2 * x2 = 0] (mod m2)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

627 
by (subst mult.commute, rule cong_mult_self_int) 
31719  628 
moreover note one two 
629 
ultimately show ?thesis by blast 

630 
qed 

631 

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

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

635 
proof  

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

636 
from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2 
44872  637 
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and 
638 
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" 

31719  639 
by blast 
640 
let ?x = "u1 * b1 + u2 * b2" 

641 
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

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

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

645 
apply (rule cong_scalar2_nat) 
31719  646 
apply (rule `[b2 = 0] (mod m1)`) 
647 
done 

44872  648 
then have "[?x = u1] (mod m1)" by simp 
31719  649 
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

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

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

653 
apply (rule cong_scalar2_nat) 
31719  654 
apply (rule `[b2 = 1] (mod m2)`) 
655 
done 

44872  656 
then have "[?x = u2] (mod m2)" by simp 
31719  657 
with `[?x = u1] (mod m1)` show ?thesis by blast 
658 
qed 

659 

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

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

663 
proof  

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

664 
from binary_chinese_remainder_aux_int [OF a] obtain b1 b2 
31719  665 
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and 
666 
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" 

667 
by blast 

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

669 
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

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

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

673 
apply (rule cong_scalar2_int) 
31719  674 
apply (rule `[b2 = 0] (mod m1)`) 
675 
done 

44872  676 
then have "[?x = u1] (mod m1)" by simp 
31719  677 
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

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

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

681 
apply (rule cong_scalar2_int) 
31719  682 
apply (rule `[b2 = 1] (mod m2)`) 
683 
done 

44872  684 
then have "[?x = u2] (mod m2)" by simp 
31719  685 
with `[?x = u1] (mod m1)` show ?thesis by blast 
686 
qed 

687 

44872  688 
lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow> 
31719  689 
[x = y] (mod m)" 
44872  690 
apply (cases "y \<le> x") 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

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

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

694 
apply (subst (asm) cong_sym_eq_nat) 
44872  695 
apply (simp add: cong_altdef_nat) 
31719  696 
apply (erule dvd_mult_left) 
44872  697 
done 
31719  698 

44872  699 
lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow> 
31719  700 
[x = y] (mod m)" 
44872  701 
apply (simp add: cong_altdef_int) 
31719  702 
apply (erule dvd_mult_left) 
44872  703 
done 
31719  704 

44872  705 
lemma cong_less_modulus_unique_nat: 
31719  706 
"[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y" 
707 
by (simp add: cong_nat_def) 

708 

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

709 
lemma binary_chinese_remainder_unique_nat: 
44872  710 
assumes a: "coprime (m1::nat) m2" 
711 
and nz: "m1 \<noteq> 0" "m2 \<noteq> 0" 

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

44872  714 
from binary_chinese_remainder_nat [OF a] obtain y where 
31719  715 
"[y = u1] (mod m1)" and "[y = u2] (mod m2)" 
716 
by blast 

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

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

44872  719 
by auto 
31719  720 
have one: "[?x = u1] (mod m1)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

721 
apply (rule cong_trans_nat) 
31719  722 
prefer 2 
723 
apply (rule `[y = u1] (mod m1)`) 

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

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

725 
apply (rule cong_mod_nat) 
31719  726 
using nz apply auto 
727 
done 

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

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

729 
apply (rule cong_trans_nat) 
31719  730 
prefer 2 
731 
apply (rule `[y = u2] (mod m2)`) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

732 
apply (subst mult.commute) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

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

734 
apply (rule cong_mod_nat) 
31719  735 
using nz apply auto 
736 
done 

44872  737 
have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x" 
738 
proof clarify 

31719  739 
fix z 
740 
assume "z < m1 * m2" 

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

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

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

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

745 
apply (rule cong_sym_nat) 
31719  746 
apply (rule `[z = u1] (mod m1)`) 
747 
done 

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

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

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

751 
apply (rule cong_sym_nat) 
31719  752 
apply (rule `[z = u2] (mod m2)`) 
753 
done 

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

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

755 
by (auto intro: coprime_cong_mult_nat a) 
31719  756 
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

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

758 
apply (auto, erule cong_sym_nat) 
31719  759 
done 
44872  760 
qed 
761 
with less one two show ?thesis by auto 

31719  762 
qed 
763 

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

764 
lemma chinese_remainder_aux_nat: 
44872  765 
fixes A :: "'a set" 
766 
and m :: "'a \<Rightarrow> nat" 

767 
assumes fin: "finite A" 

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

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

31719  770 
proof (rule finite_set_choice, rule fin, rule ballI) 
771 
fix i 

772 
assume "i : A" 

773 
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

774 
by (intro setprod_coprime_nat, auto) 
44872  775 
then have "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

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

44872  779 
moreover have "[(PROD j : A  {i}. m j) * x = 0] 
31719  780 
(mod (PROD j : A  {i}. m j))" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

781 
by (subst mult.commute, rule cong_mult_self_nat) 
44872  782 
ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] 
31719  783 
(mod setprod m (A  {i}))" 
784 
by blast 

785 
qed 

786 

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

787 
lemma chinese_remainder_nat: 
44872  788 
fixes A :: "'a set" 
789 
and m :: "'a \<Rightarrow> nat" 

790 
and u :: "'a \<Rightarrow> nat" 

791 
assumes fin: "finite A" 

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

31719  793 
shows "EX x. (ALL i:A. [x = u i] (mod m i))" 
794 
proof  

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

795 
from chinese_remainder_aux_nat [OF fin cop] obtain b where 
44872  796 
bprop: "ALL i:A. [b i = 1] (mod m i) \<and> 
31719  797 
[b i = 0] (mod (PROD j : A  {i}. m j))" 
798 
by blast 

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

800 
show "?thesis" 

801 
proof (rule exI, clarify) 

802 
fix i 

803 
assume a: "i : A" 

44872  804 
show "[?x = u i] (mod m i)" 
31719  805 
proof  
44872  806 
from fin a have "?x = (SUM j:{i}. u j * b j) + 
31719  807 
(SUM j:A{i}. u j * b j)" 
57418  808 
by (subst setsum.union_disjoint [symmetric], auto intro: setsum.cong) 
44872  809 
then have "[?x = u i * b i + (SUM j:A{i}. u j * b j)] (mod m i)" 
31719  810 
by auto 
811 
also have "[u i * b i + (SUM j:A{i}. u j * b j) = 

812 
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

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

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

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

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

819 
apply (rule cong_dvd_modulus_nat) 
31719  820 
apply (drule (1) bspec) 
821 
apply (erule conjE) 

822 
apply assumption 

823 
apply (rule dvd_setprod) 

824 
using fin a apply auto 

825 
done 

826 
finally show ?thesis 

827 
by simp 

828 
qed 

829 
qed 

830 
qed 

831 

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

44872  835 
[x = y] (mod (PROD i:A. m i))" 
31719  836 
apply (induct set: finite) 
837 
apply auto 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

838 
apply (metis coprime_cong_mult_nat mult.commute setprod_coprime_nat) 
44872  839 
done 
31719  840 

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

841 
lemma chinese_remainder_unique_nat: 
44872  842 
fixes A :: "'a set" 
843 
and m :: "'a \<Rightarrow> nat" 

844 
and u :: "'a \<Rightarrow> nat" 

845 
assumes fin: "finite A" 

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

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

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

44872  850 
from chinese_remainder_nat [OF fin cop] 
851 
obtain y where one: "(ALL i:A. [y = u i] (mod m i))" 

31719  852 
by blast 
853 
let ?x = "y mod (PROD i:A. m i)" 

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

855 
by auto 

44872  856 
then have less: "?x < (PROD i:A. m i)" 
31719  857 
by auto 
858 
have cong: "ALL i:A. [?x = u i] (mod m i)" 

859 
apply auto 

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

860 
apply (rule cong_trans_nat) 
31719  861 
prefer 2 
862 
using one apply auto 

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

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

864 
apply (rule cong_mod_nat) 
31719  865 
using prodnz apply auto 
866 
apply (rule dvd_setprod) 

867 
apply (rule fin) 

868 
apply assumption 

869 
done 

44872  870 
have unique: "ALL z. z < (PROD i:A. m i) \<and> 
31719  871 
(ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x" 
872 
proof (clarify) 

873 
fix z 

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

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

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

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

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

880 
apply (rule cong_sym_nat) 
31719  881 
using zcong apply auto 
882 
done 

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

44872  884 
apply (intro coprime_cong_prod_nat) 
885 
apply auto 

886 
done 

31719  887 
with zless less show "z = ?x" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

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

889 
apply (auto, erule cong_sym_nat) 
31719  890 
done 
44872  891 
qed 
892 
from less cong unique show ?thesis by blast 

31719  893 
qed 
894 

895 
end 