author | paulson <lp15@cam.ac.uk> |
Fri, 24 Jan 2014 15:21:00 +0000 | |
changeset 55130 | 70db8d380d62 |
parent 54489 | 03ff4d1e6784 |
child 55161 | 8eb891539804 |
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 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 |
||
40 |
subsection {* Main definitions *} |
|
41 |
||
42 |
class cong = |
|
44872 | 43 |
fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))") |
31719 | 44 |
begin |
45 |
||
44872 | 46 |
abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))") |
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 |
||
77 |
subsection {* Set up Transfer *} |
|
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 |
||
100 |
subsection {* Congruence *} |
|
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: |
44872 | 157 |
"(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow> |
31719 | 158 |
[c = d] (mod m) \<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: |
31719 | 162 |
assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and |
163 |
"[c = d] (mod m)" |
|
164 |
shows "[a - c = b - d] (mod m)" |
|
41541 | 165 |
using assms by (rule cong_diff_aux_int [transferred]); |
31719 | 166 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
167 |
lemma cong_mult_nat: |
31719 | 168 |
"[(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
|
169 |
unfolding cong_nat_def by (metis mod_mult_cong) |
31719 | 170 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
171 |
lemma cong_mult_int: |
31719 | 172 |
"[(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
|
173 |
unfolding cong_int_def by (metis mod_mult_cong) |
31719 | 174 |
|
44872 | 175 |
lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)" |
176 |
by (induct k) (auto simp add: cong_mult_nat) |
|
177 |
||
178 |
lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)" |
|
179 |
by (induct k) (auto simp add: cong_mult_int) |
|
180 |
||
181 |
lemma cong_setsum_nat [rule_format]: |
|
182 |
"(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> |
|
31719 | 183 |
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)" |
44872 | 184 |
apply (cases "finite A") |
31719 | 185 |
apply (induct set: finite) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
186 |
apply (auto intro: cong_add_nat) |
44872 | 187 |
done |
31719 | 188 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
189 |
lemma cong_setsum_int [rule_format]: |
44872 | 190 |
"(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> |
31719 | 191 |
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)" |
44872 | 192 |
apply (cases "finite A") |
31719 | 193 |
apply (induct set: finite) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
194 |
apply (auto intro: cong_add_int) |
44872 | 195 |
done |
31719 | 196 |
|
44872 | 197 |
lemma cong_setprod_nat [rule_format]: |
198 |
"(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> |
|
31719 | 199 |
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)" |
44872 | 200 |
apply (cases "finite A") |
31719 | 201 |
apply (induct set: finite) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
202 |
apply (auto intro: cong_mult_nat) |
44872 | 203 |
done |
31719 | 204 |
|
44872 | 205 |
lemma cong_setprod_int [rule_format]: |
206 |
"(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> |
|
31719 | 207 |
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)" |
44872 | 208 |
apply (cases "finite A") |
31719 | 209 |
apply (induct set: finite) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
210 |
apply (auto intro: cong_mult_int) |
44872 | 211 |
done |
31719 | 212 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
213 |
lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)" |
44872 | 214 |
by (rule cong_mult_nat) simp_all |
31719 | 215 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
216 |
lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)" |
44872 | 217 |
by (rule cong_mult_int) simp_all |
31719 | 218 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
219 |
lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)" |
44872 | 220 |
by (rule cong_mult_nat) simp_all |
31719 | 221 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
222 |
lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)" |
44872 | 223 |
by (rule cong_mult_int) simp_all |
31719 | 224 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
225 |
lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)" |
44872 | 226 |
unfolding cong_nat_def by auto |
31719 | 227 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
228 |
lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)" |
44872 | 229 |
unfolding cong_int_def by auto |
31719 | 230 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
231 |
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
|
232 |
by (metis cong_add_int cong_diff_int cong_refl_int diff_add_cancel diff_self) |
31719 | 233 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
234 |
lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow> |
31719 | 235 |
[(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
|
236 |
by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int) |
31719 | 237 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
238 |
lemma cong_eq_diff_cong_0_nat: |
31719 | 239 |
assumes "(a::nat) >= b" |
240 |
shows "[a = b] (mod m) = [a - b = 0] (mod m)" |
|
41541 | 241 |
using assms by (rule cong_eq_diff_cong_0_aux_int [transferred]) |
31719 | 242 |
|
44872 | 243 |
lemma cong_diff_cong_0'_nat: |
244 |
"[(x::nat) = y] (mod n) \<longleftrightarrow> |
|
31719 | 245 |
(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
|
246 |
by (metis cong_eq_diff_cong_0_nat cong_sym_nat nat_le_linear) |
31719 | 247 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
248 |
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
|
249 |
apply (subst cong_eq_diff_cong_0_nat, assumption) |
31719 | 250 |
apply (unfold cong_nat_def) |
251 |
apply (simp add: dvd_eq_mod_eq_0 [symmetric]) |
|
44872 | 252 |
done |
31719 | 253 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
254 |
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
|
255 |
apply (subst cong_eq_diff_cong_0_int) |
31719 | 256 |
apply (unfold cong_int_def) |
257 |
apply (simp add: dvd_eq_mod_eq_0 [symmetric]) |
|
44872 | 258 |
done |
31719 | 259 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
260 |
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
|
261 |
by (simp add: cong_altdef_int) |
31719 | 262 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
263 |
lemma cong_square_int: |
31719 | 264 |
"\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk> |
265 |
\<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
|
266 |
apply (simp only: cong_altdef_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
267 |
apply (subst prime_dvd_mult_eq_int [symmetric], assumption) |
36350 | 268 |
apply (auto simp add: field_simps) |
44872 | 269 |
done |
31719 | 270 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
271 |
lemma cong_mult_rcancel_int: |
44872 | 272 |
"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
|
273 |
apply (subst (1 2) cong_altdef_int) |
31719 | 274 |
apply (subst left_diff_distrib [symmetric]) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
275 |
apply (rule coprime_dvd_mult_iff_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
276 |
apply (subst gcd_commute_int, assumption) |
44872 | 277 |
done |
31719 | 278 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
279 |
lemma cong_mult_rcancel_nat: |
31719 | 280 |
assumes "coprime k (m::nat)" |
281 |
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
|
282 |
apply (rule cong_mult_rcancel_int [transferred]) |
41541 | 283 |
using assms apply auto |
44872 | 284 |
done |
31719 | 285 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
286 |
lemma cong_mult_lcancel_nat: |
44872 | 287 |
"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
|
288 |
by (simp add: mult_commute cong_mult_rcancel_nat) |
31719 | 289 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
290 |
lemma cong_mult_lcancel_int: |
44872 | 291 |
"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
|
292 |
by (simp add: mult_commute cong_mult_rcancel_int) |
31719 | 293 |
|
294 |
(* was zcong_zgcd_zmult_zmod *) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
295 |
lemma coprime_cong_mult_int: |
31719 | 296 |
"[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n |
297 |
\<Longrightarrow> [a = b] (mod m * n)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
298 |
apply (simp only: cong_altdef_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
299 |
apply (erule (2) divides_mult_int) |
41541 | 300 |
done |
31719 | 301 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
302 |
lemma coprime_cong_mult_nat: |
31719 | 303 |
assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n" |
304 |
shows "[a = b] (mod m * n)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
305 |
apply (rule coprime_cong_mult_int [transferred]) |
41541 | 306 |
using assms apply auto |
307 |
done |
|
31719 | 308 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
309 |
lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow> |
31719 | 310 |
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" |
41541 | 311 |
by (auto simp add: cong_nat_def) |
31719 | 312 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
313 |
lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow> |
31719 | 314 |
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" |
41541 | 315 |
by (auto simp add: cong_int_def) |
31719 | 316 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
317 |
lemma cong_less_unique_nat: |
31719 | 318 |
"0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
319 |
apply auto |
|
320 |
apply (rule_tac x = "a mod m" in exI) |
|
321 |
apply (unfold cong_nat_def, auto) |
|
44872 | 322 |
done |
31719 | 323 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
324 |
lemma cong_less_unique_int: |
31719 | 325 |
"0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
326 |
apply auto |
|
327 |
apply (rule_tac x = "a mod m" in exI) |
|
41541 | 328 |
apply (unfold cong_int_def, auto) |
329 |
done |
|
31719 | 330 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
331 |
lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)" |
36350 | 332 |
apply (auto simp add: cong_altdef_int dvd_def field_simps) |
31719 | 333 |
apply (rule_tac [!] x = "-k" in exI, auto) |
44872 | 334 |
done |
31719 | 335 |
|
44872 | 336 |
lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) = |
31719 | 337 |
(\<exists>k1 k2. b + k1 * m = a + k2 * m)" |
338 |
apply (rule iffI) |
|
44872 | 339 |
apply (cases "b <= a") |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
340 |
apply (subst (asm) cong_altdef_nat, assumption) |
31719 | 341 |
apply (unfold dvd_def, auto) |
342 |
apply (rule_tac x = k in exI) |
|
343 |
apply (rule_tac x = 0 in exI) |
|
36350 | 344 |
apply (auto simp add: field_simps) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
345 |
apply (subst (asm) cong_sym_eq_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
346 |
apply (subst (asm) cong_altdef_nat) |
31719 | 347 |
apply force |
348 |
apply (unfold dvd_def, auto) |
|
349 |
apply (rule_tac x = 0 in exI) |
|
350 |
apply (rule_tac x = k in exI) |
|
36350 | 351 |
apply (auto simp add: field_simps) |
31719 | 352 |
apply (unfold cong_nat_def) |
353 |
apply (subgoal_tac "a mod m = (a + k2 * m) mod m") |
|
354 |
apply (erule ssubst)back |
|
355 |
apply (erule subst) |
|
356 |
apply auto |
|
44872 | 357 |
done |
31719 | 358 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
359 |
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
|
360 |
apply (subst (asm) cong_iff_lin_int, auto) |
44872 | 361 |
apply (subst add_commute) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
362 |
apply (subst (2) gcd_commute_int) |
31719 | 363 |
apply (subst mult_commute) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
364 |
apply (subst gcd_add_mult_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
365 |
apply (rule gcd_commute_int) |
41541 | 366 |
done |
31719 | 367 |
|
44872 | 368 |
lemma cong_gcd_eq_nat: |
31719 | 369 |
assumes "[(a::nat) = b] (mod m)" |
370 |
shows "gcd a m = gcd b m" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
371 |
apply (rule cong_gcd_eq_int [transferred]) |
41541 | 372 |
using assms apply auto |
373 |
done |
|
31719 | 374 |
|
44872 | 375 |
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
|
376 |
by (auto simp add: cong_gcd_eq_nat) |
31719 | 377 |
|
44872 | 378 |
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
|
379 |
by (auto simp add: cong_gcd_eq_int) |
31719 | 380 |
|
44872 | 381 |
lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = [a mod m = b mod m] (mod m)" |
31719 | 382 |
by (auto simp add: cong_nat_def) |
383 |
||
44872 | 384 |
lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = [a mod m = b mod m] (mod m)" |
31719 | 385 |
by (auto simp add: cong_int_def) |
386 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
387 |
lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)" |
44872 | 388 |
apply (subst (1 2) cong_altdef_int) |
389 |
apply auto |
|
390 |
done |
|
31719 | 391 |
|
392 |
(* |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
393 |
lemma mod_dvd_mod_int: |
31719 | 394 |
"0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)" |
395 |
apply (unfold dvd_def, auto) |
|
396 |
apply (rule mod_mod_cancel) |
|
397 |
apply auto |
|
44872 | 398 |
done |
31719 | 399 |
|
400 |
lemma mod_dvd_mod: |
|
401 |
assumes "0 < (m::nat)" and "m dvd b" |
|
402 |
shows "(a mod b mod m) = (a mod m)" |
|
403 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
404 |
apply (rule mod_dvd_mod_int [transferred]) |
41541 | 405 |
using assms apply auto |
406 |
done |
|
31719 | 407 |
*) |
408 |
||
44872 | 409 |
lemma cong_add_lcancel_nat: |
410 |
"[(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
|
411 |
by (simp add: cong_iff_lin_nat) |
31719 | 412 |
|
44872 | 413 |
lemma cong_add_lcancel_int: |
414 |
"[(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
|
415 |
by (simp add: cong_iff_lin_int) |
31719 | 416 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
417 |
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
|
418 |
by (simp add: cong_iff_lin_nat) |
31719 | 419 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
420 |
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
|
421 |
by (simp add: cong_iff_lin_int) |
31719 | 422 |
|
44872 | 423 |
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
|
424 |
by (simp add: cong_iff_lin_nat) |
31719 | 425 |
|
44872 | 426 |
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
|
427 |
by (simp add: cong_iff_lin_int) |
31719 | 428 |
|
44872 | 429 |
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
|
430 |
by (simp add: cong_iff_lin_nat) |
31719 | 431 |
|
44872 | 432 |
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
|
433 |
by (simp add: cong_iff_lin_int) |
31719 | 434 |
|
44872 | 435 |
lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> |
31719 | 436 |
[x = y] (mod n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
437 |
apply (auto simp add: cong_iff_lin_nat dvd_def) |
31719 | 438 |
apply (rule_tac x="k1 * k" in exI) |
439 |
apply (rule_tac x="k2 * k" in exI) |
|
36350 | 440 |
apply (simp add: field_simps) |
44872 | 441 |
done |
31719 | 442 |
|
44872 | 443 |
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
|
444 |
by (auto simp add: cong_altdef_int dvd_def) |
31719 | 445 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
446 |
lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y" |
44872 | 447 |
unfolding cong_nat_def by (auto simp add: dvd_eq_mod_eq_0) |
31719 | 448 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
449 |
lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y" |
44872 | 450 |
unfolding cong_int_def by (auto simp add: dvd_eq_mod_eq_0) |
31719 | 451 |
|
44872 | 452 |
lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" |
31719 | 453 |
by (simp add: cong_nat_def) |
454 |
||
44872 | 455 |
lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" |
31719 | 456 |
by (simp add: cong_int_def) |
457 |
||
44872 | 458 |
lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0 |
31719 | 459 |
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)" |
460 |
by (simp add: cong_nat_def mod_mult2_eq mod_add_left_eq) |
|
461 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
462 |
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
|
463 |
apply (simp add: cong_altdef_int) |
31719 | 464 |
apply (subst dvd_minus_iff [symmetric]) |
36350 | 465 |
apply (simp add: field_simps) |
44872 | 466 |
done |
31719 | 467 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
468 |
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
|
469 |
by (auto simp add: cong_altdef_int) |
31719 | 470 |
|
44872 | 471 |
lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0 |
31719 | 472 |
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)" |
44872 | 473 |
apply (cases "b > 0") |
31719 | 474 |
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
|
475 |
apply (subst (1 2) cong_modulus_neg_int) |
31719 | 476 |
apply (unfold cong_int_def) |
477 |
apply (subgoal_tac "a * b = (-a * -b)") |
|
478 |
apply (erule ssubst) |
|
479 |
apply (subst zmod_zmult2_eq) |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47163
diff
changeset
|
480 |
apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right) |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47163
diff
changeset
|
481 |
apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 semiring_numeral_div_class.diff_zero)+ |
44872 | 482 |
done |
31719 | 483 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
484 |
lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))" |
44872 | 485 |
apply (cases "a = 0") |
31719 | 486 |
apply force |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
487 |
apply (subst (asm) cong_altdef_nat) |
31719 | 488 |
apply auto |
44872 | 489 |
done |
31719 | 490 |
|
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset
|
491 |
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
|
492 |
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
|
493 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
494 |
lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)" |
44872 | 495 |
unfolding cong_nat_def by auto |
31719 | 496 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
497 |
lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))" |
44872 | 498 |
unfolding cong_int_def by (auto simp add: zmult_eq_1_iff) |
31719 | 499 |
|
44872 | 500 |
lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow> |
31719 | 501 |
a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)" |
44872 | 502 |
apply (cases "n = 1") |
31719 | 503 |
apply auto [1] |
504 |
apply (drule_tac x = "a - 1" in spec) |
|
505 |
apply force |
|
44872 | 506 |
apply (cases "a = 0") |
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset
|
507 |
apply (auto simp add: cong_0_1_nat') [1] |
31719 | 508 |
apply (rule iffI) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
509 |
apply (drule cong_to_1_nat) |
31719 | 510 |
apply (unfold dvd_def) |
511 |
apply auto [1] |
|
512 |
apply (rule_tac x = k in exI) |
|
36350 | 513 |
apply (auto simp add: field_simps) [1] |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
514 |
apply (subst cong_altdef_nat) |
31719 | 515 |
apply (auto simp add: dvd_def) |
44872 | 516 |
done |
31719 | 517 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
518 |
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
|
519 |
apply (subst cong_altdef_nat) |
31719 | 520 |
apply assumption |
36350 | 521 |
apply (unfold dvd_def, auto simp add: field_simps) |
31719 | 522 |
apply (rule_tac x = k in exI) |
523 |
apply auto |
|
44872 | 524 |
done |
31719 | 525 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
526 |
lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)" |
44872 | 527 |
apply (cases "n = 0") |
31719 | 528 |
apply force |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
529 |
apply (frule bezout_nat [of a n], auto) |
31719 | 530 |
apply (rule exI, erule ssubst) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
531 |
apply (rule cong_trans_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
532 |
apply (rule cong_add_nat) |
31719 | 533 |
apply (subst mult_commute) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
534 |
apply (rule cong_mult_self_nat) |
31719 | 535 |
prefer 2 |
536 |
apply simp |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
537 |
apply (rule cong_refl_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
538 |
apply (rule cong_refl_nat) |
44872 | 539 |
done |
31719 | 540 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
541 |
lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)" |
44872 | 542 |
apply (cases "n = 0") |
543 |
apply (cases "a \<ge> 0") |
|
31719 | 544 |
apply auto |
545 |
apply (rule_tac x = "-1" in exI) |
|
546 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
547 |
apply (insert bezout_int [of a n], auto) |
31719 | 548 |
apply (rule exI) |
549 |
apply (erule subst) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
550 |
apply (rule cong_trans_int) |
31719 | 551 |
prefer 2 |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
552 |
apply (rule cong_add_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
553 |
apply (rule cong_refl_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
554 |
apply (rule cong_sym_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
555 |
apply (rule cong_mult_self_int) |
31719 | 556 |
apply simp |
557 |
apply (subst mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
558 |
apply (rule cong_refl_int) |
44872 | 559 |
done |
560 |
||
561 |
lemma cong_solve_dvd_nat: |
|
31719 | 562 |
assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d" |
563 |
shows "EX x. [a * x = d] (mod n)" |
|
564 |
proof - |
|
44872 | 565 |
from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)" |
31719 | 566 |
by auto |
44872 | 567 |
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
|
568 |
by (elim cong_scalar2_nat) |
31719 | 569 |
also from b have "(d div gcd a n) * gcd a n = d" |
570 |
by (rule dvd_div_mult_self) |
|
571 |
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" |
|
572 |
by auto |
|
573 |
finally show ?thesis |
|
574 |
by auto |
|
575 |
qed |
|
576 |
||
44872 | 577 |
lemma cong_solve_dvd_int: |
31719 | 578 |
assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d" |
579 |
shows "EX x. [a * x = d] (mod n)" |
|
580 |
proof - |
|
44872 | 581 |
from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)" |
31719 | 582 |
by auto |
44872 | 583 |
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
|
584 |
by (elim cong_scalar2_int) |
31719 | 585 |
also from b have "(d div gcd a n) * gcd a n = d" |
586 |
by (rule dvd_div_mult_self) |
|
587 |
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" |
|
588 |
by auto |
|
589 |
finally show ?thesis |
|
590 |
by auto |
|
591 |
qed |
|
592 |
||
44872 | 593 |
lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)" |
594 |
apply (cases "a = 0") |
|
31719 | 595 |
apply force |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
596 |
apply (frule cong_solve_nat [of a n]) |
31719 | 597 |
apply auto |
44872 | 598 |
done |
31719 | 599 |
|
44872 | 600 |
lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)" |
601 |
apply (cases "a = 0") |
|
31719 | 602 |
apply auto |
44872 | 603 |
apply (cases "n \<ge> 0") |
31719 | 604 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
605 |
apply (frule cong_solve_int [of a n]) |
31719 | 606 |
apply auto |
44872 | 607 |
done |
31719 | 608 |
|
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset
|
609 |
lemma coprime_iff_invertible_nat: "m > Suc 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
610 |
apply (auto intro: cong_solve_coprime_nat) |
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset
|
611 |
apply (metis cong_solve_nat gcd_nat.left_neutral nat_neq_iff) |
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset
|
612 |
apply (unfold cong_nat_def, auto intro: invertible_coprime_nat [unfolded One_nat_def]) |
44872 | 613 |
done |
31719 | 614 |
|
44872 | 615 |
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
|
616 |
apply (auto intro: cong_solve_coprime_int) |
31719 | 617 |
apply (unfold cong_int_def) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
618 |
apply (auto intro: invertible_coprime_int) |
44872 | 619 |
done |
31719 | 620 |
|
44872 | 621 |
lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m = |
31719 | 622 |
(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
|
623 |
apply (subst coprime_iff_invertible_int) |
31719 | 624 |
apply auto |
625 |
apply (auto simp add: cong_int_def) |
|
626 |
apply (rule_tac x = "x mod m" in exI) |
|
627 |
apply (auto simp add: mod_mult_right_eq [symmetric]) |
|
44872 | 628 |
done |
31719 | 629 |
|
630 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
631 |
lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow> |
31719 | 632 |
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" |
44872 | 633 |
apply (cases "y \<le> x") |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
634 |
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
|
635 |
apply (rule cong_sym_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
636 |
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
|
637 |
apply (auto simp add: cong_altdef_nat lcm_least_nat) |
44872 | 638 |
done |
31719 | 639 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
640 |
lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow> |
31719 | 641 |
[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
|
642 |
by (auto simp add: cong_altdef_int lcm_least_int) [1] |
31719 | 643 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
644 |
lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow> |
31719 | 645 |
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)" |
44872 | 646 |
apply (frule (1) cong_cong_lcm_nat) |
647 |
back |
|
31719 | 648 |
apply (simp add: lcm_nat_def) |
44872 | 649 |
done |
31719 | 650 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
651 |
lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow> |
31719 | 652 |
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)" |
44872 | 653 |
apply (frule (1) cong_cong_lcm_int) |
654 |
back |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
655 |
apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric]) |
44872 | 656 |
done |
31719 | 657 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
658 |
lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow> |
31719 | 659 |
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
660 |
(ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow> |
|
661 |
[x = y] (mod (PROD i:A. m i))" |
|
662 |
apply (induct set: finite) |
|
663 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
664 |
apply (rule cong_cong_coprime_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
665 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
666 |
apply (rule setprod_coprime_nat) |
31719 | 667 |
apply auto |
44872 | 668 |
done |
31719 | 669 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
670 |
lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow> |
31719 | 671 |
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
672 |
(ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow> |
|
673 |
[x = y] (mod (PROD i:A. m i))" |
|
674 |
apply (induct set: finite) |
|
675 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
676 |
apply (rule cong_cong_coprime_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
677 |
apply (subst gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
678 |
apply (rule setprod_coprime_int) |
31719 | 679 |
apply auto |
44872 | 680 |
done |
31719 | 681 |
|
44872 | 682 |
lemma binary_chinese_remainder_aux_nat: |
31719 | 683 |
assumes a: "coprime (m1::nat) m2" |
684 |
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> |
|
685 |
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
|
686 |
proof - |
|
44872 | 687 |
from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)" |
31719 | 688 |
by auto |
44872 | 689 |
from a have b: "coprime m2 m1" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
690 |
by (subst gcd_commute_nat) |
44872 | 691 |
from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)" |
31719 | 692 |
by auto |
693 |
have "[m1 * x1 = 0] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
694 |
by (subst mult_commute, rule cong_mult_self_nat) |
31719 | 695 |
moreover have "[m2 * x2 = 0] (mod m2)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
696 |
by (subst mult_commute, rule cong_mult_self_nat) |
31719 | 697 |
moreover note one two |
698 |
ultimately show ?thesis by blast |
|
699 |
qed |
|
700 |
||
44872 | 701 |
lemma binary_chinese_remainder_aux_int: |
31719 | 702 |
assumes a: "coprime (m1::int) m2" |
703 |
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> |
|
704 |
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
|
705 |
proof - |
|
44872 | 706 |
from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)" |
31719 | 707 |
by auto |
44872 | 708 |
from a have b: "coprime m2 m1" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
709 |
by (subst gcd_commute_int) |
44872 | 710 |
from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)" |
31719 | 711 |
by auto |
712 |
have "[m1 * x1 = 0] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
713 |
by (subst mult_commute, rule cong_mult_self_int) |
31719 | 714 |
moreover have "[m2 * x2 = 0] (mod m2)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
715 |
by (subst mult_commute, rule cong_mult_self_int) |
31719 | 716 |
moreover note one two |
717 |
ultimately show ?thesis by blast |
|
718 |
qed |
|
719 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
720 |
lemma binary_chinese_remainder_nat: |
31719 | 721 |
assumes a: "coprime (m1::nat) m2" |
722 |
shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
723 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
724 |
from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2 |
44872 | 725 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and |
726 |
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
31719 | 727 |
by blast |
728 |
let ?x = "u1 * b1 + u2 * b2" |
|
729 |
have "[?x = u1 * 1 + u2 * 0] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
730 |
apply (rule cong_add_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
731 |
apply (rule cong_scalar2_nat) |
31719 | 732 |
apply (rule `[b1 = 1] (mod m1)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
733 |
apply (rule cong_scalar2_nat) |
31719 | 734 |
apply (rule `[b2 = 0] (mod m1)`) |
735 |
done |
|
44872 | 736 |
then have "[?x = u1] (mod m1)" by simp |
31719 | 737 |
have "[?x = u1 * 0 + u2 * 1] (mod m2)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
738 |
apply (rule cong_add_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
739 |
apply (rule cong_scalar2_nat) |
31719 | 740 |
apply (rule `[b1 = 0] (mod m2)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
741 |
apply (rule cong_scalar2_nat) |
31719 | 742 |
apply (rule `[b2 = 1] (mod m2)`) |
743 |
done |
|
44872 | 744 |
then have "[?x = u2] (mod m2)" by simp |
31719 | 745 |
with `[?x = u1] (mod m1)` show ?thesis by blast |
746 |
qed |
|
747 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
748 |
lemma binary_chinese_remainder_int: |
31719 | 749 |
assumes a: "coprime (m1::int) m2" |
750 |
shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
751 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
752 |
from binary_chinese_remainder_aux_int [OF a] obtain b1 b2 |
31719 | 753 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and |
754 |
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
755 |
by blast |
|
756 |
let ?x = "u1 * b1 + u2 * b2" |
|
757 |
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
|
758 |
apply (rule cong_add_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
759 |
apply (rule cong_scalar2_int) |
31719 | 760 |
apply (rule `[b1 = 1] (mod m1)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
761 |
apply (rule cong_scalar2_int) |
31719 | 762 |
apply (rule `[b2 = 0] (mod m1)`) |
763 |
done |
|
44872 | 764 |
then have "[?x = u1] (mod m1)" by simp |
31719 | 765 |
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
|
766 |
apply (rule cong_add_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
767 |
apply (rule cong_scalar2_int) |
31719 | 768 |
apply (rule `[b1 = 0] (mod m2)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
769 |
apply (rule cong_scalar2_int) |
31719 | 770 |
apply (rule `[b2 = 1] (mod m2)`) |
771 |
done |
|
44872 | 772 |
then have "[?x = u2] (mod m2)" by simp |
31719 | 773 |
with `[?x = u1] (mod m1)` show ?thesis by blast |
774 |
qed |
|
775 |
||
44872 | 776 |
lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow> |
31719 | 777 |
[x = y] (mod m)" |
44872 | 778 |
apply (cases "y \<le> x") |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
779 |
apply (simp add: cong_altdef_nat) |
31719 | 780 |
apply (erule dvd_mult_left) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
781 |
apply (rule cong_sym_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
782 |
apply (subst (asm) cong_sym_eq_nat) |
44872 | 783 |
apply (simp add: cong_altdef_nat) |
31719 | 784 |
apply (erule dvd_mult_left) |
44872 | 785 |
done |
31719 | 786 |
|
44872 | 787 |
lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow> |
31719 | 788 |
[x = y] (mod m)" |
44872 | 789 |
apply (simp add: cong_altdef_int) |
31719 | 790 |
apply (erule dvd_mult_left) |
44872 | 791 |
done |
31719 | 792 |
|
44872 | 793 |
lemma cong_less_modulus_unique_nat: |
31719 | 794 |
"[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y" |
795 |
by (simp add: cong_nat_def) |
|
796 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
797 |
lemma binary_chinese_remainder_unique_nat: |
44872 | 798 |
assumes a: "coprime (m1::nat) m2" |
799 |
and nz: "m1 \<noteq> 0" "m2 \<noteq> 0" |
|
31719 | 800 |
shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
801 |
proof - |
|
44872 | 802 |
from binary_chinese_remainder_nat [OF a] obtain y where |
31719 | 803 |
"[y = u1] (mod m1)" and "[y = u2] (mod m2)" |
804 |
by blast |
|
805 |
let ?x = "y mod (m1 * m2)" |
|
806 |
from nz have less: "?x < m1 * m2" |
|
44872 | 807 |
by auto |
31719 | 808 |
have one: "[?x = u1] (mod m1)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
809 |
apply (rule cong_trans_nat) |
31719 | 810 |
prefer 2 |
811 |
apply (rule `[y = u1] (mod m1)`) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
812 |
apply (rule cong_modulus_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
813 |
apply (rule cong_mod_nat) |
31719 | 814 |
using nz apply auto |
815 |
done |
|
816 |
have two: "[?x = u2] (mod m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
817 |
apply (rule cong_trans_nat) |
31719 | 818 |
prefer 2 |
819 |
apply (rule `[y = u2] (mod m2)`) |
|
820 |
apply (subst mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
821 |
apply (rule cong_modulus_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
822 |
apply (rule cong_mod_nat) |
31719 | 823 |
using nz apply auto |
824 |
done |
|
44872 | 825 |
have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x" |
826 |
proof clarify |
|
31719 | 827 |
fix z |
828 |
assume "z < m1 * m2" |
|
829 |
assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)" |
|
830 |
have "[?x = z] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
831 |
apply (rule cong_trans_nat) |
31719 | 832 |
apply (rule `[?x = u1] (mod m1)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
833 |
apply (rule cong_sym_nat) |
31719 | 834 |
apply (rule `[z = u1] (mod m1)`) |
835 |
done |
|
836 |
moreover have "[?x = z] (mod m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
837 |
apply (rule cong_trans_nat) |
31719 | 838 |
apply (rule `[?x = u2] (mod m2)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
839 |
apply (rule cong_sym_nat) |
31719 | 840 |
apply (rule `[z = u2] (mod m2)`) |
841 |
done |
|
842 |
ultimately have "[?x = z] (mod m1 * m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
843 |
by (auto intro: coprime_cong_mult_nat a) |
31719 | 844 |
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
|
845 |
apply (intro cong_less_modulus_unique_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
846 |
apply (auto, erule cong_sym_nat) |
31719 | 847 |
done |
44872 | 848 |
qed |
849 |
with less one two show ?thesis by auto |
|
31719 | 850 |
qed |
851 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
852 |
lemma chinese_remainder_aux_nat: |
44872 | 853 |
fixes A :: "'a set" |
854 |
and m :: "'a \<Rightarrow> nat" |
|
855 |
assumes fin: "finite A" |
|
856 |
and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
|
857 |
shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))" |
|
31719 | 858 |
proof (rule finite_set_choice, rule fin, rule ballI) |
859 |
fix i |
|
860 |
assume "i : A" |
|
861 |
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
|
862 |
by (intro setprod_coprime_nat, auto) |
44872 | 863 |
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
|
864 |
by (elim cong_solve_coprime_nat) |
31719 | 865 |
then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)" |
866 |
by auto |
|
44872 | 867 |
moreover have "[(PROD j : A - {i}. m j) * x = 0] |
31719 | 868 |
(mod (PROD j : A - {i}. m j))" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
869 |
by (subst mult_commute, rule cong_mult_self_nat) |
44872 | 870 |
ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] |
31719 | 871 |
(mod setprod m (A - {i}))" |
872 |
by blast |
|
873 |
qed |
|
874 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
875 |
lemma chinese_remainder_nat: |
44872 | 876 |
fixes A :: "'a set" |
877 |
and m :: "'a \<Rightarrow> nat" |
|
878 |
and u :: "'a \<Rightarrow> nat" |
|
879 |
assumes fin: "finite A" |
|
880 |
and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
|
31719 | 881 |
shows "EX x. (ALL i:A. [x = u i] (mod m i))" |
882 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
883 |
from chinese_remainder_aux_nat [OF fin cop] obtain b where |
44872 | 884 |
bprop: "ALL i:A. [b i = 1] (mod m i) \<and> |
31719 | 885 |
[b i = 0] (mod (PROD j : A - {i}. m j))" |
886 |
by blast |
|
887 |
let ?x = "SUM i:A. (u i) * (b i)" |
|
888 |
show "?thesis" |
|
889 |
proof (rule exI, clarify) |
|
890 |
fix i |
|
891 |
assume a: "i : A" |
|
44872 | 892 |
show "[?x = u i] (mod m i)" |
31719 | 893 |
proof - |
44872 | 894 |
from fin a have "?x = (SUM j:{i}. u j * b j) + |
31719 | 895 |
(SUM j:A-{i}. u j * b j)" |
896 |
by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong) |
|
44872 | 897 |
then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)" |
31719 | 898 |
by auto |
899 |
also have "[u i * b i + (SUM j:A-{i}. u j * b j) = |
|
900 |
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
|
901 |
apply (rule cong_add_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
902 |
apply (rule cong_scalar2_nat) |
31719 | 903 |
using bprop a apply blast |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
904 |
apply (rule cong_setsum_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
905 |
apply (rule cong_scalar2_nat) |
31719 | 906 |
using bprop apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
907 |
apply (rule cong_dvd_modulus_nat) |
31719 | 908 |
apply (drule (1) bspec) |
909 |
apply (erule conjE) |
|
910 |
apply assumption |
|
911 |
apply (rule dvd_setprod) |
|
912 |
using fin a apply auto |
|
913 |
done |
|
914 |
finally show ?thesis |
|
915 |
by simp |
|
916 |
qed |
|
917 |
qed |
|
918 |
qed |
|
919 |
||
44872 | 920 |
lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow> |
31719 | 921 |
(ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
922 |
(ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow> |
|
44872 | 923 |
[x = y] (mod (PROD i:A. m i))" |
31719 | 924 |
apply (induct set: finite) |
925 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
926 |
apply (erule (1) coprime_cong_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
927 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
928 |
apply (rule setprod_coprime_nat) |
31719 | 929 |
apply auto |
44872 | 930 |
done |
31719 | 931 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
932 |
lemma chinese_remainder_unique_nat: |
44872 | 933 |
fixes A :: "'a set" |
934 |
and m :: "'a \<Rightarrow> nat" |
|
935 |
and u :: "'a \<Rightarrow> nat" |
|
936 |
assumes fin: "finite A" |
|
937 |
and nz: "ALL i:A. m i \<noteq> 0" |
|
938 |
and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
|
31719 | 939 |
shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))" |
940 |
proof - |
|
44872 | 941 |
from chinese_remainder_nat [OF fin cop] |
942 |
obtain y where one: "(ALL i:A. [y = u i] (mod m i))" |
|
31719 | 943 |
by blast |
944 |
let ?x = "y mod (PROD i:A. m i)" |
|
945 |
from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0" |
|
946 |
by auto |
|
44872 | 947 |
then have less: "?x < (PROD i:A. m i)" |
31719 | 948 |
by auto |
949 |
have cong: "ALL i:A. [?x = u i] (mod m i)" |
|
950 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
951 |
apply (rule cong_trans_nat) |
31719 | 952 |
prefer 2 |
953 |
using one apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
954 |
apply (rule cong_dvd_modulus_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
955 |
apply (rule cong_mod_nat) |
31719 | 956 |
using prodnz apply auto |
957 |
apply (rule dvd_setprod) |
|
958 |
apply (rule fin) |
|
959 |
apply assumption |
|
960 |
done |
|
44872 | 961 |
have unique: "ALL z. z < (PROD i:A. m i) \<and> |
31719 | 962 |
(ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x" |
963 |
proof (clarify) |
|
964 |
fix z |
|
965 |
assume zless: "z < (PROD i:A. m i)" |
|
966 |
assume zcong: "(ALL i:A. [z = u i] (mod m i))" |
|
967 |
have "ALL i:A. [?x = z] (mod m i)" |
|
44872 | 968 |
apply clarify |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
969 |
apply (rule cong_trans_nat) |
31719 | 970 |
using cong apply (erule bspec) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
971 |
apply (rule cong_sym_nat) |
31719 | 972 |
using zcong apply auto |
973 |
done |
|
974 |
with fin cop have "[?x = z] (mod (PROD i:A. m i))" |
|
44872 | 975 |
apply (intro coprime_cong_prod_nat) |
976 |
apply auto |
|
977 |
done |
|
31719 | 978 |
with zless less show "z = ?x" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
979 |
apply (intro cong_less_modulus_unique_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
980 |
apply (auto, erule cong_sym_nat) |
31719 | 981 |
done |
44872 | 982 |
qed |
983 |
from less cong unique show ?thesis by blast |
|
31719 | 984 |
qed |
985 |
||
986 |
end |