author | paulson <lp15@cam.ac.uk> |
Tue, 04 Feb 2014 21:28:38 +0000 | |
changeset 55321 | eadea363deb6 |
parent 55242 | 413ec965f95d |
child 55337 | 5d45fb978d5a |
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: |
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)" |
41541 | 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))" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
254 |
apply (subst cong_eq_diff_cong_0_int) |
31719 | 255 |
apply (unfold cong_int_def) |
256 |
apply (simp add: dvd_eq_mod_eq_0 [symmetric]) |
|
44872 | 257 |
done |
31719 | 258 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
259 |
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
|
260 |
by (simp add: cong_altdef_int) |
31719 | 261 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
262 |
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
|
263 |
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
|
264 |
shows "\<lbrakk> prime p; 0 < a; [a * a = 1] (mod p) \<rbrakk> |
31719 | 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 |
55161 | 596 |
apply (metis cong_solve_nat) |
44872 | 597 |
done |
31719 | 598 |
|
44872 | 599 |
lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)" |
600 |
apply (cases "a = 0") |
|
31719 | 601 |
apply auto |
44872 | 602 |
apply (cases "n \<ge> 0") |
31719 | 603 |
apply auto |
55161 | 604 |
apply (metis cong_solve_int) |
605 |
done |
|
606 |
||
607 |
lemma coprime_iff_invertible_nat: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))" |
|
608 |
apply (auto intro: cong_solve_coprime_nat) |
|
609 |
apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral) |
|
610 |
apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat |
|
611 |
gcd_lcm_complete_lattice_nat.inf_bot_right gcd_nat.commute) |
|
44872 | 612 |
done |
31719 | 613 |
|
55161 | 614 |
lemma coprime_iff_invertible_int: "m > (0::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))" |
615 |
apply (auto intro: cong_solve_coprime_int) |
|
616 |
apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd_int.commute gcd_red_int) |
|
44872 | 617 |
done |
31719 | 618 |
|
55161 | 619 |
lemma coprime_iff_invertible'_nat: "m > 0 \<Longrightarrow> coprime a m = |
620 |
(EX x. 0 \<le> x & x < m & [a * x = Suc 0] (mod m))" |
|
621 |
apply (subst coprime_iff_invertible_nat) |
|
622 |
apply auto |
|
623 |
apply (auto simp add: cong_nat_def) |
|
624 |
apply (rule_tac x = "x mod m" in exI) |
|
625 |
apply (metis mod_less_divisor mod_mult_right_eq) |
|
44872 | 626 |
done |
31719 | 627 |
|
55161 | 628 |
lemma coprime_iff_invertible'_int: "m > (0::int) \<Longrightarrow> coprime a m = |
31719 | 629 |
(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
|
630 |
apply (subst coprime_iff_invertible_int) |
31719 | 631 |
apply auto |
632 |
apply (auto simp add: cong_int_def) |
|
633 |
apply (rule_tac x = "x mod m" in exI) |
|
634 |
apply (auto simp add: mod_mult_right_eq [symmetric]) |
|
44872 | 635 |
done |
31719 | 636 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
637 |
lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow> |
31719 | 638 |
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" |
44872 | 639 |
apply (cases "y \<le> x") |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
640 |
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
|
641 |
apply (rule cong_sym_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
642 |
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
|
643 |
apply (auto simp add: cong_altdef_nat lcm_least_nat) |
44872 | 644 |
done |
31719 | 645 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
646 |
lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow> |
31719 | 647 |
[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
|
648 |
by (auto simp add: cong_altdef_int lcm_least_int) [1] |
31719 | 649 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
650 |
lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow> |
31719 | 651 |
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)" |
44872 | 652 |
apply (frule (1) cong_cong_lcm_nat) |
653 |
back |
|
31719 | 654 |
apply (simp add: lcm_nat_def) |
44872 | 655 |
done |
31719 | 656 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
657 |
lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow> |
31719 | 658 |
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)" |
44872 | 659 |
apply (frule (1) cong_cong_lcm_int) |
660 |
back |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
661 |
apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric]) |
44872 | 662 |
done |
31719 | 663 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
664 |
lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow> |
31719 | 665 |
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
666 |
(ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow> |
|
667 |
[x = y] (mod (PROD i:A. m i))" |
|
668 |
apply (induct set: finite) |
|
669 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
670 |
apply (rule cong_cong_coprime_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
671 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
672 |
apply (rule setprod_coprime_nat) |
31719 | 673 |
apply auto |
44872 | 674 |
done |
31719 | 675 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
676 |
lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow> |
31719 | 677 |
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
678 |
(ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow> |
|
679 |
[x = y] (mod (PROD i:A. m i))" |
|
680 |
apply (induct set: finite) |
|
681 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
682 |
apply (rule cong_cong_coprime_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
683 |
apply (subst gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
684 |
apply (rule setprod_coprime_int) |
31719 | 685 |
apply auto |
44872 | 686 |
done |
31719 | 687 |
|
44872 | 688 |
lemma binary_chinese_remainder_aux_nat: |
31719 | 689 |
assumes a: "coprime (m1::nat) m2" |
690 |
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> |
|
691 |
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
|
692 |
proof - |
|
44872 | 693 |
from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)" |
31719 | 694 |
by auto |
44872 | 695 |
from a have b: "coprime m2 m1" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
696 |
by (subst gcd_commute_nat) |
44872 | 697 |
from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)" |
31719 | 698 |
by auto |
699 |
have "[m1 * x1 = 0] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
700 |
by (subst mult_commute, rule cong_mult_self_nat) |
31719 | 701 |
moreover have "[m2 * x2 = 0] (mod m2)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
702 |
by (subst mult_commute, rule cong_mult_self_nat) |
31719 | 703 |
moreover note one two |
704 |
ultimately show ?thesis by blast |
|
705 |
qed |
|
706 |
||
44872 | 707 |
lemma binary_chinese_remainder_aux_int: |
31719 | 708 |
assumes a: "coprime (m1::int) m2" |
709 |
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> |
|
710 |
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" |
|
711 |
proof - |
|
44872 | 712 |
from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)" |
31719 | 713 |
by auto |
44872 | 714 |
from a have b: "coprime m2 m1" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
715 |
by (subst gcd_commute_int) |
44872 | 716 |
from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)" |
31719 | 717 |
by auto |
718 |
have "[m1 * x1 = 0] (mod m1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
719 |
by (subst mult_commute, rule cong_mult_self_int) |
31719 | 720 |
moreover have "[m2 * x2 = 0] (mod m2)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
721 |
by (subst mult_commute, rule cong_mult_self_int) |
31719 | 722 |
moreover note one two |
723 |
ultimately show ?thesis by blast |
|
724 |
qed |
|
725 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
726 |
lemma binary_chinese_remainder_nat: |
31719 | 727 |
assumes a: "coprime (m1::nat) m2" |
728 |
shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
729 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
730 |
from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2 |
44872 | 731 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and |
732 |
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
31719 | 733 |
by blast |
734 |
let ?x = "u1 * b1 + u2 * b2" |
|
735 |
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
|
736 |
apply (rule cong_add_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
737 |
apply (rule cong_scalar2_nat) |
31719 | 738 |
apply (rule `[b1 = 1] (mod m1)`) |
31952
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 `[b2 = 0] (mod m1)`) |
741 |
done |
|
44872 | 742 |
then have "[?x = u1] (mod m1)" by simp |
31719 | 743 |
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
|
744 |
apply (rule cong_add_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
745 |
apply (rule cong_scalar2_nat) |
31719 | 746 |
apply (rule `[b1 = 0] (mod m2)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
747 |
apply (rule cong_scalar2_nat) |
31719 | 748 |
apply (rule `[b2 = 1] (mod m2)`) |
749 |
done |
|
44872 | 750 |
then have "[?x = u2] (mod m2)" by simp |
31719 | 751 |
with `[?x = u1] (mod m1)` show ?thesis by blast |
752 |
qed |
|
753 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
754 |
lemma binary_chinese_remainder_int: |
31719 | 755 |
assumes a: "coprime (m1::int) m2" |
756 |
shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
|
757 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
758 |
from binary_chinese_remainder_aux_int [OF a] obtain b1 b2 |
31719 | 759 |
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and |
760 |
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" |
|
761 |
by blast |
|
762 |
let ?x = "u1 * b1 + u2 * b2" |
|
763 |
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
|
764 |
apply (rule cong_add_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
765 |
apply (rule cong_scalar2_int) |
31719 | 766 |
apply (rule `[b1 = 1] (mod m1)`) |
31952
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 `[b2 = 0] (mod m1)`) |
769 |
done |
|
44872 | 770 |
then have "[?x = u1] (mod m1)" by simp |
31719 | 771 |
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
|
772 |
apply (rule cong_add_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
773 |
apply (rule cong_scalar2_int) |
31719 | 774 |
apply (rule `[b1 = 0] (mod m2)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
775 |
apply (rule cong_scalar2_int) |
31719 | 776 |
apply (rule `[b2 = 1] (mod m2)`) |
777 |
done |
|
44872 | 778 |
then have "[?x = u2] (mod m2)" by simp |
31719 | 779 |
with `[?x = u1] (mod m1)` show ?thesis by blast |
780 |
qed |
|
781 |
||
44872 | 782 |
lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow> |
31719 | 783 |
[x = y] (mod m)" |
44872 | 784 |
apply (cases "y \<le> x") |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
785 |
apply (simp add: cong_altdef_nat) |
31719 | 786 |
apply (erule dvd_mult_left) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
787 |
apply (rule cong_sym_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
788 |
apply (subst (asm) cong_sym_eq_nat) |
44872 | 789 |
apply (simp add: cong_altdef_nat) |
31719 | 790 |
apply (erule dvd_mult_left) |
44872 | 791 |
done |
31719 | 792 |
|
44872 | 793 |
lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow> |
31719 | 794 |
[x = y] (mod m)" |
44872 | 795 |
apply (simp add: cong_altdef_int) |
31719 | 796 |
apply (erule dvd_mult_left) |
44872 | 797 |
done |
31719 | 798 |
|
44872 | 799 |
lemma cong_less_modulus_unique_nat: |
31719 | 800 |
"[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y" |
801 |
by (simp add: cong_nat_def) |
|
802 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
803 |
lemma binary_chinese_remainder_unique_nat: |
44872 | 804 |
assumes a: "coprime (m1::nat) m2" |
805 |
and nz: "m1 \<noteq> 0" "m2 \<noteq> 0" |
|
31719 | 806 |
shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)" |
807 |
proof - |
|
44872 | 808 |
from binary_chinese_remainder_nat [OF a] obtain y where |
31719 | 809 |
"[y = u1] (mod m1)" and "[y = u2] (mod m2)" |
810 |
by blast |
|
811 |
let ?x = "y mod (m1 * m2)" |
|
812 |
from nz have less: "?x < m1 * m2" |
|
44872 | 813 |
by auto |
31719 | 814 |
have one: "[?x = u1] (mod m1)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
815 |
apply (rule cong_trans_nat) |
31719 | 816 |
prefer 2 |
817 |
apply (rule `[y = u1] (mod m1)`) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
818 |
apply (rule cong_modulus_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
819 |
apply (rule cong_mod_nat) |
31719 | 820 |
using nz apply auto |
821 |
done |
|
822 |
have two: "[?x = u2] (mod m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
823 |
apply (rule cong_trans_nat) |
31719 | 824 |
prefer 2 |
825 |
apply (rule `[y = u2] (mod m2)`) |
|
826 |
apply (subst mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
827 |
apply (rule cong_modulus_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
828 |
apply (rule cong_mod_nat) |
31719 | 829 |
using nz apply auto |
830 |
done |
|
44872 | 831 |
have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x" |
832 |
proof clarify |
|
31719 | 833 |
fix z |
834 |
assume "z < m1 * m2" |
|
835 |
assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)" |
|
836 |
have "[?x = z] (mod m1)" |
|
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 = u1] (mod m1)`) |
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 = u1] (mod m1)`) |
841 |
done |
|
842 |
moreover have "[?x = z] (mod m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
843 |
apply (rule cong_trans_nat) |
31719 | 844 |
apply (rule `[?x = u2] (mod m2)`) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
845 |
apply (rule cong_sym_nat) |
31719 | 846 |
apply (rule `[z = u2] (mod m2)`) |
847 |
done |
|
848 |
ultimately have "[?x = z] (mod m1 * m2)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
849 |
by (auto intro: coprime_cong_mult_nat a) |
31719 | 850 |
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
|
851 |
apply (intro cong_less_modulus_unique_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
852 |
apply (auto, erule cong_sym_nat) |
31719 | 853 |
done |
44872 | 854 |
qed |
855 |
with less one two show ?thesis by auto |
|
31719 | 856 |
qed |
857 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
858 |
lemma chinese_remainder_aux_nat: |
44872 | 859 |
fixes A :: "'a set" |
860 |
and m :: "'a \<Rightarrow> nat" |
|
861 |
assumes fin: "finite A" |
|
862 |
and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
|
863 |
shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))" |
|
31719 | 864 |
proof (rule finite_set_choice, rule fin, rule ballI) |
865 |
fix i |
|
866 |
assume "i : A" |
|
867 |
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
|
868 |
by (intro setprod_coprime_nat, auto) |
44872 | 869 |
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
|
870 |
by (elim cong_solve_coprime_nat) |
31719 | 871 |
then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)" |
872 |
by auto |
|
44872 | 873 |
moreover have "[(PROD j : A - {i}. m j) * x = 0] |
31719 | 874 |
(mod (PROD j : A - {i}. m j))" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
875 |
by (subst mult_commute, rule cong_mult_self_nat) |
44872 | 876 |
ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] |
31719 | 877 |
(mod setprod m (A - {i}))" |
878 |
by blast |
|
879 |
qed |
|
880 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
881 |
lemma chinese_remainder_nat: |
44872 | 882 |
fixes A :: "'a set" |
883 |
and m :: "'a \<Rightarrow> nat" |
|
884 |
and u :: "'a \<Rightarrow> nat" |
|
885 |
assumes fin: "finite A" |
|
886 |
and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
|
31719 | 887 |
shows "EX x. (ALL i:A. [x = u i] (mod m i))" |
888 |
proof - |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
889 |
from chinese_remainder_aux_nat [OF fin cop] obtain b where |
44872 | 890 |
bprop: "ALL i:A. [b i = 1] (mod m i) \<and> |
31719 | 891 |
[b i = 0] (mod (PROD j : A - {i}. m j))" |
892 |
by blast |
|
893 |
let ?x = "SUM i:A. (u i) * (b i)" |
|
894 |
show "?thesis" |
|
895 |
proof (rule exI, clarify) |
|
896 |
fix i |
|
897 |
assume a: "i : A" |
|
44872 | 898 |
show "[?x = u i] (mod m i)" |
31719 | 899 |
proof - |
44872 | 900 |
from fin a have "?x = (SUM j:{i}. u j * b j) + |
31719 | 901 |
(SUM j:A-{i}. u j * b j)" |
902 |
by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong) |
|
44872 | 903 |
then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)" |
31719 | 904 |
by auto |
905 |
also have "[u i * b i + (SUM j:A-{i}. u j * b j) = |
|
906 |
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
|
907 |
apply (rule cong_add_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
908 |
apply (rule cong_scalar2_nat) |
31719 | 909 |
using bprop a apply blast |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
910 |
apply (rule cong_setsum_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
911 |
apply (rule cong_scalar2_nat) |
31719 | 912 |
using bprop apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
913 |
apply (rule cong_dvd_modulus_nat) |
31719 | 914 |
apply (drule (1) bspec) |
915 |
apply (erule conjE) |
|
916 |
apply assumption |
|
917 |
apply (rule dvd_setprod) |
|
918 |
using fin a apply auto |
|
919 |
done |
|
920 |
finally show ?thesis |
|
921 |
by simp |
|
922 |
qed |
|
923 |
qed |
|
924 |
qed |
|
925 |
||
44872 | 926 |
lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow> |
31719 | 927 |
(ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow> |
928 |
(ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow> |
|
44872 | 929 |
[x = y] (mod (PROD i:A. m i))" |
31719 | 930 |
apply (induct set: finite) |
931 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
932 |
apply (erule (1) coprime_cong_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
933 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
934 |
apply (rule setprod_coprime_nat) |
31719 | 935 |
apply auto |
44872 | 936 |
done |
31719 | 937 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
938 |
lemma chinese_remainder_unique_nat: |
44872 | 939 |
fixes A :: "'a set" |
940 |
and m :: "'a \<Rightarrow> nat" |
|
941 |
and u :: "'a \<Rightarrow> nat" |
|
942 |
assumes fin: "finite A" |
|
943 |
and nz: "ALL i:A. m i \<noteq> 0" |
|
944 |
and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" |
|
31719 | 945 |
shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))" |
946 |
proof - |
|
44872 | 947 |
from chinese_remainder_nat [OF fin cop] |
948 |
obtain y where one: "(ALL i:A. [y = u i] (mod m i))" |
|
31719 | 949 |
by blast |
950 |
let ?x = "y mod (PROD i:A. m i)" |
|
951 |
from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0" |
|
952 |
by auto |
|
44872 | 953 |
then have less: "?x < (PROD i:A. m i)" |
31719 | 954 |
by auto |
955 |
have cong: "ALL i:A. [?x = u i] (mod m i)" |
|
956 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
957 |
apply (rule cong_trans_nat) |
31719 | 958 |
prefer 2 |
959 |
using one apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
960 |
apply (rule cong_dvd_modulus_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
961 |
apply (rule cong_mod_nat) |
31719 | 962 |
using prodnz apply auto |
963 |
apply (rule dvd_setprod) |
|
964 |
apply (rule fin) |
|
965 |
apply assumption |
|
966 |
done |
|
44872 | 967 |
have unique: "ALL z. z < (PROD i:A. m i) \<and> |
31719 | 968 |
(ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x" |
969 |
proof (clarify) |
|
970 |
fix z |
|
971 |
assume zless: "z < (PROD i:A. m i)" |
|
972 |
assume zcong: "(ALL i:A. [z = u i] (mod m i))" |
|
973 |
have "ALL i:A. [?x = z] (mod m i)" |
|
44872 | 974 |
apply clarify |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
975 |
apply (rule cong_trans_nat) |
31719 | 976 |
using cong apply (erule bspec) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
977 |
apply (rule cong_sym_nat) |
31719 | 978 |
using zcong apply auto |
979 |
done |
|
980 |
with fin cop have "[?x = z] (mod (PROD i:A. m i))" |
|
44872 | 981 |
apply (intro coprime_cong_prod_nat) |
982 |
apply auto |
|
983 |
done |
|
31719 | 984 |
with zless less show "z = ?x" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
985 |
apply (intro cong_less_modulus_unique_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset
|
986 |
apply (auto, erule cong_sym_nat) |
31719 | 987 |
done |
44872 | 988 |
qed |
989 |
from less cong unique show ?thesis by blast |
|
31719 | 990 |
qed |
991 |
||
992 |
end |