author | paulson <lp15@cam.ac.uk> |
Mon, 19 Feb 2018 16:44:45 +0000 | |
changeset 67673 | c8caefb20564 |
parent 67115 | 2977773a481c |
child 68707 | 5b269897df9d |
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 |
||
67115 | 157 |
lemma cong_modulus_minus_iff [iff]: |
67087 | 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 |
||
67115 | 177 |
lemma cong_add_lcancel: |
178 |
"[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
|
179 |
by (simp add: cong_iff_lin algebra_simps) |
|
180 |
||
181 |
lemma cong_add_rcancel: |
|
182 |
"[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
|
183 |
by (simp add: cong_iff_lin algebra_simps) |
|
184 |
||
185 |
lemma cong_add_lcancel_0: |
|
186 |
"[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
|
187 |
using cong_add_lcancel [of a x 0 n] by simp |
|
188 |
||
189 |
lemma cong_add_rcancel_0: |
|
190 |
"[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
|
191 |
using cong_add_rcancel [of x a 0 n] by simp |
|
192 |
||
193 |
lemma cong_dvd_modulus: |
|
194 |
"[x = y] (mod n)" if "[x = y] (mod m)" and "n dvd m" |
|
195 |
using that by (auto intro: dvd_trans simp add: cong_iff_dvd_diff) |
|
196 |
||
197 |
lemma cong_modulus_mult: |
|
198 |
"[x = y] (mod m)" if "[x = y] (mod m * n)" |
|
199 |
using that by (simp add: cong_iff_dvd_diff) (rule dvd_mult_left) |
|
200 |
||
31719 | 201 |
end |
202 |
||
67115 | 203 |
lemma cong_abs [simp]: |
204 |
"[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)" |
|
205 |
for x y :: "'a :: {unique_euclidean_ring, linordered_idom}" |
|
206 |
by (simp add: cong_iff_dvd_diff) |
|
207 |
||
208 |
lemma cong_square: |
|
209 |
"prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)" |
|
210 |
for a p :: "'a :: {normalization_semidom, linordered_idom, unique_euclidean_ring}" |
|
211 |
by (auto simp add: cong_iff_dvd_diff square_diff_one_factored dest: prime_dvd_multD) |
|
212 |
||
213 |
lemma cong_mult_rcancel: |
|
214 |
"[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)" |
|
215 |
if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}" |
|
216 |
using that by (auto simp add: cong_iff_dvd_diff left_diff_distrib [symmetric] ac_simps coprime_dvd_mult_right_iff) |
|
217 |
||
218 |
lemma cong_mult_lcancel: |
|
219 |
"[k * a = k * b] (mod m) = [a = b] (mod m)" |
|
220 |
if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}" |
|
221 |
using that cong_mult_rcancel [of k m a b] by (simp add: ac_simps) |
|
222 |
||
223 |
lemma coprime_cong_mult: |
|
224 |
"[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)" |
|
225 |
for a b :: "'a :: {unique_euclidean_ring, semiring_gcd}" |
|
226 |
by (simp add: cong_iff_dvd_diff divides_mult) |
|
227 |
||
228 |
lemma cong_gcd_eq: |
|
229 |
"gcd a m = gcd b m" if "[a = b] (mod m)" |
|
230 |
for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}" |
|
231 |
proof (cases "m = 0") |
|
232 |
case True |
|
233 |
with that show ?thesis |
|
234 |
by simp |
|
235 |
next |
|
236 |
case False |
|
237 |
moreover have "gcd (a mod m) m = gcd (b mod m) m" |
|
238 |
using that by (simp add: cong_def) |
|
239 |
ultimately show ?thesis |
|
240 |
by simp |
|
241 |
qed |
|
242 |
||
243 |
lemma cong_imp_coprime: |
|
244 |
"[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m" |
|
245 |
for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}" |
|
246 |
by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq) |
|
247 |
||
248 |
lemma cong_cong_prod_coprime: |
|
249 |
"[x = y] (mod (\<Prod>i\<in>A. m i))" if |
|
250 |
"(\<forall>i\<in>A. [x = y] (mod m i))" |
|
251 |
"(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))" |
|
252 |
for x y :: "'a :: {unique_euclidean_ring, semiring_gcd}" |
|
253 |
using that by (induct A rule: infinite_finite_induct) |
|
254 |
(auto intro!: coprime_cong_mult prod_coprime_right) |
|
255 |
||
66380 | 256 |
|
66888 | 257 |
subsection \<open>Congruences on @{typ nat} and @{typ int}\<close> |
31719 | 258 |
|
66888 | 259 |
lemma cong_int_iff: |
260 |
"[int m = int q] (mod int n) \<longleftrightarrow> [m = q] (mod n)" |
|
261 |
by (simp add: cong_def of_nat_mod [symmetric]) |
|
262 |
||
263 |
lemma cong_Suc_0 [simp, presburger]: |
|
264 |
"[m = n] (mod Suc 0)" |
|
265 |
using cong_1 [of m n] by simp |
|
31719 | 266 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
267 |
lemma cong_diff_nat: |
66888 | 268 |
"[a - c = b - d] (mod m)" if "[a = b] (mod m)" "[c = d] (mod m)" |
66954 | 269 |
and "a \<ge> c" "b \<ge> d" for a b c d m :: nat |
270 |
proof - |
|
271 |
have "[c + (a - c) = d + (b - d)] (mod m)" |
|
272 |
using that by simp |
|
273 |
with \<open>[c = d] (mod m)\<close> have "[c + (a - c) = c + (b - d)] (mod m)" |
|
274 |
using mod_add_cong by (auto simp add: cong_def) fastforce |
|
275 |
then show ?thesis |
|
276 |
by (simp add: cong_def nat_mod_eq_iff) |
|
277 |
qed |
|
31719 | 278 |
|
66888 | 279 |
lemma cong_diff_iff_cong_0_nat: |
66954 | 280 |
"[a - b = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)" if "a \<ge> b" for a b :: nat |
281 |
using that by (auto simp add: cong_def le_imp_diff_is_add dest: nat_mod_eq_lemma) |
|
31719 | 282 |
|
66954 | 283 |
lemma cong_diff_iff_cong_0_nat': |
284 |
"[nat \<bar>int a - int b\<bar> = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)" |
|
285 |
proof (cases "b \<le> a") |
|
286 |
case True |
|
287 |
then show ?thesis |
|
288 |
by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of b a m]) |
|
289 |
next |
|
290 |
case False |
|
291 |
then have "a \<le> b" |
|
292 |
by simp |
|
293 |
then show ?thesis |
|
294 |
by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of a b m]) |
|
295 |
(auto simp add: cong_def) |
|
296 |
qed |
|
297 |
||
298 |
lemma cong_altdef_nat: |
|
299 |
"a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)" |
|
66380 | 300 |
for a b :: nat |
66888 | 301 |
by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat) |
31719 | 302 |
|
66954 | 303 |
lemma cong_altdef_nat': |
304 |
"[a = b] (mod m) \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>" |
|
67085 | 305 |
using cong_diff_iff_cong_0_nat' [of a b m] |
306 |
by (simp only: cong_0_iff [symmetric]) |
|
66954 | 307 |
|
308 |
lemma cong_mult_rcancel_nat: |
|
309 |
"[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)" |
|
310 |
if "coprime k m" for a k m :: nat |
|
311 |
proof - |
|
312 |
have "[a * k = b * k] (mod m) \<longleftrightarrow> m dvd nat \<bar>int (a * k) - int (b * k)\<bar>" |
|
313 |
by (simp add: cong_altdef_nat') |
|
314 |
also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>(int a - int b) * int k\<bar>" |
|
315 |
by (simp add: algebra_simps) |
|
316 |
also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar> * k" |
|
317 |
by (simp add: abs_mult nat_times_as_int) |
|
318 |
also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>" |
|
67051 | 319 |
by (rule coprime_dvd_mult_left_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>) |
66954 | 320 |
also have "\<dots> \<longleftrightarrow> [a = b] (mod m)" |
321 |
by (simp add: cong_altdef_nat') |
|
322 |
finally show ?thesis . |
|
323 |
qed |
|
31719 | 324 |
|
66954 | 325 |
lemma cong_mult_lcancel_nat: |
326 |
"[k * a = k * b] (mod m) = [a = b] (mod m)" |
|
327 |
if "coprime k m" for a k m :: nat |
|
328 |
using that by (simp add: cong_mult_rcancel_nat ac_simps) |
|
31719 | 329 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
330 |
lemma coprime_cong_mult_nat: |
66380 | 331 |
"[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)" |
332 |
for a b :: nat |
|
66954 | 333 |
by (simp add: cong_altdef_nat' divides_mult) |
31719 | 334 |
|
66380 | 335 |
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" |
336 |
for a b :: nat |
|
66888 | 337 |
by (auto simp add: cong_def) |
31719 | 338 |
|
66380 | 339 |
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" |
340 |
for a b :: int |
|
66888 | 341 |
by (auto simp add: cong_def) |
31719 | 342 |
|
66380 | 343 |
lemma cong_less_unique_nat: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
344 |
for a m :: nat |
|
66888 | 345 |
by (auto simp: cong_def) (metis mod_less_divisor mod_mod_trivial) |
31719 | 346 |
|
66380 | 347 |
lemma cong_less_unique_int: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
348 |
for a m :: int |
|
66888 | 349 |
by (auto simp: cong_def) (metis mod_mod_trivial pos_mod_conj) |
31719 | 350 |
|
66380 | 351 |
lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)" |
352 |
(is "?lhs = ?rhs") |
|
353 |
for a b :: nat |
|
354 |
proof |
|
355 |
assume ?lhs |
|
55371 | 356 |
show ?rhs |
357 |
proof (cases "b \<le> a") |
|
358 |
case True |
|
66380 | 359 |
with \<open>?lhs\<close> show ?rhs |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
360 |
by (metis cong_altdef_nat dvd_def le_add_diff_inverse add_0_right mult_0 mult.commute) |
55371 | 361 |
next |
362 |
case False |
|
66380 | 363 |
with \<open>?lhs\<close> show ?rhs |
66888 | 364 |
by (metis cong_def mult.commute nat_le_linear nat_mod_eq_lemma) |
55371 | 365 |
qed |
366 |
next |
|
367 |
assume ?rhs |
|
368 |
then show ?lhs |
|
66888 | 369 |
by (metis cong_def mult.commute nat_mod_eq_iff) |
55371 | 370 |
qed |
31719 | 371 |
|
66380 | 372 |
lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)" |
373 |
for a b :: nat |
|
66888 | 374 |
by simp |
31719 | 375 |
|
66380 | 376 |
lemma cong_cong_mod_int: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)" |
377 |
for a b :: int |
|
66888 | 378 |
by simp |
31719 | 379 |
|
66380 | 380 |
lemma cong_add_lcancel_nat: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
381 |
for a x y :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
382 |
by (simp add: cong_iff_lin_nat) |
31719 | 383 |
|
66380 | 384 |
lemma cong_add_rcancel_nat: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
385 |
for a x y :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
386 |
by (simp add: cong_iff_lin_nat) |
31719 | 387 |
|
66380 | 388 |
lemma cong_add_lcancel_0_nat: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
389 |
for a x :: nat |
|
67085 | 390 |
using cong_add_lcancel_nat [of a x 0 n] by simp |
31719 | 391 |
|
66380 | 392 |
lemma cong_add_rcancel_0_nat: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
393 |
for a x :: nat |
|
67085 | 394 |
using cong_add_rcancel_nat [of x a 0 n] by simp |
66380 | 395 |
|
396 |
lemma cong_dvd_modulus_nat: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)" |
|
397 |
for x y :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
398 |
apply (auto simp add: cong_iff_lin_nat dvd_def) |
66380 | 399 |
apply (rule_tac x= "k1 * k" in exI) |
400 |
apply (rule_tac x= "k2 * k" in exI) |
|
36350 | 401 |
apply (simp add: field_simps) |
44872 | 402 |
done |
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) |
|
67115 | 458 |
apply (metis cong_iff_lin 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 |
|
67115 | 556 |
by (auto simp add: cong_iff_dvd_diff lcm_least) |
31719 | 557 |
|
66888 | 558 |
lemma cong_cong_prod_coprime_nat: |
559 |
"[x = y] (mod (\<Prod>i\<in>A. m i))" if |
|
67115 | 560 |
"(\<forall>i\<in>A. [x = y] (mod m i))" |
66888 | 561 |
"(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))" |
67115 | 562 |
for x y :: nat |
563 |
using that by (induct A rule: infinite_finite_induct) |
|
564 |
(auto intro!: coprime_cong_mult_nat prod_coprime_right) |
|
31719 | 565 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
566 |
lemma binary_chinese_remainder_nat: |
66380 | 567 |
fixes m1 m2 :: nat |
568 |
assumes a: "coprime m1 m2" |
|
569 |
shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
31719 | 570 |
proof - |
67086 | 571 |
have "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
572 |
proof - |
|
573 |
from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" |
|
574 |
by auto |
|
575 |
from a have b: "coprime m2 m1" |
|
576 |
by (simp add: ac_simps) |
|
577 |
from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" |
|
578 |
by auto |
|
579 |
have "[m1 * x1 = 0] (mod m1)" |
|
580 |
by (simp add: cong_mult_self_left) |
|
581 |
moreover have "[m2 * x2 = 0] (mod m2)" |
|
582 |
by (simp add: cong_mult_self_left) |
|
583 |
ultimately show ?thesis |
|
584 |
using 1 2 by blast |
|
585 |
qed |
|
586 |
then obtain b1 b2 |
|
66380 | 587 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" |
588 |
and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
31719 | 589 |
by blast |
590 |
let ?x = "u1 * b1 + u2 * b2" |
|
591 |
have "[?x = u1 * 1 + u2 * 0] (mod m1)" |
|
66888 | 592 |
using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast |
44872 | 593 |
then have "[?x = u1] (mod m1)" by simp |
31719 | 594 |
have "[?x = u1 * 0 + u2 * 1] (mod m2)" |
66888 | 595 |
using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left by blast |
66380 | 596 |
then have "[?x = u2] (mod m2)" |
597 |
by simp |
|
598 |
with \<open>[?x = u1] (mod m1)\<close> show ?thesis |
|
599 |
by blast |
|
31719 | 600 |
qed |
601 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
602 |
lemma binary_chinese_remainder_int: |
66380 | 603 |
fixes m1 m2 :: int |
604 |
assumes a: "coprime m1 m2" |
|
605 |
shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
31719 | 606 |
proof - |
67086 | 607 |
have "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
608 |
proof - |
|
609 |
from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" |
|
610 |
by auto |
|
611 |
from a have b: "coprime m2 m1" |
|
612 |
by (simp add: ac_simps) |
|
613 |
from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" |
|
614 |
by auto |
|
615 |
have "[m1 * x1 = 0] (mod m1)" |
|
616 |
by (simp add: cong_mult_self_left) |
|
617 |
moreover have "[m2 * x2 = 0] (mod m2)" |
|
618 |
by (simp add: cong_mult_self_left) |
|
619 |
ultimately show ?thesis |
|
620 |
using 1 2 by blast |
|
621 |
qed |
|
622 |
then obtain b1 b2 |
|
66380 | 623 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" |
624 |
and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
31719 | 625 |
by blast |
626 |
let ?x = "u1 * b1 + u2 * b2" |
|
627 |
have "[?x = u1 * 1 + u2 * 0] (mod m1)" |
|
66888 | 628 |
using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast |
44872 | 629 |
then have "[?x = u1] (mod m1)" by simp |
31719 | 630 |
have "[?x = u1 * 0 + u2 * 1] (mod m2)" |
66888 | 631 |
using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left by blast |
44872 | 632 |
then have "[?x = u2] (mod m2)" by simp |
66380 | 633 |
with \<open>[?x = u1] (mod m1)\<close> show ?thesis |
634 |
by blast |
|
31719 | 635 |
qed |
636 |
||
66380 | 637 |
lemma cong_modulus_mult_nat: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)" |
638 |
for x y :: nat |
|
44872 | 639 |
apply (cases "y \<le> x") |
67085 | 640 |
apply (auto simp add: cong_altdef_nat elim: dvd_mult_left) |
641 |
apply (metis cong_def mod_mult_cong_right) |
|
44872 | 642 |
done |
31719 | 643 |
|
66380 | 644 |
lemma cong_less_modulus_unique_nat: "[x = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y" |
645 |
for x y :: nat |
|
66888 | 646 |
by (simp add: cong_def) |
31719 | 647 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
648 |
lemma binary_chinese_remainder_unique_nat: |
66380 | 649 |
fixes m1 m2 :: nat |
650 |
assumes a: "coprime m1 m2" |
|
44872 | 651 |
and nz: "m1 \<noteq> 0" "m2 \<noteq> 0" |
63901 | 652 |
shows "\<exists>!x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
31719 | 653 |
proof - |
66380 | 654 |
from binary_chinese_remainder_nat [OF a] obtain y |
655 |
where "[y = u1] (mod m1)" and "[y = u2] (mod m2)" |
|
31719 | 656 |
by blast |
657 |
let ?x = "y mod (m1 * m2)" |
|
658 |
from nz have less: "?x < m1 * m2" |
|
44872 | 659 |
by auto |
66380 | 660 |
have 1: "[?x = u1] (mod m1)" |
66888 | 661 |
apply (rule cong_trans) |
66380 | 662 |
prefer 2 |
663 |
apply (rule \<open>[y = u1] (mod m1)\<close>) |
|
66888 | 664 |
apply (rule cong_modulus_mult_nat [of _ _ _ m2]) |
665 |
apply simp |
|
31719 | 666 |
done |
66380 | 667 |
have 2: "[?x = u2] (mod m2)" |
66888 | 668 |
apply (rule cong_trans) |
66380 | 669 |
prefer 2 |
670 |
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
|
671 |
apply (subst mult.commute) |
66888 | 672 |
apply (rule cong_modulus_mult_nat [of _ _ _ m1]) |
673 |
apply simp |
|
31719 | 674 |
done |
66380 | 675 |
have "\<forall>z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x" |
44872 | 676 |
proof clarify |
31719 | 677 |
fix z |
678 |
assume "z < m1 * m2" |
|
679 |
assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)" |
|
680 |
have "[?x = z] (mod m1)" |
|
66888 | 681 |
apply (rule cong_trans) |
66380 | 682 |
apply (rule \<open>[?x = u1] (mod m1)\<close>) |
66888 | 683 |
apply (rule cong_sym) |
60526 | 684 |
apply (rule \<open>[z = u1] (mod m1)\<close>) |
31719 | 685 |
done |
686 |
moreover have "[?x = z] (mod m2)" |
|
66888 | 687 |
apply (rule cong_trans) |
66380 | 688 |
apply (rule \<open>[?x = u2] (mod m2)\<close>) |
66888 | 689 |
apply (rule cong_sym) |
60526 | 690 |
apply (rule \<open>[z = u2] (mod m2)\<close>) |
31719 | 691 |
done |
692 |
ultimately have "[?x = z] (mod m1 * m2)" |
|
66888 | 693 |
using a by (auto intro: coprime_cong_mult_nat simp add: mod_mult_cong_left mod_mult_cong_right) |
60526 | 694 |
with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x" |
67085 | 695 |
by (auto simp add: cong_def) |
44872 | 696 |
qed |
66380 | 697 |
with less 1 2 show ?thesis by auto |
31719 | 698 |
qed |
699 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
700 |
lemma chinese_remainder_nat: |
44872 | 701 |
fixes A :: "'a set" |
702 |
and m :: "'a \<Rightarrow> nat" |
|
703 |
and u :: "'a \<Rightarrow> nat" |
|
704 |
assumes fin: "finite A" |
|
66380 | 705 |
and cop: "\<forall>i \<in> A. \<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)" |
706 |
shows "\<exists>x. \<forall>i \<in> A. [x = u i] (mod m i)" |
|
31719 | 707 |
proof - |
67086 | 708 |
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)))" |
709 |
proof (rule finite_set_choice, rule fin, rule ballI) |
|
710 |
fix i |
|
711 |
assume "i \<in> A" |
|
712 |
with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)" |
|
713 |
by (intro prod_coprime_left) auto |
|
714 |
then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (mod m i)" |
|
715 |
by (elim cong_solve_coprime_nat) |
|
716 |
then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)" |
|
717 |
by auto |
|
718 |
moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))" |
|
719 |
by (simp add: cong_0_iff) |
|
720 |
ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))" |
|
721 |
by blast |
|
722 |
qed |
|
723 |
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 | 724 |
by blast |
61954 | 725 |
let ?x = "\<Sum>i\<in>A. (u i) * (b i)" |
66380 | 726 |
show ?thesis |
31719 | 727 |
proof (rule exI, clarify) |
728 |
fix i |
|
66380 | 729 |
assume a: "i \<in> A" |
44872 | 730 |
show "[?x = u i] (mod m i)" |
31719 | 731 |
proof - |
66380 | 732 |
from fin a have "?x = (\<Sum>j \<in> {i}. u j * b j) + (\<Sum>j \<in> A - {i}. u j * b j)" |
733 |
by (subst sum.union_disjoint [symmetric]) (auto intro: sum.cong) |
|
61954 | 734 |
then have "[?x = u i * b i + (\<Sum>j \<in> A - {i}. u j * b j)] (mod m i)" |
31719 | 735 |
by auto |
61954 | 736 |
also have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) = |
737 |
u i * 1 + (\<Sum>j \<in> A - {i}. u j * 0)] (mod m i)" |
|
66888 | 738 |
apply (rule cong_add) |
739 |
apply (rule cong_scalar_left) |
|
66380 | 740 |
using b a apply blast |
66888 | 741 |
apply (rule cong_sum) |
742 |
apply (rule cong_scalar_left) |
|
67085 | 743 |
using b apply (auto simp add: mod_eq_0_iff_dvd cong_def) |
744 |
apply (rule dvd_trans [of _ "prod m (A - {x})" "b x" for x]) |
|
745 |
using a fin apply auto |
|
31719 | 746 |
done |
747 |
finally show ?thesis |
|
748 |
by simp |
|
749 |
qed |
|
750 |
qed |
|
751 |
qed |
|
752 |
||
66888 | 753 |
lemma coprime_cong_prod_nat: |
754 |
"[x = y] (mod (\<Prod>i\<in>A. m i))" |
|
755 |
if "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
|
756 |
and "\<forall>i\<in>A. [x = y] (mod m i)" for x y :: nat |
|
757 |
using that apply (induct A rule: infinite_finite_induct) |
|
67051 | 758 |
apply auto |
759 |
apply (metis coprime_cong_mult_nat prod_coprime_right) |
|
44872 | 760 |
done |
31719 | 761 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
762 |
lemma chinese_remainder_unique_nat: |
44872 | 763 |
fixes A :: "'a set" |
764 |
and m :: "'a \<Rightarrow> nat" |
|
765 |
and u :: "'a \<Rightarrow> nat" |
|
766 |
assumes fin: "finite A" |
|
61954 | 767 |
and nz: "\<forall>i\<in>A. m i \<noteq> 0" |
66380 | 768 |
and cop: "\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)" |
63901 | 769 |
shows "\<exists>!x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))" |
31719 | 770 |
proof - |
44872 | 771 |
from chinese_remainder_nat [OF fin cop] |
66380 | 772 |
obtain y where one: "(\<forall>i\<in>A. [y = u i] (mod m i))" |
31719 | 773 |
by blast |
61954 | 774 |
let ?x = "y mod (\<Prod>i\<in>A. m i)" |
775 |
from fin nz have prodnz: "(\<Prod>i\<in>A. m i) \<noteq> 0" |
|
31719 | 776 |
by auto |
61954 | 777 |
then have less: "?x < (\<Prod>i\<in>A. m i)" |
31719 | 778 |
by auto |
66380 | 779 |
have cong: "\<forall>i\<in>A. [?x = u i] (mod m i)" |
67085 | 780 |
using fin one |
781 |
by (auto simp add: cong_def dvd_prod_eqI mod_mod_cancel) |
|
66380 | 782 |
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" |
783 |
proof clarify |
|
31719 | 784 |
fix z |
61954 | 785 |
assume zless: "z < (\<Prod>i\<in>A. m i)" |
66380 | 786 |
assume zcong: "(\<forall>i\<in>A. [z = u i] (mod m i))" |
787 |
have "\<forall>i\<in>A. [?x = z] (mod m i)" |
|
67085 | 788 |
using cong zcong by (auto simp add: cong_def) |
61954 | 789 |
with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))" |
67085 | 790 |
by (intro coprime_cong_prod_nat) auto |
31719 | 791 |
with zless less show "z = ?x" |
67085 | 792 |
by (auto simp add: cong_def) |
44872 | 793 |
qed |
66380 | 794 |
from less cong unique show ?thesis |
795 |
by blast |
|
31719 | 796 |
qed |
797 |
||
67115 | 798 |
|
799 |
subsection \<open>Aliasses\<close> |
|
800 |
||
801 |
lemma cong_altdef_int: |
|
802 |
"[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)" |
|
803 |
for a b :: int |
|
804 |
by (fact cong_iff_dvd_diff) |
|
805 |
||
806 |
lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)" |
|
807 |
for a b :: int |
|
808 |
by (fact cong_iff_lin) |
|
809 |
||
810 |
lemma cong_minus_int: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)" |
|
811 |
for a b :: int |
|
812 |
by (fact cong_modulus_minus_iff) |
|
813 |
||
814 |
lemma cong_add_lcancel_int: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
|
815 |
for a x y :: int |
|
816 |
by (fact cong_add_lcancel) |
|
817 |
||
818 |
lemma cong_add_rcancel_int: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
|
819 |
for a x y :: int |
|
820 |
by (fact cong_add_rcancel) |
|
821 |
||
822 |
lemma cong_add_lcancel_0_int: |
|
823 |
"[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
|
824 |
for a x :: int |
|
825 |
by (fact cong_add_lcancel_0) |
|
826 |
||
827 |
lemma cong_add_rcancel_0_int: |
|
828 |
"[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
|
829 |
for a x :: int |
|
830 |
by (fact cong_add_rcancel_0) |
|
831 |
||
832 |
lemma cong_dvd_modulus_int: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)" |
|
833 |
for x y :: int |
|
834 |
by (fact cong_dvd_modulus) |
|
835 |
||
836 |
lemma cong_abs_int: |
|
837 |
"[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)" |
|
838 |
for x y :: int |
|
839 |
by (fact cong_abs) |
|
840 |
||
841 |
lemma cong_square_int: |
|
842 |
"prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)" |
|
843 |
for a :: int |
|
844 |
by (fact cong_square) |
|
845 |
||
846 |
lemma cong_mult_rcancel_int: |
|
847 |
"[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)" |
|
848 |
if "coprime k m" for a k m :: int |
|
849 |
using that by (fact cong_mult_rcancel) |
|
850 |
||
851 |
lemma cong_mult_lcancel_int: |
|
852 |
"[k * a = k * b] (mod m) = [a = b] (mod m)" |
|
853 |
if "coprime k m" for a k m :: int |
|
854 |
using that by (fact cong_mult_lcancel) |
|
855 |
||
856 |
lemma coprime_cong_mult_int: |
|
857 |
"[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)" |
|
858 |
for a b :: int |
|
859 |
by (fact coprime_cong_mult) |
|
860 |
||
861 |
lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m" |
|
862 |
for a b :: nat |
|
863 |
by (fact cong_gcd_eq) |
|
864 |
||
865 |
lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m" |
|
866 |
for a b :: int |
|
867 |
by (fact cong_gcd_eq) |
|
868 |
||
869 |
lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m" |
|
870 |
for a b :: nat |
|
871 |
by (fact cong_imp_coprime) |
|
872 |
||
873 |
lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m" |
|
874 |
for a b :: int |
|
875 |
by (fact cong_imp_coprime) |
|
876 |
||
877 |
lemma cong_cong_prod_coprime_int: |
|
878 |
"[x = y] (mod (\<Prod>i\<in>A. m i))" if |
|
879 |
"(\<forall>i\<in>A. [x = y] (mod m i))" |
|
880 |
"(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))" |
|
881 |
for x y :: int |
|
882 |
using that by (fact cong_cong_prod_coprime) |
|
883 |
||
884 |
lemma cong_modulus_mult_int: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)" |
|
885 |
for x y :: int |
|
886 |
by (fact cong_modulus_mult) |
|
887 |
||
31719 | 888 |
end |