author | haftmann |
Sun, 08 Oct 2017 22:28:22 +0200 | |
changeset 66817 | 0b12755ccbb2 |
parent 66453 | cc19f7ca2ed6 |
child 66837 | 6ba663ff2b1c |
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 |
||
63167 | 35 |
subsection \<open>Turn off \<open>One_nat_def\<close>\<close> |
31719 | 36 |
|
66380 | 37 |
lemma power_eq_one_eq_nat [simp]: "x^m = 1 \<longleftrightarrow> m = 0 \<or> x = 1" |
38 |
for x m :: nat |
|
44872 | 39 |
by (induct m) auto |
31719 | 40 |
|
41 |
declare mod_pos_pos_trivial [simp] |
|
42 |
||
43 |
||
60526 | 44 |
subsection \<open>Main definitions\<close> |
31719 | 45 |
|
46 |
class cong = |
|
66380 | 47 |
fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(()mod _'))") |
31719 | 48 |
begin |
49 |
||
58937 | 50 |
abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(()mod _'))") |
44872 | 51 |
where "notcong x y m \<equiv> \<not> cong x y m" |
31719 | 52 |
|
53 |
end |
|
54 |
||
66380 | 55 |
|
56 |
subsubsection \<open>Definitions for the natural numbers\<close> |
|
31719 | 57 |
|
58 |
instantiation nat :: cong |
|
44872 | 59 |
begin |
31719 | 60 |
|
44872 | 61 |
definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" |
66380 | 62 |
where "cong_nat x y m \<longleftrightarrow> x mod m = y mod m" |
31719 | 63 |
|
44872 | 64 |
instance .. |
31719 | 65 |
|
66 |
end |
|
67 |
||
68 |
||
66380 | 69 |
subsubsection \<open>Definitions for the integers\<close> |
31719 | 70 |
|
71 |
instantiation int :: cong |
|
44872 | 72 |
begin |
31719 | 73 |
|
44872 | 74 |
definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" |
66380 | 75 |
where "cong_int x y m \<longleftrightarrow> x mod m = y mod m" |
31719 | 76 |
|
44872 | 77 |
instance .. |
31719 | 78 |
|
79 |
end |
|
80 |
||
81 |
||
60526 | 82 |
subsection \<open>Set up Transfer\<close> |
31719 | 83 |
|
84 |
||
85 |
lemma transfer_nat_int_cong: |
|
66380 | 86 |
"x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> m \<ge> 0 \<Longrightarrow> [nat x = nat y] (mod (nat m)) \<longleftrightarrow> [x = y] (mod m)" |
87 |
for x y m :: int |
|
44872 | 88 |
unfolding cong_int_def cong_nat_def |
66817 | 89 |
by (metis int_nat_eq nat_mod_distrib zmod_int) |
31719 | 90 |
|
66380 | 91 |
declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong] |
31719 | 92 |
|
66380 | 93 |
lemma transfer_int_nat_cong: "[int x = int y] (mod (int m)) = [x = y] (mod m)" |
94 |
by (auto simp add: cong_int_def cong_nat_def) (auto simp add: zmod_int [symmetric]) |
|
31719 | 95 |
|
66380 | 96 |
declare transfer_morphism_int_nat [transfer add return: transfer_int_nat_cong] |
31719 | 97 |
|
98 |
||
60526 | 99 |
subsection \<open>Congruence\<close> |
31719 | 100 |
|
101 |
(* was zcong_0, etc. *) |
|
66380 | 102 |
lemma cong_0_nat [simp, presburger]: "[a = b] (mod 0) \<longleftrightarrow> a = b" |
103 |
for a b :: nat |
|
104 |
by (auto simp: cong_nat_def) |
|
31719 | 105 |
|
66380 | 106 |
lemma cong_0_int [simp, presburger]: "[a = b] (mod 0) \<longleftrightarrow> a = b" |
107 |
for a b :: int |
|
108 |
by (auto simp: cong_int_def) |
|
31719 | 109 |
|
66380 | 110 |
lemma cong_1_nat [simp, presburger]: "[a = b] (mod 1)" |
111 |
for a b :: nat |
|
112 |
by (auto simp: cong_nat_def) |
|
31719 | 113 |
|
66380 | 114 |
lemma cong_Suc_0_nat [simp, presburger]: "[a = b] (mod Suc 0)" |
115 |
for a b :: nat |
|
116 |
by (auto simp: cong_nat_def) |
|
31719 | 117 |
|
66380 | 118 |
lemma cong_1_int [simp, presburger]: "[a = b] (mod 1)" |
119 |
for a b :: int |
|
120 |
by (auto simp: cong_int_def) |
|
31719 | 121 |
|
66380 | 122 |
lemma cong_refl_nat [simp]: "[k = k] (mod m)" |
123 |
for k :: nat |
|
124 |
by (auto simp: cong_nat_def) |
|
31719 | 125 |
|
66380 | 126 |
lemma cong_refl_int [simp]: "[k = k] (mod m)" |
127 |
for k :: int |
|
128 |
by (auto simp: cong_int_def) |
|
31719 | 129 |
|
66380 | 130 |
lemma cong_sym_nat: "[a = b] (mod m) \<Longrightarrow> [b = a] (mod m)" |
131 |
for a b :: nat |
|
132 |
by (auto simp: cong_nat_def) |
|
31719 | 133 |
|
66380 | 134 |
lemma cong_sym_int: "[a = b] (mod m) \<Longrightarrow> [b = a] (mod m)" |
135 |
for a b :: int |
|
136 |
by (auto simp: cong_int_def) |
|
31719 | 137 |
|
66380 | 138 |
lemma cong_sym_eq_nat: "[a = b] (mod m) = [b = a] (mod m)" |
139 |
for a b :: nat |
|
140 |
by (auto simp: cong_nat_def) |
|
31719 | 141 |
|
66380 | 142 |
lemma cong_sym_eq_int: "[a = b] (mod m) = [b = a] (mod m)" |
143 |
for a b :: int |
|
144 |
by (auto simp: cong_int_def) |
|
31719 | 145 |
|
66380 | 146 |
lemma cong_trans_nat [trans]: "[a = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)" |
147 |
for a b c :: nat |
|
148 |
by (auto simp: cong_nat_def) |
|
31719 | 149 |
|
66380 | 150 |
lemma cong_trans_int [trans]: "[a = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)" |
151 |
for a b c :: int |
|
152 |
by (auto simp: cong_int_def) |
|
31719 | 153 |
|
66380 | 154 |
lemma cong_add_nat: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)" |
155 |
for a b c :: nat |
|
156 |
unfolding cong_nat_def by (metis mod_add_cong) |
|
31719 | 157 |
|
66380 | 158 |
lemma cong_add_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)" |
159 |
for a b c :: int |
|
160 |
unfolding cong_int_def by (metis mod_add_cong) |
|
31719 | 161 |
|
66380 | 162 |
lemma cong_diff_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)" |
163 |
for a b c :: int |
|
164 |
unfolding cong_int_def by (metis mod_diff_cong) |
|
31719 | 165 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
166 |
lemma cong_diff_aux_int: |
66380 | 167 |
"[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> |
168 |
a \<ge> c \<Longrightarrow> b \<ge> d \<Longrightarrow> [tsub a c = tsub b d] (mod m)" |
|
169 |
for a b c d :: int |
|
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset
|
170 |
by (metis cong_diff_int tsub_eq) |
31719 | 171 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
172 |
lemma cong_diff_nat: |
66380 | 173 |
fixes a b c d :: nat |
174 |
assumes "[a = b] (mod m)" "[c = d] (mod m)" "a \<ge> c" "b \<ge> d" |
|
31719 | 175 |
shows "[a - c = b - d] (mod m)" |
58860 | 176 |
using assms by (rule cong_diff_aux_int [transferred]) |
31719 | 177 |
|
66380 | 178 |
lemma cong_mult_nat: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)" |
179 |
for a b c d :: nat |
|
180 |
unfolding cong_nat_def by (metis mod_mult_cong) |
|
31719 | 181 |
|
66380 | 182 |
lemma cong_mult_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)" |
183 |
for a b c d :: int |
|
184 |
unfolding cong_int_def by (metis mod_mult_cong) |
|
44872 | 185 |
|
66380 | 186 |
lemma cong_exp_nat: "[x = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)" |
187 |
for x y :: nat |
|
188 |
by (induct k) (auto simp: cong_mult_nat) |
|
44872 | 189 |
|
66380 | 190 |
lemma cong_exp_int: "[x = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)" |
191 |
for x y :: int |
|
192 |
by (induct k) (auto simp: cong_mult_int) |
|
31719 | 193 |
|
66380 | 194 |
lemma cong_sum_nat: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)" |
195 |
for f g :: "'a \<Rightarrow> nat" |
|
196 |
by (induct A rule: infinite_finite_induct) (auto intro: cong_add_nat) |
|
197 |
||
198 |
lemma cong_sum_int: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)" |
|
199 |
for f g :: "'a \<Rightarrow> int" |
|
200 |
by (induct A rule: infinite_finite_induct) (auto intro: cong_add_int) |
|
31719 | 201 |
|
66380 | 202 |
lemma cong_prod_nat: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)" |
203 |
for f g :: "'a \<Rightarrow> nat" |
|
204 |
by (induct A rule: infinite_finite_induct) (auto intro: cong_mult_nat) |
|
31719 | 205 |
|
66380 | 206 |
lemma cong_prod_int: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)" |
207 |
for f g :: "'a \<Rightarrow> int" |
|
208 |
by (induct A rule: infinite_finite_induct) (auto intro: cong_mult_int) |
|
31719 | 209 |
|
66380 | 210 |
lemma cong_scalar_nat: "[a = b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)" |
211 |
for a b k :: nat |
|
44872 | 212 |
by (rule cong_mult_nat) simp_all |
31719 | 213 |
|
66380 | 214 |
lemma cong_scalar_int: "[a = b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)" |
215 |
for a b k :: int |
|
44872 | 216 |
by (rule cong_mult_int) simp_all |
31719 | 217 |
|
66380 | 218 |
lemma cong_scalar2_nat: "[a = b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)" |
219 |
for a b k :: nat |
|
44872 | 220 |
by (rule cong_mult_nat) simp_all |
31719 | 221 |
|
66380 | 222 |
lemma cong_scalar2_int: "[a = b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)" |
223 |
for a b k :: int |
|
44872 | 224 |
by (rule cong_mult_int) simp_all |
31719 | 225 |
|
66380 | 226 |
lemma cong_mult_self_nat: "[a * m = 0] (mod m)" |
227 |
for a m :: nat |
|
228 |
by (auto simp: cong_nat_def) |
|
31719 | 229 |
|
66380 | 230 |
lemma cong_mult_self_int: "[a * m = 0] (mod m)" |
231 |
for a m :: int |
|
232 |
by (auto simp: cong_int_def) |
|
31719 | 233 |
|
66380 | 234 |
lemma cong_eq_diff_cong_0_int: "[a = b] (mod m) = [a - b = 0] (mod m)" |
235 |
for a b :: int |
|
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset
|
236 |
by (metis cong_add_int cong_diff_int cong_refl_int diff_add_cancel diff_self) |
31719 | 237 |
|
66380 | 238 |
lemma cong_eq_diff_cong_0_aux_int: "a \<ge> b \<Longrightarrow> [a = b] (mod m) = [tsub a b = 0] (mod m)" |
239 |
for a b :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
240 |
by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int) |
31719 | 241 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
242 |
lemma cong_eq_diff_cong_0_nat: |
66380 | 243 |
fixes a b :: nat |
244 |
assumes "a \<ge> b" |
|
31719 | 245 |
shows "[a = b] (mod m) = [a - b = 0] (mod m)" |
41541 | 246 |
using assms by (rule cong_eq_diff_cong_0_aux_int [transferred]) |
31719 | 247 |
|
44872 | 248 |
lemma cong_diff_cong_0'_nat: |
66380 | 249 |
"[x = y] (mod n) \<longleftrightarrow> (if x \<le> y then [y - x = 0] (mod n) else [x - y = 0] (mod n))" |
250 |
for x y :: nat |
|
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset
|
251 |
by (metis cong_eq_diff_cong_0_nat cong_sym_nat nat_le_linear) |
31719 | 252 |
|
66380 | 253 |
lemma cong_altdef_nat: "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)" |
254 |
for a b :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
255 |
apply (subst cong_eq_diff_cong_0_nat, assumption) |
31719 | 256 |
apply (unfold cong_nat_def) |
257 |
apply (simp add: dvd_eq_mod_eq_0 [symmetric]) |
|
44872 | 258 |
done |
31719 | 259 |
|
66380 | 260 |
lemma cong_altdef_int: "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)" |
261 |
for a b :: int |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64272
diff
changeset
|
262 |
by (metis cong_int_def mod_eq_dvd_iff) |
31719 | 263 |
|
66380 | 264 |
lemma cong_abs_int: "[x = y] (mod abs m) \<longleftrightarrow> [x = y] (mod m)" |
265 |
for x y :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
266 |
by (simp add: cong_altdef_int) |
31719 | 267 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
268 |
lemma cong_square_int: |
66380 | 269 |
"prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)" |
270 |
for a :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
271 |
apply (simp only: cong_altdef_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
272 |
apply (subst prime_dvd_mult_eq_int [symmetric], assumption) |
36350 | 273 |
apply (auto simp add: field_simps) |
44872 | 274 |
done |
31719 | 275 |
|
66380 | 276 |
lemma cong_mult_rcancel_int: "coprime k m \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)" |
277 |
for a k m :: int |
|
62353
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62349
diff
changeset
|
278 |
by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute) |
31719 | 279 |
|
66380 | 280 |
lemma cong_mult_rcancel_nat: "coprime k m \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)" |
281 |
for a k m :: nat |
|
55371 | 282 |
by (metis cong_mult_rcancel_int [transferred]) |
31719 | 283 |
|
66380 | 284 |
lemma cong_mult_lcancel_nat: "coprime k m \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)" |
285 |
for a k m :: nat |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
286 |
by (simp add: mult.commute cong_mult_rcancel_nat) |
31719 | 287 |
|
66380 | 288 |
lemma cong_mult_lcancel_int: "coprime k m \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)" |
289 |
for a k m :: int |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
290 |
by (simp add: mult.commute cong_mult_rcancel_int) |
31719 | 291 |
|
292 |
(* was zcong_zgcd_zmult_zmod *) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
293 |
lemma coprime_cong_mult_int: |
66380 | 294 |
"[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)" |
295 |
for a b :: int |
|
296 |
by (metis divides_mult cong_altdef_int) |
|
31719 | 297 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
298 |
lemma coprime_cong_mult_nat: |
66380 | 299 |
"[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)" |
300 |
for a b :: nat |
|
301 |
by (metis coprime_cong_mult_int [transferred]) |
|
31719 | 302 |
|
66380 | 303 |
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" |
304 |
for a b :: nat |
|
41541 | 305 |
by (auto simp add: cong_nat_def) |
31719 | 306 |
|
66380 | 307 |
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" |
308 |
for a b :: int |
|
41541 | 309 |
by (auto simp add: cong_int_def) |
31719 | 310 |
|
66380 | 311 |
lemma cong_less_unique_nat: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
312 |
for a m :: nat |
|
55371 | 313 |
by (auto simp: cong_nat_def) (metis mod_less_divisor mod_mod_trivial) |
31719 | 314 |
|
66380 | 315 |
lemma cong_less_unique_int: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
316 |
for a m :: int |
|
55371 | 317 |
by (auto simp: cong_int_def) (metis mod_mod_trivial pos_mod_conj) |
31719 | 318 |
|
66380 | 319 |
lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)" |
320 |
for a b :: int |
|
55371 | 321 |
apply (auto simp add: cong_altdef_int dvd_def) |
31719 | 322 |
apply (rule_tac [!] x = "-k" in exI, auto) |
44872 | 323 |
done |
31719 | 324 |
|
66380 | 325 |
lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)" |
326 |
(is "?lhs = ?rhs") |
|
327 |
for a b :: nat |
|
328 |
proof |
|
329 |
assume ?lhs |
|
55371 | 330 |
show ?rhs |
331 |
proof (cases "b \<le> a") |
|
332 |
case True |
|
66380 | 333 |
with \<open>?lhs\<close> show ?rhs |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
334 |
by (metis cong_altdef_nat dvd_def le_add_diff_inverse add_0_right mult_0 mult.commute) |
55371 | 335 |
next |
336 |
case False |
|
66380 | 337 |
with \<open>?lhs\<close> show ?rhs |
55371 | 338 |
apply (subst (asm) cong_sym_eq_nat) |
339 |
apply (auto simp: cong_altdef_nat) |
|
340 |
apply (metis add_0_right add_diff_inverse dvd_div_mult_self less_or_eq_imp_le mult_0) |
|
341 |
done |
|
342 |
qed |
|
343 |
next |
|
344 |
assume ?rhs |
|
345 |
then show ?lhs |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
346 |
by (metis cong_nat_def mod_mult_self2 mult.commute) |
55371 | 347 |
qed |
31719 | 348 |
|
66380 | 349 |
lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m" |
350 |
for a b :: int |
|
55371 | 351 |
by (metis cong_int_def gcd_red_int) |
31719 | 352 |
|
66380 | 353 |
lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m" |
354 |
for a b :: nat |
|
63092 | 355 |
by (metis cong_gcd_eq_int [transferred]) |
31719 | 356 |
|
66380 | 357 |
lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m" |
358 |
for a b :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
359 |
by (auto simp add: cong_gcd_eq_nat) |
31719 | 360 |
|
66380 | 361 |
lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m" |
362 |
for a b :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
363 |
by (auto simp add: cong_gcd_eq_int) |
31719 | 364 |
|
66380 | 365 |
lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)" |
366 |
for a b :: nat |
|
31719 | 367 |
by (auto simp add: cong_nat_def) |
368 |
||
66380 | 369 |
lemma cong_cong_mod_int: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)" |
370 |
for a b :: int |
|
31719 | 371 |
by (auto simp add: cong_int_def) |
372 |
||
66380 | 373 |
lemma cong_minus_int [iff]: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)" |
374 |
for a b :: int |
|
55371 | 375 |
by (metis cong_iff_lin_int minus_equation_iff mult_minus_left mult_minus_right) |
31719 | 376 |
|
377 |
(* |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
378 |
lemma mod_dvd_mod_int: |
31719 | 379 |
"0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)" |
380 |
apply (unfold dvd_def, auto) |
|
381 |
apply (rule mod_mod_cancel) |
|
382 |
apply auto |
|
44872 | 383 |
done |
31719 | 384 |
|
385 |
lemma mod_dvd_mod: |
|
386 |
assumes "0 < (m::nat)" and "m dvd b" |
|
387 |
shows "(a mod b mod m) = (a mod m)" |
|
388 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
389 |
apply (rule mod_dvd_mod_int [transferred]) |
41541 | 390 |
using assms apply auto |
391 |
done |
|
31719 | 392 |
*) |
393 |
||
66380 | 394 |
lemma cong_add_lcancel_nat: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
395 |
for a x y :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
396 |
by (simp add: cong_iff_lin_nat) |
31719 | 397 |
|
66380 | 398 |
lemma cong_add_lcancel_int: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
399 |
for a x y :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
400 |
by (simp add: cong_iff_lin_int) |
31719 | 401 |
|
66380 | 402 |
lemma cong_add_rcancel_nat: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
403 |
for a x y :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
404 |
by (simp add: cong_iff_lin_nat) |
31719 | 405 |
|
66380 | 406 |
lemma cong_add_rcancel_int: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
407 |
for a x y :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
408 |
by (simp add: cong_iff_lin_int) |
31719 | 409 |
|
66380 | 410 |
lemma cong_add_lcancel_0_nat: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
411 |
for a x :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
412 |
by (simp add: cong_iff_lin_nat) |
31719 | 413 |
|
66380 | 414 |
lemma cong_add_lcancel_0_int: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
415 |
for a x :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
416 |
by (simp add: cong_iff_lin_int) |
31719 | 417 |
|
66380 | 418 |
lemma cong_add_rcancel_0_nat: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
419 |
for a x :: nat |
|
420 |
by (simp add: cong_iff_lin_nat) |
|
421 |
||
422 |
lemma cong_add_rcancel_0_int: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
|
423 |
for a x :: int |
|
424 |
by (simp add: cong_iff_lin_int) |
|
425 |
||
426 |
lemma cong_dvd_modulus_nat: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)" |
|
427 |
for x y :: nat |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
428 |
apply (auto simp add: cong_iff_lin_nat dvd_def) |
66380 | 429 |
apply (rule_tac x= "k1 * k" in exI) |
430 |
apply (rule_tac x= "k2 * k" in exI) |
|
36350 | 431 |
apply (simp add: field_simps) |
44872 | 432 |
done |
31719 | 433 |
|
66380 | 434 |
lemma cong_dvd_modulus_int: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)" |
435 |
for x y :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
436 |
by (auto simp add: cong_altdef_int dvd_def) |
31719 | 437 |
|
66380 | 438 |
lemma cong_dvd_eq_nat: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y" |
439 |
for x y :: nat |
|
440 |
by (auto simp: cong_nat_def dvd_eq_mod_eq_0) |
|
31719 | 441 |
|
66380 | 442 |
lemma cong_dvd_eq_int: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y" |
443 |
for x y :: int |
|
444 |
by (auto simp: cong_int_def dvd_eq_mod_eq_0) |
|
31719 | 445 |
|
66380 | 446 |
lemma cong_mod_nat: "n \<noteq> 0 \<Longrightarrow> [a mod n = a] (mod n)" |
447 |
for a n :: nat |
|
31719 | 448 |
by (simp add: cong_nat_def) |
449 |
||
66380 | 450 |
lemma cong_mod_int: "n \<noteq> 0 \<Longrightarrow> [a mod n = a] (mod n)" |
451 |
for a n :: int |
|
31719 | 452 |
by (simp add: cong_int_def) |
453 |
||
66380 | 454 |
lemma mod_mult_cong_nat: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)" |
455 |
for a b :: nat |
|
31719 | 456 |
by (simp add: cong_nat_def mod_mult2_eq mod_add_left_eq) |
457 |
||
66380 | 458 |
lemma neg_cong_int: "[a = b] (mod m) \<longleftrightarrow> [- a = - b] (mod m)" |
459 |
for a b :: int |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64272
diff
changeset
|
460 |
by (metis cong_int_def minus_minus mod_minus_cong) |
31719 | 461 |
|
66380 | 462 |
lemma cong_modulus_neg_int: "[a = b] (mod m) \<longleftrightarrow> [a = b] (mod - m)" |
463 |
for a b :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
464 |
by (auto simp add: cong_altdef_int) |
31719 | 465 |
|
66380 | 466 |
lemma mod_mult_cong_int: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)" |
467 |
for a b :: int |
|
468 |
proof (cases "b > 0") |
|
469 |
case True |
|
470 |
then show ?thesis |
|
471 |
by (simp add: cong_int_def mod_mod_cancel mod_add_left_eq) |
|
472 |
next |
|
473 |
case False |
|
474 |
then show ?thesis |
|
475 |
apply (subst (1 2) cong_modulus_neg_int) |
|
476 |
apply (unfold cong_int_def) |
|
477 |
apply (subgoal_tac "a * b = (- a * - b)") |
|
478 |
apply (erule ssubst) |
|
479 |
apply (subst zmod_zmult2_eq) |
|
480 |
apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right) |
|
481 |
apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 diff_zero)+ |
|
482 |
done |
|
483 |
qed |
|
484 |
||
485 |
lemma cong_to_1_nat: |
|
486 |
fixes a :: nat |
|
487 |
assumes "[a = 1] (mod n)" |
|
488 |
shows "n dvd (a - 1)" |
|
489 |
proof (cases "a = 0") |
|
490 |
case True |
|
491 |
then show ?thesis by force |
|
492 |
next |
|
493 |
case False |
|
494 |
with assms show ?thesis by (metis cong_altdef_nat leI less_one) |
|
495 |
qed |
|
496 |
||
497 |
lemma cong_0_1_nat': "[0 = Suc 0] (mod n) \<longleftrightarrow> n = Suc 0" |
|
498 |
by (auto simp: cong_nat_def) |
|
499 |
||
500 |
lemma cong_0_1_nat: "[0 = 1] (mod n) \<longleftrightarrow> n = 1" |
|
501 |
for n :: nat |
|
502 |
by (auto simp: cong_nat_def) |
|
503 |
||
504 |
lemma cong_0_1_int: "[0 = 1] (mod n) \<longleftrightarrow> n = 1 \<or> n = - 1" |
|
505 |
for n :: int |
|
506 |
by (auto simp: cong_int_def zmult_eq_1_iff) |
|
507 |
||
508 |
lemma cong_to_1'_nat: "[a = 1] (mod n) \<longleftrightarrow> a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)" |
|
509 |
for a :: nat |
|
510 |
by (metis add.right_neutral cong_0_1_nat cong_iff_lin_nat cong_to_1_nat |
|
511 |
dvd_div_mult_self leI le_add_diff_inverse less_one mult_eq_if) |
|
512 |
||
513 |
lemma cong_le_nat: "y \<le> x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)" |
|
514 |
for x y :: nat |
|
515 |
by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def mult.commute) |
|
516 |
||
517 |
lemma cong_solve_nat: |
|
518 |
fixes a :: nat |
|
519 |
assumes "a \<noteq> 0" |
|
520 |
shows "\<exists>x. [a * x = gcd a n] (mod n)" |
|
521 |
proof (cases "n = 0") |
|
522 |
case True |
|
523 |
then show ?thesis by force |
|
524 |
next |
|
525 |
case False |
|
526 |
then show ?thesis |
|
527 |
using bezout_nat [of a n, OF \<open>a \<noteq> 0\<close>] |
|
528 |
by auto (metis cong_add_rcancel_0_nat cong_mult_self_nat mult.commute) |
|
529 |
qed |
|
530 |
||
531 |
lemma cong_solve_int: "a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)" |
|
532 |
for a :: int |
|
533 |
apply (cases "n = 0") |
|
534 |
apply (cases "a \<ge> 0") |
|
535 |
apply auto |
|
536 |
apply (rule_tac x = "-1" in exI) |
|
537 |
apply auto |
|
538 |
apply (insert bezout_int [of a n], auto) |
|
539 |
apply (metis cong_iff_lin_int mult.commute) |
|
44872 | 540 |
done |
31719 | 541 |
|
44872 | 542 |
lemma cong_solve_dvd_nat: |
66380 | 543 |
fixes a :: nat |
544 |
assumes a: "a \<noteq> 0" and b: "gcd a n dvd d" |
|
545 |
shows "\<exists>x. [a * x = d] (mod n)" |
|
31719 | 546 |
proof - |
44872 | 547 |
from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)" |
31719 | 548 |
by auto |
44872 | 549 |
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
|
550 |
by (elim cong_scalar2_nat) |
31719 | 551 |
also from b have "(d div gcd a n) * gcd a n = d" |
552 |
by (rule dvd_div_mult_self) |
|
553 |
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" |
|
554 |
by auto |
|
555 |
finally show ?thesis |
|
556 |
by auto |
|
557 |
qed |
|
558 |
||
44872 | 559 |
lemma cong_solve_dvd_int: |
31719 | 560 |
assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d" |
66380 | 561 |
shows "\<exists>x. [a * x = d] (mod n)" |
31719 | 562 |
proof - |
44872 | 563 |
from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)" |
31719 | 564 |
by auto |
44872 | 565 |
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
|
566 |
by (elim cong_scalar2_int) |
31719 | 567 |
also from b have "(d div gcd a n) * gcd a n = d" |
568 |
by (rule dvd_div_mult_self) |
|
569 |
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" |
|
570 |
by auto |
|
571 |
finally show ?thesis |
|
572 |
by auto |
|
573 |
qed |
|
574 |
||
66380 | 575 |
lemma cong_solve_coprime_nat: |
576 |
fixes a :: nat |
|
577 |
assumes "coprime a n" |
|
578 |
shows "\<exists>x. [a * x = 1] (mod n)" |
|
579 |
proof (cases "a = 0") |
|
580 |
case True |
|
581 |
with assms show ?thesis by force |
|
582 |
next |
|
583 |
case False |
|
584 |
with assms show ?thesis by (metis cong_solve_nat) |
|
585 |
qed |
|
31719 | 586 |
|
66380 | 587 |
lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)" |
44872 | 588 |
apply (cases "a = 0") |
66380 | 589 |
apply auto |
590 |
apply (cases "n \<ge> 0") |
|
591 |
apply auto |
|
55161 | 592 |
apply (metis cong_solve_int) |
593 |
done |
|
594 |
||
62349
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
595 |
lemma coprime_iff_invertible_nat: |
66380 | 596 |
"m > 0 \<Longrightarrow> coprime a m = (\<exists>x. [a * x = Suc 0] (mod m))" |
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset
|
597 |
by (metis One_nat_def cong_gcd_eq_nat cong_solve_coprime_nat coprime_lmult gcd.commute gcd_Suc_0) |
66380 | 598 |
|
599 |
lemma coprime_iff_invertible_int: "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))" |
|
600 |
for m :: int |
|
55161 | 601 |
apply (auto intro: cong_solve_coprime_int) |
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset
|
602 |
apply (metis cong_int_def coprime_mul_eq gcd_1_int gcd.commute gcd_red_int) |
44872 | 603 |
done |
31719 | 604 |
|
66380 | 605 |
lemma coprime_iff_invertible'_nat: |
606 |
"m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))" |
|
55161 | 607 |
apply (subst coprime_iff_invertible_nat) |
66380 | 608 |
apply auto |
55161 | 609 |
apply (auto simp add: cong_nat_def) |
610 |
apply (metis mod_less_divisor mod_mult_right_eq) |
|
44872 | 611 |
done |
31719 | 612 |
|
66380 | 613 |
lemma coprime_iff_invertible'_int: |
614 |
"m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = 1] (mod m))" |
|
615 |
for m :: int |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
616 |
apply (subst coprime_iff_invertible_int) |
66380 | 617 |
apply (auto simp add: cong_int_def) |
55371 | 618 |
apply (metis mod_mult_right_eq pos_mod_conj) |
44872 | 619 |
done |
31719 | 620 |
|
66380 | 621 |
lemma cong_cong_lcm_nat: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" |
622 |
for x y :: nat |
|
44872 | 623 |
apply (cases "y \<le> x") |
62348 | 624 |
apply (metis cong_altdef_nat lcm_least) |
62349
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
625 |
apply (meson cong_altdef_nat cong_sym_nat lcm_least_iff nat_le_linear) |
44872 | 626 |
done |
31719 | 627 |
|
66380 | 628 |
lemma cong_cong_lcm_int: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" |
629 |
for x y :: int |
|
630 |
by (auto simp add: cong_altdef_int lcm_least) |
|
31719 | 631 |
|
64272 | 632 |
lemma cong_cong_prod_coprime_nat [rule_format]: "finite A \<Longrightarrow> |
61954 | 633 |
(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
634 |
(\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow> |
|
635 |
[x = y] (mod (\<Prod>i\<in>A. m i))" |
|
31719 | 636 |
apply (induct set: finite) |
637 |
apply auto |
|
64272 | 638 |
apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime) |
44872 | 639 |
done |
31719 | 640 |
|
64272 | 641 |
lemma cong_cong_prod_coprime_int [rule_format]: "finite A \<Longrightarrow> |
61954 | 642 |
(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
643 |
(\<forall>i\<in>A. [(x::int) = y] (mod m i)) \<longrightarrow> |
|
644 |
[x = y] (mod (\<Prod>i\<in>A. m i))" |
|
31719 | 645 |
apply (induct set: finite) |
646 |
apply auto |
|
64272 | 647 |
apply (metis coprime_cong_mult_int gcd.commute prod_coprime) |
44872 | 648 |
done |
31719 | 649 |
|
44872 | 650 |
lemma binary_chinese_remainder_aux_nat: |
66380 | 651 |
fixes m1 m2 :: nat |
652 |
assumes a: "coprime m1 m2" |
|
653 |
shows "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
|
31719 | 654 |
proof - |
66380 | 655 |
from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" |
31719 | 656 |
by auto |
44872 | 657 |
from a have b: "coprime m2 m1" |
62348 | 658 |
by (subst gcd.commute) |
66380 | 659 |
from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" |
31719 | 660 |
by auto |
661 |
have "[m1 * x1 = 0] (mod m1)" |
|
66380 | 662 |
by (subst mult.commute) (rule cong_mult_self_nat) |
31719 | 663 |
moreover have "[m2 * x2 = 0] (mod m2)" |
66380 | 664 |
by (subst mult.commute) (rule cong_mult_self_nat) |
665 |
ultimately show ?thesis |
|
666 |
using 1 2 by blast |
|
31719 | 667 |
qed |
668 |
||
44872 | 669 |
lemma binary_chinese_remainder_aux_int: |
66380 | 670 |
fixes m1 m2 :: int |
671 |
assumes a: "coprime m1 m2" |
|
672 |
shows "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
|
31719 | 673 |
proof - |
66380 | 674 |
from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" |
31719 | 675 |
by auto |
44872 | 676 |
from a have b: "coprime m2 m1" |
62348 | 677 |
by (subst gcd.commute) |
66380 | 678 |
from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" |
31719 | 679 |
by auto |
680 |
have "[m1 * x1 = 0] (mod m1)" |
|
66380 | 681 |
by (subst mult.commute) (rule cong_mult_self_int) |
31719 | 682 |
moreover have "[m2 * x2 = 0] (mod m2)" |
66380 | 683 |
by (subst mult.commute) (rule cong_mult_self_int) |
684 |
ultimately show ?thesis |
|
685 |
using 1 2 by blast |
|
31719 | 686 |
qed |
687 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
688 |
lemma binary_chinese_remainder_nat: |
66380 | 689 |
fixes m1 m2 :: nat |
690 |
assumes a: "coprime m1 m2" |
|
691 |
shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
31719 | 692 |
proof - |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
693 |
from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2 |
66380 | 694 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" |
695 |
and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
31719 | 696 |
by blast |
697 |
let ?x = "u1 * b1 + u2 * b2" |
|
698 |
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
|
699 |
apply (rule cong_add_nat) |
66380 | 700 |
apply (rule cong_scalar2_nat) |
701 |
apply (rule \<open>[b1 = 1] (mod m1)\<close>) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
702 |
apply (rule cong_scalar2_nat) |
60526 | 703 |
apply (rule \<open>[b2 = 0] (mod m1)\<close>) |
31719 | 704 |
done |
44872 | 705 |
then have "[?x = u1] (mod m1)" by simp |
31719 | 706 |
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
|
707 |
apply (rule cong_add_nat) |
66380 | 708 |
apply (rule cong_scalar2_nat) |
709 |
apply (rule \<open>[b1 = 0] (mod m2)\<close>) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
710 |
apply (rule cong_scalar2_nat) |
60526 | 711 |
apply (rule \<open>[b2 = 1] (mod m2)\<close>) |
31719 | 712 |
done |
66380 | 713 |
then have "[?x = u2] (mod m2)" |
714 |
by simp |
|
715 |
with \<open>[?x = u1] (mod m1)\<close> show ?thesis |
|
716 |
by blast |
|
31719 | 717 |
qed |
718 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
719 |
lemma binary_chinese_remainder_int: |
66380 | 720 |
fixes m1 m2 :: int |
721 |
assumes a: "coprime m1 m2" |
|
722 |
shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
31719 | 723 |
proof - |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
724 |
from binary_chinese_remainder_aux_int [OF a] obtain b1 b2 |
66380 | 725 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" |
726 |
and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
31719 | 727 |
by blast |
728 |
let ?x = "u1 * b1 + u2 * b2" |
|
729 |
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
|
730 |
apply (rule cong_add_int) |
66380 | 731 |
apply (rule cong_scalar2_int) |
732 |
apply (rule \<open>[b1 = 1] (mod m1)\<close>) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
733 |
apply (rule cong_scalar2_int) |
60526 | 734 |
apply (rule \<open>[b2 = 0] (mod m1)\<close>) |
31719 | 735 |
done |
44872 | 736 |
then have "[?x = u1] (mod m1)" by simp |
31719 | 737 |
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
|
738 |
apply (rule cong_add_int) |
66380 | 739 |
apply (rule cong_scalar2_int) |
740 |
apply (rule \<open>[b1 = 0] (mod m2)\<close>) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
741 |
apply (rule cong_scalar2_int) |
60526 | 742 |
apply (rule \<open>[b2 = 1] (mod m2)\<close>) |
31719 | 743 |
done |
44872 | 744 |
then have "[?x = u2] (mod m2)" by simp |
66380 | 745 |
with \<open>[?x = u1] (mod m1)\<close> show ?thesis |
746 |
by blast |
|
31719 | 747 |
qed |
748 |
||
66380 | 749 |
lemma cong_modulus_mult_nat: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)" |
750 |
for x y :: nat |
|
44872 | 751 |
apply (cases "y \<le> x") |
66380 | 752 |
apply (simp add: cong_altdef_nat) |
753 |
apply (erule dvd_mult_left) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
754 |
apply (rule cong_sym_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
755 |
apply (subst (asm) cong_sym_eq_nat) |
44872 | 756 |
apply (simp add: cong_altdef_nat) |
31719 | 757 |
apply (erule dvd_mult_left) |
44872 | 758 |
done |
31719 | 759 |
|
66380 | 760 |
lemma cong_modulus_mult_int: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)" |
761 |
for x y :: int |
|
44872 | 762 |
apply (simp add: cong_altdef_int) |
31719 | 763 |
apply (erule dvd_mult_left) |
44872 | 764 |
done |
31719 | 765 |
|
66380 | 766 |
lemma cong_less_modulus_unique_nat: "[x = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y" |
767 |
for x y :: nat |
|
31719 | 768 |
by (simp add: cong_nat_def) |
769 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
770 |
lemma binary_chinese_remainder_unique_nat: |
66380 | 771 |
fixes m1 m2 :: nat |
772 |
assumes a: "coprime m1 m2" |
|
44872 | 773 |
and nz: "m1 \<noteq> 0" "m2 \<noteq> 0" |
63901 | 774 |
shows "\<exists>!x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
31719 | 775 |
proof - |
66380 | 776 |
from binary_chinese_remainder_nat [OF a] obtain y |
777 |
where "[y = u1] (mod m1)" and "[y = u2] (mod m2)" |
|
31719 | 778 |
by blast |
779 |
let ?x = "y mod (m1 * m2)" |
|
780 |
from nz have less: "?x < m1 * m2" |
|
44872 | 781 |
by auto |
66380 | 782 |
have 1: "[?x = u1] (mod m1)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
783 |
apply (rule cong_trans_nat) |
66380 | 784 |
prefer 2 |
785 |
apply (rule \<open>[y = u1] (mod m1)\<close>) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
786 |
apply (rule cong_modulus_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
787 |
apply (rule cong_mod_nat) |
31719 | 788 |
using nz apply auto |
789 |
done |
|
66380 | 790 |
have 2: "[?x = u2] (mod m2)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
791 |
apply (rule cong_trans_nat) |
66380 | 792 |
prefer 2 |
793 |
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
|
794 |
apply (subst mult.commute) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
795 |
apply (rule cong_modulus_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
796 |
apply (rule cong_mod_nat) |
31719 | 797 |
using nz apply auto |
798 |
done |
|
66380 | 799 |
have "\<forall>z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x" |
44872 | 800 |
proof clarify |
31719 | 801 |
fix z |
802 |
assume "z < m1 * m2" |
|
803 |
assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)" |
|
804 |
have "[?x = z] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
805 |
apply (rule cong_trans_nat) |
66380 | 806 |
apply (rule \<open>[?x = u1] (mod m1)\<close>) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
807 |
apply (rule cong_sym_nat) |
60526 | 808 |
apply (rule \<open>[z = u1] (mod m1)\<close>) |
31719 | 809 |
done |
810 |
moreover have "[?x = z] (mod m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
811 |
apply (rule cong_trans_nat) |
66380 | 812 |
apply (rule \<open>[?x = u2] (mod m2)\<close>) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
813 |
apply (rule cong_sym_nat) |
60526 | 814 |
apply (rule \<open>[z = u2] (mod m2)\<close>) |
31719 | 815 |
done |
816 |
ultimately have "[?x = z] (mod m1 * m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
817 |
by (auto intro: coprime_cong_mult_nat a) |
60526 | 818 |
with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
819 |
apply (intro cong_less_modulus_unique_nat) |
66380 | 820 |
apply (auto, erule cong_sym_nat) |
31719 | 821 |
done |
44872 | 822 |
qed |
66380 | 823 |
with less 1 2 show ?thesis by auto |
31719 | 824 |
qed |
825 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
826 |
lemma chinese_remainder_aux_nat: |
44872 | 827 |
fixes A :: "'a set" |
828 |
and m :: "'a \<Rightarrow> nat" |
|
829 |
assumes fin: "finite A" |
|
66380 | 830 |
and cop: "\<forall>i \<in> A. (\<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
831 |
shows "\<exists>b. (\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))" |
|
31719 | 832 |
proof (rule finite_set_choice, rule fin, rule ballI) |
833 |
fix i |
|
66380 | 834 |
assume "i \<in> A" |
61954 | 835 |
with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)" |
66380 | 836 |
by (intro prod_coprime) auto |
837 |
then have "\<exists>x. [(\<Prod>j \<in> 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
|
838 |
by (elim cong_solve_coprime_nat) |
61954 | 839 |
then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)" |
31719 | 840 |
by auto |
66380 | 841 |
moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
842 |
by (subst mult.commute, rule cong_mult_self_nat) |
66380 | 843 |
ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))" |
31719 | 844 |
by blast |
845 |
qed |
|
846 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
847 |
lemma chinese_remainder_nat: |
44872 | 848 |
fixes A :: "'a set" |
849 |
and m :: "'a \<Rightarrow> nat" |
|
850 |
and u :: "'a \<Rightarrow> nat" |
|
851 |
assumes fin: "finite A" |
|
66380 | 852 |
and cop: "\<forall>i \<in> A. \<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)" |
853 |
shows "\<exists>x. \<forall>i \<in> A. [x = u i] (mod m i)" |
|
31719 | 854 |
proof - |
66380 | 855 |
from chinese_remainder_aux_nat [OF fin cop] |
856 |
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 | 857 |
by blast |
61954 | 858 |
let ?x = "\<Sum>i\<in>A. (u i) * (b i)" |
66380 | 859 |
show ?thesis |
31719 | 860 |
proof (rule exI, clarify) |
861 |
fix i |
|
66380 | 862 |
assume a: "i \<in> A" |
44872 | 863 |
show "[?x = u i] (mod m i)" |
31719 | 864 |
proof - |
66380 | 865 |
from fin a have "?x = (\<Sum>j \<in> {i}. u j * b j) + (\<Sum>j \<in> A - {i}. u j * b j)" |
866 |
by (subst sum.union_disjoint [symmetric]) (auto intro: sum.cong) |
|
61954 | 867 |
then have "[?x = u i * b i + (\<Sum>j \<in> A - {i}. u j * b j)] (mod m i)" |
31719 | 868 |
by auto |
61954 | 869 |
also have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) = |
870 |
u i * 1 + (\<Sum>j \<in> 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
|
871 |
apply (rule cong_add_nat) |
66380 | 872 |
apply (rule cong_scalar2_nat) |
873 |
using b a apply blast |
|
64267 | 874 |
apply (rule cong_sum_nat) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
875 |
apply (rule cong_scalar2_nat) |
66380 | 876 |
using b apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
877 |
apply (rule cong_dvd_modulus_nat) |
66380 | 878 |
apply (drule (1) bspec) |
879 |
apply (erule conjE) |
|
880 |
apply assumption |
|
59010 | 881 |
apply rule |
31719 | 882 |
using fin a apply auto |
883 |
done |
|
884 |
finally show ?thesis |
|
885 |
by simp |
|
886 |
qed |
|
887 |
qed |
|
888 |
qed |
|
889 |
||
44872 | 890 |
lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow> |
61954 | 891 |
(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
892 |
(\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow> |
|
893 |
[x = y] (mod (\<Prod>i\<in>A. m i))" |
|
31719 | 894 |
apply (induct set: finite) |
895 |
apply auto |
|
64272 | 896 |
apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime) |
44872 | 897 |
done |
31719 | 898 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
899 |
lemma chinese_remainder_unique_nat: |
44872 | 900 |
fixes A :: "'a set" |
901 |
and m :: "'a \<Rightarrow> nat" |
|
902 |
and u :: "'a \<Rightarrow> nat" |
|
903 |
assumes fin: "finite A" |
|
61954 | 904 |
and nz: "\<forall>i\<in>A. m i \<noteq> 0" |
66380 | 905 |
and cop: "\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)" |
63901 | 906 |
shows "\<exists>!x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))" |
31719 | 907 |
proof - |
44872 | 908 |
from chinese_remainder_nat [OF fin cop] |
66380 | 909 |
obtain y where one: "(\<forall>i\<in>A. [y = u i] (mod m i))" |
31719 | 910 |
by blast |
61954 | 911 |
let ?x = "y mod (\<Prod>i\<in>A. m i)" |
912 |
from fin nz have prodnz: "(\<Prod>i\<in>A. m i) \<noteq> 0" |
|
31719 | 913 |
by auto |
61954 | 914 |
then have less: "?x < (\<Prod>i\<in>A. m i)" |
31719 | 915 |
by auto |
66380 | 916 |
have cong: "\<forall>i\<in>A. [?x = u i] (mod m i)" |
31719 | 917 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
918 |
apply (rule cong_trans_nat) |
66380 | 919 |
prefer 2 |
31719 | 920 |
using one apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
921 |
apply (rule cong_dvd_modulus_nat) |
66380 | 922 |
apply (rule cong_mod_nat) |
31719 | 923 |
using prodnz apply auto |
59010 | 924 |
apply rule |
66380 | 925 |
apply (rule fin) |
31719 | 926 |
apply assumption |
927 |
done |
|
66380 | 928 |
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" |
929 |
proof clarify |
|
31719 | 930 |
fix z |
61954 | 931 |
assume zless: "z < (\<Prod>i\<in>A. m i)" |
66380 | 932 |
assume zcong: "(\<forall>i\<in>A. [z = u i] (mod m i))" |
933 |
have "\<forall>i\<in>A. [?x = z] (mod m i)" |
|
44872 | 934 |
apply clarify |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
935 |
apply (rule cong_trans_nat) |
31719 | 936 |
using cong apply (erule bspec) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
937 |
apply (rule cong_sym_nat) |
31719 | 938 |
using zcong apply auto |
939 |
done |
|
61954 | 940 |
with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))" |
44872 | 941 |
apply (intro coprime_cong_prod_nat) |
66380 | 942 |
apply auto |
44872 | 943 |
done |
31719 | 944 |
with zless less show "z = ?x" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
945 |
apply (intro cong_less_modulus_unique_nat) |
66380 | 946 |
apply auto |
947 |
apply (erule cong_sym_nat) |
|
31719 | 948 |
done |
44872 | 949 |
qed |
66380 | 950 |
from less cong unique show ?thesis |
951 |
by blast |
|
31719 | 952 |
qed |
953 |
||
954 |
end |