author | nipkow |
Tue, 23 Jun 2009 12:58:53 +0200 | |
changeset 31766 | f767c5b1702e |
parent 31734 | a4a79836d07b |
child 31798 | fe9a3043d36c |
permissions | -rw-r--r-- |
31706 | 1 |
(* Title: GCD.thy |
2 |
Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, |
|
3 |
Thomas M. Rasmussen, Jeremy Avigad |
|
4 |
||
5 |
||
6 |
This file deals with the functions gcd and lcm, and properties of |
|
7 |
primes. Definitions and lemmas are proved uniformly for the natural |
|
8 |
numbers and integers. |
|
9 |
||
10 |
This file combines and revises a number of prior developments. |
|
11 |
||
12 |
The original theories "GCD" and "Primes" were by Christophe Tabacznyj |
|
13 |
and Lawrence C. Paulson, based on \cite{davenport92}. They introduced |
|
14 |
gcd, lcm, and prime for the natural numbers. |
|
15 |
||
16 |
The original theory "IntPrimes" was by Thomas M. Rasmussen, and |
|
17 |
extended gcd, lcm, primes to the integers. Amine Chaieb provided |
|
18 |
another extension of the notions to the integers, and added a number |
|
19 |
of results to "Primes" and "GCD". IntPrimes also defined and developed |
|
20 |
the congruence relations on the integers. The notion was extended to |
|
21 |
the natural numbers by Chiaeb. |
|
22 |
||
21256 | 23 |
*) |
24 |
||
31706 | 25 |
|
26 |
header {* GCD *} |
|
21256 | 27 |
|
28 |
theory GCD |
|
31706 | 29 |
imports NatTransfer |
30 |
begin |
|
31 |
||
32 |
declare One_nat_def [simp del] |
|
33 |
||
34 |
subsection {* gcd *} |
|
35 |
||
36 |
class gcd = one + |
|
37 |
||
38 |
fixes |
|
39 |
gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and |
|
40 |
lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
41 |
||
21256 | 42 |
begin |
43 |
||
31706 | 44 |
abbreviation |
45 |
coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
46 |
where |
|
47 |
"coprime x y == (gcd x y = 1)" |
|
48 |
||
49 |
end |
|
50 |
||
51 |
class prime = one + |
|
52 |
||
53 |
fixes |
|
54 |
prime :: "'a \<Rightarrow> bool" |
|
55 |
||
56 |
||
57 |
(* definitions for the natural numbers *) |
|
58 |
||
59 |
instantiation nat :: gcd |
|
60 |
||
61 |
begin |
|
21256 | 62 |
|
31706 | 63 |
fun |
64 |
gcd_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
65 |
where |
|
66 |
"gcd_nat x y = |
|
67 |
(if y = 0 then x else gcd y (x mod y))" |
|
68 |
||
69 |
definition |
|
70 |
lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
71 |
where |
|
72 |
"lcm_nat x y = x * y div (gcd x y)" |
|
73 |
||
74 |
instance proof qed |
|
75 |
||
76 |
end |
|
77 |
||
78 |
||
79 |
instantiation nat :: prime |
|
80 |
||
81 |
begin |
|
21256 | 82 |
|
21263 | 83 |
definition |
31706 | 84 |
prime_nat :: "nat \<Rightarrow> bool" |
85 |
where |
|
31709 | 86 |
[code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" |
31706 | 87 |
|
88 |
instance proof qed |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
89 |
|
31706 | 90 |
end |
91 |
||
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
92 |
|
31706 | 93 |
(* definitions for the integers *) |
94 |
||
95 |
instantiation int :: gcd |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
96 |
|
31706 | 97 |
begin |
21256 | 98 |
|
31706 | 99 |
definition |
100 |
gcd_int :: "int \<Rightarrow> int \<Rightarrow> int" |
|
101 |
where |
|
102 |
"gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))" |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
103 |
|
31706 | 104 |
definition |
105 |
lcm_int :: "int \<Rightarrow> int \<Rightarrow> int" |
|
106 |
where |
|
107 |
"lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))" |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
108 |
|
31706 | 109 |
instance proof qed |
110 |
||
111 |
end |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
112 |
|
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
113 |
|
31706 | 114 |
instantiation int :: prime |
115 |
||
116 |
begin |
|
117 |
||
118 |
definition |
|
119 |
prime_int :: "int \<Rightarrow> bool" |
|
120 |
where |
|
31709 | 121 |
[code del]: "prime_int p = prime (nat p)" |
31706 | 122 |
|
123 |
instance proof qed |
|
124 |
||
125 |
end |
|
126 |
||
127 |
||
128 |
subsection {* Set up Transfer *} |
|
129 |
||
130 |
||
131 |
lemma transfer_nat_int_gcd: |
|
132 |
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)" |
|
133 |
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)" |
|
134 |
"(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x" |
|
135 |
unfolding gcd_int_def lcm_int_def prime_int_def |
|
136 |
by auto |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
137 |
|
31706 | 138 |
lemma transfer_nat_int_gcd_closures: |
139 |
"x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0" |
|
140 |
"x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0" |
|
141 |
by (auto simp add: gcd_int_def lcm_int_def) |
|
142 |
||
143 |
declare TransferMorphism_nat_int[transfer add return: |
|
144 |
transfer_nat_int_gcd transfer_nat_int_gcd_closures] |
|
145 |
||
146 |
lemma transfer_int_nat_gcd: |
|
147 |
"gcd (int x) (int y) = int (gcd x y)" |
|
148 |
"lcm (int x) (int y) = int (lcm x y)" |
|
149 |
"prime (int x) = prime x" |
|
150 |
by (unfold gcd_int_def lcm_int_def prime_int_def, auto) |
|
151 |
||
152 |
lemma transfer_int_nat_gcd_closures: |
|
153 |
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0" |
|
154 |
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0" |
|
155 |
by (auto simp add: gcd_int_def lcm_int_def) |
|
156 |
||
157 |
declare TransferMorphism_int_nat[transfer add return: |
|
158 |
transfer_int_nat_gcd transfer_int_nat_gcd_closures] |
|
159 |
||
160 |
||
161 |
||
162 |
subsection {* GCD *} |
|
163 |
||
164 |
(* was gcd_induct *) |
|
165 |
lemma nat_gcd_induct: |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
166 |
fixes m n :: nat |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
167 |
assumes "\<And>m. P m 0" |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
168 |
and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n" |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
169 |
shows "P m n" |
31706 | 170 |
apply (rule gcd_nat.induct) |
171 |
apply (case_tac "y = 0") |
|
172 |
using assms apply simp_all |
|
173 |
done |
|
174 |
||
175 |
(* specific to int *) |
|
176 |
||
177 |
lemma int_gcd_neg1 [simp]: "gcd (-x::int) y = gcd x y" |
|
178 |
by (simp add: gcd_int_def) |
|
179 |
||
180 |
lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y" |
|
181 |
by (simp add: gcd_int_def) |
|
182 |
||
183 |
lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)" |
|
184 |
by (simp add: gcd_int_def) |
|
185 |
||
186 |
lemma int_gcd_cases: |
|
187 |
fixes x :: int and y |
|
188 |
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" |
|
189 |
and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))" |
|
190 |
and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)" |
|
191 |
and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))" |
|
192 |
shows "P (gcd x y)" |
|
193 |
by (insert prems, auto simp add: int_gcd_neg1 int_gcd_neg2, arith) |
|
21256 | 194 |
|
31706 | 195 |
lemma int_gcd_ge_0 [simp]: "gcd (x::int) y >= 0" |
196 |
by (simp add: gcd_int_def) |
|
197 |
||
198 |
lemma int_lcm_neg1: "lcm (-x::int) y = lcm x y" |
|
199 |
by (simp add: lcm_int_def) |
|
200 |
||
201 |
lemma int_lcm_neg2: "lcm (x::int) (-y) = lcm x y" |
|
202 |
by (simp add: lcm_int_def) |
|
203 |
||
204 |
lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)" |
|
205 |
by (simp add: lcm_int_def) |
|
21256 | 206 |
|
31706 | 207 |
lemma int_lcm_cases: |
208 |
fixes x :: int and y |
|
209 |
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" |
|
210 |
and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))" |
|
211 |
and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)" |
|
212 |
and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))" |
|
213 |
shows "P (lcm x y)" |
|
214 |
by (insert prems, auto simp add: int_lcm_neg1 int_lcm_neg2, arith) |
|
215 |
||
216 |
lemma int_lcm_ge_0 [simp]: "lcm (x::int) y >= 0" |
|
217 |
by (simp add: lcm_int_def) |
|
218 |
||
219 |
(* was gcd_0, etc. *) |
|
220 |
lemma nat_gcd_0 [simp]: "gcd (x::nat) 0 = x" |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
221 |
by simp |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
222 |
|
31706 | 223 |
(* was igcd_0, etc. *) |
224 |
lemma int_gcd_0 [simp]: "gcd (x::int) 0 = abs x" |
|
225 |
by (unfold gcd_int_def, auto) |
|
226 |
||
227 |
lemma nat_gcd_0_left [simp]: "gcd 0 (x::nat) = x" |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
228 |
by simp |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
229 |
|
31706 | 230 |
lemma int_gcd_0_left [simp]: "gcd 0 (x::int) = abs x" |
231 |
by (unfold gcd_int_def, auto) |
|
232 |
||
233 |
lemma nat_gcd_red: "gcd (x::nat) y = gcd y (x mod y)" |
|
234 |
by (case_tac "y = 0", auto) |
|
235 |
||
236 |
(* weaker, but useful for the simplifier *) |
|
237 |
||
238 |
lemma nat_gcd_non_0: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" |
|
239 |
by simp |
|
240 |
||
241 |
lemma nat_gcd_1 [simp]: "gcd (m::nat) 1 = 1" |
|
21263 | 242 |
by simp |
21256 | 243 |
|
31706 | 244 |
lemma nat_gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" |
245 |
by (simp add: One_nat_def) |
|
246 |
||
247 |
lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1" |
|
248 |
by (simp add: gcd_int_def) |
|
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
30042
diff
changeset
|
249 |
|
31706 | 250 |
lemma nat_gcd_self [simp]: "gcd (x::nat) x = x" |
251 |
by simp |
|
252 |
||
253 |
lemma int_gcd_def [simp]: "gcd (x::int) x = abs x" |
|
254 |
by (subst int_gcd_abs, auto simp add: gcd_int_def) |
|
255 |
||
256 |
declare gcd_nat.simps [simp del] |
|
21256 | 257 |
|
258 |
text {* |
|
27556 | 259 |
\medskip @{term "gcd m n"} divides @{text m} and @{text n}. The |
21256 | 260 |
conjunctions don't seem provable separately. |
261 |
*} |
|
262 |
||
31706 | 263 |
lemma nat_gcd_dvd1 [iff]: "(gcd (m::nat)) n dvd m" |
264 |
and nat_gcd_dvd2 [iff]: "(gcd m n) dvd n" |
|
265 |
apply (induct m n rule: nat_gcd_induct) |
|
266 |
apply (simp_all add: nat_gcd_non_0) |
|
21256 | 267 |
apply (blast dest: dvd_mod_imp_dvd) |
31706 | 268 |
done |
269 |
||
270 |
thm nat_gcd_dvd1 [transferred] |
|
271 |
||
272 |
lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x" |
|
273 |
apply (subst int_gcd_abs) |
|
274 |
apply (rule dvd_trans) |
|
275 |
apply (rule nat_gcd_dvd1 [transferred]) |
|
276 |
apply auto |
|
277 |
done |
|
21256 | 278 |
|
31706 | 279 |
lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y" |
280 |
apply (subst int_gcd_abs) |
|
281 |
apply (rule dvd_trans) |
|
282 |
apply (rule nat_gcd_dvd2 [transferred]) |
|
283 |
apply auto |
|
284 |
done |
|
285 |
||
31730 | 286 |
lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m" |
287 |
by(metis nat_gcd_dvd1 dvd_trans) |
|
288 |
||
289 |
lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n" |
|
290 |
by(metis nat_gcd_dvd2 dvd_trans) |
|
291 |
||
292 |
lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m" |
|
293 |
by(metis int_gcd_dvd1 dvd_trans) |
|
294 |
||
295 |
lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n" |
|
296 |
by(metis int_gcd_dvd2 dvd_trans) |
|
297 |
||
31706 | 298 |
lemma nat_gcd_le1 [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a" |
299 |
by (rule dvd_imp_le, auto) |
|
300 |
||
301 |
lemma nat_gcd_le2 [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b" |
|
302 |
by (rule dvd_imp_le, auto) |
|
303 |
||
304 |
lemma int_gcd_le1 [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a" |
|
305 |
by (rule zdvd_imp_le, auto) |
|
21256 | 306 |
|
31706 | 307 |
lemma int_gcd_le2 [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b" |
308 |
by (rule zdvd_imp_le, auto) |
|
309 |
||
310 |
lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n" |
|
311 |
by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod) |
|
312 |
||
313 |
lemma int_gcd_greatest: |
|
314 |
assumes "(k::int) dvd m" and "k dvd n" |
|
315 |
shows "k dvd gcd m n" |
|
316 |
||
317 |
apply (subst int_gcd_abs) |
|
318 |
apply (subst abs_dvd_iff [symmetric]) |
|
319 |
apply (rule nat_gcd_greatest [transferred]) |
|
320 |
using prems apply auto |
|
321 |
done |
|
21256 | 322 |
|
31706 | 323 |
lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) = |
324 |
(k dvd m & k dvd n)" |
|
325 |
by (blast intro!: nat_gcd_greatest intro: dvd_trans) |
|
326 |
||
327 |
lemma int_gcd_greatest_iff: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)" |
|
328 |
by (blast intro!: int_gcd_greatest intro: dvd_trans) |
|
21256 | 329 |
|
31706 | 330 |
lemma nat_gcd_zero [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)" |
331 |
by (simp only: dvd_0_left_iff [symmetric] nat_gcd_greatest_iff) |
|
21256 | 332 |
|
31706 | 333 |
lemma int_gcd_zero [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" |
334 |
by (auto simp add: gcd_int_def) |
|
21256 | 335 |
|
31706 | 336 |
lemma nat_gcd_pos [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)" |
337 |
by (insert nat_gcd_zero [of m n], arith) |
|
21256 | 338 |
|
31706 | 339 |
lemma int_gcd_pos [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)" |
340 |
by (insert int_gcd_zero [of m n], insert int_gcd_ge_0 [of m n], arith) |
|
341 |
||
342 |
lemma nat_gcd_commute: "gcd (m::nat) n = gcd n m" |
|
343 |
by (rule dvd_anti_sym, auto) |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
344 |
|
31706 | 345 |
lemma int_gcd_commute: "gcd (m::int) n = gcd n m" |
346 |
by (auto simp add: gcd_int_def nat_gcd_commute) |
|
347 |
||
348 |
lemma nat_gcd_assoc: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)" |
|
349 |
apply (rule dvd_anti_sym) |
|
350 |
apply (blast intro: dvd_trans)+ |
|
351 |
done |
|
21256 | 352 |
|
31706 | 353 |
lemma int_gcd_assoc: "gcd (gcd (k::int) m) n = gcd k (gcd m n)" |
354 |
by (auto simp add: gcd_int_def nat_gcd_assoc) |
|
355 |
||
31766 | 356 |
lemmas nat_gcd_left_commute = |
357 |
mk_left_commute[of gcd, OF nat_gcd_assoc nat_gcd_commute] |
|
31706 | 358 |
|
31766 | 359 |
lemmas int_gcd_left_commute = |
360 |
mk_left_commute[of gcd, OF int_gcd_assoc int_gcd_commute] |
|
31706 | 361 |
|
362 |
lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute |
|
363 |
-- {* gcd is an AC-operator *} |
|
21256 | 364 |
|
31706 | 365 |
lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute |
366 |
||
367 |
lemma nat_gcd_1_left [simp]: "gcd (1::nat) m = 1" |
|
368 |
by (subst nat_gcd_commute, simp) |
|
369 |
||
370 |
lemma nat_gcd_Suc_0_left [simp]: "gcd (Suc 0) m = Suc 0" |
|
371 |
by (subst nat_gcd_commute, simp add: One_nat_def) |
|
372 |
||
373 |
lemma int_gcd_1_left [simp]: "gcd (1::int) m = 1" |
|
374 |
by (subst int_gcd_commute, simp) |
|
21256 | 375 |
|
31706 | 376 |
lemma nat_gcd_unique: "(d::nat) dvd a \<and> d dvd b \<and> |
377 |
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" |
|
378 |
apply auto |
|
379 |
apply (rule dvd_anti_sym) |
|
380 |
apply (erule (1) nat_gcd_greatest) |
|
381 |
apply auto |
|
382 |
done |
|
21256 | 383 |
|
31706 | 384 |
lemma int_gcd_unique: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and> |
385 |
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" |
|
386 |
apply (case_tac "d = 0") |
|
387 |
apply force |
|
388 |
apply (rule iffI) |
|
389 |
apply (rule zdvd_anti_sym) |
|
390 |
apply arith |
|
391 |
apply (subst int_gcd_pos) |
|
392 |
apply clarsimp |
|
393 |
apply (drule_tac x = "d + 1" in spec) |
|
394 |
apply (frule zdvd_imp_le) |
|
395 |
apply (auto intro: int_gcd_greatest) |
|
396 |
done |
|
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
30042
diff
changeset
|
397 |
|
21256 | 398 |
text {* |
399 |
\medskip Multiplication laws |
|
400 |
*} |
|
401 |
||
31706 | 402 |
lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)" |
21256 | 403 |
-- {* \cite[page 27]{davenport92} *} |
31706 | 404 |
apply (induct m n rule: nat_gcd_induct) |
405 |
apply simp |
|
21256 | 406 |
apply (case_tac "k = 0") |
31706 | 407 |
apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2) |
408 |
done |
|
21256 | 409 |
|
31706 | 410 |
lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)" |
411 |
apply (subst (1 2) int_gcd_abs) |
|
412 |
apply (simp add: abs_mult) |
|
413 |
apply (rule nat_gcd_mult_distrib [transferred]) |
|
414 |
apply auto |
|
415 |
done |
|
21256 | 416 |
|
31706 | 417 |
lemma nat_gcd_mult [simp]: "gcd (k::nat) (k * n) = k" |
418 |
by (rule nat_gcd_mult_distrib [of k 1 n, simplified, symmetric]) |
|
21256 | 419 |
|
31706 | 420 |
lemma int_gcd_mult [simp]: "gcd (k::int) (k * n) = abs k" |
421 |
by (rule int_gcd_mult_distrib [of k 1 n, simplified, symmetric]) |
|
422 |
||
423 |
lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m" |
|
424 |
apply (insert nat_gcd_mult_distrib [of m k n]) |
|
21256 | 425 |
apply simp |
426 |
apply (erule_tac t = m in ssubst) |
|
427 |
apply simp |
|
428 |
done |
|
429 |
||
31706 | 430 |
lemma int_coprime_dvd_mult: |
431 |
assumes "coprime (k::int) n" and "k dvd m * n" |
|
432 |
shows "k dvd m" |
|
21256 | 433 |
|
31706 | 434 |
using prems |
435 |
apply (subst abs_dvd_iff [symmetric]) |
|
436 |
apply (subst dvd_abs_iff [symmetric]) |
|
437 |
apply (subst (asm) int_gcd_abs) |
|
438 |
apply (rule nat_coprime_dvd_mult [transferred]) |
|
439 |
apply auto |
|
440 |
apply (subst abs_mult [symmetric], auto) |
|
441 |
done |
|
442 |
||
443 |
lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow> |
|
444 |
(k dvd m * n) = (k dvd m)" |
|
445 |
by (auto intro: nat_coprime_dvd_mult) |
|
446 |
||
447 |
lemma int_coprime_dvd_mult_iff: "coprime (k::int) n \<Longrightarrow> |
|
448 |
(k dvd m * n) = (k dvd m)" |
|
449 |
by (auto intro: int_coprime_dvd_mult) |
|
450 |
||
451 |
lemma nat_gcd_mult_cancel: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n" |
|
21256 | 452 |
apply (rule dvd_anti_sym) |
31706 | 453 |
apply (rule nat_gcd_greatest) |
454 |
apply (rule_tac n = k in nat_coprime_dvd_mult) |
|
455 |
apply (simp add: nat_gcd_assoc) |
|
456 |
apply (simp add: nat_gcd_commute) |
|
457 |
apply (simp_all add: mult_commute) |
|
458 |
done |
|
21256 | 459 |
|
31706 | 460 |
lemma int_gcd_mult_cancel: |
461 |
assumes "coprime (k::int) n" |
|
462 |
shows "gcd (k * m) n = gcd m n" |
|
463 |
||
464 |
using prems |
|
465 |
apply (subst (1 2) int_gcd_abs) |
|
466 |
apply (subst abs_mult) |
|
467 |
apply (rule nat_gcd_mult_cancel [transferred]) |
|
468 |
apply (auto simp add: int_gcd_abs [symmetric]) |
|
469 |
done |
|
21256 | 470 |
|
471 |
text {* \medskip Addition laws *} |
|
472 |
||
31706 | 473 |
lemma nat_gcd_add1 [simp]: "gcd ((m::nat) + n) n = gcd m n" |
474 |
apply (case_tac "n = 0") |
|
475 |
apply (simp_all add: nat_gcd_non_0) |
|
476 |
done |
|
477 |
||
478 |
lemma nat_gcd_add2 [simp]: "gcd (m::nat) (m + n) = gcd m n" |
|
479 |
apply (subst (1 2) nat_gcd_commute) |
|
480 |
apply (subst add_commute) |
|
481 |
apply simp |
|
482 |
done |
|
483 |
||
484 |
(* to do: add the other variations? *) |
|
485 |
||
486 |
lemma nat_gcd_diff1: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n" |
|
487 |
by (subst nat_gcd_add1 [symmetric], auto) |
|
488 |
||
489 |
lemma nat_gcd_diff2: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n" |
|
490 |
apply (subst nat_gcd_commute) |
|
491 |
apply (subst nat_gcd_diff1 [symmetric]) |
|
492 |
apply auto |
|
493 |
apply (subst nat_gcd_commute) |
|
494 |
apply (subst nat_gcd_diff1) |
|
495 |
apply assumption |
|
496 |
apply (rule nat_gcd_commute) |
|
497 |
done |
|
498 |
||
499 |
lemma int_gcd_non_0: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)" |
|
500 |
apply (frule_tac b = y and a = x in pos_mod_sign) |
|
501 |
apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib) |
|
502 |
apply (auto simp add: nat_gcd_non_0 nat_mod_distrib [symmetric] |
|
503 |
zmod_zminus1_eq_if) |
|
504 |
apply (frule_tac a = x in pos_mod_bound) |
|
505 |
apply (subst (1 2) nat_gcd_commute) |
|
506 |
apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2 |
|
507 |
nat_le_eq_zle) |
|
508 |
done |
|
21256 | 509 |
|
31706 | 510 |
lemma int_gcd_red: "gcd (x::int) y = gcd y (x mod y)" |
511 |
apply (case_tac "y = 0") |
|
512 |
apply force |
|
513 |
apply (case_tac "y > 0") |
|
514 |
apply (subst int_gcd_non_0, auto) |
|
515 |
apply (insert int_gcd_non_0 [of "-y" "-x"]) |
|
516 |
apply (auto simp add: int_gcd_neg1 int_gcd_neg2) |
|
517 |
done |
|
518 |
||
519 |
lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n" |
|
520 |
apply (case_tac "n = 0", force) |
|
521 |
apply (subst (1 2) int_gcd_red) |
|
522 |
apply auto |
|
523 |
done |
|
524 |
||
525 |
lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n" |
|
526 |
apply (subst int_gcd_commute) |
|
527 |
apply (subst add_commute) |
|
528 |
apply (subst int_gcd_add1) |
|
529 |
apply (subst int_gcd_commute) |
|
530 |
apply (rule refl) |
|
531 |
done |
|
21256 | 532 |
|
31706 | 533 |
lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n" |
534 |
by (induct k, simp_all add: ring_simps) |
|
21256 | 535 |
|
31706 | 536 |
lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n" |
537 |
apply (subgoal_tac "ALL s. ALL m. ALL n. |
|
538 |
gcd m (int (s::nat) * m + n) = gcd m n") |
|
539 |
apply (case_tac "k >= 0") |
|
540 |
apply (drule_tac x = "nat k" in spec, force) |
|
541 |
apply (subst (1 2) int_gcd_neg2 [symmetric]) |
|
542 |
apply (drule_tac x = "nat (- k)" in spec) |
|
543 |
apply (drule_tac x = "m" in spec) |
|
544 |
apply (drule_tac x = "-n" in spec) |
|
545 |
apply auto |
|
546 |
apply (rule nat_induct) |
|
547 |
apply auto |
|
548 |
apply (auto simp add: left_distrib) |
|
549 |
apply (subst add_assoc) |
|
550 |
apply simp |
|
551 |
done |
|
21256 | 552 |
|
31706 | 553 |
(* to do: differences, and all variations of addition rules |
554 |
as simplification rules for nat and int *) |
|
555 |
||
556 |
lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n" |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
557 |
using mult_dvd_mono [of 1] by auto |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
558 |
|
31706 | 559 |
(* to do: add the three variations of these, and for ints? *) |
560 |
||
31734 | 561 |
lemma finite_divisors_nat: |
562 |
assumes "(m::nat)~= 0" shows "finite{d. d dvd m}" |
|
563 |
proof- |
|
564 |
have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite) |
|
565 |
from finite_subset[OF _ this] show ?thesis using assms |
|
566 |
by(bestsimp intro!:dvd_imp_le) |
|
567 |
qed |
|
568 |
||
569 |
lemma finite_divisors_int: |
|
570 |
assumes "(i::int) ~= 0" shows "finite{d. d dvd i}" |
|
571 |
proof- |
|
572 |
have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if) |
|
573 |
hence "finite{d. abs d <= abs i}" by simp |
|
574 |
from finite_subset[OF _ this] show ?thesis using assms |
|
575 |
by(bestsimp intro!:dvd_imp_le_int) |
|
576 |
qed |
|
577 |
||
578 |
lemma gcd_is_Max_divisors_nat: |
|
579 |
"m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})" |
|
580 |
apply(rule Max_eqI[THEN sym]) |
|
581 |
apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat) |
|
582 |
apply simp |
|
583 |
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le nat_gcd_greatest_iff nat_gcd_pos) |
|
584 |
apply simp |
|
585 |
done |
|
586 |
||
587 |
lemma gcd_is_Max_divisors_int: |
|
588 |
"m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})" |
|
589 |
apply(rule Max_eqI[THEN sym]) |
|
590 |
apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int) |
|
591 |
apply simp |
|
592 |
apply (metis int_gcd_greatest_iff int_gcd_pos zdvd_imp_le) |
|
593 |
apply simp |
|
594 |
done |
|
595 |
||
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
596 |
|
31706 | 597 |
subsection {* Coprimality *} |
598 |
||
599 |
lemma nat_div_gcd_coprime [intro]: |
|
600 |
assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0" |
|
601 |
shows "coprime (a div gcd a b) (b div gcd a b)" |
|
22367 | 602 |
proof - |
27556 | 603 |
let ?g = "gcd a b" |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
604 |
let ?a' = "a div ?g" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
605 |
let ?b' = "b div ?g" |
27556 | 606 |
let ?g' = "gcd ?a' ?b'" |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
607 |
have dvdg: "?g dvd a" "?g dvd b" by simp_all |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
608 |
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all |
22367 | 609 |
from dvdg dvdg' obtain ka kb ka' kb' where |
610 |
kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'" |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
611 |
unfolding dvd_def by blast |
31706 | 612 |
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" |
613 |
by simp_all |
|
22367 | 614 |
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" |
615 |
by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] |
|
616 |
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) |
|
31706 | 617 |
have "?g \<noteq> 0" using nz by (simp add: nat_gcd_zero) |
618 |
then have gp: "?g > 0" by arith |
|
619 |
from nat_gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . |
|
22367 | 620 |
with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
621 |
qed |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
622 |
|
31706 | 623 |
lemma int_div_gcd_coprime [intro]: |
624 |
assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0" |
|
625 |
shows "coprime (a div gcd a b) (b div gcd a b)" |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
626 |
|
31706 | 627 |
apply (subst (1 2 3) int_gcd_abs) |
628 |
apply (subst (1 2) abs_div) |
|
629 |
apply auto |
|
630 |
prefer 3 |
|
631 |
apply (rule nat_div_gcd_coprime [transferred]) |
|
632 |
using nz apply (auto simp add: int_gcd_abs [symmetric]) |
|
633 |
done |
|
634 |
||
635 |
lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)" |
|
636 |
using nat_gcd_unique[of 1 a b, simplified] by auto |
|
637 |
||
638 |
lemma nat_coprime_Suc_0: |
|
639 |
"coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)" |
|
640 |
using nat_coprime by (simp add: One_nat_def) |
|
641 |
||
642 |
lemma int_coprime: "coprime (a::int) b \<longleftrightarrow> |
|
643 |
(\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)" |
|
644 |
using int_gcd_unique [of 1 a b] |
|
645 |
apply clarsimp |
|
646 |
apply (erule subst) |
|
647 |
apply (rule iffI) |
|
648 |
apply force |
|
649 |
apply (drule_tac x = "abs e" in exI) |
|
650 |
apply (case_tac "e >= 0") |
|
651 |
apply force |
|
652 |
apply force |
|
653 |
done |
|
654 |
||
655 |
lemma nat_gcd_coprime: |
|
656 |
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and |
|
657 |
b: "b = b' * gcd a b" |
|
658 |
shows "coprime a' b'" |
|
659 |
||
660 |
apply (subgoal_tac "a' = a div gcd a b") |
|
661 |
apply (erule ssubst) |
|
662 |
apply (subgoal_tac "b' = b div gcd a b") |
|
663 |
apply (erule ssubst) |
|
664 |
apply (rule nat_div_gcd_coprime) |
|
665 |
using prems |
|
666 |
apply force |
|
667 |
apply (subst (1) b) |
|
668 |
using z apply force |
|
669 |
apply (subst (1) a) |
|
670 |
using z apply force |
|
671 |
done |
|
672 |
||
673 |
lemma int_gcd_coprime: |
|
674 |
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and |
|
675 |
b: "b = b' * gcd a b" |
|
676 |
shows "coprime a' b'" |
|
677 |
||
678 |
apply (subgoal_tac "a' = a div gcd a b") |
|
679 |
apply (erule ssubst) |
|
680 |
apply (subgoal_tac "b' = b div gcd a b") |
|
681 |
apply (erule ssubst) |
|
682 |
apply (rule int_div_gcd_coprime) |
|
683 |
using prems |
|
684 |
apply force |
|
685 |
apply (subst (1) b) |
|
686 |
using z apply force |
|
687 |
apply (subst (1) a) |
|
688 |
using z apply force |
|
689 |
done |
|
690 |
||
691 |
lemma nat_coprime_mult: assumes da: "coprime (d::nat) a" and db: "coprime d b" |
|
692 |
shows "coprime d (a * b)" |
|
693 |
apply (subst nat_gcd_commute) |
|
694 |
using da apply (subst nat_gcd_mult_cancel) |
|
695 |
apply (subst nat_gcd_commute, assumption) |
|
696 |
apply (subst nat_gcd_commute, rule db) |
|
697 |
done |
|
698 |
||
699 |
lemma int_coprime_mult: assumes da: "coprime (d::int) a" and db: "coprime d b" |
|
700 |
shows "coprime d (a * b)" |
|
701 |
apply (subst int_gcd_commute) |
|
702 |
using da apply (subst int_gcd_mult_cancel) |
|
703 |
apply (subst int_gcd_commute, assumption) |
|
704 |
apply (subst int_gcd_commute, rule db) |
|
705 |
done |
|
706 |
||
707 |
lemma nat_coprime_lmult: |
|
708 |
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" |
|
709 |
proof - |
|
710 |
have "gcd d a dvd gcd d (a * b)" |
|
711 |
by (rule nat_gcd_greatest, auto) |
|
712 |
with dab show ?thesis |
|
713 |
by auto |
|
714 |
qed |
|
715 |
||
716 |
lemma int_coprime_lmult: |
|
717 |
assumes dab: "coprime (d::int) (a * b)" shows "coprime d a" |
|
718 |
proof - |
|
719 |
have "gcd d a dvd gcd d (a * b)" |
|
720 |
by (rule int_gcd_greatest, auto) |
|
721 |
with dab show ?thesis |
|
722 |
by auto |
|
723 |
qed |
|
724 |
||
725 |
lemma nat_coprime_rmult: |
|
726 |
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d b" |
|
727 |
proof - |
|
728 |
have "gcd d b dvd gcd d (a * b)" |
|
729 |
by (rule nat_gcd_greatest, auto intro: dvd_mult) |
|
730 |
with dab show ?thesis |
|
731 |
by auto |
|
732 |
qed |
|
733 |
||
734 |
lemma int_coprime_rmult: |
|
735 |
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" |
|
736 |
proof - |
|
737 |
have "gcd d b dvd gcd d (a * b)" |
|
738 |
by (rule int_gcd_greatest, auto intro: dvd_mult) |
|
739 |
with dab show ?thesis |
|
740 |
by auto |
|
741 |
qed |
|
742 |
||
743 |
lemma nat_coprime_mul_eq: "coprime (d::nat) (a * b) \<longleftrightarrow> |
|
744 |
coprime d a \<and> coprime d b" |
|
745 |
using nat_coprime_rmult[of d a b] nat_coprime_lmult[of d a b] |
|
746 |
nat_coprime_mult[of d a b] |
|
747 |
by blast |
|
748 |
||
749 |
lemma int_coprime_mul_eq: "coprime (d::int) (a * b) \<longleftrightarrow> |
|
750 |
coprime d a \<and> coprime d b" |
|
751 |
using int_coprime_rmult[of d a b] int_coprime_lmult[of d a b] |
|
752 |
int_coprime_mult[of d a b] |
|
753 |
by blast |
|
754 |
||
755 |
lemma nat_gcd_coprime_exists: |
|
756 |
assumes nz: "gcd (a::nat) b \<noteq> 0" |
|
757 |
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'" |
|
758 |
apply (rule_tac x = "a div gcd a b" in exI) |
|
759 |
apply (rule_tac x = "b div gcd a b" in exI) |
|
760 |
using nz apply (auto simp add: nat_div_gcd_coprime dvd_div_mult) |
|
761 |
done |
|
762 |
||
763 |
lemma int_gcd_coprime_exists: |
|
764 |
assumes nz: "gcd (a::int) b \<noteq> 0" |
|
765 |
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'" |
|
766 |
apply (rule_tac x = "a div gcd a b" in exI) |
|
767 |
apply (rule_tac x = "b div gcd a b" in exI) |
|
768 |
using nz apply (auto simp add: int_div_gcd_coprime dvd_div_mult_self) |
|
769 |
done |
|
770 |
||
771 |
lemma nat_coprime_exp: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)" |
|
772 |
by (induct n, simp_all add: nat_coprime_mult) |
|
773 |
||
774 |
lemma int_coprime_exp: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)" |
|
775 |
by (induct n, simp_all add: int_coprime_mult) |
|
776 |
||
777 |
lemma nat_coprime_exp2 [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)" |
|
778 |
apply (rule nat_coprime_exp) |
|
779 |
apply (subst nat_gcd_commute) |
|
780 |
apply (rule nat_coprime_exp) |
|
781 |
apply (subst nat_gcd_commute, assumption) |
|
782 |
done |
|
783 |
||
784 |
lemma int_coprime_exp2 [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)" |
|
785 |
apply (rule int_coprime_exp) |
|
786 |
apply (subst int_gcd_commute) |
|
787 |
apply (rule int_coprime_exp) |
|
788 |
apply (subst int_gcd_commute, assumption) |
|
789 |
done |
|
790 |
||
791 |
lemma nat_gcd_exp: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" |
|
792 |
proof (cases) |
|
793 |
assume "a = 0 & b = 0" |
|
794 |
thus ?thesis by simp |
|
795 |
next assume "~(a = 0 & b = 0)" |
|
796 |
hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)" |
|
797 |
by auto |
|
798 |
hence "gcd ((a div gcd a b)^n * (gcd a b)^n) |
|
799 |
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" |
|
800 |
apply (subst (1 2) mult_commute) |
|
801 |
apply (subst nat_gcd_mult_distrib [symmetric]) |
|
802 |
apply simp |
|
803 |
done |
|
804 |
also have "(a div gcd a b)^n * (gcd a b)^n = a^n" |
|
805 |
apply (subst div_power) |
|
806 |
apply auto |
|
807 |
apply (rule dvd_div_mult_self) |
|
808 |
apply (rule dvd_power_same) |
|
809 |
apply auto |
|
810 |
done |
|
811 |
also have "(b div gcd a b)^n * (gcd a b)^n = b^n" |
|
812 |
apply (subst div_power) |
|
813 |
apply auto |
|
814 |
apply (rule dvd_div_mult_self) |
|
815 |
apply (rule dvd_power_same) |
|
816 |
apply auto |
|
817 |
done |
|
818 |
finally show ?thesis . |
|
819 |
qed |
|
820 |
||
821 |
lemma int_gcd_exp: "gcd ((a::int)^n) (b^n) = (gcd a b)^n" |
|
822 |
apply (subst (1 2) int_gcd_abs) |
|
823 |
apply (subst (1 2) power_abs) |
|
824 |
apply (rule nat_gcd_exp [where n = n, transferred]) |
|
825 |
apply auto |
|
826 |
done |
|
827 |
||
828 |
lemma nat_coprime_divprod: "(d::nat) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b" |
|
829 |
using nat_coprime_dvd_mult_iff[of d a b] |
|
830 |
by (auto simp add: mult_commute) |
|
831 |
||
832 |
lemma int_coprime_divprod: "(d::int) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b" |
|
833 |
using int_coprime_dvd_mult_iff[of d a b] |
|
834 |
by (auto simp add: mult_commute) |
|
835 |
||
836 |
lemma nat_division_decomp: assumes dc: "(a::nat) dvd b * c" |
|
837 |
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" |
|
838 |
proof- |
|
839 |
let ?g = "gcd a b" |
|
840 |
{assume "?g = 0" with dc have ?thesis by auto} |
|
841 |
moreover |
|
842 |
{assume z: "?g \<noteq> 0" |
|
843 |
from nat_gcd_coprime_exists[OF z] |
|
844 |
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" |
|
845 |
by blast |
|
846 |
have thb: "?g dvd b" by auto |
|
847 |
from ab'(1) have "a' dvd a" unfolding dvd_def by blast |
|
848 |
with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp |
|
849 |
from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto |
|
850 |
hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc) |
|
851 |
with z have th_1: "a' dvd b' * c" by auto |
|
852 |
from nat_coprime_dvd_mult[OF ab'(3)] th_1 |
|
853 |
have thc: "a' dvd c" by (subst (asm) mult_commute, blast) |
|
854 |
from ab' have "a = ?g*a'" by algebra |
|
855 |
with thb thc have ?thesis by blast } |
|
856 |
ultimately show ?thesis by blast |
|
857 |
qed |
|
858 |
||
859 |
lemma int_division_decomp: assumes dc: "(a::int) dvd b * c" |
|
860 |
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" |
|
861 |
proof- |
|
862 |
let ?g = "gcd a b" |
|
863 |
{assume "?g = 0" with dc have ?thesis by auto} |
|
864 |
moreover |
|
865 |
{assume z: "?g \<noteq> 0" |
|
866 |
from int_gcd_coprime_exists[OF z] |
|
867 |
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" |
|
868 |
by blast |
|
869 |
have thb: "?g dvd b" by auto |
|
870 |
from ab'(1) have "a' dvd a" unfolding dvd_def by blast |
|
871 |
with dc have th0: "a' dvd b*c" |
|
872 |
using dvd_trans[of a' a "b*c"] by simp |
|
873 |
from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto |
|
874 |
hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc) |
|
875 |
with z have th_1: "a' dvd b' * c" by auto |
|
876 |
from int_coprime_dvd_mult[OF ab'(3)] th_1 |
|
877 |
have thc: "a' dvd c" by (subst (asm) mult_commute, blast) |
|
878 |
from ab' have "a = ?g*a'" by algebra |
|
879 |
with thb thc have ?thesis by blast } |
|
880 |
ultimately show ?thesis by blast |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
881 |
qed |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
882 |
|
31706 | 883 |
lemma nat_pow_divides_pow: |
884 |
assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" |
|
885 |
shows "a dvd b" |
|
886 |
proof- |
|
887 |
let ?g = "gcd a b" |
|
888 |
from n obtain m where m: "n = Suc m" by (cases n, simp_all) |
|
889 |
{assume "?g = 0" with ab n have ?thesis by auto } |
|
890 |
moreover |
|
891 |
{assume z: "?g \<noteq> 0" |
|
892 |
hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv) |
|
893 |
from nat_gcd_coprime_exists[OF z] |
|
894 |
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" |
|
895 |
by blast |
|
896 |
from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" |
|
897 |
by (simp add: ab'(1,2)[symmetric]) |
|
898 |
hence "?g^n*a'^n dvd ?g^n *b'^n" |
|
899 |
by (simp only: power_mult_distrib mult_commute) |
|
900 |
with zn z n have th0:"a'^n dvd b'^n" by auto |
|
901 |
have "a' dvd a'^n" by (simp add: m) |
|
902 |
with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp |
|
903 |
hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute) |
|
904 |
from nat_coprime_dvd_mult[OF nat_coprime_exp [OF ab'(3), of m]] th1 |
|
905 |
have "a' dvd b'" by (subst (asm) mult_commute, blast) |
|
906 |
hence "a'*?g dvd b'*?g" by simp |
|
907 |
with ab'(1,2) have ?thesis by simp } |
|
908 |
ultimately show ?thesis by blast |
|
909 |
qed |
|
910 |
||
911 |
lemma int_pow_divides_pow: |
|
912 |
assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0" |
|
913 |
shows "a dvd b" |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
914 |
proof- |
31706 | 915 |
let ?g = "gcd a b" |
916 |
from n obtain m where m: "n = Suc m" by (cases n, simp_all) |
|
917 |
{assume "?g = 0" with ab n have ?thesis by auto } |
|
918 |
moreover |
|
919 |
{assume z: "?g \<noteq> 0" |
|
920 |
hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv) |
|
921 |
from int_gcd_coprime_exists[OF z] |
|
922 |
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" |
|
923 |
by blast |
|
924 |
from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" |
|
925 |
by (simp add: ab'(1,2)[symmetric]) |
|
926 |
hence "?g^n*a'^n dvd ?g^n *b'^n" |
|
927 |
by (simp only: power_mult_distrib mult_commute) |
|
928 |
with zn z n have th0:"a'^n dvd b'^n" by auto |
|
929 |
have "a' dvd a'^n" by (simp add: m) |
|
930 |
with th0 have "a' dvd b'^n" |
|
931 |
using dvd_trans[of a' "a'^n" "b'^n"] by simp |
|
932 |
hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute) |
|
933 |
from int_coprime_dvd_mult[OF int_coprime_exp [OF ab'(3), of m]] th1 |
|
934 |
have "a' dvd b'" by (subst (asm) mult_commute, blast) |
|
935 |
hence "a'*?g dvd b'*?g" by simp |
|
936 |
with ab'(1,2) have ?thesis by simp } |
|
937 |
ultimately show ?thesis by blast |
|
938 |
qed |
|
939 |
||
940 |
lemma nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)" |
|
941 |
by (auto intro: nat_pow_divides_pow dvd_power_same) |
|
942 |
||
943 |
lemma int_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)" |
|
944 |
by (auto intro: int_pow_divides_pow dvd_power_same) |
|
945 |
||
946 |
lemma nat_divides_mult: |
|
947 |
assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n" |
|
948 |
shows "m * n dvd r" |
|
949 |
proof- |
|
950 |
from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'" |
|
951 |
unfolding dvd_def by blast |
|
952 |
from mr n' have "m dvd n'*n" by (simp add: mult_commute) |
|
953 |
hence "m dvd n'" using nat_coprime_dvd_mult_iff[OF mn] by simp |
|
954 |
then obtain k where k: "n' = m*k" unfolding dvd_def by blast |
|
955 |
from n' k show ?thesis unfolding dvd_def by auto |
|
956 |
qed |
|
957 |
||
958 |
lemma int_divides_mult: |
|
959 |
assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n" |
|
960 |
shows "m * n dvd r" |
|
961 |
proof- |
|
962 |
from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'" |
|
963 |
unfolding dvd_def by blast |
|
964 |
from mr n' have "m dvd n'*n" by (simp add: mult_commute) |
|
965 |
hence "m dvd n'" using int_coprime_dvd_mult_iff[OF mn] by simp |
|
966 |
then obtain k where k: "n' = m*k" unfolding dvd_def by blast |
|
967 |
from n' k show ?thesis unfolding dvd_def by auto |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
968 |
qed |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
969 |
|
31706 | 970 |
lemma nat_coprime_plus_one [simp]: "coprime ((n::nat) + 1) n" |
971 |
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)") |
|
972 |
apply force |
|
973 |
apply (rule nat_dvd_diff) |
|
974 |
apply auto |
|
975 |
done |
|
976 |
||
977 |
lemma nat_coprime_Suc [simp]: "coprime (Suc n) n" |
|
978 |
using nat_coprime_plus_one by (simp add: One_nat_def) |
|
979 |
||
980 |
lemma int_coprime_plus_one [simp]: "coprime ((n::int) + 1) n" |
|
981 |
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)") |
|
982 |
apply force |
|
983 |
apply (rule dvd_diff) |
|
984 |
apply auto |
|
985 |
done |
|
986 |
||
987 |
lemma nat_coprime_minus_one: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n" |
|
988 |
using nat_coprime_plus_one [of "n - 1"] |
|
989 |
nat_gcd_commute [of "n - 1" n] by auto |
|
990 |
||
991 |
lemma int_coprime_minus_one: "coprime ((n::int) - 1) n" |
|
992 |
using int_coprime_plus_one [of "n - 1"] |
|
993 |
int_gcd_commute [of "n - 1" n] by auto |
|
994 |
||
995 |
lemma nat_setprod_coprime [rule_format]: |
|
996 |
"(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x" |
|
997 |
apply (case_tac "finite A") |
|
998 |
apply (induct set: finite) |
|
999 |
apply (auto simp add: nat_gcd_mult_cancel) |
|
1000 |
done |
|
1001 |
||
1002 |
lemma int_setprod_coprime [rule_format]: |
|
1003 |
"(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x" |
|
1004 |
apply (case_tac "finite A") |
|
1005 |
apply (induct set: finite) |
|
1006 |
apply (auto simp add: int_gcd_mult_cancel) |
|
1007 |
done |
|
1008 |
||
1009 |
lemma nat_prime_odd: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" |
|
1010 |
unfolding prime_nat_def |
|
1011 |
apply (subst even_mult_two_ex) |
|
1012 |
apply clarify |
|
1013 |
apply (drule_tac x = 2 in spec) |
|
1014 |
apply auto |
|
1015 |
done |
|
1016 |
||
1017 |
lemma int_prime_odd: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" |
|
1018 |
unfolding prime_int_def |
|
1019 |
apply (frule nat_prime_odd) |
|
1020 |
apply (auto simp add: even_nat_def) |
|
1021 |
done |
|
1022 |
||
1023 |
lemma nat_coprime_common_divisor: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> |
|
1024 |
x dvd b \<Longrightarrow> x = 1" |
|
1025 |
apply (subgoal_tac "x dvd gcd a b") |
|
1026 |
apply simp |
|
1027 |
apply (erule (1) nat_gcd_greatest) |
|
1028 |
done |
|
1029 |
||
1030 |
lemma int_coprime_common_divisor: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> |
|
1031 |
x dvd b \<Longrightarrow> abs x = 1" |
|
1032 |
apply (subgoal_tac "x dvd gcd a b") |
|
1033 |
apply simp |
|
1034 |
apply (erule (1) int_gcd_greatest) |
|
1035 |
done |
|
1036 |
||
1037 |
lemma nat_coprime_divisors: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> |
|
1038 |
coprime d e" |
|
1039 |
apply (auto simp add: dvd_def) |
|
1040 |
apply (frule int_coprime_lmult) |
|
1041 |
apply (subst int_gcd_commute) |
|
1042 |
apply (subst (asm) (2) int_gcd_commute) |
|
1043 |
apply (erule int_coprime_lmult) |
|
1044 |
done |
|
1045 |
||
1046 |
lemma nat_invertible_coprime: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m" |
|
1047 |
apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red) |
|
1048 |
done |
|
1049 |
||
1050 |
lemma int_invertible_coprime: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m" |
|
1051 |
apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red) |
|
1052 |
done |
|
1053 |
||
1054 |
||
1055 |
subsection {* Bezout's theorem *} |
|
1056 |
||
1057 |
(* Function bezw returns a pair of witnesses to Bezout's theorem -- |
|
1058 |
see the theorems that follow the definition. *) |
|
1059 |
fun |
|
1060 |
bezw :: "nat \<Rightarrow> nat \<Rightarrow> int * int" |
|
1061 |
where |
|
1062 |
"bezw x y = |
|
1063 |
(if y = 0 then (1, 0) else |
|
1064 |
(snd (bezw y (x mod y)), |
|
1065 |
fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))" |
|
1066 |
||
1067 |
lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp |
|
1068 |
||
1069 |
lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)), |
|
1070 |
fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))" |
|
1071 |
by simp |
|
1072 |
||
1073 |
declare bezw.simps [simp del] |
|
1074 |
||
1075 |
lemma bezw_aux [rule_format]: |
|
1076 |
"fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)" |
|
1077 |
proof (induct x y rule: nat_gcd_induct) |
|
1078 |
fix m :: nat |
|
1079 |
show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)" |
|
1080 |
by auto |
|
1081 |
next fix m :: nat and n |
|
1082 |
assume ngt0: "n > 0" and |
|
1083 |
ih: "fst (bezw n (m mod n)) * int n + |
|
1084 |
snd (bezw n (m mod n)) * int (m mod n) = |
|
1085 |
int (gcd n (m mod n))" |
|
1086 |
thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)" |
|
1087 |
apply (simp add: bezw_non_0 nat_gcd_non_0) |
|
1088 |
apply (erule subst) |
|
1089 |
apply (simp add: ring_simps) |
|
1090 |
apply (subst mod_div_equality [of m n, symmetric]) |
|
1091 |
(* applying simp here undoes the last substitution! |
|
1092 |
what is procedure cancel_div_mod? *) |
|
1093 |
apply (simp only: ring_simps zadd_int [symmetric] |
|
1094 |
zmult_int [symmetric]) |
|
1095 |
done |
|
1096 |
qed |
|
1097 |
||
1098 |
lemma int_bezout: |
|
1099 |
fixes x y |
|
1100 |
shows "EX u v. u * (x::int) + v * y = gcd x y" |
|
1101 |
proof - |
|
1102 |
have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow> |
|
1103 |
EX u v. u * x + v * y = gcd x y" |
|
1104 |
apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI) |
|
1105 |
apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI) |
|
1106 |
apply (unfold gcd_int_def) |
|
1107 |
apply simp |
|
1108 |
apply (subst bezw_aux [symmetric]) |
|
1109 |
apply auto |
|
1110 |
done |
|
1111 |
have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) | |
|
1112 |
(x \<le> 0 \<and> y \<le> 0)" |
|
1113 |
by auto |
|
1114 |
moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis" |
|
1115 |
by (erule (1) bezout_aux) |
|
1116 |
moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis" |
|
1117 |
apply (insert bezout_aux [of x "-y"]) |
|
1118 |
apply auto |
|
1119 |
apply (rule_tac x = u in exI) |
|
1120 |
apply (rule_tac x = "-v" in exI) |
|
1121 |
apply (subst int_gcd_neg2 [symmetric]) |
|
1122 |
apply auto |
|
1123 |
done |
|
1124 |
moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis" |
|
1125 |
apply (insert bezout_aux [of "-x" y]) |
|
1126 |
apply auto |
|
1127 |
apply (rule_tac x = "-u" in exI) |
|
1128 |
apply (rule_tac x = v in exI) |
|
1129 |
apply (subst int_gcd_neg1 [symmetric]) |
|
1130 |
apply auto |
|
1131 |
done |
|
1132 |
moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis" |
|
1133 |
apply (insert bezout_aux [of "-x" "-y"]) |
|
1134 |
apply auto |
|
1135 |
apply (rule_tac x = "-u" in exI) |
|
1136 |
apply (rule_tac x = "-v" in exI) |
|
1137 |
apply (subst int_gcd_neg1 [symmetric]) |
|
1138 |
apply (subst int_gcd_neg2 [symmetric]) |
|
1139 |
apply auto |
|
1140 |
done |
|
1141 |
ultimately show ?thesis by blast |
|
1142 |
qed |
|
1143 |
||
1144 |
text {* versions of Bezout for nat, by Amine Chaieb *} |
|
1145 |
||
1146 |
lemma ind_euclid: |
|
1147 |
assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" |
|
1148 |
and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1149 |
shows "P a b" |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1150 |
proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct) |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1151 |
fix n a b |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1152 |
assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b" |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1153 |
have "a = b \<or> a < b \<or> b < a" by arith |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1154 |
moreover {assume eq: "a= b" |
31706 | 1155 |
from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq |
1156 |
by simp} |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1157 |
moreover |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1158 |
{assume lt: "a < b" |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1159 |
hence "a + b - a < n \<or> a = 0" using H(2) by arith |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1160 |
moreover |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1161 |
{assume "a =0" with z c have "P a b" by blast } |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1162 |
moreover |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1163 |
{assume ab: "a + b - a < n" |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1164 |
have th0: "a + b - a = a + (b - a)" using lt by arith |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1165 |
from add[rule_format, OF H(1)[rule_format, OF ab th0]] |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1166 |
have "P a b" by (simp add: th0[symmetric])} |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1167 |
ultimately have "P a b" by blast} |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1168 |
moreover |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1169 |
{assume lt: "a > b" |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1170 |
hence "b + a - b < n \<or> b = 0" using H(2) by arith |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1171 |
moreover |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1172 |
{assume "b =0" with z c have "P a b" by blast } |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1173 |
moreover |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1174 |
{assume ab: "b + a - b < n" |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1175 |
have th0: "b + a - b = b + (a - b)" using lt by arith |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1176 |
from add[rule_format, OF H(1)[rule_format, OF ab th0]] |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1177 |
have "P b a" by (simp add: th0[symmetric]) |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1178 |
hence "P a b" using c by blast } |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1179 |
ultimately have "P a b" by blast} |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1180 |
ultimately show "P a b" by blast |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1181 |
qed |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1182 |
|
31706 | 1183 |
lemma nat_bezout_lemma: |
1184 |
assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> |
|
1185 |
(a * x = b * y + d \<or> b * x = a * y + d)" |
|
1186 |
shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and> |
|
1187 |
(a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)" |
|
1188 |
using ex |
|
1189 |
apply clarsimp |
|
1190 |
apply (rule_tac x="d" in exI, simp add: dvd_add) |
|
1191 |
apply (case_tac "a * x = b * y + d" , simp_all) |
|
1192 |
apply (rule_tac x="x + y" in exI) |
|
1193 |
apply (rule_tac x="y" in exI) |
|
1194 |
apply algebra |
|
1195 |
apply (rule_tac x="x" in exI) |
|
1196 |
apply (rule_tac x="x + y" in exI) |
|
1197 |
apply algebra |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1198 |
done |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1199 |
|
31706 | 1200 |
lemma nat_bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> |
1201 |
(a * x = b * y + d \<or> b * x = a * y + d)" |
|
1202 |
apply(induct a b rule: ind_euclid) |
|
1203 |
apply blast |
|
1204 |
apply clarify |
|
1205 |
apply (rule_tac x="a" in exI, simp add: dvd_add) |
|
1206 |
apply clarsimp |
|
1207 |
apply (rule_tac x="d" in exI) |
|
1208 |
apply (case_tac "a * x = b * y + d", simp_all add: dvd_add) |
|
1209 |
apply (rule_tac x="x+y" in exI) |
|
1210 |
apply (rule_tac x="y" in exI) |
|
1211 |
apply algebra |
|
1212 |
apply (rule_tac x="x" in exI) |
|
1213 |
apply (rule_tac x="x+y" in exI) |
|
1214 |
apply algebra |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1215 |
done |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1216 |
|
31706 | 1217 |
lemma nat_bezout1: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> |
1218 |
(a * x - b * y = d \<or> b * x - a * y = d)" |
|
1219 |
using nat_bezout_add[of a b] |
|
1220 |
apply clarsimp |
|
1221 |
apply (rule_tac x="d" in exI, simp) |
|
1222 |
apply (rule_tac x="x" in exI) |
|
1223 |
apply (rule_tac x="y" in exI) |
|
1224 |
apply auto |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1225 |
done |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1226 |
|
31706 | 1227 |
lemma nat_bezout_add_strong: assumes nz: "a \<noteq> (0::nat)" |
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1228 |
shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d" |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1229 |
proof- |
31706 | 1230 |
from nz have ap: "a > 0" by simp |
1231 |
from nat_bezout_add[of a b] |
|
1232 |
have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or> |
|
1233 |
(\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1234 |
moreover |
31706 | 1235 |
{fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d" |
1236 |
from H have ?thesis by blast } |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1237 |
moreover |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1238 |
{fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d" |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1239 |
{assume b0: "b = 0" with H have ?thesis by simp} |
31706 | 1240 |
moreover |
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1241 |
{assume b: "b \<noteq> 0" hence bp: "b > 0" by simp |
31706 | 1242 |
from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b" |
1243 |
by auto |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1244 |
moreover |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1245 |
{assume db: "d=b" |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1246 |
from prems have ?thesis apply simp |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1247 |
apply (rule exI[where x = b], simp) |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1248 |
apply (rule exI[where x = b]) |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1249 |
by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)} |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1250 |
moreover |
31706 | 1251 |
{assume db: "d < b" |
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1252 |
{assume "x=0" hence ?thesis using prems by simp } |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1253 |
moreover |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1254 |
{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1255 |
from db have "d \<le> b - 1" by simp |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1256 |
hence "d*b \<le> b*(b - 1)" by simp |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1257 |
with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"] |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1258 |
have dble: "d*b \<le> x*b*(b - 1)" using bp by simp |
31706 | 1259 |
from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)" |
1260 |
by simp |
|
1261 |
hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x" |
|
1262 |
by (simp only: mult_assoc right_distrib) |
|
1263 |
hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" |
|
1264 |
by algebra |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1265 |
hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp |
31706 | 1266 |
hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" |
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1267 |
by (simp only: diff_add_assoc[OF dble, of d, symmetric]) |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1268 |
hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d" |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1269 |
by (simp only: diff_mult_distrib2 add_commute mult_ac) |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1270 |
hence ?thesis using H(1,2) |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1271 |
apply - |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1272 |
apply (rule exI[where x=d], simp) |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1273 |
apply (rule exI[where x="(b - 1) * y"]) |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1274 |
by (rule exI[where x="x*(b - 1) - d"], simp)} |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1275 |
ultimately have ?thesis by blast} |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1276 |
ultimately have ?thesis by blast} |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1277 |
ultimately have ?thesis by blast} |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1278 |
ultimately show ?thesis by blast |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1279 |
qed |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1280 |
|
31706 | 1281 |
lemma nat_bezout: assumes a: "(a::nat) \<noteq> 0" |
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1282 |
shows "\<exists>x y. a * x = b * y + gcd a b" |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1283 |
proof- |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1284 |
let ?g = "gcd a b" |
31706 | 1285 |
from nat_bezout_add_strong[OF a, of b] |
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1286 |
obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1287 |
from d(1,2) have "d dvd ?g" by simp |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1288 |
then obtain k where k: "?g = d*k" unfolding dvd_def by blast |
31706 | 1289 |
from d(3) have "a * x * k = (b * y + d) *k " by auto |
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1290 |
hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k) |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1291 |
thus ?thesis by blast |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1292 |
qed |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1293 |
|
31706 | 1294 |
|
1295 |
subsection {* LCM *} |
|
1296 |
||
1297 |
lemma int_lcm_altdef: "lcm (a::int) b = (abs a) * (abs b) div gcd a b" |
|
1298 |
by (simp add: lcm_int_def lcm_nat_def zdiv_int |
|
1299 |
zmult_int [symmetric] gcd_int_def) |
|
1300 |
||
1301 |
lemma nat_prod_gcd_lcm: "(m::nat) * n = gcd m n * lcm m n" |
|
1302 |
unfolding lcm_nat_def |
|
1303 |
by (simp add: dvd_mult_div_cancel [OF nat_gcd_dvd_prod]) |
|
1304 |
||
1305 |
lemma int_prod_gcd_lcm: "abs(m::int) * abs n = gcd m n * lcm m n" |
|
1306 |
unfolding lcm_int_def gcd_int_def |
|
1307 |
apply (subst int_mult [symmetric]) |
|
1308 |
apply (subst nat_prod_gcd_lcm [symmetric]) |
|
1309 |
apply (subst nat_abs_mult_distrib [symmetric]) |
|
1310 |
apply (simp, simp add: abs_mult) |
|
1311 |
done |
|
1312 |
||
1313 |
lemma nat_lcm_0 [simp]: "lcm (m::nat) 0 = 0" |
|
1314 |
unfolding lcm_nat_def by simp |
|
1315 |
||
1316 |
lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0" |
|
1317 |
unfolding lcm_int_def by simp |
|
1318 |
||
1319 |
lemma nat_lcm_1 [simp]: "lcm (m::nat) 1 = m" |
|
1320 |
unfolding lcm_nat_def by simp |
|
1321 |
||
1322 |
lemma nat_lcm_Suc_0 [simp]: "lcm (m::nat) (Suc 0) = m" |
|
1323 |
unfolding lcm_nat_def by (simp add: One_nat_def) |
|
1324 |
||
1325 |
lemma int_lcm_1 [simp]: "lcm (m::int) 1 = abs m" |
|
1326 |
unfolding lcm_int_def by simp |
|
1327 |
||
1328 |
lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0" |
|
1329 |
unfolding lcm_nat_def by simp |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1330 |
|
31706 | 1331 |
lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0" |
1332 |
unfolding lcm_int_def by simp |
|
1333 |
||
1334 |
lemma nat_lcm_1_left [simp]: "lcm (1::nat) m = m" |
|
1335 |
unfolding lcm_nat_def by simp |
|
1336 |
||
1337 |
lemma nat_lcm_Suc_0_left [simp]: "lcm (Suc 0) m = m" |
|
1338 |
unfolding lcm_nat_def by (simp add: One_nat_def) |
|
1339 |
||
1340 |
lemma int_lcm_1_left [simp]: "lcm (1::int) m = abs m" |
|
1341 |
unfolding lcm_int_def by simp |
|
1342 |
||
1343 |
lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m" |
|
1344 |
unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps) |
|
1345 |
||
1346 |
lemma int_lcm_commute: "lcm (m::int) n = lcm n m" |
|
1347 |
unfolding lcm_int_def by (subst nat_lcm_commute, rule refl) |
|
1348 |
||
1349 |
||
1350 |
lemma nat_lcm_pos: |
|
1351 |
assumes mpos: "(m::nat) > 0" |
|
1352 |
and npos: "n>0" |
|
1353 |
shows "lcm m n > 0" |
|
1354 |
proof(rule ccontr, simp add: lcm_nat_def nat_gcd_zero) |
|
1355 |
assume h:"m*n div gcd m n = 0" |
|
1356 |
from mpos npos have "gcd m n \<noteq> 0" using nat_gcd_zero by simp |
|
1357 |
hence gcdp: "gcd m n > 0" by simp |
|
1358 |
with h |
|
1359 |
have "m*n < gcd m n" |
|
1360 |
by (cases "m * n < gcd m n") |
|
1361 |
(auto simp add: div_if[OF gcdp, where m="m*n"]) |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1362 |
moreover |
31706 | 1363 |
have "gcd m n dvd m" by simp |
1364 |
with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp |
|
1365 |
with npos have t1:"gcd m n*n \<le> m*n" by simp |
|
1366 |
have "gcd m n \<le> gcd m n*n" using npos by simp |
|
1367 |
with t1 have "gcd m n \<le> m*n" by arith |
|
1368 |
ultimately show "False" by simp |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1369 |
qed |
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1370 |
|
31706 | 1371 |
lemma int_lcm_pos: |
1372 |
assumes mneq0: "(m::int) ~= 0" |
|
1373 |
and npos: "n ~= 0" |
|
1374 |
shows "lcm m n > 0" |
|
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset
|
1375 |
|
31706 | 1376 |
apply (subst int_lcm_abs) |
1377 |
apply (rule nat_lcm_pos [transferred]) |
|
1378 |
using prems apply auto |
|
1379 |
done |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1380 |
|
31706 | 1381 |
lemma nat_dvd_pos: |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1382 |
fixes n m :: nat |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1383 |
assumes "n > 0" and "m dvd n" |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1384 |
shows "m > 0" |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1385 |
using assms by (cases m) auto |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1386 |
|
31706 | 1387 |
lemma nat_lcm_least: |
1388 |
assumes "(m::nat) dvd k" and "n dvd k" |
|
27556 | 1389 |
shows "lcm m n dvd k" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1390 |
proof (cases k) |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1391 |
case 0 then show ?thesis by auto |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1392 |
next |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1393 |
case (Suc _) then have pos_k: "k > 0" by auto |
31706 | 1394 |
from assms nat_dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto |
1395 |
with nat_gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1396 |
from assms obtain p where k_m: "k = m * p" using dvd_def by blast |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1397 |
from assms obtain q where k_n: "k = n * q" using dvd_def by blast |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1398 |
from pos_k k_m have pos_p: "p > 0" by auto |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1399 |
from pos_k k_n have pos_q: "q > 0" by auto |
27556 | 1400 |
have "k * k * gcd q p = k * gcd (k * q) (k * p)" |
31706 | 1401 |
by (simp add: mult_ac nat_gcd_mult_distrib) |
27556 | 1402 |
also have "\<dots> = k * gcd (m * p * q) (n * q * p)" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1403 |
by (simp add: k_m [symmetric] k_n [symmetric]) |
27556 | 1404 |
also have "\<dots> = k * p * q * gcd m n" |
31706 | 1405 |
by (simp add: mult_ac nat_gcd_mult_distrib) |
27556 | 1406 |
finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1407 |
by (simp only: k_m [symmetric] k_n [symmetric]) |
27556 | 1408 |
then have "p * q * m * n * gcd q p = p * q * k * gcd m n" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1409 |
by (simp add: mult_ac) |
27556 | 1410 |
with pos_p pos_q have "m * n * gcd q p = k * gcd m n" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1411 |
by simp |
31706 | 1412 |
with nat_prod_gcd_lcm [of m n] |
27556 | 1413 |
have "lcm m n * gcd q p * gcd m n = k * gcd m n" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1414 |
by (simp add: mult_ac) |
31706 | 1415 |
with pos_gcd have "lcm m n * gcd q p = k" by auto |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1416 |
then show ?thesis using dvd_def by auto |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1417 |
qed |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1418 |
|
31706 | 1419 |
lemma int_lcm_least: |
1420 |
assumes "(m::int) dvd k" and "n dvd k" |
|
1421 |
shows "lcm m n dvd k" |
|
1422 |
||
1423 |
apply (subst int_lcm_abs) |
|
1424 |
apply (rule dvd_trans) |
|
1425 |
apply (rule nat_lcm_least [transferred, of _ "abs k" _]) |
|
1426 |
using prems apply auto |
|
1427 |
done |
|
1428 |
||
31730 | 1429 |
lemma nat_lcm_dvd1: "(m::nat) dvd lcm m n" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1430 |
proof (cases m) |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1431 |
case 0 then show ?thesis by simp |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1432 |
next |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1433 |
case (Suc _) |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1434 |
then have mpos: "m > 0" by simp |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1435 |
show ?thesis |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1436 |
proof (cases n) |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1437 |
case 0 then show ?thesis by simp |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1438 |
next |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1439 |
case (Suc _) |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1440 |
then have npos: "n > 0" by simp |
27556 | 1441 |
have "gcd m n dvd n" by simp |
1442 |
then obtain k where "n = gcd m n * k" using dvd_def by auto |
|
31706 | 1443 |
then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" |
1444 |
by (simp add: mult_ac) |
|
1445 |
also have "\<dots> = m * k" using mpos npos nat_gcd_zero by simp |
|
1446 |
finally show ?thesis by (simp add: lcm_nat_def) |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1447 |
qed |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1448 |
qed |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1449 |
|
31730 | 1450 |
lemma int_lcm_dvd1: "(m::int) dvd lcm m n" |
31706 | 1451 |
apply (subst int_lcm_abs) |
1452 |
apply (rule dvd_trans) |
|
1453 |
prefer 2 |
|
1454 |
apply (rule nat_lcm_dvd1 [transferred]) |
|
1455 |
apply auto |
|
1456 |
done |
|
1457 |
||
31730 | 1458 |
lemma nat_lcm_dvd2: "(n::nat) dvd lcm m n" |
31706 | 1459 |
by (subst nat_lcm_commute, rule nat_lcm_dvd1) |
1460 |
||
31730 | 1461 |
lemma int_lcm_dvd2: "(n::int) dvd lcm m n" |
31706 | 1462 |
by (subst int_lcm_commute, rule int_lcm_dvd1) |
1463 |
||
31730 | 1464 |
lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n" |
31729 | 1465 |
by(metis nat_lcm_dvd1 dvd_trans) |
1466 |
||
31730 | 1467 |
lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n" |
31729 | 1468 |
by(metis nat_lcm_dvd2 dvd_trans) |
1469 |
||
31730 | 1470 |
lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n" |
31729 | 1471 |
by(metis int_lcm_dvd1 dvd_trans) |
1472 |
||
31730 | 1473 |
lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n" |
31729 | 1474 |
by(metis int_lcm_dvd2 dvd_trans) |
1475 |
||
31706 | 1476 |
lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and> |
1477 |
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b" |
|
31730 | 1478 |
by (auto intro: dvd_anti_sym nat_lcm_least nat_lcm_dvd1 nat_lcm_dvd2) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1479 |
|
31706 | 1480 |
lemma int_lcm_unique: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and> |
1481 |
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b" |
|
1482 |
by (auto intro: dvd_anti_sym [transferred] int_lcm_least) |
|
1483 |
||
1484 |
lemma nat_lcm_dvd_eq [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y" |
|
1485 |
apply (rule sym) |
|
1486 |
apply (subst nat_lcm_unique [symmetric]) |
|
1487 |
apply auto |
|
1488 |
done |
|
1489 |
||
1490 |
lemma int_lcm_dvd_eq [simp]: "0 <= y \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm x y = y" |
|
1491 |
apply (rule sym) |
|
1492 |
apply (subst int_lcm_unique [symmetric]) |
|
1493 |
apply auto |
|
1494 |
done |
|
1495 |
||
1496 |
lemma nat_lcm_dvd_eq' [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y" |
|
1497 |
by (subst nat_lcm_commute, erule nat_lcm_dvd_eq) |
|
1498 |
||
1499 |
lemma int_lcm_dvd_eq' [simp]: "y >= 0 \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm y x = y" |
|
1500 |
by (subst int_lcm_commute, erule (1) int_lcm_dvd_eq) |
|
1501 |
||
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1502 |
|
31766 | 1503 |
lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)" |
1504 |
apply(rule nat_lcm_unique[THEN iffD1]) |
|
1505 |
apply (metis dvd.order_trans nat_lcm_unique) |
|
1506 |
done |
|
1507 |
||
1508 |
lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)" |
|
1509 |
apply(rule int_lcm_unique[THEN iffD1]) |
|
1510 |
apply (metis dvd_trans int_lcm_unique) |
|
1511 |
done |
|
1512 |
||
1513 |
lemmas lcm_left_commute_nat = |
|
1514 |
mk_left_commute[of lcm, OF lcm_assoc_nat nat_lcm_commute] |
|
1515 |
||
1516 |
lemmas lcm_left_commute_int = |
|
1517 |
mk_left_commute[of lcm, OF lcm_assoc_int int_lcm_commute] |
|
1518 |
||
1519 |
lemmas lcm_ac_nat = lcm_assoc_nat nat_lcm_commute lcm_left_commute_nat |
|
1520 |
lemmas lcm_ac_int = lcm_assoc_int int_lcm_commute lcm_left_commute_int |
|
1521 |
||
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1522 |
|
31706 | 1523 |
subsection {* Primes *} |
22367 | 1524 |
|
31706 | 1525 |
(* Is there a better way to handle these, rather than making them |
1526 |
elim rules? *) |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
1527 |
|
31706 | 1528 |
lemma nat_prime_ge_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= 0" |
1529 |
by (unfold prime_nat_def, auto) |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
1530 |
|
31706 | 1531 |
lemma nat_prime_gt_0 [elim]: "prime (p::nat) \<Longrightarrow> p > 0" |
1532 |
by (unfold prime_nat_def, auto) |
|
22367 | 1533 |
|
31706 | 1534 |
lemma nat_prime_ge_1 [elim]: "prime (p::nat) \<Longrightarrow> p >= 1" |
1535 |
by (unfold prime_nat_def, auto) |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
1536 |
|
31706 | 1537 |
lemma nat_prime_gt_1 [elim]: "prime (p::nat) \<Longrightarrow> p > 1" |
1538 |
by (unfold prime_nat_def, auto) |
|
22367 | 1539 |
|
31706 | 1540 |
lemma nat_prime_ge_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0" |
1541 |
by (unfold prime_nat_def, auto) |
|
22367 | 1542 |
|
31706 | 1543 |
lemma nat_prime_gt_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0" |
1544 |
by (unfold prime_nat_def, auto) |
|
1545 |
||
1546 |
lemma nat_prime_ge_2 [elim]: "prime (p::nat) \<Longrightarrow> p >= 2" |
|
1547 |
by (unfold prime_nat_def, auto) |
|
1548 |
||
1549 |
lemma int_prime_ge_0 [elim]: "prime (p::int) \<Longrightarrow> p >= 0" |
|
1550 |
by (unfold prime_int_def prime_nat_def, auto) |
|
22367 | 1551 |
|
31706 | 1552 |
lemma int_prime_gt_0 [elim]: "prime (p::int) \<Longrightarrow> p > 0" |
1553 |
by (unfold prime_int_def prime_nat_def, auto) |
|
1554 |
||
1555 |
lemma int_prime_ge_1 [elim]: "prime (p::int) \<Longrightarrow> p >= 1" |
|
1556 |
by (unfold prime_int_def prime_nat_def, auto) |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
1557 |
|
31706 | 1558 |
lemma int_prime_gt_1 [elim]: "prime (p::int) \<Longrightarrow> p > 1" |
1559 |
by (unfold prime_int_def prime_nat_def, auto) |
|
1560 |
||
1561 |
lemma int_prime_ge_2 [elim]: "prime (p::int) \<Longrightarrow> p >= 2" |
|
1562 |
by (unfold prime_int_def prime_nat_def, auto) |
|
22367 | 1563 |
|
31706 | 1564 |
thm prime_nat_def; |
1565 |
thm prime_nat_def [transferred]; |
|
1566 |
||
1567 |
lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow> |
|
1568 |
m = 1 \<or> m = p))" |
|
1569 |
using prime_nat_def [transferred] |
|
1570 |
apply (case_tac "p >= 0") |
|
1571 |
by (blast, auto simp add: int_prime_ge_0) |
|
1572 |
||
1573 |
(* To do: determine primality of any numeral *) |
|
1574 |
||
1575 |
lemma nat_zero_not_prime [simp]: "~prime (0::nat)" |
|
1576 |
by (simp add: prime_nat_def) |
|
1577 |
||
1578 |
lemma int_zero_not_prime [simp]: "~prime (0::int)" |
|
1579 |
by (simp add: prime_int_def) |
|
1580 |
||
1581 |
lemma nat_one_not_prime [simp]: "~prime (1::nat)" |
|
1582 |
by (simp add: prime_nat_def) |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
1583 |
|
31706 | 1584 |
lemma nat_Suc_0_not_prime [simp]: "~prime (Suc 0)" |
1585 |
by (simp add: prime_nat_def One_nat_def) |
|
1586 |
||
1587 |
lemma int_one_not_prime [simp]: "~prime (1::int)" |
|
1588 |
by (simp add: prime_int_def) |
|
1589 |
||
1590 |
lemma nat_two_is_prime [simp]: "prime (2::nat)" |
|
1591 |
apply (auto simp add: prime_nat_def) |
|
1592 |
apply (case_tac m) |
|
1593 |
apply (auto dest!: dvd_imp_le) |
|
1594 |
done |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
1595 |
|
31706 | 1596 |
lemma int_two_is_prime [simp]: "prime (2::int)" |
1597 |
by (rule nat_two_is_prime [transferred direction: nat "op <= (0::int)"]) |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1598 |
|
31706 | 1599 |
lemma nat_prime_imp_coprime: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n" |
1600 |
apply (unfold prime_nat_def) |
|
1601 |
apply (metis nat_gcd_dvd1 nat_gcd_dvd2) |
|
1602 |
done |
|
1603 |
||
1604 |
lemma int_prime_imp_coprime: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n" |
|
1605 |
apply (unfold prime_int_altdef) |
|
1606 |
apply (metis int_gcd_dvd1 int_gcd_dvd2 int_gcd_ge_0) |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1607 |
done |
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1608 |
|
31706 | 1609 |
lemma nat_prime_dvd_mult: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" |
1610 |
by (blast intro: nat_coprime_dvd_mult nat_prime_imp_coprime) |
|
1611 |
||
1612 |
lemma int_prime_dvd_mult: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" |
|
1613 |
by (blast intro: int_coprime_dvd_mult int_prime_imp_coprime) |
|
1614 |
||
1615 |
lemma nat_prime_dvd_mult_eq [simp]: "prime (p::nat) \<Longrightarrow> |
|
1616 |
p dvd m * n = (p dvd m \<or> p dvd n)" |
|
1617 |
by (rule iffI, rule nat_prime_dvd_mult, auto) |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1618 |
|
31706 | 1619 |
lemma int_prime_dvd_mult_eq [simp]: "prime (p::int) \<Longrightarrow> |
1620 |
p dvd m * n = (p dvd m \<or> p dvd n)" |
|
1621 |
by (rule iffI, rule int_prime_dvd_mult, auto) |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1622 |
|
31706 | 1623 |
lemma nat_not_prime_eq_prod: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow> |
1624 |
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n" |
|
1625 |
unfolding prime_nat_def dvd_def apply auto |
|
1626 |
apply (subgoal_tac "k > 1") |
|
1627 |
apply force |
|
1628 |
apply (subgoal_tac "k ~= 0") |
|
1629 |
apply force |
|
1630 |
apply (rule notI) |
|
1631 |
apply force |
|
1632 |
done |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1633 |
|
31706 | 1634 |
(* there's a lot of messing around with signs of products here -- |
1635 |
could this be made more automatic? *) |
|
1636 |
lemma int_not_prime_eq_prod: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow> |
|
1637 |
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n" |
|
1638 |
unfolding prime_int_altdef dvd_def |
|
1639 |
apply auto |
|
1640 |
apply (rule_tac x = m in exI) |
|
1641 |
apply (rule_tac x = k in exI) |
|
1642 |
apply (auto simp add: mult_compare_simps) |
|
1643 |
apply (subgoal_tac "k > 0") |
|
1644 |
apply arith |
|
1645 |
apply (case_tac "k <= 0") |
|
1646 |
apply (subgoal_tac "m * k <= 0") |
|
1647 |
apply force |
|
1648 |
apply (subst zero_compare_simps(8)) |
|
1649 |
apply auto |
|
1650 |
apply (subgoal_tac "m * k <= 0") |
|
1651 |
apply force |
|
1652 |
apply (subst zero_compare_simps(8)) |
|
1653 |
apply auto |
|
1654 |
done |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1655 |
|
31706 | 1656 |
lemma nat_prime_dvd_power [rule_format]: "prime (p::nat) --> |
1657 |
n > 0 --> (p dvd x^n --> p dvd x)" |
|
1658 |
by (induct n rule: nat_induct, auto) |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1659 |
|
31706 | 1660 |
lemma int_prime_dvd_power [rule_format]: "prime (p::int) --> |
1661 |
n > 0 --> (p dvd x^n --> p dvd x)" |
|
1662 |
apply (induct n rule: nat_induct, auto) |
|
1663 |
apply (frule int_prime_ge_0) |
|
1664 |
apply auto |
|
1665 |
done |
|
1666 |
||
1667 |
lemma nat_prime_imp_power_coprime: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> |
|
1668 |
coprime a (p^m)" |
|
1669 |
apply (rule nat_coprime_exp) |
|
1670 |
apply (subst nat_gcd_commute) |
|
1671 |
apply (erule (1) nat_prime_imp_coprime) |
|
1672 |
done |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1673 |
|
31706 | 1674 |
lemma int_prime_imp_power_coprime: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> |
1675 |
coprime a (p^m)" |
|
1676 |
apply (rule int_coprime_exp) |
|
1677 |
apply (subst int_gcd_commute) |
|
1678 |
apply (erule (1) int_prime_imp_coprime) |
|
1679 |
done |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1680 |
|
31706 | 1681 |
lemma nat_primes_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" |
1682 |
apply (rule nat_prime_imp_coprime, assumption) |
|
1683 |
apply (unfold prime_nat_def, auto) |
|
1684 |
done |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1685 |
|
31706 | 1686 |
lemma int_primes_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" |
1687 |
apply (rule int_prime_imp_coprime, assumption) |
|
1688 |
apply (unfold prime_int_altdef, clarify) |
|
1689 |
apply (drule_tac x = q in spec) |
|
1690 |
apply (drule_tac x = p in spec) |
|
1691 |
apply auto |
|
1692 |
done |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1693 |
|
31706 | 1694 |
lemma nat_primes_imp_powers_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> |
1695 |
coprime (p^m) (q^n)" |
|
1696 |
by (rule nat_coprime_exp2, rule nat_primes_coprime) |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1697 |
|
31706 | 1698 |
lemma int_primes_imp_powers_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> |
1699 |
coprime (p^m) (q^n)" |
|
1700 |
by (rule int_coprime_exp2, rule int_primes_coprime) |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1701 |
|
31706 | 1702 |
lemma nat_prime_factor: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n" |
1703 |
apply (induct n rule: nat_less_induct) |
|
1704 |
apply (case_tac "n = 0") |
|
1705 |
using nat_two_is_prime apply blast |
|
1706 |
apply (case_tac "prime n") |
|
1707 |
apply blast |
|
1708 |
apply (subgoal_tac "n > 1") |
|
1709 |
apply (frule (1) nat_not_prime_eq_prod) |
|
1710 |
apply (auto intro: dvd_mult dvd_mult2) |
|
1711 |
done |
|
23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset
|
1712 |
|
31706 | 1713 |
(* An Isar version: |
1714 |
||
1715 |
lemma nat_prime_factor_b: |
|
1716 |
fixes n :: nat |
|
1717 |
assumes "n \<noteq> 1" |
|
1718 |
shows "\<exists>p. prime p \<and> p dvd n" |
|
23983 | 1719 |
|
31706 | 1720 |
using `n ~= 1` |
1721 |
proof (induct n rule: nat_less_induct) |
|
1722 |
fix n :: nat |
|
1723 |
assume "n ~= 1" and |
|
1724 |
ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)" |
|
1725 |
thus "\<exists>p. prime p \<and> p dvd n" |
|
1726 |
proof - |
|
1727 |
{ |
|
1728 |
assume "n = 0" |
|
1729 |
moreover note nat_two_is_prime |
|
1730 |
ultimately have ?thesis |
|
1731 |
by (auto simp del: nat_two_is_prime) |
|
1732 |
} |
|
1733 |
moreover |
|
1734 |
{ |
|
1735 |
assume "prime n" |
|
1736 |
hence ?thesis by auto |
|
1737 |
} |
|
1738 |
moreover |
|
1739 |
{ |
|
1740 |
assume "n ~= 0" and "~ prime n" |
|
1741 |
with `n ~= 1` have "n > 1" by auto |
|
1742 |
with `~ prime n` and nat_not_prime_eq_prod obtain m k where |
|
1743 |
"n = m * k" and "1 < m" and "m < n" by blast |
|
1744 |
with ih obtain p where "prime p" and "p dvd m" by blast |
|
1745 |
with `n = m * k` have ?thesis by auto |
|
1746 |
} |
|
1747 |
ultimately show ?thesis by blast |
|
1748 |
qed |
|
23983 | 1749 |
qed |
1750 |
||
31706 | 1751 |
*) |
1752 |
||
1753 |
text {* One property of coprimality is easier to prove via prime factors. *} |
|
1754 |
||
1755 |
lemma nat_prime_divprod_pow: |
|
1756 |
assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b" |
|
1757 |
shows "p^n dvd a \<or> p^n dvd b" |
|
1758 |
proof- |
|
1759 |
{assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis |
|
1760 |
apply (cases "n=0", simp_all) |
|
1761 |
apply (cases "a=1", simp_all) done} |
|
1762 |
moreover |
|
1763 |
{assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1" |
|
1764 |
then obtain m where m: "n = Suc m" by (cases n, auto) |
|
1765 |
from n have "p dvd p^n" by (intro dvd_power, auto) |
|
1766 |
also note pab |
|
1767 |
finally have pab': "p dvd a * b". |
|
1768 |
from nat_prime_dvd_mult[OF p pab'] |
|
1769 |
have "p dvd a \<or> p dvd b" . |
|
1770 |
moreover |
|
1771 |
{assume pa: "p dvd a" |
|
1772 |
have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute) |
|
1773 |
from nat_coprime_common_divisor [OF ab, OF pa] p have "\<not> p dvd b" by auto |
|
1774 |
with p have "coprime b p" |
|
1775 |
by (subst nat_gcd_commute, intro nat_prime_imp_coprime) |
|
1776 |
hence pnb: "coprime (p^n) b" |
|
1777 |
by (subst nat_gcd_commute, rule nat_coprime_exp) |
|
1778 |
from nat_coprime_divprod[OF pnba pnb] have ?thesis by blast } |
|
1779 |
moreover |
|
1780 |
{assume pb: "p dvd b" |
|
1781 |
have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute) |
|
1782 |
from nat_coprime_common_divisor [OF ab, of p] pb p have "\<not> p dvd a" |
|
1783 |
by auto |
|
1784 |
with p have "coprime a p" |
|
1785 |
by (subst nat_gcd_commute, intro nat_prime_imp_coprime) |
|
1786 |
hence pna: "coprime (p^n) a" |
|
1787 |
by (subst nat_gcd_commute, rule nat_coprime_exp) |
|
1788 |
from nat_coprime_divprod[OF pab pna] have ?thesis by blast } |
|
1789 |
ultimately have ?thesis by blast} |
|
1790 |
ultimately show ?thesis by blast |
|
23983 | 1791 |
qed |
1792 |
||
21256 | 1793 |
end |