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