author | haftmann |
Thu, 23 Nov 2017 17:03:27 +0000 | |
changeset 67087 | 733017b19de9 |
parent 67086 | 59d07a95be0e |
child 67115 | 2977773a481c |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Number_Theory/Cong.thy |
66380 | 2 |
Author: Christophe Tabacznyj |
3 |
Author: Lawrence C. Paulson |
|
4 |
Author: Amine Chaieb |
|
5 |
Author: Thomas M. Rasmussen |
|
6 |
Author: Jeremy Avigad |
|
31719 | 7 |
|
8 |
Defines congruence (notation: [x = y] (mod z)) for natural numbers and |
|
9 |
integers. |
|
10 |
||
11 |
This file combines and revises a number of prior developments. |
|
12 |
||
13 |
The original theories "GCD" and "Primes" were by Christophe Tabacznyj |
|
58623 | 14 |
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced |
31719 | 15 |
gcd, lcm, and prime for the natural numbers. |
16 |
||
17 |
The original theory "IntPrimes" was by Thomas M. Rasmussen, and |
|
18 |
extended gcd, lcm, primes to the integers. Amine Chaieb provided |
|
19 |
another extension of the notions to the integers, and added a number |
|
44872 | 20 |
of results to "Primes" and "GCD". |
31719 | 21 |
|
22 |
The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and |
|
23 |
developed the congruence relations on the integers. The notion was |
|
33718 | 24 |
extended to the natural numbers by Chaieb. Jeremy Avigad combined |
31719 | 25 |
these, revised and tidied them, made the development uniform for the |
26 |
natural numbers and the integers, and added a number of new theorems. |
|
27 |
*) |
|
28 |
||
60526 | 29 |
section \<open>Congruence\<close> |
31719 | 30 |
|
31 |
theory Cong |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66380
diff
changeset
|
32 |
imports "HOL-Computational_Algebra.Primes" |
31719 | 33 |
begin |
34 |
||
66888 | 35 |
subsection \<open>Generic congruences\<close> |
36 |
||
37 |
context unique_euclidean_semiring |
|
31719 | 38 |
begin |
39 |
||
66888 | 40 |
definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(()mod _'))") |
41 |
where "cong b c a \<longleftrightarrow> b mod a = c mod a" |
|
42 |
||
58937 | 43 |
abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(()mod _'))") |
66888 | 44 |
where "notcong b c a \<equiv> \<not> cong b c a" |
45 |
||
46 |
lemma cong_refl [simp]: |
|
47 |
"[b = b] (mod a)" |
|
48 |
by (simp add: cong_def) |
|
49 |
||
50 |
lemma cong_sym: |
|
51 |
"[b = c] (mod a) \<Longrightarrow> [c = b] (mod a)" |
|
52 |
by (simp add: cong_def) |
|
53 |
||
54 |
lemma cong_sym_eq: |
|
55 |
"[b = c] (mod a) \<longleftrightarrow> [c = b] (mod a)" |
|
56 |
by (auto simp add: cong_def) |
|
57 |
||
58 |
lemma cong_trans [trans]: |
|
59 |
"[b = c] (mod a) \<Longrightarrow> [c = d] (mod a) \<Longrightarrow> [b = d] (mod a)" |
|
60 |
by (simp add: cong_def) |
|
61 |
||
67085 | 62 |
lemma cong_mult_self_right: |
63 |
"[b * a = 0] (mod a)" |
|
64 |
by (simp add: cong_def) |
|
65 |
||
66 |
lemma cong_mult_self_left: |
|
67 |
"[a * b = 0] (mod a)" |
|
68 |
by (simp add: cong_def) |
|
69 |
||
70 |
lemma cong_mod_left [simp]: |
|
71 |
"[b mod a = c] (mod a) \<longleftrightarrow> [b = c] (mod a)" |
|
72 |
by (simp add: cong_def) |
|
73 |
||
74 |
lemma cong_mod_right [simp]: |
|
75 |
"[b = c mod a] (mod a) \<longleftrightarrow> [b = c] (mod a)" |
|
76 |
by (simp add: cong_def) |
|
77 |
||
78 |
lemma cong_0 [simp, presburger]: |
|
79 |
"[b = c] (mod 0) \<longleftrightarrow> b = c" |
|
80 |
by (simp add: cong_def) |
|
81 |
||
82 |
lemma cong_1 [simp, presburger]: |
|
83 |
"[b = c] (mod 1)" |
|
84 |
by (simp add: cong_def) |
|
85 |
||
86 |
lemma cong_dvd_iff: |
|
87 |
"a dvd b \<longleftrightarrow> a dvd c" if "[b = c] (mod a)" |
|
88 |
using that by (auto simp: cong_def dvd_eq_mod_eq_0) |
|
89 |
||
90 |
lemma cong_0_iff: "[b = 0] (mod a) \<longleftrightarrow> a dvd b" |
|
91 |
by (simp add: cong_def dvd_eq_mod_eq_0) |
|
92 |
||
66888 | 93 |
lemma cong_add: |
94 |
"[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b + d = c + e] (mod a)" |
|
95 |
by (auto simp add: cong_def intro: mod_add_cong) |
|
96 |
||
97 |
lemma cong_mult: |
|
98 |
"[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b * d = c * e] (mod a)" |
|
99 |
by (auto simp add: cong_def intro: mod_mult_cong) |
|
100 |
||
67085 | 101 |
lemma cong_scalar_right: |
102 |
"[b = c] (mod a) \<Longrightarrow> [b * d = c * d] (mod a)" |
|
103 |
by (simp add: cong_mult) |
|
104 |
||
105 |
lemma cong_scalar_left: |
|
106 |
"[b = c] (mod a) \<Longrightarrow> [d * b = d * c] (mod a)" |
|
107 |
by (simp add: cong_mult) |
|
108 |
||
66888 | 109 |
lemma cong_pow: |
110 |
"[b = c] (mod a) \<Longrightarrow> [b ^ n = c ^ n] (mod a)" |
|
111 |
by (simp add: cong_def power_mod [symmetric, of b n a] power_mod [symmetric, of c n a]) |
|
112 |
||
113 |
lemma cong_sum: |
|
114 |
"[sum f A = sum g A] (mod a)" if "\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod a)" |
|
115 |
using that by (induct A rule: infinite_finite_induct) (auto intro: cong_add) |
|
116 |
||
117 |
lemma cong_prod: |
|
118 |
"[prod f A = prod g A] (mod a)" if "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod a))" |
|
119 |
using that by (induct A rule: infinite_finite_induct) (auto intro: cong_mult) |
|
120 |
||
121 |
lemma mod_mult_cong_right: |
|
122 |
"[c mod (a * b) = d] (mod a) \<longleftrightarrow> [c = d] (mod a)" |
|
123 |
by (simp add: cong_def mod_mod_cancel mod_add_left_eq) |
|
124 |
||
125 |
lemma mod_mult_cong_left: |
|
126 |
"[c mod (b * a) = d] (mod a) \<longleftrightarrow> [c = d] (mod a)" |
|
127 |
using mod_mult_cong_right [of c a b d] by (simp add: ac_simps) |
|
128 |
||
129 |
end |
|
130 |
||
131 |
context unique_euclidean_ring |
|
132 |
begin |
|
133 |
||
134 |
lemma cong_diff: |
|
135 |
"[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b - d = c - e] (mod a)" |
|
136 |
by (auto simp add: cong_def intro: mod_diff_cong) |
|
137 |
||
138 |
lemma cong_diff_iff_cong_0: |
|
139 |
"[b - c = 0] (mod a) \<longleftrightarrow> [b = c] (mod a)" (is "?P \<longleftrightarrow> ?Q") |
|
140 |
proof |
|
141 |
assume ?P |
|
142 |
then have "[b - c + c = 0 + c] (mod a)" |
|
143 |
by (rule cong_add) simp |
|
144 |
then show ?Q |
|
145 |
by simp |
|
146 |
next |
|
147 |
assume ?Q |
|
148 |
with cong_diff [of b c a c c] show ?P |
|
149 |
by simp |
|
150 |
qed |
|
151 |
||
152 |
lemma cong_minus_minus_iff: |
|
153 |
"[- b = - c] (mod a) \<longleftrightarrow> [b = c] (mod a)" |
|
154 |
using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of "- b" "- c" a] |
|
155 |
by (simp add: cong_0_iff dvd_diff_commute) |
|
156 |
||
67087 | 157 |
lemma cong_modulus_minus_iff: |
158 |
"[b = c] (mod - a) \<longleftrightarrow> [b = c] (mod a)" |
|
66888 | 159 |
using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of b c " -a"] |
160 |
by (simp add: cong_0_iff) |
|
31719 | 161 |
|
67087 | 162 |
lemma cong_iff_dvd_diff: |
163 |
"[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)" |
|
164 |
by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0) |
|
165 |
||
166 |
lemma cong_iff_lin: |
|
167 |
"[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)" (is "?P \<longleftrightarrow> ?Q") |
|
168 |
proof - |
|
169 |
have "?P \<longleftrightarrow> m dvd b - a" |
|
170 |
by (simp add: cong_iff_dvd_diff dvd_diff_commute) |
|
171 |
also have "\<dots> \<longleftrightarrow> ?Q" |
|
172 |
by (auto simp add: algebra_simps elim!: dvdE) |
|
173 |
finally show ?thesis |
|
174 |
by simp |
|
175 |
qed |
|
176 |
||
31719 | 177 |
end |
178 |
||
66380 | 179 |
|
66888 | 180 |
subsection \<open>Congruences on @{typ nat} and @{typ int}\<close> |
31719 | 181 |
|
66888 | 182 |
lemma cong_int_iff: |
183 |
"[int m = int q] (mod int n) \<longleftrightarrow> [m = q] (mod n)" |
|
184 |
by (simp add: cong_def of_nat_mod [symmetric]) |
|
185 |
||
186 |
lemma cong_Suc_0 [simp, presburger]: |
|
187 |
"[m = n] (mod Suc 0)" |
|
188 |
using cong_1 [of m n] by simp |
|
31719 | 189 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
190 |
lemma cong_diff_nat: |
66888 | 191 |
"[a - c = b - d] (mod m)" if "[a = b] (mod m)" "[c = d] (mod m)" |
66954 | 192 |
and "a \<ge> c" "b \<ge> d" for a b c d m :: nat |
193 |
proof - |
|
194 |
have "[c + (a - c) = d + (b - d)] (mod m)" |
|
195 |
using that by simp |
|
196 |
with \<open>[c = d] (mod m)\<close> have "[c + (a - c) = c + (b - d)] (mod m)" |
|
197 |
using mod_add_cong by (auto simp add: cong_def) fastforce |
|
198 |
then show ?thesis |
|
199 |
by (simp add: cong_def nat_mod_eq_iff) |
|
200 |
qed |
|
31719 | 201 |
|
66888 | 202 |
lemma cong_diff_iff_cong_0_nat: |
66954 | 203 |
"[a - b = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)" if "a \<ge> b" for a b :: nat |
204 |
using that by (auto simp add: cong_def le_imp_diff_is_add dest: nat_mod_eq_lemma) |
|
31719 | 205 |
|
66954 | 206 |
lemma cong_diff_iff_cong_0_nat': |
207 |
"[nat \<bar>int a - int b\<bar> = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)" |
|
208 |
proof (cases "b \<le> a") |
|
209 |
case True |
|
210 |
then show ?thesis |
|
211 |
by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of b a m]) |
|
212 |
next |
|
213 |
case False |
|
214 |
then have "a \<le> b" |
|
215 |
by simp |
|
216 |
then show ?thesis |
|
217 |
by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of a b m]) |
|
218 |
(auto simp add: cong_def) |
|
219 |
qed |
|
220 |
||
221 |
lemma cong_altdef_nat: |
|
222 |
"a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)" |
|
66380 | 223 |
for a b :: nat |
66888 | 224 |
by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat) |
31719 | 225 |
|
66954 | 226 |
lemma cong_altdef_nat': |
227 |
"[a = b] (mod m) \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>" |
|
67085 | 228 |
using cong_diff_iff_cong_0_nat' [of a b m] |
229 |
by (simp only: cong_0_iff [symmetric]) |
|
66954 | 230 |
|
231 |
lemma cong_altdef_int: |
|
232 |
"[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)" |
|
66380 | 233 |
for a b :: int |
67087 | 234 |
by (fact cong_iff_dvd_diff) |
31719 | 235 |
|
67085 | 236 |
lemma cong_abs_int [simp]: "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)" |
66380 | 237 |
for x y :: int |
67087 | 238 |
by (simp add: cong_iff_dvd_diff) |
31719 | 239 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
240 |
lemma cong_square_int: |
66380 | 241 |
"prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)" |
242 |
for a :: int |
|
67087 | 243 |
apply (simp only: cong_iff_dvd_diff) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
244 |
apply (subst prime_dvd_mult_eq_int [symmetric], assumption) |
36350 | 245 |
apply (auto simp add: field_simps) |
44872 | 246 |
done |
31719 | 247 |
|
66954 | 248 |
lemma cong_mult_rcancel_int: |
249 |
"[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)" |
|
250 |
if "coprime k m" for a k m :: int |
|
67051 | 251 |
using that by (simp add: cong_altdef_int) |
252 |
(metis coprime_commute coprime_dvd_mult_right_iff mult.commute right_diff_distrib') |
|
31719 | 253 |
|
66954 | 254 |
lemma cong_mult_rcancel_nat: |
255 |
"[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)" |
|
256 |
if "coprime k m" for a k m :: nat |
|
257 |
proof - |
|
258 |
have "[a * k = b * k] (mod m) \<longleftrightarrow> m dvd nat \<bar>int (a * k) - int (b * k)\<bar>" |
|
259 |
by (simp add: cong_altdef_nat') |
|
260 |
also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>(int a - int b) * int k\<bar>" |
|
261 |
by (simp add: algebra_simps) |
|
262 |
also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar> * k" |
|
263 |
by (simp add: abs_mult nat_times_as_int) |
|
264 |
also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>" |
|
67051 | 265 |
by (rule coprime_dvd_mult_left_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>) |
66954 | 266 |
also have "\<dots> \<longleftrightarrow> [a = b] (mod m)" |
267 |
by (simp add: cong_altdef_nat') |
|
268 |
finally show ?thesis . |
|
269 |
qed |
|
31719 | 270 |
|
66954 | 271 |
lemma cong_mult_lcancel_int: |
272 |
"[k * a = k * b] (mod m) = [a = b] (mod m)" |
|
273 |
if "coprime k m" for a k m :: int |
|
274 |
using that by (simp add: cong_mult_rcancel_int ac_simps) |
|
275 |
||
276 |
lemma cong_mult_lcancel_nat: |
|
277 |
"[k * a = k * b] (mod m) = [a = b] (mod m)" |
|
278 |
if "coprime k m" for a k m :: nat |
|
279 |
using that by (simp add: cong_mult_rcancel_nat ac_simps) |
|
31719 | 280 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
281 |
lemma coprime_cong_mult_int: |
66380 | 282 |
"[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)" |
283 |
for a b :: int |
|
66954 | 284 |
by (simp add: cong_altdef_int divides_mult) |
31719 | 285 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
286 |
lemma coprime_cong_mult_nat: |
66380 | 287 |
"[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)" |
288 |
for a b :: nat |
|
66954 | 289 |
by (simp add: cong_altdef_nat' divides_mult) |
31719 | 290 |
|
66380 | 291 |
lemma cong_less_imp_eq_nat: "0 \<le> a \<Longrightarrow> a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" |
292 |
for a b :: nat |
|
66888 | 293 |
by (auto simp add: cong_def) |
31719 | 294 |
|
66380 | 295 |
lemma cong_less_imp_eq_int: "0 \<le> a \<Longrightarrow> a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" |
296 |
for a b :: int |
|
66888 | 297 |
by (auto simp add: cong_def) |
31719 | 298 |
|
66380 | 299 |
lemma cong_less_unique_nat: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
300 |
for a m :: nat |
|
66888 | 301 |
by (auto simp: cong_def) (metis mod_less_divisor mod_mod_trivial) |
31719 | 302 |
|
66380 | 303 |
lemma cong_less_unique_int: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
304 |
for a m :: int |
|
66888 | 305 |
by (auto simp: cong_def) (metis mod_mod_trivial pos_mod_conj) |
31719 | 306 |
|
66380 | 307 |
lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)" |
308 |
for a b :: int |
|
67087 | 309 |
by (fact cong_iff_lin) |
31719 | 310 |
|
66380 | 311 |
lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)" |
312 |
(is "?lhs = ?rhs") |
|
313 |
for a b :: nat |
|
314 |
proof |
|
315 |
assume ?lhs |
|
55371 | 316 |
show ?rhs |
317 |
proof (cases "b \<le> a") |
|
318 |
case True |
|
66380 | 319 |
with \<open>?lhs\<close> show ?rhs |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
320 |
by (metis cong_altdef_nat dvd_def le_add_diff_inverse add_0_right mult_0 mult.commute) |
55371 | 321 |
next |
322 |
case False |
|
66380 | 323 |
with \<open>?lhs\<close> show ?rhs |
66888 | 324 |
by (metis cong_def mult.commute nat_le_linear nat_mod_eq_lemma) |
55371 | 325 |
qed |
326 |
next |
|
327 |
assume ?rhs |
|
328 |
then show ?lhs |
|
66888 | 329 |
by (metis cong_def mult.commute nat_mod_eq_iff) |
55371 | 330 |
qed |
31719 | 331 |
|
66954 | 332 |
lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m" |
333 |
for a b :: nat |
|
334 |
by (auto simp add: cong_def) (metis gcd_red_nat) |
|
335 |
||
66380 | 336 |
lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m" |
337 |
for a b :: int |
|
66888 | 338 |
by (auto simp add: cong_def) (metis gcd_red_int) |
31719 | 339 |
|
66380 | 340 |
lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m" |
341 |
for a b :: nat |
|
67085 | 342 |
by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq_nat) |
31719 | 343 |
|
66380 | 344 |
lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m" |
345 |
for a b :: int |
|
67085 | 346 |
by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq_int) |
31719 | 347 |
|
66380 | 348 |
lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)" |
349 |
for a b :: nat |
|
66888 | 350 |
by simp |
31719 | 351 |
|
66380 | 352 |
lemma cong_cong_mod_int: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)" |
353 |
for a b :: int |
|
66888 | 354 |
by simp |
31719 | 355 |
|
66380 | 356 |
lemma cong_minus_int [iff]: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)" |
357 |
for a b :: int |
|
67087 | 358 |
by (fact cong_modulus_minus_iff) |
31719 | 359 |
|
66380 | 360 |
lemma cong_add_lcancel_nat: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
361 |
for a x y :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
362 |
by (simp add: cong_iff_lin_nat) |
31719 | 363 |
|
66380 | 364 |
lemma cong_add_lcancel_int: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
365 |
for a x y :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
366 |
by (simp add: cong_iff_lin_int) |
31719 | 367 |
|
66380 | 368 |
lemma cong_add_rcancel_nat: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
369 |
for a x y :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
370 |
by (simp add: cong_iff_lin_nat) |
31719 | 371 |
|
66380 | 372 |
lemma cong_add_rcancel_int: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
373 |
for a x y :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
374 |
by (simp add: cong_iff_lin_int) |
31719 | 375 |
|
66380 | 376 |
lemma cong_add_lcancel_0_nat: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
377 |
for a x :: nat |
|
67085 | 378 |
using cong_add_lcancel_nat [of a x 0 n] by simp |
31719 | 379 |
|
66380 | 380 |
lemma cong_add_lcancel_0_int: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
381 |
for a x :: int |
|
67085 | 382 |
using cong_add_lcancel_int [of a x 0 n] by simp |
31719 | 383 |
|
66380 | 384 |
lemma cong_add_rcancel_0_nat: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
385 |
for a x :: nat |
|
67085 | 386 |
using cong_add_rcancel_nat [of x a 0 n] by simp |
66380 | 387 |
|
388 |
lemma cong_add_rcancel_0_int: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
|
389 |
for a x :: int |
|
67085 | 390 |
using cong_add_rcancel_int [of x a 0 n] by simp |
66380 | 391 |
|
392 |
lemma cong_dvd_modulus_nat: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)" |
|
393 |
for x y :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
394 |
apply (auto simp add: cong_iff_lin_nat dvd_def) |
66380 | 395 |
apply (rule_tac x= "k1 * k" in exI) |
396 |
apply (rule_tac x= "k2 * k" in exI) |
|
36350 | 397 |
apply (simp add: field_simps) |
44872 | 398 |
done |
31719 | 399 |
|
66380 | 400 |
lemma cong_dvd_modulus_int: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)" |
401 |
for x y :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
402 |
by (auto simp add: cong_altdef_int dvd_def) |
31719 | 403 |
|
66380 | 404 |
lemma cong_to_1_nat: |
405 |
fixes a :: nat |
|
406 |
assumes "[a = 1] (mod n)" |
|
407 |
shows "n dvd (a - 1)" |
|
408 |
proof (cases "a = 0") |
|
409 |
case True |
|
410 |
then show ?thesis by force |
|
411 |
next |
|
412 |
case False |
|
413 |
with assms show ?thesis by (metis cong_altdef_nat leI less_one) |
|
414 |
qed |
|
415 |
||
416 |
lemma cong_0_1_nat': "[0 = Suc 0] (mod n) \<longleftrightarrow> n = Suc 0" |
|
66888 | 417 |
by (auto simp: cong_def) |
66380 | 418 |
|
419 |
lemma cong_0_1_nat: "[0 = 1] (mod n) \<longleftrightarrow> n = 1" |
|
420 |
for n :: nat |
|
66888 | 421 |
by (auto simp: cong_def) |
66380 | 422 |
|
423 |
lemma cong_0_1_int: "[0 = 1] (mod n) \<longleftrightarrow> n = 1 \<or> n = - 1" |
|
424 |
for n :: int |
|
66888 | 425 |
by (auto simp: cong_def zmult_eq_1_iff) |
66380 | 426 |
|
427 |
lemma cong_to_1'_nat: "[a = 1] (mod n) \<longleftrightarrow> a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)" |
|
428 |
for a :: nat |
|
429 |
by (metis add.right_neutral cong_0_1_nat cong_iff_lin_nat cong_to_1_nat |
|
430 |
dvd_div_mult_self leI le_add_diff_inverse less_one mult_eq_if) |
|
431 |
||
432 |
lemma cong_le_nat: "y \<le> x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)" |
|
433 |
for x y :: nat |
|
66837 | 434 |
by (auto simp add: cong_altdef_nat le_imp_diff_is_add elim!: dvdE) |
66380 | 435 |
|
436 |
lemma cong_solve_nat: |
|
437 |
fixes a :: nat |
|
438 |
assumes "a \<noteq> 0" |
|
439 |
shows "\<exists>x. [a * x = gcd a n] (mod n)" |
|
440 |
proof (cases "n = 0") |
|
441 |
case True |
|
442 |
then show ?thesis by force |
|
443 |
next |
|
444 |
case False |
|
445 |
then show ?thesis |
|
446 |
using bezout_nat [of a n, OF \<open>a \<noteq> 0\<close>] |
|
66888 | 447 |
by auto (metis cong_add_rcancel_0_nat cong_mult_self_left) |
66380 | 448 |
qed |
449 |
||
450 |
lemma cong_solve_int: "a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)" |
|
451 |
for a :: int |
|
452 |
apply (cases "n = 0") |
|
453 |
apply (cases "a \<ge> 0") |
|
454 |
apply auto |
|
455 |
apply (rule_tac x = "-1" in exI) |
|
456 |
apply auto |
|
457 |
apply (insert bezout_int [of a n], auto) |
|
458 |
apply (metis cong_iff_lin_int mult.commute) |
|
44872 | 459 |
done |
31719 | 460 |
|
44872 | 461 |
lemma cong_solve_dvd_nat: |
66380 | 462 |
fixes a :: nat |
463 |
assumes a: "a \<noteq> 0" and b: "gcd a n dvd d" |
|
464 |
shows "\<exists>x. [a * x = d] (mod n)" |
|
31719 | 465 |
proof - |
44872 | 466 |
from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)" |
31719 | 467 |
by auto |
44872 | 468 |
then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" |
66888 | 469 |
using cong_scalar_left by blast |
31719 | 470 |
also from b have "(d div gcd a n) * gcd a n = d" |
471 |
by (rule dvd_div_mult_self) |
|
472 |
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" |
|
473 |
by auto |
|
474 |
finally show ?thesis |
|
475 |
by auto |
|
476 |
qed |
|
477 |
||
44872 | 478 |
lemma cong_solve_dvd_int: |
31719 | 479 |
assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d" |
66380 | 480 |
shows "\<exists>x. [a * x = d] (mod n)" |
31719 | 481 |
proof - |
44872 | 482 |
from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)" |
31719 | 483 |
by auto |
44872 | 484 |
then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" |
66888 | 485 |
using cong_scalar_left by blast |
31719 | 486 |
also from b have "(d div gcd a n) * gcd a n = d" |
487 |
by (rule dvd_div_mult_self) |
|
488 |
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" |
|
489 |
by auto |
|
490 |
finally show ?thesis |
|
491 |
by auto |
|
492 |
qed |
|
493 |
||
66380 | 494 |
lemma cong_solve_coprime_nat: |
67051 | 495 |
"\<exists>x. [a * x = Suc 0] (mod n)" if "coprime a n" |
496 |
using that cong_solve_nat [of a n] by (cases "a = 0") simp_all |
|
31719 | 497 |
|
67051 | 498 |
lemma cong_solve_coprime_int: |
499 |
"\<exists>x. [a * x = 1] (mod n)" if "coprime a n" for a n x :: int |
|
500 |
using that cong_solve_int [of a n] by (cases "a = 0") |
|
501 |
(auto simp add: zabs_def split: if_splits) |
|
55161 | 502 |
|
62349
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
503 |
lemma coprime_iff_invertible_nat: |
67085 | 504 |
"coprime a m \<longleftrightarrow> (\<exists>x. [a * x = Suc 0] (mod m))" (is "?P \<longleftrightarrow> ?Q") |
505 |
proof |
|
506 |
assume ?P then show ?Q |
|
507 |
by (auto dest!: cong_solve_coprime_nat) |
|
508 |
next |
|
509 |
assume ?Q |
|
510 |
then obtain b where "[a * b = Suc 0] (mod m)" |
|
511 |
by blast |
|
512 |
with coprime_mod_left_iff [of m "a * b"] show ?P |
|
513 |
by (cases "m = 0 \<or> m = 1") |
|
514 |
(unfold cong_def, auto simp add: cong_def) |
|
515 |
qed |
|
66380 | 516 |
|
67051 | 517 |
lemma coprime_iff_invertible_int: |
67085 | 518 |
"coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))" (is "?P \<longleftrightarrow> ?Q") for m :: int |
519 |
proof |
|
520 |
assume ?P then show ?Q |
|
521 |
by (auto dest: cong_solve_coprime_int) |
|
522 |
next |
|
523 |
assume ?Q |
|
524 |
then obtain b where "[a * b = 1] (mod m)" |
|
525 |
by blast |
|
526 |
with coprime_mod_left_iff [of m "a * b"] show ?P |
|
527 |
by (cases "m = 0 \<or> m = 1") |
|
528 |
(unfold cong_def, auto simp add: zmult_eq_1_iff) |
|
529 |
qed |
|
31719 | 530 |
|
66380 | 531 |
lemma coprime_iff_invertible'_nat: |
532 |
"m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))" |
|
55161 | 533 |
apply (subst coprime_iff_invertible_nat) |
66380 | 534 |
apply auto |
66888 | 535 |
apply (auto simp add: cong_def) |
55161 | 536 |
apply (metis mod_less_divisor mod_mult_right_eq) |
44872 | 537 |
done |
31719 | 538 |
|
66380 | 539 |
lemma coprime_iff_invertible'_int: |
540 |
"m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = 1] (mod m))" |
|
541 |
for m :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
542 |
apply (subst coprime_iff_invertible_int) |
66888 | 543 |
apply (auto simp add: cong_def) |
55371 | 544 |
apply (metis mod_mult_right_eq pos_mod_conj) |
44872 | 545 |
done |
31719 | 546 |
|
66380 | 547 |
lemma cong_cong_lcm_nat: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" |
548 |
for x y :: nat |
|
44872 | 549 |
apply (cases "y \<le> x") |
66888 | 550 |
apply (simp add: cong_altdef_nat) |
551 |
apply (meson cong_altdef_nat cong_sym lcm_least_iff nat_le_linear) |
|
44872 | 552 |
done |
31719 | 553 |
|
66380 | 554 |
lemma cong_cong_lcm_int: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" |
555 |
for x y :: int |
|
556 |
by (auto simp add: cong_altdef_int lcm_least) |
|
31719 | 557 |
|
66888 | 558 |
lemma cong_cong_prod_coprime_nat: |
559 |
"[x = y] (mod (\<Prod>i\<in>A. m i))" if |
|
560 |
"(\<forall>i\<in>A. [(x::nat) = y] (mod m i))" |
|
561 |
and "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))" |
|
562 |
using that apply (induct A rule: infinite_finite_induct) |
|
563 |
apply auto |
|
67051 | 564 |
apply (metis coprime_cong_mult_nat prod_coprime_right) |
44872 | 565 |
done |
31719 | 566 |
|
67051 | 567 |
lemma cong_cong_prod_coprime_int: |
66888 | 568 |
"[x = y] (mod (\<Prod>i\<in>A. m i))" if |
569 |
"(\<forall>i\<in>A. [(x::int) = y] (mod m i))" |
|
570 |
"(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))" |
|
571 |
using that apply (induct A rule: infinite_finite_induct) |
|
67051 | 572 |
apply auto |
573 |
apply (metis coprime_cong_mult_int prod_coprime_right) |
|
44872 | 574 |
done |
31719 | 575 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
576 |
lemma binary_chinese_remainder_nat: |
66380 | 577 |
fixes m1 m2 :: nat |
578 |
assumes a: "coprime m1 m2" |
|
579 |
shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
31719 | 580 |
proof - |
67086 | 581 |
have "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
582 |
proof - |
|
583 |
from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" |
|
584 |
by auto |
|
585 |
from a have b: "coprime m2 m1" |
|
586 |
by (simp add: ac_simps) |
|
587 |
from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" |
|
588 |
by auto |
|
589 |
have "[m1 * x1 = 0] (mod m1)" |
|
590 |
by (simp add: cong_mult_self_left) |
|
591 |
moreover have "[m2 * x2 = 0] (mod m2)" |
|
592 |
by (simp add: cong_mult_self_left) |
|
593 |
ultimately show ?thesis |
|
594 |
using 1 2 by blast |
|
595 |
qed |
|
596 |
then obtain b1 b2 |
|
66380 | 597 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" |
598 |
and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
31719 | 599 |
by blast |
600 |
let ?x = "u1 * b1 + u2 * b2" |
|
601 |
have "[?x = u1 * 1 + u2 * 0] (mod m1)" |
|
66888 | 602 |
using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast |
44872 | 603 |
then have "[?x = u1] (mod m1)" by simp |
31719 | 604 |
have "[?x = u1 * 0 + u2 * 1] (mod m2)" |
66888 | 605 |
using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left by blast |
66380 | 606 |
then have "[?x = u2] (mod m2)" |
607 |
by simp |
|
608 |
with \<open>[?x = u1] (mod m1)\<close> show ?thesis |
|
609 |
by blast |
|
31719 | 610 |
qed |
611 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
612 |
lemma binary_chinese_remainder_int: |
66380 | 613 |
fixes m1 m2 :: int |
614 |
assumes a: "coprime m1 m2" |
|
615 |
shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
31719 | 616 |
proof - |
67086 | 617 |
have "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
618 |
proof - |
|
619 |
from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" |
|
620 |
by auto |
|
621 |
from a have b: "coprime m2 m1" |
|
622 |
by (simp add: ac_simps) |
|
623 |
from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" |
|
624 |
by auto |
|
625 |
have "[m1 * x1 = 0] (mod m1)" |
|
626 |
by (simp add: cong_mult_self_left) |
|
627 |
moreover have "[m2 * x2 = 0] (mod m2)" |
|
628 |
by (simp add: cong_mult_self_left) |
|
629 |
ultimately show ?thesis |
|
630 |
using 1 2 by blast |
|
631 |
qed |
|
632 |
then obtain b1 b2 |
|
66380 | 633 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" |
634 |
and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
31719 | 635 |
by blast |
636 |
let ?x = "u1 * b1 + u2 * b2" |
|
637 |
have "[?x = u1 * 1 + u2 * 0] (mod m1)" |
|
66888 | 638 |
using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast |
44872 | 639 |
then have "[?x = u1] (mod m1)" by simp |
31719 | 640 |
have "[?x = u1 * 0 + u2 * 1] (mod m2)" |
66888 | 641 |
using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left by blast |
44872 | 642 |
then have "[?x = u2] (mod m2)" by simp |
66380 | 643 |
with \<open>[?x = u1] (mod m1)\<close> show ?thesis |
644 |
by blast |
|
31719 | 645 |
qed |
646 |
||
66380 | 647 |
lemma cong_modulus_mult_nat: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)" |
648 |
for x y :: nat |
|
44872 | 649 |
apply (cases "y \<le> x") |
67085 | 650 |
apply (auto simp add: cong_altdef_nat elim: dvd_mult_left) |
651 |
apply (metis cong_def mod_mult_cong_right) |
|
44872 | 652 |
done |
31719 | 653 |
|
66380 | 654 |
lemma cong_modulus_mult_int: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)" |
655 |
for x y :: int |
|
44872 | 656 |
apply (simp add: cong_altdef_int) |
31719 | 657 |
apply (erule dvd_mult_left) |
44872 | 658 |
done |
31719 | 659 |
|
66380 | 660 |
lemma cong_less_modulus_unique_nat: "[x = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y" |
661 |
for x y :: nat |
|
66888 | 662 |
by (simp add: cong_def) |
31719 | 663 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
664 |
lemma binary_chinese_remainder_unique_nat: |
66380 | 665 |
fixes m1 m2 :: nat |
666 |
assumes a: "coprime m1 m2" |
|
44872 | 667 |
and nz: "m1 \<noteq> 0" "m2 \<noteq> 0" |
63901 | 668 |
shows "\<exists>!x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
31719 | 669 |
proof - |
66380 | 670 |
from binary_chinese_remainder_nat [OF a] obtain y |
671 |
where "[y = u1] (mod m1)" and "[y = u2] (mod m2)" |
|
31719 | 672 |
by blast |
673 |
let ?x = "y mod (m1 * m2)" |
|
674 |
from nz have less: "?x < m1 * m2" |
|
44872 | 675 |
by auto |
66380 | 676 |
have 1: "[?x = u1] (mod m1)" |
66888 | 677 |
apply (rule cong_trans) |
66380 | 678 |
prefer 2 |
679 |
apply (rule \<open>[y = u1] (mod m1)\<close>) |
|
66888 | 680 |
apply (rule cong_modulus_mult_nat [of _ _ _ m2]) |
681 |
apply simp |
|
31719 | 682 |
done |
66380 | 683 |
have 2: "[?x = u2] (mod m2)" |
66888 | 684 |
apply (rule cong_trans) |
66380 | 685 |
prefer 2 |
686 |
apply (rule \<open>[y = u2] (mod m2)\<close>) |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
687 |
apply (subst mult.commute) |
66888 | 688 |
apply (rule cong_modulus_mult_nat [of _ _ _ m1]) |
689 |
apply simp |
|
31719 | 690 |
done |
66380 | 691 |
have "\<forall>z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x" |
44872 | 692 |
proof clarify |
31719 | 693 |
fix z |
694 |
assume "z < m1 * m2" |
|
695 |
assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)" |
|
696 |
have "[?x = z] (mod m1)" |
|
66888 | 697 |
apply (rule cong_trans) |
66380 | 698 |
apply (rule \<open>[?x = u1] (mod m1)\<close>) |
66888 | 699 |
apply (rule cong_sym) |
60526 | 700 |
apply (rule \<open>[z = u1] (mod m1)\<close>) |
31719 | 701 |
done |
702 |
moreover have "[?x = z] (mod m2)" |
|
66888 | 703 |
apply (rule cong_trans) |
66380 | 704 |
apply (rule \<open>[?x = u2] (mod m2)\<close>) |
66888 | 705 |
apply (rule cong_sym) |
60526 | 706 |
apply (rule \<open>[z = u2] (mod m2)\<close>) |
31719 | 707 |
done |
708 |
ultimately have "[?x = z] (mod m1 * m2)" |
|
66888 | 709 |
using a by (auto intro: coprime_cong_mult_nat simp add: mod_mult_cong_left mod_mult_cong_right) |
60526 | 710 |
with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x" |
67085 | 711 |
by (auto simp add: cong_def) |
44872 | 712 |
qed |
66380 | 713 |
with less 1 2 show ?thesis by auto |
31719 | 714 |
qed |
715 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
716 |
lemma chinese_remainder_nat: |
44872 | 717 |
fixes A :: "'a set" |
718 |
and m :: "'a \<Rightarrow> nat" |
|
719 |
and u :: "'a \<Rightarrow> nat" |
|
720 |
assumes fin: "finite A" |
|
66380 | 721 |
and cop: "\<forall>i \<in> A. \<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)" |
722 |
shows "\<exists>x. \<forall>i \<in> A. [x = u i] (mod m i)" |
|
31719 | 723 |
proof - |
67086 | 724 |
have "\<exists>b. (\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))" |
725 |
proof (rule finite_set_choice, rule fin, rule ballI) |
|
726 |
fix i |
|
727 |
assume "i \<in> A" |
|
728 |
with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)" |
|
729 |
by (intro prod_coprime_left) auto |
|
730 |
then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (mod m i)" |
|
731 |
by (elim cong_solve_coprime_nat) |
|
732 |
then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)" |
|
733 |
by auto |
|
734 |
moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))" |
|
735 |
by (simp add: cong_0_iff) |
|
736 |
ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))" |
|
737 |
by blast |
|
738 |
qed |
|
739 |
then obtain b where b: "\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))" |
|
31719 | 740 |
by blast |
61954 | 741 |
let ?x = "\<Sum>i\<in>A. (u i) * (b i)" |
66380 | 742 |
show ?thesis |
31719 | 743 |
proof (rule exI, clarify) |
744 |
fix i |
|
66380 | 745 |
assume a: "i \<in> A" |
44872 | 746 |
show "[?x = u i] (mod m i)" |
31719 | 747 |
proof - |
66380 | 748 |
from fin a have "?x = (\<Sum>j \<in> {i}. u j * b j) + (\<Sum>j \<in> A - {i}. u j * b j)" |
749 |
by (subst sum.union_disjoint [symmetric]) (auto intro: sum.cong) |
|
61954 | 750 |
then have "[?x = u i * b i + (\<Sum>j \<in> A - {i}. u j * b j)] (mod m i)" |
31719 | 751 |
by auto |
61954 | 752 |
also have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) = |
753 |
u i * 1 + (\<Sum>j \<in> A - {i}. u j * 0)] (mod m i)" |
|
66888 | 754 |
apply (rule cong_add) |
755 |
apply (rule cong_scalar_left) |
|
66380 | 756 |
using b a apply blast |
66888 | 757 |
apply (rule cong_sum) |
758 |
apply (rule cong_scalar_left) |
|
67085 | 759 |
using b apply (auto simp add: mod_eq_0_iff_dvd cong_def) |
760 |
apply (rule dvd_trans [of _ "prod m (A - {x})" "b x" for x]) |
|
761 |
using a fin apply auto |
|
31719 | 762 |
done |
763 |
finally show ?thesis |
|
764 |
by simp |
|
765 |
qed |
|
766 |
qed |
|
767 |
qed |
|
768 |
||
66888 | 769 |
lemma coprime_cong_prod_nat: |
770 |
"[x = y] (mod (\<Prod>i\<in>A. m i))" |
|
771 |
if "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
|
772 |
and "\<forall>i\<in>A. [x = y] (mod m i)" for x y :: nat |
|
773 |
using that apply (induct A rule: infinite_finite_induct) |
|
67051 | 774 |
apply auto |
775 |
apply (metis coprime_cong_mult_nat prod_coprime_right) |
|
44872 | 776 |
done |
31719 | 777 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
778 |
lemma chinese_remainder_unique_nat: |
44872 | 779 |
fixes A :: "'a set" |
780 |
and m :: "'a \<Rightarrow> nat" |
|
781 |
and u :: "'a \<Rightarrow> nat" |
|
782 |
assumes fin: "finite A" |
|
61954 | 783 |
and nz: "\<forall>i\<in>A. m i \<noteq> 0" |
66380 | 784 |
and cop: "\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)" |
63901 | 785 |
shows "\<exists>!x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))" |
31719 | 786 |
proof - |
44872 | 787 |
from chinese_remainder_nat [OF fin cop] |
66380 | 788 |
obtain y where one: "(\<forall>i\<in>A. [y = u i] (mod m i))" |
31719 | 789 |
by blast |
61954 | 790 |
let ?x = "y mod (\<Prod>i\<in>A. m i)" |
791 |
from fin nz have prodnz: "(\<Prod>i\<in>A. m i) \<noteq> 0" |
|
31719 | 792 |
by auto |
61954 | 793 |
then have less: "?x < (\<Prod>i\<in>A. m i)" |
31719 | 794 |
by auto |
66380 | 795 |
have cong: "\<forall>i\<in>A. [?x = u i] (mod m i)" |
67085 | 796 |
using fin one |
797 |
by (auto simp add: cong_def dvd_prod_eqI mod_mod_cancel) |
|
66380 | 798 |
have unique: "\<forall>z. z < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [z = u i] (mod m i)) \<longrightarrow> z = ?x" |
799 |
proof clarify |
|
31719 | 800 |
fix z |
61954 | 801 |
assume zless: "z < (\<Prod>i\<in>A. m i)" |
66380 | 802 |
assume zcong: "(\<forall>i\<in>A. [z = u i] (mod m i))" |
803 |
have "\<forall>i\<in>A. [?x = z] (mod m i)" |
|
67085 | 804 |
using cong zcong by (auto simp add: cong_def) |
61954 | 805 |
with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))" |
67085 | 806 |
by (intro coprime_cong_prod_nat) auto |
31719 | 807 |
with zless less show "z = ?x" |
67085 | 808 |
by (auto simp add: cong_def) |
44872 | 809 |
qed |
66380 | 810 |
from less cong unique show ?thesis |
811 |
by blast |
|
31719 | 812 |
qed |
813 |
||
814 |
end |