author | haftmann |
Mon, 26 Apr 2010 11:34:19 +0200 | |
changeset 36350 | bc7982c54e37 |
parent 35644 | d20cf282342e |
child 37293 | 2c9ed7478e6e |
permissions | -rw-r--r-- |
31719 | 1 |
(* Title: HOL/Library/Cong.thy |
2 |
ID: |
|
3 |
Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, |
|
4 |
Thomas M. Rasmussen, Jeremy Avigad |
|
5 |
||
6 |
||
7 |
Defines congruence (notation: [x = y] (mod z)) for natural numbers and |
|
8 |
integers. |
|
9 |
||
10 |
This file combines and revises a number of prior developments. |
|
11 |
||
12 |
The original theories "GCD" and "Primes" were by Christophe Tabacznyj |
|
13 |
and Lawrence C. Paulson, based on \cite{davenport92}. They introduced |
|
14 |
gcd, lcm, and prime for the natural numbers. |
|
15 |
||
16 |
The original theory "IntPrimes" was by Thomas M. Rasmussen, and |
|
17 |
extended gcd, lcm, primes to the integers. Amine Chaieb provided |
|
18 |
another extension of the notions to the integers, and added a number |
|
19 |
of results to "Primes" and "GCD". |
|
20 |
||
21 |
The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and |
|
22 |
developed the congruence relations on the integers. The notion was |
|
33718 | 23 |
extended to the natural numbers by Chaieb. Jeremy Avigad combined |
31719 | 24 |
these, revised and tidied them, made the development uniform for the |
25 |
natural numbers and the integers, and added a number of new theorems. |
|
26 |
||
27 |
*) |
|
28 |
||
29 |
||
30 |
header {* Congruence *} |
|
31 |
||
32 |
theory Cong |
|
32479 | 33 |
imports GCD Primes |
31719 | 34 |
begin |
35 |
||
36 |
subsection {* Turn off One_nat_def *} |
|
37 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
38 |
lemma induct'_nat [case_names zero plus1, induct type: nat]: |
31719 | 39 |
"\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n" |
40 |
by (erule nat_induct) (simp add:One_nat_def) |
|
41 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
42 |
lemma cases_nat [case_names zero plus1, cases type: nat]: |
31719 | 43 |
"P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
44 |
by(metis induct'_nat) |
31719 | 45 |
|
46 |
lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n" |
|
47 |
by (simp add: One_nat_def) |
|
48 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
49 |
lemma power_eq_one_eq_nat [simp]: |
31719 | 50 |
"((x::nat)^m = 1) = (m = 0 | x = 1)" |
51 |
by (induct m, auto) |
|
52 |
||
53 |
lemma card_insert_if' [simp]: "finite A \<Longrightarrow> |
|
54 |
card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)" |
|
55 |
by (auto simp add: insert_absorb) |
|
56 |
||
57 |
(* why wasn't card_insert_if a simp rule? *) |
|
58 |
declare card_insert_disjoint [simp del] |
|
59 |
||
60 |
lemma nat_1' [simp]: "nat 1 = 1" |
|
61 |
by simp |
|
62 |
||
31792 | 63 |
(* For those annoying moments where Suc reappears, use Suc_eq_plus1 *) |
31719 | 64 |
|
65 |
declare nat_1 [simp del] |
|
66 |
declare add_2_eq_Suc [simp del] |
|
67 |
declare add_2_eq_Suc' [simp del] |
|
68 |
||
69 |
||
70 |
declare mod_pos_pos_trivial [simp] |
|
71 |
||
72 |
||
73 |
subsection {* Main definitions *} |
|
74 |
||
75 |
class cong = |
|
76 |
||
77 |
fixes |
|
78 |
cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))") |
|
79 |
||
80 |
begin |
|
81 |
||
82 |
abbreviation |
|
83 |
notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))") |
|
84 |
where |
|
85 |
"notcong x y m == (~cong x y m)" |
|
86 |
||
87 |
end |
|
88 |
||
89 |
(* definitions for the natural numbers *) |
|
90 |
||
91 |
instantiation nat :: cong |
|
92 |
||
93 |
begin |
|
94 |
||
95 |
definition |
|
96 |
cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" |
|
97 |
where |
|
98 |
"cong_nat x y m = ((x mod m) = (y mod m))" |
|
99 |
||
100 |
instance proof qed |
|
101 |
||
102 |
end |
|
103 |
||
104 |
||
105 |
(* definitions for the integers *) |
|
106 |
||
107 |
instantiation int :: cong |
|
108 |
||
109 |
begin |
|
110 |
||
111 |
definition |
|
112 |
cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" |
|
113 |
where |
|
114 |
"cong_int x y m = ((x mod m) = (y mod m))" |
|
115 |
||
116 |
instance proof qed |
|
117 |
||
118 |
end |
|
119 |
||
120 |
||
121 |
subsection {* Set up Transfer *} |
|
122 |
||
123 |
||
124 |
lemma transfer_nat_int_cong: |
|
125 |
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow> |
|
126 |
([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))" |
|
127 |
unfolding cong_int_def cong_nat_def |
|
128 |
apply (auto simp add: nat_mod_distrib [symmetric]) |
|
129 |
apply (subst (asm) eq_nat_nat_iff) |
|
130 |
apply (case_tac "m = 0", force, rule pos_mod_sign, force)+ |
|
131 |
apply assumption |
|
132 |
done |
|
133 |
||
35644 | 134 |
declare transfer_morphism_nat_int[transfer add return: |
31719 | 135 |
transfer_nat_int_cong] |
136 |
||
137 |
lemma transfer_int_nat_cong: |
|
138 |
"[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)" |
|
139 |
apply (auto simp add: cong_int_def cong_nat_def) |
|
140 |
apply (auto simp add: zmod_int [symmetric]) |
|
141 |
done |
|
142 |
||
35644 | 143 |
declare transfer_morphism_int_nat[transfer add return: |
31719 | 144 |
transfer_int_nat_cong] |
145 |
||
146 |
||
147 |
subsection {* Congruence *} |
|
148 |
||
149 |
(* was zcong_0, etc. *) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
150 |
lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)" |
31719 | 151 |
by (unfold cong_nat_def, auto) |
152 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
153 |
lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)" |
31719 | 154 |
by (unfold cong_int_def, auto) |
155 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
156 |
lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)" |
31719 | 157 |
by (unfold cong_nat_def, auto) |
158 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
159 |
lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)" |
31719 | 160 |
by (unfold cong_nat_def, auto simp add: One_nat_def) |
161 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
162 |
lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)" |
31719 | 163 |
by (unfold cong_int_def, auto) |
164 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
165 |
lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)" |
31719 | 166 |
by (unfold cong_nat_def, auto) |
167 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
168 |
lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)" |
31719 | 169 |
by (unfold cong_int_def, auto) |
170 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
171 |
lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)" |
31719 | 172 |
by (unfold cong_nat_def, auto) |
173 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
174 |
lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)" |
31719 | 175 |
by (unfold cong_int_def, auto) |
176 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
177 |
lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)" |
31719 | 178 |
by (unfold cong_nat_def, auto) |
179 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
180 |
lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)" |
31719 | 181 |
by (unfold cong_int_def, auto) |
182 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
183 |
lemma cong_trans_nat [trans]: |
31719 | 184 |
"[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)" |
185 |
by (unfold cong_nat_def, auto) |
|
186 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
187 |
lemma cong_trans_int [trans]: |
31719 | 188 |
"[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)" |
189 |
by (unfold cong_int_def, auto) |
|
190 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
191 |
lemma cong_add_nat: |
31719 | 192 |
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)" |
193 |
apply (unfold cong_nat_def) |
|
194 |
apply (subst (1 2) mod_add_eq) |
|
195 |
apply simp |
|
196 |
done |
|
197 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
198 |
lemma cong_add_int: |
31719 | 199 |
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)" |
200 |
apply (unfold cong_int_def) |
|
201 |
apply (subst (1 2) mod_add_left_eq) |
|
202 |
apply (subst (1 2) mod_add_right_eq) |
|
203 |
apply simp |
|
204 |
done |
|
205 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
206 |
lemma cong_diff_int: |
31719 | 207 |
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)" |
208 |
apply (unfold cong_int_def) |
|
209 |
apply (subst (1 2) mod_diff_eq) |
|
210 |
apply simp |
|
211 |
done |
|
212 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
213 |
lemma cong_diff_aux_int: |
31719 | 214 |
"(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow> |
215 |
[c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)" |
|
216 |
apply (subst (1 2) tsub_eq) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
217 |
apply (auto intro: cong_diff_int) |
31719 | 218 |
done; |
219 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
220 |
lemma cong_diff_nat: |
31719 | 221 |
assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and |
222 |
"[c = d] (mod m)" |
|
223 |
shows "[a - c = b - d] (mod m)" |
|
224 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
225 |
using prems by (rule cong_diff_aux_int [transferred]); |
31719 | 226 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
227 |
lemma cong_mult_nat: |
31719 | 228 |
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)" |
229 |
apply (unfold cong_nat_def) |
|
230 |
apply (subst (1 2) mod_mult_eq) |
|
231 |
apply simp |
|
232 |
done |
|
233 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
234 |
lemma cong_mult_int: |
31719 | 235 |
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)" |
236 |
apply (unfold cong_int_def) |
|
237 |
apply (subst (1 2) zmod_zmult1_eq) |
|
238 |
apply (subst (1 2) mult_commute) |
|
239 |
apply (subst (1 2) zmod_zmult1_eq) |
|
240 |
apply simp |
|
241 |
done |
|
242 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
243 |
lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)" |
31719 | 244 |
apply (induct k) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
245 |
apply (auto simp add: cong_refl_nat cong_mult_nat) |
31719 | 246 |
done |
247 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
248 |
lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)" |
31719 | 249 |
apply (induct k) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
250 |
apply (auto simp add: cong_refl_int cong_mult_int) |
31719 | 251 |
done |
252 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
253 |
lemma cong_setsum_nat [rule_format]: |
31719 | 254 |
"(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> |
255 |
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)" |
|
256 |
apply (case_tac "finite A") |
|
257 |
apply (induct set: finite) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
258 |
apply (auto intro: cong_add_nat) |
31719 | 259 |
done |
260 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
261 |
lemma cong_setsum_int [rule_format]: |
31719 | 262 |
"(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> |
263 |
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)" |
|
264 |
apply (case_tac "finite A") |
|
265 |
apply (induct set: finite) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
266 |
apply (auto intro: cong_add_int) |
31719 | 267 |
done |
268 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
269 |
lemma cong_setprod_nat [rule_format]: |
31719 | 270 |
"(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> |
271 |
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)" |
|
272 |
apply (case_tac "finite A") |
|
273 |
apply (induct set: finite) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
274 |
apply (auto intro: cong_mult_nat) |
31719 | 275 |
done |
276 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
277 |
lemma cong_setprod_int [rule_format]: |
31719 | 278 |
"(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> |
279 |
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)" |
|
280 |
apply (case_tac "finite A") |
|
281 |
apply (induct set: finite) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
282 |
apply (auto intro: cong_mult_int) |
31719 | 283 |
done |
284 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
285 |
lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
286 |
by (rule cong_mult_nat, simp_all) |
31719 | 287 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
288 |
lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
289 |
by (rule cong_mult_int, simp_all) |
31719 | 290 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
291 |
lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
292 |
by (rule cong_mult_nat, simp_all) |
31719 | 293 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
294 |
lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
295 |
by (rule cong_mult_int, simp_all) |
31719 | 296 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
297 |
lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)" |
31719 | 298 |
by (unfold cong_nat_def, auto) |
299 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
300 |
lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)" |
31719 | 301 |
by (unfold cong_int_def, auto) |
302 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
303 |
lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)" |
31719 | 304 |
apply (rule iffI) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
305 |
apply (erule cong_diff_int [of a b m b b, simplified]) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
306 |
apply (erule cong_add_int [of "a - b" 0 m b b, simplified]) |
31719 | 307 |
done |
308 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
309 |
lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow> |
31719 | 310 |
[(a::int) = b] (mod m) = [tsub a b = 0] (mod m)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
311 |
by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int) |
31719 | 312 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
313 |
lemma cong_eq_diff_cong_0_nat: |
31719 | 314 |
assumes "(a::nat) >= b" |
315 |
shows "[a = b] (mod m) = [a - b = 0] (mod m)" |
|
316 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
317 |
using prems by (rule cong_eq_diff_cong_0_aux_int [transferred]) |
31719 | 318 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
319 |
lemma cong_diff_cong_0'_nat: |
31719 | 320 |
"[(x::nat) = y] (mod n) \<longleftrightarrow> |
321 |
(if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))" |
|
322 |
apply (case_tac "y <= x") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
323 |
apply (frule cong_eq_diff_cong_0_nat [where m = n]) |
31719 | 324 |
apply auto [1] |
325 |
apply (subgoal_tac "x <= y") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
326 |
apply (frule cong_eq_diff_cong_0_nat [where m = n]) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
327 |
apply (subst cong_sym_eq_nat) |
31719 | 328 |
apply auto |
329 |
done |
|
330 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
331 |
lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
332 |
apply (subst cong_eq_diff_cong_0_nat, assumption) |
31719 | 333 |
apply (unfold cong_nat_def) |
334 |
apply (simp add: dvd_eq_mod_eq_0 [symmetric]) |
|
335 |
done |
|
336 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
337 |
lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
338 |
apply (subst cong_eq_diff_cong_0_int) |
31719 | 339 |
apply (unfold cong_int_def) |
340 |
apply (simp add: dvd_eq_mod_eq_0 [symmetric]) |
|
341 |
done |
|
342 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
343 |
lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
344 |
by (simp add: cong_altdef_int) |
31719 | 345 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
346 |
lemma cong_square_int: |
31719 | 347 |
"\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk> |
348 |
\<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
349 |
apply (simp only: cong_altdef_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
350 |
apply (subst prime_dvd_mult_eq_int [symmetric], assumption) |
31719 | 351 |
(* any way around this? *) |
352 |
apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)") |
|
36350 | 353 |
apply (auto simp add: field_simps) |
31719 | 354 |
done |
355 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
356 |
lemma cong_mult_rcancel_int: |
31719 | 357 |
"coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
358 |
apply (subst (1 2) cong_altdef_int) |
31719 | 359 |
apply (subst left_diff_distrib [symmetric]) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
360 |
apply (rule coprime_dvd_mult_iff_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
361 |
apply (subst gcd_commute_int, assumption) |
31719 | 362 |
done |
363 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
364 |
lemma cong_mult_rcancel_nat: |
31719 | 365 |
assumes "coprime k (m::nat)" |
366 |
shows "[a * k = b * k] (mod m) = [a = b] (mod m)" |
|
367 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
368 |
apply (rule cong_mult_rcancel_int [transferred]) |
31719 | 369 |
using prems apply auto |
370 |
done |
|
371 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
372 |
lemma cong_mult_lcancel_nat: |
31719 | 373 |
"coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
374 |
by (simp add: mult_commute cong_mult_rcancel_nat) |
31719 | 375 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
376 |
lemma cong_mult_lcancel_int: |
31719 | 377 |
"coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
378 |
by (simp add: mult_commute cong_mult_rcancel_int) |
31719 | 379 |
|
380 |
(* was zcong_zgcd_zmult_zmod *) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
381 |
lemma coprime_cong_mult_int: |
31719 | 382 |
"[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n |
383 |
\<Longrightarrow> [a = b] (mod m * n)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
384 |
apply (simp only: cong_altdef_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
385 |
apply (erule (2) divides_mult_int) |
31719 | 386 |
done |
387 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
388 |
lemma coprime_cong_mult_nat: |
31719 | 389 |
assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n" |
390 |
shows "[a = b] (mod m * n)" |
|
391 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
392 |
apply (rule coprime_cong_mult_int [transferred]) |
31719 | 393 |
using prems apply auto |
394 |
done |
|
395 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
396 |
lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow> |
31719 | 397 |
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" |
398 |
by (auto simp add: cong_nat_def mod_pos_pos_trivial) |
|
399 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
400 |
lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow> |
31719 | 401 |
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" |
402 |
by (auto simp add: cong_int_def mod_pos_pos_trivial) |
|
403 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
404 |
lemma cong_less_unique_nat: |
31719 | 405 |
"0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
406 |
apply auto |
|
407 |
apply (rule_tac x = "a mod m" in exI) |
|
408 |
apply (unfold cong_nat_def, auto) |
|
409 |
done |
|
410 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
411 |
lemma cong_less_unique_int: |
31719 | 412 |
"0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
413 |
apply auto |
|
414 |
apply (rule_tac x = "a mod m" in exI) |
|
415 |
apply (unfold cong_int_def, auto simp add: mod_pos_pos_trivial) |
|
416 |
done |
|
417 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
418 |
lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)" |
36350 | 419 |
apply (auto simp add: cong_altdef_int dvd_def field_simps) |
31719 | 420 |
apply (rule_tac [!] x = "-k" in exI, auto) |
421 |
done |
|
422 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
423 |
lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) = |
31719 | 424 |
(\<exists>k1 k2. b + k1 * m = a + k2 * m)" |
425 |
apply (rule iffI) |
|
426 |
apply (case_tac "b <= a") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
427 |
apply (subst (asm) cong_altdef_nat, assumption) |
31719 | 428 |
apply (unfold dvd_def, auto) |
429 |
apply (rule_tac x = k in exI) |
|
430 |
apply (rule_tac x = 0 in exI) |
|
36350 | 431 |
apply (auto simp add: field_simps) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
432 |
apply (subst (asm) cong_sym_eq_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
433 |
apply (subst (asm) cong_altdef_nat) |
31719 | 434 |
apply force |
435 |
apply (unfold dvd_def, auto) |
|
436 |
apply (rule_tac x = 0 in exI) |
|
437 |
apply (rule_tac x = k in exI) |
|
36350 | 438 |
apply (auto simp add: field_simps) |
31719 | 439 |
apply (unfold cong_nat_def) |
440 |
apply (subgoal_tac "a mod m = (a + k2 * m) mod m") |
|
441 |
apply (erule ssubst)back |
|
442 |
apply (erule subst) |
|
443 |
apply auto |
|
444 |
done |
|
445 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
446 |
lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
447 |
apply (subst (asm) cong_iff_lin_int, auto) |
31719 | 448 |
apply (subst add_commute) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
449 |
apply (subst (2) gcd_commute_int) |
31719 | 450 |
apply (subst mult_commute) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
451 |
apply (subst gcd_add_mult_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
452 |
apply (rule gcd_commute_int) |
31719 | 453 |
done |
454 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
455 |
lemma cong_gcd_eq_nat: |
31719 | 456 |
assumes "[(a::nat) = b] (mod m)" |
457 |
shows "gcd a m = gcd b m" |
|
458 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
459 |
apply (rule cong_gcd_eq_int [transferred]) |
31719 | 460 |
using prems apply auto |
461 |
done |
|
462 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
463 |
lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> |
31719 | 464 |
coprime b m" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
465 |
by (auto simp add: cong_gcd_eq_nat) |
31719 | 466 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
467 |
lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> |
31719 | 468 |
coprime b m" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
469 |
by (auto simp add: cong_gcd_eq_int) |
31719 | 470 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
471 |
lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = |
31719 | 472 |
[a mod m = b mod m] (mod m)" |
473 |
by (auto simp add: cong_nat_def) |
|
474 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
475 |
lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = |
31719 | 476 |
[a mod m = b mod m] (mod m)" |
477 |
by (auto simp add: cong_int_def) |
|
478 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
479 |
lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
480 |
by (subst (1 2) cong_altdef_int, auto) |
31719 | 481 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
482 |
lemma cong_zero_nat [iff]: "[(a::nat) = b] (mod 0) = (a = b)" |
31719 | 483 |
by (auto simp add: cong_nat_def) |
484 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
485 |
lemma cong_zero_int [iff]: "[(a::int) = b] (mod 0) = (a = b)" |
31719 | 486 |
by (auto simp add: cong_int_def) |
487 |
||
488 |
(* |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
489 |
lemma mod_dvd_mod_int: |
31719 | 490 |
"0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)" |
491 |
apply (unfold dvd_def, auto) |
|
492 |
apply (rule mod_mod_cancel) |
|
493 |
apply auto |
|
494 |
done |
|
495 |
||
496 |
lemma mod_dvd_mod: |
|
497 |
assumes "0 < (m::nat)" and "m dvd b" |
|
498 |
shows "(a mod b mod m) = (a mod m)" |
|
499 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
500 |
apply (rule mod_dvd_mod_int [transferred]) |
31719 | 501 |
using prems apply auto |
502 |
done |
|
503 |
*) |
|
504 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
505 |
lemma cong_add_lcancel_nat: |
31719 | 506 |
"[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
507 |
by (simp add: cong_iff_lin_nat) |
31719 | 508 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
509 |
lemma cong_add_lcancel_int: |
31719 | 510 |
"[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
511 |
by (simp add: cong_iff_lin_int) |
31719 | 512 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
513 |
lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
514 |
by (simp add: cong_iff_lin_nat) |
31719 | 515 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
516 |
lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
517 |
by (simp add: cong_iff_lin_int) |
31719 | 518 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
519 |
lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
520 |
by (simp add: cong_iff_lin_nat) |
31719 | 521 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
522 |
lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
523 |
by (simp add: cong_iff_lin_int) |
31719 | 524 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
525 |
lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
526 |
by (simp add: cong_iff_lin_nat) |
31719 | 527 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
528 |
lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
529 |
by (simp add: cong_iff_lin_int) |
31719 | 530 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
531 |
lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> |
31719 | 532 |
[x = y] (mod n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
533 |
apply (auto simp add: cong_iff_lin_nat dvd_def) |
31719 | 534 |
apply (rule_tac x="k1 * k" in exI) |
535 |
apply (rule_tac x="k2 * k" in exI) |
|
36350 | 536 |
apply (simp add: field_simps) |
31719 | 537 |
done |
538 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
539 |
lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> |
31719 | 540 |
[x = y] (mod n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
541 |
by (auto simp add: cong_altdef_int dvd_def) |
31719 | 542 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
543 |
lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y" |
31719 | 544 |
by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0) |
545 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
546 |
lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y" |
31719 | 547 |
by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0) |
548 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
549 |
lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" |
31719 | 550 |
by (simp add: cong_nat_def) |
551 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
552 |
lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" |
31719 | 553 |
by (simp add: cong_int_def) |
554 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
555 |
lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0 |
31719 | 556 |
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)" |
557 |
by (simp add: cong_nat_def mod_mult2_eq mod_add_left_eq) |
|
558 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
559 |
lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
560 |
apply (simp add: cong_altdef_int) |
31719 | 561 |
apply (subst dvd_minus_iff [symmetric]) |
36350 | 562 |
apply (simp add: field_simps) |
31719 | 563 |
done |
564 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
565 |
lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
566 |
by (auto simp add: cong_altdef_int) |
31719 | 567 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
568 |
lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0 |
31719 | 569 |
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)" |
570 |
apply (case_tac "b > 0") |
|
571 |
apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
572 |
apply (subst (1 2) cong_modulus_neg_int) |
31719 | 573 |
apply (unfold cong_int_def) |
574 |
apply (subgoal_tac "a * b = (-a * -b)") |
|
575 |
apply (erule ssubst) |
|
576 |
apply (subst zmod_zmult2_eq) |
|
577 |
apply (auto simp add: mod_add_left_eq) |
|
578 |
done |
|
579 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
580 |
lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))" |
31719 | 581 |
apply (case_tac "a = 0") |
582 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
583 |
apply (subst (asm) cong_altdef_nat) |
31719 | 584 |
apply auto |
585 |
done |
|
586 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
587 |
lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)" |
31719 | 588 |
by (unfold cong_nat_def, auto) |
589 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
590 |
lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))" |
31719 | 591 |
by (unfold cong_int_def, auto simp add: zmult_eq_1_iff) |
592 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
593 |
lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow> |
31719 | 594 |
a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)" |
595 |
apply (case_tac "n = 1") |
|
596 |
apply auto [1] |
|
597 |
apply (drule_tac x = "a - 1" in spec) |
|
598 |
apply force |
|
599 |
apply (case_tac "a = 0") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
600 |
apply (auto simp add: cong_0_1_nat) [1] |
31719 | 601 |
apply (rule iffI) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
602 |
apply (drule cong_to_1_nat) |
31719 | 603 |
apply (unfold dvd_def) |
604 |
apply auto [1] |
|
605 |
apply (rule_tac x = k in exI) |
|
36350 | 606 |
apply (auto simp add: field_simps) [1] |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
607 |
apply (subst cong_altdef_nat) |
31719 | 608 |
apply (auto simp add: dvd_def) |
609 |
done |
|
610 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
611 |
lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
612 |
apply (subst cong_altdef_nat) |
31719 | 613 |
apply assumption |
36350 | 614 |
apply (unfold dvd_def, auto simp add: field_simps) |
31719 | 615 |
apply (rule_tac x = k in exI) |
616 |
apply auto |
|
617 |
done |
|
618 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
619 |
lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)" |
31719 | 620 |
apply (case_tac "n = 0") |
621 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
622 |
apply (frule bezout_nat [of a n], auto) |
31719 | 623 |
apply (rule exI, erule ssubst) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
624 |
apply (rule cong_trans_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
625 |
apply (rule cong_add_nat) |
31719 | 626 |
apply (subst mult_commute) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
627 |
apply (rule cong_mult_self_nat) |
31719 | 628 |
prefer 2 |
629 |
apply simp |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
630 |
apply (rule cong_refl_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
631 |
apply (rule cong_refl_nat) |
31719 | 632 |
done |
633 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
634 |
lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)" |
31719 | 635 |
apply (case_tac "n = 0") |
636 |
apply (case_tac "a \<ge> 0") |
|
637 |
apply auto |
|
638 |
apply (rule_tac x = "-1" in exI) |
|
639 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
640 |
apply (insert bezout_int [of a n], auto) |
31719 | 641 |
apply (rule exI) |
642 |
apply (erule subst) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
643 |
apply (rule cong_trans_int) |
31719 | 644 |
prefer 2 |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
645 |
apply (rule cong_add_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
646 |
apply (rule cong_refl_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
647 |
apply (rule cong_sym_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
648 |
apply (rule cong_mult_self_int) |
31719 | 649 |
apply simp |
650 |
apply (subst mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
651 |
apply (rule cong_refl_int) |
31719 | 652 |
done |
653 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
654 |
lemma cong_solve_dvd_nat: |
31719 | 655 |
assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d" |
656 |
shows "EX x. [a * x = d] (mod n)" |
|
657 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
658 |
from cong_solve_nat [OF a] obtain x where |
31719 | 659 |
"[a * x = gcd a n](mod n)" |
660 |
by auto |
|
661 |
hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
662 |
by (elim cong_scalar2_nat) |
31719 | 663 |
also from b have "(d div gcd a n) * gcd a n = d" |
664 |
by (rule dvd_div_mult_self) |
|
665 |
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" |
|
666 |
by auto |
|
667 |
finally show ?thesis |
|
668 |
by auto |
|
669 |
qed |
|
670 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
671 |
lemma cong_solve_dvd_int: |
31719 | 672 |
assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d" |
673 |
shows "EX x. [a * x = d] (mod n)" |
|
674 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
675 |
from cong_solve_int [OF a] obtain x where |
31719 | 676 |
"[a * x = gcd a n](mod n)" |
677 |
by auto |
|
678 |
hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
679 |
by (elim cong_scalar2_int) |
31719 | 680 |
also from b have "(d div gcd a n) * gcd a n = d" |
681 |
by (rule dvd_div_mult_self) |
|
682 |
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" |
|
683 |
by auto |
|
684 |
finally show ?thesis |
|
685 |
by auto |
|
686 |
qed |
|
687 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
688 |
lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> |
31719 | 689 |
EX x. [a * x = 1] (mod n)" |
690 |
apply (case_tac "a = 0") |
|
691 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
692 |
apply (frule cong_solve_nat [of a n]) |
31719 | 693 |
apply auto |
694 |
done |
|
695 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
696 |
lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> |
31719 | 697 |
EX x. [a * x = 1] (mod n)" |
698 |
apply (case_tac "a = 0") |
|
699 |
apply auto |
|
700 |
apply (case_tac "n \<ge> 0") |
|
701 |
apply auto |
|
702 |
apply (subst cong_int_def, auto) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
703 |
apply (frule cong_solve_int [of a n]) |
31719 | 704 |
apply auto |
705 |
done |
|
706 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
707 |
lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = |
31719 | 708 |
(EX x. [a * x = 1] (mod m))" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
709 |
apply (auto intro: cong_solve_coprime_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
710 |
apply (unfold cong_nat_def, auto intro: invertible_coprime_nat) |
31719 | 711 |
done |
712 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
713 |
lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = |
31719 | 714 |
(EX x. [a * x = 1] (mod m))" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
715 |
apply (auto intro: cong_solve_coprime_int) |
31719 | 716 |
apply (unfold cong_int_def) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
717 |
apply (auto intro: invertible_coprime_int) |
31719 | 718 |
done |
719 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
720 |
lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m = |
31719 | 721 |
(EX x. 0 <= x & x < m & [a * x = 1] (mod m))" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
722 |
apply (subst coprime_iff_invertible_int) |
31719 | 723 |
apply auto |
724 |
apply (auto simp add: cong_int_def) |
|
725 |
apply (rule_tac x = "x mod m" in exI) |
|
726 |
apply (auto simp add: mod_mult_right_eq [symmetric]) |
|
727 |
done |
|
728 |
||
729 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
730 |
lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow> |
31719 | 731 |
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" |
732 |
apply (case_tac "y \<le> x") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
733 |
apply (auto simp add: cong_altdef_nat lcm_least_nat) [1] |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
734 |
apply (rule cong_sym_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
735 |
apply (subst (asm) (1 2) cong_sym_eq_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
736 |
apply (auto simp add: cong_altdef_nat lcm_least_nat) |
31719 | 737 |
done |
738 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
739 |
lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow> |
31719 | 740 |
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
741 |
by (auto simp add: cong_altdef_int lcm_least_int) [1] |
31719 | 742 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
743 |
lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow> |
31719 | 744 |
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
745 |
apply (frule (1) cong_cong_lcm_nat)back |
31719 | 746 |
apply (simp add: lcm_nat_def) |
747 |
done |
|
748 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
749 |
lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow> |
31719 | 750 |
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
751 |
apply (frule (1) cong_cong_lcm_int)back |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
752 |
apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric]) |
31719 | 753 |
done |
754 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
755 |
lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow> |
31719 | 756 |
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
757 |
(ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow> |
|
758 |
[x = y] (mod (PROD i:A. m i))" |
|
759 |
apply (induct set: finite) |
|
760 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
761 |
apply (rule cong_cong_coprime_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
762 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
763 |
apply (rule setprod_coprime_nat) |
31719 | 764 |
apply auto |
765 |
done |
|
766 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
767 |
lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow> |
31719 | 768 |
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
769 |
(ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow> |
|
770 |
[x = y] (mod (PROD i:A. m i))" |
|
771 |
apply (induct set: finite) |
|
772 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
773 |
apply (rule cong_cong_coprime_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
774 |
apply (subst gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
775 |
apply (rule setprod_coprime_int) |
31719 | 776 |
apply auto |
777 |
done |
|
778 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
779 |
lemma binary_chinese_remainder_aux_nat: |
31719 | 780 |
assumes a: "coprime (m1::nat) m2" |
781 |
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> |
|
782 |
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
|
783 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
784 |
from cong_solve_coprime_nat [OF a] |
31719 | 785 |
obtain x1 where one: "[m1 * x1 = 1] (mod m2)" |
786 |
by auto |
|
787 |
from a have b: "coprime m2 m1" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
788 |
by (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
789 |
from cong_solve_coprime_nat [OF b] |
31719 | 790 |
obtain x2 where two: "[m2 * x2 = 1] (mod m1)" |
791 |
by auto |
|
792 |
have "[m1 * x1 = 0] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
793 |
by (subst mult_commute, rule cong_mult_self_nat) |
31719 | 794 |
moreover have "[m2 * x2 = 0] (mod m2)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
795 |
by (subst mult_commute, rule cong_mult_self_nat) |
31719 | 796 |
moreover note one two |
797 |
ultimately show ?thesis by blast |
|
798 |
qed |
|
799 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
800 |
lemma binary_chinese_remainder_aux_int: |
31719 | 801 |
assumes a: "coprime (m1::int) m2" |
802 |
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> |
|
803 |
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
|
804 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
805 |
from cong_solve_coprime_int [OF a] |
31719 | 806 |
obtain x1 where one: "[m1 * x1 = 1] (mod m2)" |
807 |
by auto |
|
808 |
from a have b: "coprime m2 m1" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
809 |
by (subst gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
810 |
from cong_solve_coprime_int [OF b] |
31719 | 811 |
obtain x2 where two: "[m2 * x2 = 1] (mod m1)" |
812 |
by auto |
|
813 |
have "[m1 * x1 = 0] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
814 |
by (subst mult_commute, rule cong_mult_self_int) |
31719 | 815 |
moreover have "[m2 * x2 = 0] (mod m2)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
816 |
by (subst mult_commute, rule cong_mult_self_int) |
31719 | 817 |
moreover note one two |
818 |
ultimately show ?thesis by blast |
|
819 |
qed |
|
820 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
821 |
lemma binary_chinese_remainder_nat: |
31719 | 822 |
assumes a: "coprime (m1::nat) m2" |
823 |
shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
824 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
825 |
from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2 |
31719 | 826 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and |
827 |
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
828 |
by blast |
|
829 |
let ?x = "u1 * b1 + u2 * b2" |
|
830 |
have "[?x = u1 * 1 + u2 * 0] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
831 |
apply (rule cong_add_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
832 |
apply (rule cong_scalar2_nat) |
31719 | 833 |
apply (rule `[b1 = 1] (mod m1)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
834 |
apply (rule cong_scalar2_nat) |
31719 | 835 |
apply (rule `[b2 = 0] (mod m1)`) |
836 |
done |
|
837 |
hence "[?x = u1] (mod m1)" by simp |
|
838 |
have "[?x = u1 * 0 + u2 * 1] (mod m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
839 |
apply (rule cong_add_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
840 |
apply (rule cong_scalar2_nat) |
31719 | 841 |
apply (rule `[b1 = 0] (mod m2)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
842 |
apply (rule cong_scalar2_nat) |
31719 | 843 |
apply (rule `[b2 = 1] (mod m2)`) |
844 |
done |
|
845 |
hence "[?x = u2] (mod m2)" by simp |
|
846 |
with `[?x = u1] (mod m1)` show ?thesis by blast |
|
847 |
qed |
|
848 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
849 |
lemma binary_chinese_remainder_int: |
31719 | 850 |
assumes a: "coprime (m1::int) m2" |
851 |
shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
852 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
853 |
from binary_chinese_remainder_aux_int [OF a] obtain b1 b2 |
31719 | 854 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and |
855 |
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
856 |
by blast |
|
857 |
let ?x = "u1 * b1 + u2 * b2" |
|
858 |
have "[?x = u1 * 1 + u2 * 0] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
859 |
apply (rule cong_add_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
860 |
apply (rule cong_scalar2_int) |
31719 | 861 |
apply (rule `[b1 = 1] (mod m1)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
862 |
apply (rule cong_scalar2_int) |
31719 | 863 |
apply (rule `[b2 = 0] (mod m1)`) |
864 |
done |
|
865 |
hence "[?x = u1] (mod m1)" by simp |
|
866 |
have "[?x = u1 * 0 + u2 * 1] (mod m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
867 |
apply (rule cong_add_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
868 |
apply (rule cong_scalar2_int) |
31719 | 869 |
apply (rule `[b1 = 0] (mod m2)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
870 |
apply (rule cong_scalar2_int) |
31719 | 871 |
apply (rule `[b2 = 1] (mod m2)`) |
872 |
done |
|
873 |
hence "[?x = u2] (mod m2)" by simp |
|
874 |
with `[?x = u1] (mod m1)` show ?thesis by blast |
|
875 |
qed |
|
876 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
877 |
lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow> |
31719 | 878 |
[x = y] (mod m)" |
879 |
apply (case_tac "y \<le> x") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
880 |
apply (simp add: cong_altdef_nat) |
31719 | 881 |
apply (erule dvd_mult_left) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
882 |
apply (rule cong_sym_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
883 |
apply (subst (asm) cong_sym_eq_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
884 |
apply (simp add: cong_altdef_nat) |
31719 | 885 |
apply (erule dvd_mult_left) |
886 |
done |
|
887 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
888 |
lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow> |
31719 | 889 |
[x = y] (mod m)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
890 |
apply (simp add: cong_altdef_int) |
31719 | 891 |
apply (erule dvd_mult_left) |
892 |
done |
|
893 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
894 |
lemma cong_less_modulus_unique_nat: |
31719 | 895 |
"[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y" |
896 |
by (simp add: cong_nat_def) |
|
897 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
898 |
lemma binary_chinese_remainder_unique_nat: |
31719 | 899 |
assumes a: "coprime (m1::nat) m2" and |
900 |
nz: "m1 \<noteq> 0" "m2 \<noteq> 0" |
|
901 |
shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
902 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
903 |
from binary_chinese_remainder_nat [OF a] obtain y where |
31719 | 904 |
"[y = u1] (mod m1)" and "[y = u2] (mod m2)" |
905 |
by blast |
|
906 |
let ?x = "y mod (m1 * m2)" |
|
907 |
from nz have less: "?x < m1 * m2" |
|
908 |
by auto |
|
909 |
have one: "[?x = u1] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
910 |
apply (rule cong_trans_nat) |
31719 | 911 |
prefer 2 |
912 |
apply (rule `[y = u1] (mod m1)`) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
913 |
apply (rule cong_modulus_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
914 |
apply (rule cong_mod_nat) |
31719 | 915 |
using nz apply auto |
916 |
done |
|
917 |
have two: "[?x = u2] (mod m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
918 |
apply (rule cong_trans_nat) |
31719 | 919 |
prefer 2 |
920 |
apply (rule `[y = u2] (mod m2)`) |
|
921 |
apply (subst mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
922 |
apply (rule cong_modulus_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
923 |
apply (rule cong_mod_nat) |
31719 | 924 |
using nz apply auto |
925 |
done |
|
926 |
have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> |
|
927 |
z = ?x" |
|
928 |
proof (clarify) |
|
929 |
fix z |
|
930 |
assume "z < m1 * m2" |
|
931 |
assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)" |
|
932 |
have "[?x = z] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
933 |
apply (rule cong_trans_nat) |
31719 | 934 |
apply (rule `[?x = u1] (mod m1)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
935 |
apply (rule cong_sym_nat) |
31719 | 936 |
apply (rule `[z = u1] (mod m1)`) |
937 |
done |
|
938 |
moreover have "[?x = z] (mod m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
939 |
apply (rule cong_trans_nat) |
31719 | 940 |
apply (rule `[?x = u2] (mod m2)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
941 |
apply (rule cong_sym_nat) |
31719 | 942 |
apply (rule `[z = u2] (mod m2)`) |
943 |
done |
|
944 |
ultimately have "[?x = z] (mod m1 * m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
945 |
by (auto intro: coprime_cong_mult_nat a) |
31719 | 946 |
with `z < m1 * m2` `?x < m1 * m2` show "z = ?x" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
947 |
apply (intro cong_less_modulus_unique_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
948 |
apply (auto, erule cong_sym_nat) |
31719 | 949 |
done |
950 |
qed |
|
951 |
with less one two show ?thesis |
|
952 |
by auto |
|
953 |
qed |
|
954 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
955 |
lemma chinese_remainder_aux_nat: |
31719 | 956 |
fixes A :: "'a set" and |
957 |
m :: "'a \<Rightarrow> nat" |
|
958 |
assumes fin: "finite A" and |
|
959 |
cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
|
960 |
shows "EX b. (ALL i : A. |
|
961 |
[b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))" |
|
962 |
proof (rule finite_set_choice, rule fin, rule ballI) |
|
963 |
fix i |
|
964 |
assume "i : A" |
|
965 |
with cop have "coprime (PROD j : A - {i}. m j) (m i)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
966 |
by (intro setprod_coprime_nat, auto) |
31719 | 967 |
hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
968 |
by (elim cong_solve_coprime_nat) |
31719 | 969 |
then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)" |
970 |
by auto |
|
971 |
moreover have "[(PROD j : A - {i}. m j) * x = 0] |
|
972 |
(mod (PROD j : A - {i}. m j))" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
973 |
by (subst mult_commute, rule cong_mult_self_nat) |
31719 | 974 |
ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] |
975 |
(mod setprod m (A - {i}))" |
|
976 |
by blast |
|
977 |
qed |
|
978 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
979 |
lemma chinese_remainder_nat: |
31719 | 980 |
fixes A :: "'a set" and |
981 |
m :: "'a \<Rightarrow> nat" and |
|
982 |
u :: "'a \<Rightarrow> nat" |
|
983 |
assumes |
|
984 |
fin: "finite A" and |
|
985 |
cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
|
986 |
shows "EX x. (ALL i:A. [x = u i] (mod m i))" |
|
987 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
988 |
from chinese_remainder_aux_nat [OF fin cop] obtain b where |
31719 | 989 |
bprop: "ALL i:A. [b i = 1] (mod m i) \<and> |
990 |
[b i = 0] (mod (PROD j : A - {i}. m j))" |
|
991 |
by blast |
|
992 |
let ?x = "SUM i:A. (u i) * (b i)" |
|
993 |
show "?thesis" |
|
994 |
proof (rule exI, clarify) |
|
995 |
fix i |
|
996 |
assume a: "i : A" |
|
997 |
show "[?x = u i] (mod m i)" |
|
998 |
proof - |
|
999 |
from fin a have "?x = (SUM j:{i}. u j * b j) + |
|
1000 |
(SUM j:A-{i}. u j * b j)" |
|
1001 |
by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong) |
|
1002 |
hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)" |
|
1003 |
by auto |
|
1004 |
also have "[u i * b i + (SUM j:A-{i}. u j * b j) = |
|
1005 |
u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1006 |
apply (rule cong_add_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1007 |
apply (rule cong_scalar2_nat) |
31719 | 1008 |
using bprop a apply blast |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1009 |
apply (rule cong_setsum_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1010 |
apply (rule cong_scalar2_nat) |
31719 | 1011 |
using bprop apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1012 |
apply (rule cong_dvd_modulus_nat) |
31719 | 1013 |
apply (drule (1) bspec) |
1014 |
apply (erule conjE) |
|
1015 |
apply assumption |
|
1016 |
apply (rule dvd_setprod) |
|
1017 |
using fin a apply auto |
|
1018 |
done |
|
1019 |
finally show ?thesis |
|
1020 |
by simp |
|
1021 |
qed |
|
1022 |
qed |
|
1023 |
qed |
|
1024 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1025 |
lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow> |
31719 | 1026 |
(ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
1027 |
(ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow> |
|
1028 |
[x = y] (mod (PROD i:A. m i))" |
|
1029 |
apply (induct set: finite) |
|
1030 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1031 |
apply (erule (1) coprime_cong_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1032 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1033 |
apply (rule setprod_coprime_nat) |
31719 | 1034 |
apply auto |
1035 |
done |
|
1036 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1037 |
lemma chinese_remainder_unique_nat: |
31719 | 1038 |
fixes A :: "'a set" and |
1039 |
m :: "'a \<Rightarrow> nat" and |
|
1040 |
u :: "'a \<Rightarrow> nat" |
|
1041 |
assumes |
|
1042 |
fin: "finite A" and |
|
1043 |
nz: "ALL i:A. m i \<noteq> 0" and |
|
1044 |
cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
|
1045 |
shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))" |
|
1046 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1047 |
from chinese_remainder_nat [OF fin cop] obtain y where |
31719 | 1048 |
one: "(ALL i:A. [y = u i] (mod m i))" |
1049 |
by blast |
|
1050 |
let ?x = "y mod (PROD i:A. m i)" |
|
1051 |
from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0" |
|
1052 |
by auto |
|
1053 |
hence less: "?x < (PROD i:A. m i)" |
|
1054 |
by auto |
|
1055 |
have cong: "ALL i:A. [?x = u i] (mod m i)" |
|
1056 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1057 |
apply (rule cong_trans_nat) |
31719 | 1058 |
prefer 2 |
1059 |
using one apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1060 |
apply (rule cong_dvd_modulus_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1061 |
apply (rule cong_mod_nat) |
31719 | 1062 |
using prodnz apply auto |
1063 |
apply (rule dvd_setprod) |
|
1064 |
apply (rule fin) |
|
1065 |
apply assumption |
|
1066 |
done |
|
1067 |
have unique: "ALL z. z < (PROD i:A. m i) \<and> |
|
1068 |
(ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x" |
|
1069 |
proof (clarify) |
|
1070 |
fix z |
|
1071 |
assume zless: "z < (PROD i:A. m i)" |
|
1072 |
assume zcong: "(ALL i:A. [z = u i] (mod m i))" |
|
1073 |
have "ALL i:A. [?x = z] (mod m i)" |
|
1074 |
apply clarify |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1075 |
apply (rule cong_trans_nat) |
31719 | 1076 |
using cong apply (erule bspec) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1077 |
apply (rule cong_sym_nat) |
31719 | 1078 |
using zcong apply auto |
1079 |
done |
|
1080 |
with fin cop have "[?x = z] (mod (PROD i:A. m i))" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1081 |
by (intro coprime_cong_prod_nat, auto) |
31719 | 1082 |
with zless less show "z = ?x" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1083 |
apply (intro cong_less_modulus_unique_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
1084 |
apply (auto, erule cong_sym_nat) |
31719 | 1085 |
done |
1086 |
qed |
|
1087 |
from less cong unique show ?thesis |
|
1088 |
by blast |
|
1089 |
qed |
|
1090 |
||
1091 |
end |