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