author | nipkow |
Sun, 12 Jul 2009 14:48:01 +0200 | |
changeset 31995 | 8f37cf60b885 |
parent 31992 | f8aed98faae7 |
child 31996 | 1d93369079c4 |
permissions | -rw-r--r-- |
31706 | 1 |
(* Title: GCD.thy |
2 |
Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, |
|
31798 | 3 |
Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow |
31706 | 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 |
||
31798 | 23 |
Tobias Nipkow cleaned up a lot. |
21256 | 24 |
*) |
25 |
||
31706 | 26 |
|
27 |
header {* GCD *} |
|
21256 | 28 |
|
29 |
theory GCD |
|
31706 | 30 |
imports NatTransfer |
31 |
begin |
|
32 |
||
33 |
declare One_nat_def [simp del] |
|
34 |
||
35 |
subsection {* gcd *} |
|
36 |
||
31992 | 37 |
class gcd = zero + one + dvd + |
31706 | 38 |
|
39 |
fixes |
|
40 |
gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and |
|
41 |
lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
42 |
||
21256 | 43 |
begin |
44 |
||
31706 | 45 |
abbreviation |
46 |
coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
47 |
where |
|
48 |
"coprime x y == (gcd x y = 1)" |
|
49 |
||
50 |
end |
|
51 |
||
52 |
class prime = one + |
|
53 |
||
54 |
fixes |
|
55 |
prime :: "'a \<Rightarrow> bool" |
|
56 |
||
57 |
||
58 |
(* definitions for the natural numbers *) |
|
59 |
||
60 |
instantiation nat :: gcd |
|
61 |
||
62 |
begin |
|
21256 | 63 |
|
31706 | 64 |
fun |
65 |
gcd_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
66 |
where |
|
67 |
"gcd_nat x y = |
|
68 |
(if y = 0 then x else gcd y (x mod y))" |
|
69 |
||
70 |
definition |
|
71 |
lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
72 |
where |
|
73 |
"lcm_nat x y = x * y div (gcd x y)" |
|
74 |
||
75 |
instance proof qed |
|
76 |
||
77 |
end |
|
78 |
||
79 |
||
80 |
instantiation nat :: prime |
|
81 |
||
82 |
begin |
|
21256 | 83 |
|
21263 | 84 |
definition |
31706 | 85 |
prime_nat :: "nat \<Rightarrow> bool" |
86 |
where |
|
31709 | 87 |
[code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" |
31706 | 88 |
|
89 |
instance proof qed |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
90 |
|
31706 | 91 |
end |
92 |
||
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
93 |
|
31706 | 94 |
(* definitions for the integers *) |
95 |
||
96 |
instantiation int :: gcd |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
97 |
|
31706 | 98 |
begin |
21256 | 99 |
|
31706 | 100 |
definition |
101 |
gcd_int :: "int \<Rightarrow> int \<Rightarrow> int" |
|
102 |
where |
|
103 |
"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
|
104 |
|
31706 | 105 |
definition |
106 |
lcm_int :: "int \<Rightarrow> int \<Rightarrow> int" |
|
107 |
where |
|
108 |
"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
|
109 |
|
31706 | 110 |
instance proof qed |
111 |
||
112 |
end |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
113 |
|
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
114 |
|
31706 | 115 |
instantiation int :: prime |
116 |
||
117 |
begin |
|
118 |
||
119 |
definition |
|
120 |
prime_int :: "int \<Rightarrow> bool" |
|
121 |
where |
|
31709 | 122 |
[code del]: "prime_int p = prime (nat p)" |
31706 | 123 |
|
124 |
instance proof qed |
|
125 |
||
126 |
end |
|
127 |
||
128 |
||
129 |
subsection {* Set up Transfer *} |
|
130 |
||
131 |
||
132 |
lemma transfer_nat_int_gcd: |
|
133 |
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)" |
|
134 |
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)" |
|
135 |
"(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x" |
|
136 |
unfolding gcd_int_def lcm_int_def prime_int_def |
|
137 |
by auto |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
138 |
|
31706 | 139 |
lemma transfer_nat_int_gcd_closures: |
140 |
"x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0" |
|
141 |
"x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0" |
|
142 |
by (auto simp add: gcd_int_def lcm_int_def) |
|
143 |
||
144 |
declare TransferMorphism_nat_int[transfer add return: |
|
145 |
transfer_nat_int_gcd transfer_nat_int_gcd_closures] |
|
146 |
||
147 |
lemma transfer_int_nat_gcd: |
|
148 |
"gcd (int x) (int y) = int (gcd x y)" |
|
149 |
"lcm (int x) (int y) = int (lcm x y)" |
|
150 |
"prime (int x) = prime x" |
|
151 |
by (unfold gcd_int_def lcm_int_def prime_int_def, auto) |
|
152 |
||
153 |
lemma transfer_int_nat_gcd_closures: |
|
154 |
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0" |
|
155 |
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0" |
|
156 |
by (auto simp add: gcd_int_def lcm_int_def) |
|
157 |
||
158 |
declare TransferMorphism_int_nat[transfer add return: |
|
159 |
transfer_int_nat_gcd transfer_int_nat_gcd_closures] |
|
160 |
||
161 |
||
162 |
||
163 |
subsection {* GCD *} |
|
164 |
||
165 |
(* was gcd_induct *) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
166 |
lemma gcd_nat_induct: |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
167 |
fixes m n :: nat |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
168 |
assumes "\<And>m. P m 0" |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
169 |
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
|
170 |
shows "P m n" |
31706 | 171 |
apply (rule gcd_nat.induct) |
172 |
apply (case_tac "y = 0") |
|
173 |
using assms apply simp_all |
|
174 |
done |
|
175 |
||
176 |
(* specific to int *) |
|
177 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
178 |
lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y" |
31706 | 179 |
by (simp add: gcd_int_def) |
180 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
181 |
lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y" |
31706 | 182 |
by (simp add: gcd_int_def) |
183 |
||
31813 | 184 |
lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y" |
185 |
by(simp add: gcd_int_def) |
|
186 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
187 |
lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" |
31813 | 188 |
by (simp add: gcd_int_def) |
189 |
||
190 |
lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
191 |
by (metis abs_idempotent gcd_abs_int) |
31813 | 192 |
|
193 |
lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
194 |
by (metis abs_idempotent gcd_abs_int) |
31706 | 195 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
196 |
lemma gcd_cases_int: |
31706 | 197 |
fixes x :: int and y |
198 |
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" |
|
199 |
and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))" |
|
200 |
and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)" |
|
201 |
and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))" |
|
202 |
shows "P (gcd x y)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
203 |
by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith) |
21256 | 204 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
205 |
lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" |
31706 | 206 |
by (simp add: gcd_int_def) |
207 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
208 |
lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y" |
31706 | 209 |
by (simp add: lcm_int_def) |
210 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
211 |
lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y" |
31706 | 212 |
by (simp add: lcm_int_def) |
213 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
214 |
lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)" |
31706 | 215 |
by (simp add: lcm_int_def) |
21256 | 216 |
|
31814 | 217 |
lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j" |
218 |
by(simp add:lcm_int_def) |
|
219 |
||
220 |
lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y" |
|
221 |
by (metis abs_idempotent lcm_int_def) |
|
222 |
||
223 |
lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y" |
|
224 |
by (metis abs_idempotent lcm_int_def) |
|
225 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
226 |
lemma lcm_cases_int: |
31706 | 227 |
fixes x :: int and y |
228 |
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" |
|
229 |
and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))" |
|
230 |
and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)" |
|
231 |
and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))" |
|
232 |
shows "P (lcm x y)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
233 |
by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith) |
31706 | 234 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
235 |
lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0" |
31706 | 236 |
by (simp add: lcm_int_def) |
237 |
||
238 |
(* was gcd_0, etc. *) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
239 |
lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
240 |
by simp |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
241 |
|
31706 | 242 |
(* was igcd_0, etc. *) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
243 |
lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x" |
31706 | 244 |
by (unfold gcd_int_def, auto) |
245 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
246 |
lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
247 |
by simp |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
248 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
249 |
lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x" |
31706 | 250 |
by (unfold gcd_int_def, auto) |
251 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
252 |
lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)" |
31706 | 253 |
by (case_tac "y = 0", auto) |
254 |
||
255 |
(* weaker, but useful for the simplifier *) |
|
256 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
257 |
lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" |
31706 | 258 |
by simp |
259 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
260 |
lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1" |
21263 | 261 |
by simp |
21256 | 262 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
263 |
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" |
31706 | 264 |
by (simp add: One_nat_def) |
265 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
266 |
lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1" |
31706 | 267 |
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
|
268 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
269 |
lemma gcd_idem_nat: "gcd (x::nat) x = x" |
31798 | 270 |
by simp |
31706 | 271 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
272 |
lemma gcd_idem_int: "gcd (x::int) x = abs x" |
31813 | 273 |
by (auto simp add: gcd_int_def) |
31706 | 274 |
|
275 |
declare gcd_nat.simps [simp del] |
|
21256 | 276 |
|
277 |
text {* |
|
27556 | 278 |
\medskip @{term "gcd m n"} divides @{text m} and @{text n}. The |
21256 | 279 |
conjunctions don't seem provable separately. |
280 |
*} |
|
281 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
282 |
lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
283 |
and gcd_dvd2_nat [iff]: "(gcd m n) dvd n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
284 |
apply (induct m n rule: gcd_nat_induct) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
285 |
apply (simp_all add: gcd_non_0_nat) |
21256 | 286 |
apply (blast dest: dvd_mod_imp_dvd) |
31706 | 287 |
done |
288 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
289 |
lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
290 |
by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat) |
21256 | 291 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
292 |
lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
293 |
by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat) |
31706 | 294 |
|
31730 | 295 |
lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
296 |
by(metis gcd_dvd1_nat dvd_trans) |
31730 | 297 |
|
298 |
lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
299 |
by(metis gcd_dvd2_nat dvd_trans) |
31730 | 300 |
|
301 |
lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
302 |
by(metis gcd_dvd1_int dvd_trans) |
31730 | 303 |
|
304 |
lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
305 |
by(metis gcd_dvd2_int dvd_trans) |
31730 | 306 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
307 |
lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a" |
31706 | 308 |
by (rule dvd_imp_le, auto) |
309 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
310 |
lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b" |
31706 | 311 |
by (rule dvd_imp_le, auto) |
312 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
313 |
lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a" |
31706 | 314 |
by (rule zdvd_imp_le, auto) |
21256 | 315 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
316 |
lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b" |
31706 | 317 |
by (rule zdvd_imp_le, auto) |
318 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
319 |
lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
320 |
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod) |
31706 | 321 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
322 |
lemma gcd_greatest_int: |
31813 | 323 |
"(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
324 |
apply (subst gcd_abs_int) |
31706 | 325 |
apply (subst abs_dvd_iff [symmetric]) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
326 |
apply (rule gcd_greatest_nat [transferred]) |
31813 | 327 |
apply auto |
31706 | 328 |
done |
21256 | 329 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
330 |
lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) = |
31706 | 331 |
(k dvd m & k dvd n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
332 |
by (blast intro!: gcd_greatest_nat intro: dvd_trans) |
31706 | 333 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
334 |
lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
335 |
by (blast intro!: gcd_greatest_int intro: dvd_trans) |
21256 | 336 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
337 |
lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
338 |
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat) |
21256 | 339 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
340 |
lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" |
31706 | 341 |
by (auto simp add: gcd_int_def) |
21256 | 342 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
343 |
lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
344 |
by (insert gcd_zero_nat [of m n], arith) |
21256 | 345 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
346 |
lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
347 |
by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) |
31706 | 348 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
349 |
lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m" |
31706 | 350 |
by (rule dvd_anti_sym, auto) |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
351 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
352 |
lemma gcd_commute_int: "gcd (m::int) n = gcd n m" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
353 |
by (auto simp add: gcd_int_def gcd_commute_nat) |
31706 | 354 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
355 |
lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)" |
31706 | 356 |
apply (rule dvd_anti_sym) |
357 |
apply (blast intro: dvd_trans)+ |
|
358 |
done |
|
21256 | 359 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
360 |
lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
361 |
by (auto simp add: gcd_int_def gcd_assoc_nat) |
31706 | 362 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
363 |
lemmas gcd_left_commute_nat = |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
364 |
mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat] |
31706 | 365 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
366 |
lemmas gcd_left_commute_int = |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
367 |
mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int] |
31706 | 368 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
369 |
lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat |
31706 | 370 |
-- {* gcd is an AC-operator *} |
21256 | 371 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
372 |
lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int |
31706 | 373 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
374 |
lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and> |
31706 | 375 |
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" |
376 |
apply auto |
|
377 |
apply (rule dvd_anti_sym) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
378 |
apply (erule (1) gcd_greatest_nat) |
31706 | 379 |
apply auto |
380 |
done |
|
21256 | 381 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
382 |
lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and> |
31706 | 383 |
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" |
384 |
apply (case_tac "d = 0") |
|
385 |
apply force |
|
386 |
apply (rule iffI) |
|
387 |
apply (rule zdvd_anti_sym) |
|
388 |
apply arith |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
389 |
apply (subst gcd_pos_int) |
31706 | 390 |
apply clarsimp |
391 |
apply (drule_tac x = "d + 1" in spec) |
|
392 |
apply (frule zdvd_imp_le) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
393 |
apply (auto intro: gcd_greatest_int) |
31706 | 394 |
done |
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
30042
diff
changeset
|
395 |
|
31798 | 396 |
lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
397 |
by (metis dvd.eq_iff gcd_unique_nat) |
31798 | 398 |
|
399 |
lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
400 |
by (metis dvd.eq_iff gcd_unique_nat) |
31798 | 401 |
|
402 |
lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
403 |
by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int) |
31798 | 404 |
|
405 |
lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
406 |
by (metis gcd_proj1_if_dvd_int gcd_commute_int) |
31798 | 407 |
|
408 |
||
21256 | 409 |
text {* |
410 |
\medskip Multiplication laws |
|
411 |
*} |
|
412 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
413 |
lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)" |
21256 | 414 |
-- {* \cite[page 27]{davenport92} *} |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
415 |
apply (induct m n rule: gcd_nat_induct) |
31706 | 416 |
apply simp |
21256 | 417 |
apply (case_tac "k = 0") |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
418 |
apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2) |
31706 | 419 |
done |
21256 | 420 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
421 |
lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
422 |
apply (subst (1 2) gcd_abs_int) |
31813 | 423 |
apply (subst (1 2) abs_mult) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
424 |
apply (rule gcd_mult_distrib_nat [transferred]) |
31706 | 425 |
apply auto |
426 |
done |
|
21256 | 427 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
428 |
lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
429 |
apply (insert gcd_mult_distrib_nat [of m k n]) |
21256 | 430 |
apply simp |
431 |
apply (erule_tac t = m in ssubst) |
|
432 |
apply simp |
|
433 |
done |
|
434 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
435 |
lemma coprime_dvd_mult_int: |
31813 | 436 |
"coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m" |
437 |
apply (subst abs_dvd_iff [symmetric]) |
|
438 |
apply (subst dvd_abs_iff [symmetric]) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
439 |
apply (subst (asm) gcd_abs_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
440 |
apply (rule coprime_dvd_mult_nat [transferred]) |
31813 | 441 |
prefer 4 apply assumption |
442 |
apply auto |
|
443 |
apply (subst abs_mult [symmetric], auto) |
|
31706 | 444 |
done |
445 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
446 |
lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow> |
31706 | 447 |
(k dvd m * n) = (k dvd m)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
448 |
by (auto intro: coprime_dvd_mult_nat) |
31706 | 449 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
450 |
lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow> |
31706 | 451 |
(k dvd m * n) = (k dvd m)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
452 |
by (auto intro: coprime_dvd_mult_int) |
31706 | 453 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
454 |
lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n" |
21256 | 455 |
apply (rule dvd_anti_sym) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
456 |
apply (rule gcd_greatest_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
457 |
apply (rule_tac n = k in coprime_dvd_mult_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
458 |
apply (simp add: gcd_assoc_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
459 |
apply (simp add: gcd_commute_nat) |
31706 | 460 |
apply (simp_all add: mult_commute) |
461 |
done |
|
21256 | 462 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
463 |
lemma gcd_mult_cancel_int: |
31813 | 464 |
"coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
465 |
apply (subst (1 2) gcd_abs_int) |
31813 | 466 |
apply (subst abs_mult) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
467 |
apply (rule gcd_mult_cancel_nat [transferred], auto) |
31706 | 468 |
done |
21256 | 469 |
|
470 |
text {* \medskip Addition laws *} |
|
471 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
472 |
lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n" |
31706 | 473 |
apply (case_tac "n = 0") |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
474 |
apply (simp_all add: gcd_non_0_nat) |
31706 | 475 |
done |
476 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
477 |
lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
478 |
apply (subst (1 2) gcd_commute_nat) |
31706 | 479 |
apply (subst add_commute) |
480 |
apply simp |
|
481 |
done |
|
482 |
||
483 |
(* to do: add the other variations? *) |
|
484 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
485 |
lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
486 |
by (subst gcd_add1_nat [symmetric], auto) |
31706 | 487 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
488 |
lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
489 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
490 |
apply (subst gcd_diff1_nat [symmetric]) |
31706 | 491 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
492 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
493 |
apply (subst gcd_diff1_nat) |
31706 | 494 |
apply assumption |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
495 |
apply (rule gcd_commute_nat) |
31706 | 496 |
done |
497 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
498 |
lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)" |
31706 | 499 |
apply (frule_tac b = y and a = x in pos_mod_sign) |
500 |
apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
501 |
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] |
31706 | 502 |
zmod_zminus1_eq_if) |
503 |
apply (frule_tac a = x in pos_mod_bound) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
504 |
apply (subst (1 2) gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
505 |
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat |
31706 | 506 |
nat_le_eq_zle) |
507 |
done |
|
21256 | 508 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
509 |
lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)" |
31706 | 510 |
apply (case_tac "y = 0") |
511 |
apply force |
|
512 |
apply (case_tac "y > 0") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
513 |
apply (subst gcd_non_0_int, auto) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
514 |
apply (insert gcd_non_0_int [of "-y" "-x"]) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
515 |
apply (auto simp add: gcd_neg1_int gcd_neg2_int) |
31706 | 516 |
done |
517 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
518 |
lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
519 |
by (metis gcd_red_int mod_add_self1 zadd_commute) |
31706 | 520 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
521 |
lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
522 |
by (metis gcd_add1_int gcd_commute_int zadd_commute) |
21256 | 523 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
524 |
lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
525 |
by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) |
21256 | 526 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
527 |
lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
528 |
by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute) |
31798 | 529 |
|
21256 | 530 |
|
31706 | 531 |
(* to do: differences, and all variations of addition rules |
532 |
as simplification rules for nat and int *) |
|
533 |
||
31798 | 534 |
(* FIXME remove iff *) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
535 |
lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
536 |
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
|
537 |
|
31706 | 538 |
(* to do: add the three variations of these, and for ints? *) |
539 |
||
31992 | 540 |
lemma finite_divisors_nat[simp]: |
541 |
assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}" |
|
31734 | 542 |
proof- |
543 |
have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite) |
|
544 |
from finite_subset[OF _ this] show ?thesis using assms |
|
545 |
by(bestsimp intro!:dvd_imp_le) |
|
546 |
qed |
|
547 |
||
31995 | 548 |
lemma finite_divisors_int[simp]: |
31734 | 549 |
assumes "(i::int) ~= 0" shows "finite{d. d dvd i}" |
550 |
proof- |
|
551 |
have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if) |
|
552 |
hence "finite{d. abs d <= abs i}" by simp |
|
553 |
from finite_subset[OF _ this] show ?thesis using assms |
|
554 |
by(bestsimp intro!:dvd_imp_le_int) |
|
555 |
qed |
|
556 |
||
31995 | 557 |
lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n" |
558 |
apply(rule antisym) |
|
559 |
apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le) |
|
560 |
apply simp |
|
561 |
done |
|
562 |
||
563 |
lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n" |
|
564 |
apply(rule antisym) |
|
565 |
apply(rule Max_le_iff[THEN iffD2]) |
|
566 |
apply simp |
|
567 |
apply fastsimp |
|
568 |
apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans) |
|
569 |
apply simp |
|
570 |
done |
|
571 |
||
31734 | 572 |
lemma gcd_is_Max_divisors_nat: |
573 |
"m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})" |
|
574 |
apply(rule Max_eqI[THEN sym]) |
|
31995 | 575 |
apply (metis finite_Collect_conjI finite_divisors_nat) |
31734 | 576 |
apply simp |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
577 |
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat) |
31734 | 578 |
apply simp |
579 |
done |
|
580 |
||
581 |
lemma gcd_is_Max_divisors_int: |
|
582 |
"m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})" |
|
583 |
apply(rule Max_eqI[THEN sym]) |
|
31995 | 584 |
apply (metis finite_Collect_conjI finite_divisors_int) |
31734 | 585 |
apply simp |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
586 |
apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le) |
31734 | 587 |
apply simp |
588 |
done |
|
589 |
||
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
590 |
|
31706 | 591 |
subsection {* Coprimality *} |
592 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
593 |
lemma div_gcd_coprime_nat: |
31706 | 594 |
assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0" |
595 |
shows "coprime (a div gcd a b) (b div gcd a b)" |
|
22367 | 596 |
proof - |
27556 | 597 |
let ?g = "gcd a b" |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
598 |
let ?a' = "a div ?g" |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
599 |
let ?b' = "b div ?g" |
27556 | 600 |
let ?g' = "gcd ?a' ?b'" |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
601 |
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
|
602 |
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all |
22367 | 603 |
from dvdg dvdg' obtain ka kb ka' kb' where |
604 |
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
|
605 |
unfolding dvd_def by blast |
31706 | 606 |
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" |
607 |
by simp_all |
|
22367 | 608 |
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" |
609 |
by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] |
|
610 |
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
611 |
have "?g \<noteq> 0" using nz by (simp add: gcd_zero_nat) |
31706 | 612 |
then have gp: "?g > 0" by arith |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
613 |
from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" . |
22367 | 614 |
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
|
615 |
qed |
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
616 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
617 |
lemma div_gcd_coprime_int: |
31706 | 618 |
assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0" |
619 |
shows "coprime (a div gcd a b) (b div gcd a b)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
620 |
apply (subst (1 2 3) gcd_abs_int) |
31813 | 621 |
apply (subst (1 2) abs_div) |
622 |
apply simp |
|
623 |
apply simp |
|
624 |
apply(subst (1 2) abs_gcd_int) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
625 |
apply (rule div_gcd_coprime_nat [transferred]) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
626 |
using nz apply (auto simp add: gcd_abs_int [symmetric]) |
31706 | 627 |
done |
628 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
629 |
lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
630 |
using gcd_unique_nat[of 1 a b, simplified] by auto |
31706 | 631 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
632 |
lemma coprime_Suc_0_nat: |
31706 | 633 |
"coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
634 |
using coprime_nat by (simp add: One_nat_def) |
31706 | 635 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
636 |
lemma coprime_int: "coprime (a::int) b \<longleftrightarrow> |
31706 | 637 |
(\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
638 |
using gcd_unique_int [of 1 a b] |
31706 | 639 |
apply clarsimp |
640 |
apply (erule subst) |
|
641 |
apply (rule iffI) |
|
642 |
apply force |
|
643 |
apply (drule_tac x = "abs e" in exI) |
|
644 |
apply (case_tac "e >= 0") |
|
645 |
apply force |
|
646 |
apply force |
|
647 |
done |
|
648 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
649 |
lemma gcd_coprime_nat: |
31706 | 650 |
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and |
651 |
b: "b = b' * gcd a b" |
|
652 |
shows "coprime a' b'" |
|
653 |
||
654 |
apply (subgoal_tac "a' = a div gcd a b") |
|
655 |
apply (erule ssubst) |
|
656 |
apply (subgoal_tac "b' = b div gcd a b") |
|
657 |
apply (erule ssubst) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
658 |
apply (rule div_gcd_coprime_nat) |
31706 | 659 |
using prems |
660 |
apply force |
|
661 |
apply (subst (1) b) |
|
662 |
using z apply force |
|
663 |
apply (subst (1) a) |
|
664 |
using z apply force |
|
665 |
done |
|
666 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
667 |
lemma gcd_coprime_int: |
31706 | 668 |
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and |
669 |
b: "b = b' * gcd a b" |
|
670 |
shows "coprime a' b'" |
|
671 |
||
672 |
apply (subgoal_tac "a' = a div gcd a b") |
|
673 |
apply (erule ssubst) |
|
674 |
apply (subgoal_tac "b' = b div gcd a b") |
|
675 |
apply (erule ssubst) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
676 |
apply (rule div_gcd_coprime_int) |
31706 | 677 |
using prems |
678 |
apply force |
|
679 |
apply (subst (1) b) |
|
680 |
using z apply force |
|
681 |
apply (subst (1) a) |
|
682 |
using z apply force |
|
683 |
done |
|
684 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
685 |
lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b" |
31706 | 686 |
shows "coprime d (a * b)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
687 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
688 |
using da apply (subst gcd_mult_cancel_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
689 |
apply (subst gcd_commute_nat, assumption) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
690 |
apply (subst gcd_commute_nat, rule db) |
31706 | 691 |
done |
692 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
693 |
lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b" |
31706 | 694 |
shows "coprime d (a * b)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
695 |
apply (subst gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
696 |
using da apply (subst gcd_mult_cancel_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
697 |
apply (subst gcd_commute_int, assumption) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
698 |
apply (subst gcd_commute_int, rule db) |
31706 | 699 |
done |
700 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
701 |
lemma coprime_lmult_nat: |
31706 | 702 |
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" |
703 |
proof - |
|
704 |
have "gcd d a dvd gcd d (a * b)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
705 |
by (rule gcd_greatest_nat, auto) |
31706 | 706 |
with dab show ?thesis |
707 |
by auto |
|
708 |
qed |
|
709 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
710 |
lemma coprime_lmult_int: |
31798 | 711 |
assumes "coprime (d::int) (a * b)" shows "coprime d a" |
31706 | 712 |
proof - |
713 |
have "gcd d a dvd gcd d (a * b)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
714 |
by (rule gcd_greatest_int, auto) |
31798 | 715 |
with assms show ?thesis |
31706 | 716 |
by auto |
717 |
qed |
|
718 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
719 |
lemma coprime_rmult_nat: |
31798 | 720 |
assumes "coprime (d::nat) (a * b)" shows "coprime d b" |
31706 | 721 |
proof - |
722 |
have "gcd d b dvd gcd d (a * b)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
723 |
by (rule gcd_greatest_nat, auto intro: dvd_mult) |
31798 | 724 |
with assms show ?thesis |
31706 | 725 |
by auto |
726 |
qed |
|
727 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
728 |
lemma coprime_rmult_int: |
31706 | 729 |
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" |
730 |
proof - |
|
731 |
have "gcd d b dvd gcd d (a * b)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
732 |
by (rule gcd_greatest_int, auto intro: dvd_mult) |
31706 | 733 |
with dab show ?thesis |
734 |
by auto |
|
735 |
qed |
|
736 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
737 |
lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow> |
31706 | 738 |
coprime d a \<and> coprime d b" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
739 |
using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b] |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
740 |
coprime_mult_nat[of d a b] |
31706 | 741 |
by blast |
742 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
743 |
lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow> |
31706 | 744 |
coprime d a \<and> coprime d b" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
745 |
using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b] |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
746 |
coprime_mult_int[of d a b] |
31706 | 747 |
by blast |
748 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
749 |
lemma gcd_coprime_exists_nat: |
31706 | 750 |
assumes nz: "gcd (a::nat) b \<noteq> 0" |
751 |
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'" |
|
752 |
apply (rule_tac x = "a div gcd a b" in exI) |
|
753 |
apply (rule_tac x = "b div gcd a b" in exI) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
754 |
using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult) |
31706 | 755 |
done |
756 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
757 |
lemma gcd_coprime_exists_int: |
31706 | 758 |
assumes nz: "gcd (a::int) b \<noteq> 0" |
759 |
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'" |
|
760 |
apply (rule_tac x = "a div gcd a b" in exI) |
|
761 |
apply (rule_tac x = "b div gcd a b" in exI) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
762 |
using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self) |
31706 | 763 |
done |
764 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
765 |
lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
766 |
by (induct n, simp_all add: coprime_mult_nat) |
31706 | 767 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
768 |
lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
769 |
by (induct n, simp_all add: coprime_mult_int) |
31706 | 770 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
771 |
lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
772 |
apply (rule coprime_exp_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
773 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
774 |
apply (rule coprime_exp_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
775 |
apply (subst gcd_commute_nat, assumption) |
31706 | 776 |
done |
777 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
778 |
lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
779 |
apply (rule coprime_exp_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
780 |
apply (subst gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
781 |
apply (rule coprime_exp_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
782 |
apply (subst gcd_commute_int, assumption) |
31706 | 783 |
done |
784 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
785 |
lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" |
31706 | 786 |
proof (cases) |
787 |
assume "a = 0 & b = 0" |
|
788 |
thus ?thesis by simp |
|
789 |
next assume "~(a = 0 & b = 0)" |
|
790 |
hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
791 |
by (auto simp:div_gcd_coprime_nat) |
31706 | 792 |
hence "gcd ((a div gcd a b)^n * (gcd a b)^n) |
793 |
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" |
|
794 |
apply (subst (1 2) mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
795 |
apply (subst gcd_mult_distrib_nat [symmetric]) |
31706 | 796 |
apply simp |
797 |
done |
|
798 |
also have "(a div gcd a b)^n * (gcd a b)^n = a^n" |
|
799 |
apply (subst div_power) |
|
800 |
apply auto |
|
801 |
apply (rule dvd_div_mult_self) |
|
802 |
apply (rule dvd_power_same) |
|
803 |
apply auto |
|
804 |
done |
|
805 |
also have "(b div gcd a b)^n * (gcd a b)^n = b^n" |
|
806 |
apply (subst div_power) |
|
807 |
apply auto |
|
808 |
apply (rule dvd_div_mult_self) |
|
809 |
apply (rule dvd_power_same) |
|
810 |
apply auto |
|
811 |
done |
|
812 |
finally show ?thesis . |
|
813 |
qed |
|
814 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
815 |
lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
816 |
apply (subst (1 2) gcd_abs_int) |
31706 | 817 |
apply (subst (1 2) power_abs) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
818 |
apply (rule gcd_exp_nat [where n = n, transferred]) |
31706 | 819 |
apply auto |
820 |
done |
|
821 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
822 |
lemma coprime_divprod_nat: "(d::nat) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
823 |
using coprime_dvd_mult_iff_nat[of d a b] |
31706 | 824 |
by (auto simp add: mult_commute) |
825 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
826 |
lemma coprime_divprod_int: "(d::int) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
827 |
using coprime_dvd_mult_iff_int[of d a b] |
31706 | 828 |
by (auto simp add: mult_commute) |
829 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
830 |
lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c" |
31706 | 831 |
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" |
832 |
proof- |
|
833 |
let ?g = "gcd a b" |
|
834 |
{assume "?g = 0" with dc have ?thesis by auto} |
|
835 |
moreover |
|
836 |
{assume z: "?g \<noteq> 0" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
837 |
from gcd_coprime_exists_nat[OF z] |
31706 | 838 |
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" |
839 |
by blast |
|
840 |
have thb: "?g dvd b" by auto |
|
841 |
from ab'(1) have "a' dvd a" unfolding dvd_def by blast |
|
842 |
with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp |
|
843 |
from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto |
|
844 |
hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc) |
|
845 |
with z have th_1: "a' dvd b' * c" by auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
846 |
from coprime_dvd_mult_nat[OF ab'(3)] th_1 |
31706 | 847 |
have thc: "a' dvd c" by (subst (asm) mult_commute, blast) |
848 |
from ab' have "a = ?g*a'" by algebra |
|
849 |
with thb thc have ?thesis by blast } |
|
850 |
ultimately show ?thesis by blast |
|
851 |
qed |
|
852 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
853 |
lemma division_decomp_int: assumes dc: "(a::int) dvd b * c" |
31706 | 854 |
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" |
855 |
proof- |
|
856 |
let ?g = "gcd a b" |
|
857 |
{assume "?g = 0" with dc have ?thesis by auto} |
|
858 |
moreover |
|
859 |
{assume z: "?g \<noteq> 0" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
860 |
from gcd_coprime_exists_int[OF z] |
31706 | 861 |
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" |
862 |
by blast |
|
863 |
have thb: "?g dvd b" by auto |
|
864 |
from ab'(1) have "a' dvd a" unfolding dvd_def by blast |
|
865 |
with dc have th0: "a' dvd b*c" |
|
866 |
using dvd_trans[of a' a "b*c"] by simp |
|
867 |
from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto |
|
868 |
hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc) |
|
869 |
with z have th_1: "a' dvd b' * c" by auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
870 |
from coprime_dvd_mult_int[OF ab'(3)] th_1 |
31706 | 871 |
have thc: "a' dvd c" by (subst (asm) mult_commute, blast) |
872 |
from ab' have "a = ?g*a'" by algebra |
|
873 |
with thb thc have ?thesis by blast } |
|
874 |
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
|
875 |
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
|
876 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
877 |
lemma pow_divides_pow_nat: |
31706 | 878 |
assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" |
879 |
shows "a dvd b" |
|
880 |
proof- |
|
881 |
let ?g = "gcd a b" |
|
882 |
from n obtain m where m: "n = Suc m" by (cases n, simp_all) |
|
883 |
{assume "?g = 0" with ab n have ?thesis by auto } |
|
884 |
moreover |
|
885 |
{assume z: "?g \<noteq> 0" |
|
886 |
hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
887 |
from gcd_coprime_exists_nat[OF z] |
31706 | 888 |
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" |
889 |
by blast |
|
890 |
from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" |
|
891 |
by (simp add: ab'(1,2)[symmetric]) |
|
892 |
hence "?g^n*a'^n dvd ?g^n *b'^n" |
|
893 |
by (simp only: power_mult_distrib mult_commute) |
|
894 |
with zn z n have th0:"a'^n dvd b'^n" by auto |
|
895 |
have "a' dvd a'^n" by (simp add: m) |
|
896 |
with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp |
|
897 |
hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
898 |
from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1 |
31706 | 899 |
have "a' dvd b'" by (subst (asm) mult_commute, blast) |
900 |
hence "a'*?g dvd b'*?g" by simp |
|
901 |
with ab'(1,2) have ?thesis by simp } |
|
902 |
ultimately show ?thesis by blast |
|
903 |
qed |
|
904 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
905 |
lemma pow_divides_pow_int: |
31706 | 906 |
assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0" |
907 |
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
|
908 |
proof- |
31706 | 909 |
let ?g = "gcd a b" |
910 |
from n obtain m where m: "n = Suc m" by (cases n, simp_all) |
|
911 |
{assume "?g = 0" with ab n have ?thesis by auto } |
|
912 |
moreover |
|
913 |
{assume z: "?g \<noteq> 0" |
|
914 |
hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
915 |
from gcd_coprime_exists_int[OF z] |
31706 | 916 |
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" |
917 |
by blast |
|
918 |
from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" |
|
919 |
by (simp add: ab'(1,2)[symmetric]) |
|
920 |
hence "?g^n*a'^n dvd ?g^n *b'^n" |
|
921 |
by (simp only: power_mult_distrib mult_commute) |
|
922 |
with zn z n have th0:"a'^n dvd b'^n" by auto |
|
923 |
have "a' dvd a'^n" by (simp add: m) |
|
924 |
with th0 have "a' dvd b'^n" |
|
925 |
using dvd_trans[of a' "a'^n" "b'^n"] by simp |
|
926 |
hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
927 |
from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1 |
31706 | 928 |
have "a' dvd b'" by (subst (asm) mult_commute, blast) |
929 |
hence "a'*?g dvd b'*?g" by simp |
|
930 |
with ab'(1,2) have ?thesis by simp } |
|
931 |
ultimately show ?thesis by blast |
|
932 |
qed |
|
933 |
||
31798 | 934 |
(* FIXME move to Divides(?) *) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
935 |
lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
936 |
by (auto intro: pow_divides_pow_nat dvd_power_same) |
31706 | 937 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
938 |
lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
939 |
by (auto intro: pow_divides_pow_int dvd_power_same) |
31706 | 940 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
941 |
lemma divides_mult_nat: |
31706 | 942 |
assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n" |
943 |
shows "m * n dvd r" |
|
944 |
proof- |
|
945 |
from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'" |
|
946 |
unfolding dvd_def by blast |
|
947 |
from mr n' have "m dvd n'*n" by (simp add: mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
948 |
hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp |
31706 | 949 |
then obtain k where k: "n' = m*k" unfolding dvd_def by blast |
950 |
from n' k show ?thesis unfolding dvd_def by auto |
|
951 |
qed |
|
952 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
953 |
lemma divides_mult_int: |
31706 | 954 |
assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n" |
955 |
shows "m * n dvd r" |
|
956 |
proof- |
|
957 |
from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'" |
|
958 |
unfolding dvd_def by blast |
|
959 |
from mr n' have "m dvd n'*n" by (simp add: mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
960 |
hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp |
31706 | 961 |
then obtain k where k: "n' = m*k" unfolding dvd_def by blast |
962 |
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
|
963 |
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
|
964 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
965 |
lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n" |
31706 | 966 |
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)") |
967 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
968 |
apply (rule dvd_diff_nat) |
31706 | 969 |
apply auto |
970 |
done |
|
971 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
972 |
lemma coprime_Suc_nat [simp]: "coprime (Suc n) n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
973 |
using coprime_plus_one_nat by (simp add: One_nat_def) |
31706 | 974 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
975 |
lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n" |
31706 | 976 |
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)") |
977 |
apply force |
|
978 |
apply (rule dvd_diff) |
|
979 |
apply auto |
|
980 |
done |
|
981 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
982 |
lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
983 |
using coprime_plus_one_nat [of "n - 1"] |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
984 |
gcd_commute_nat [of "n - 1" n] by auto |
31706 | 985 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
986 |
lemma coprime_minus_one_int: "coprime ((n::int) - 1) n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
987 |
using coprime_plus_one_int [of "n - 1"] |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
988 |
gcd_commute_int [of "n - 1" n] by auto |
31706 | 989 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
990 |
lemma setprod_coprime_nat [rule_format]: |
31706 | 991 |
"(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x" |
992 |
apply (case_tac "finite A") |
|
993 |
apply (induct set: finite) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
994 |
apply (auto simp add: gcd_mult_cancel_nat) |
31706 | 995 |
done |
996 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
997 |
lemma setprod_coprime_int [rule_format]: |
31706 | 998 |
"(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x" |
999 |
apply (case_tac "finite A") |
|
1000 |
apply (induct set: finite) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1001 |
apply (auto simp add: gcd_mult_cancel_int) |
31706 | 1002 |
done |
1003 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1004 |
lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" |
31706 | 1005 |
unfolding prime_nat_def |
1006 |
apply (subst even_mult_two_ex) |
|
1007 |
apply clarify |
|
1008 |
apply (drule_tac x = 2 in spec) |
|
1009 |
apply auto |
|
1010 |
done |
|
1011 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1012 |
lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" |
31706 | 1013 |
unfolding prime_int_def |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1014 |
apply (frule prime_odd_nat) |
31706 | 1015 |
apply (auto simp add: even_nat_def) |
1016 |
done |
|
1017 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1018 |
lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> |
31706 | 1019 |
x dvd b \<Longrightarrow> x = 1" |
1020 |
apply (subgoal_tac "x dvd gcd a b") |
|
1021 |
apply simp |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1022 |
apply (erule (1) gcd_greatest_nat) |
31706 | 1023 |
done |
1024 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1025 |
lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> |
31706 | 1026 |
x dvd b \<Longrightarrow> abs x = 1" |
1027 |
apply (subgoal_tac "x dvd gcd a b") |
|
1028 |
apply simp |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1029 |
apply (erule (1) gcd_greatest_int) |
31706 | 1030 |
done |
1031 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1032 |
lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> |
31706 | 1033 |
coprime d e" |
1034 |
apply (auto simp add: dvd_def) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1035 |
apply (frule coprime_lmult_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1036 |
apply (subst gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1037 |
apply (subst (asm) (2) gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1038 |
apply (erule coprime_lmult_int) |
31706 | 1039 |
done |
1040 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1041 |
lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1042 |
apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat) |
31706 | 1043 |
done |
1044 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1045 |
lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1046 |
apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int) |
31706 | 1047 |
done |
1048 |
||
1049 |
||
1050 |
subsection {* Bezout's theorem *} |
|
1051 |
||
1052 |
(* Function bezw returns a pair of witnesses to Bezout's theorem -- |
|
1053 |
see the theorems that follow the definition. *) |
|
1054 |
fun |
|
1055 |
bezw :: "nat \<Rightarrow> nat \<Rightarrow> int * int" |
|
1056 |
where |
|
1057 |
"bezw x y = |
|
1058 |
(if y = 0 then (1, 0) else |
|
1059 |
(snd (bezw y (x mod y)), |
|
1060 |
fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))" |
|
1061 |
||
1062 |
lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp |
|
1063 |
||
1064 |
lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)), |
|
1065 |
fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))" |
|
1066 |
by simp |
|
1067 |
||
1068 |
declare bezw.simps [simp del] |
|
1069 |
||
1070 |
lemma bezw_aux [rule_format]: |
|
1071 |
"fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1072 |
proof (induct x y rule: gcd_nat_induct) |
31706 | 1073 |
fix m :: nat |
1074 |
show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)" |
|
1075 |
by auto |
|
1076 |
next fix m :: nat and n |
|
1077 |
assume ngt0: "n > 0" and |
|
1078 |
ih: "fst (bezw n (m mod n)) * int n + |
|
1079 |
snd (bezw n (m mod n)) * int (m mod n) = |
|
1080 |
int (gcd n (m mod n))" |
|
1081 |
thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1082 |
apply (simp add: bezw_non_0 gcd_non_0_nat) |
31706 | 1083 |
apply (erule subst) |
1084 |
apply (simp add: ring_simps) |
|
1085 |
apply (subst mod_div_equality [of m n, symmetric]) |
|
1086 |
(* applying simp here undoes the last substitution! |
|
1087 |
what is procedure cancel_div_mod? *) |
|
1088 |
apply (simp only: ring_simps zadd_int [symmetric] |
|
1089 |
zmult_int [symmetric]) |
|
1090 |
done |
|
1091 |
qed |
|
1092 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1093 |
lemma bezout_int: |
31706 | 1094 |
fixes x y |
1095 |
shows "EX u v. u * (x::int) + v * y = gcd x y" |
|
1096 |
proof - |
|
1097 |
have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow> |
|
1098 |
EX u v. u * x + v * y = gcd x y" |
|
1099 |
apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI) |
|
1100 |
apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI) |
|
1101 |
apply (unfold gcd_int_def) |
|
1102 |
apply simp |
|
1103 |
apply (subst bezw_aux [symmetric]) |
|
1104 |
apply auto |
|
1105 |
done |
|
1106 |
have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) | |
|
1107 |
(x \<le> 0 \<and> y \<le> 0)" |
|
1108 |
by auto |
|
1109 |
moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis" |
|
1110 |
by (erule (1) bezout_aux) |
|
1111 |
moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis" |
|
1112 |
apply (insert bezout_aux [of x "-y"]) |
|
1113 |
apply auto |
|
1114 |
apply (rule_tac x = u in exI) |
|
1115 |
apply (rule_tac x = "-v" in exI) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1116 |
apply (subst gcd_neg2_int [symmetric]) |
31706 | 1117 |
apply auto |
1118 |
done |
|
1119 |
moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis" |
|
1120 |
apply (insert bezout_aux [of "-x" y]) |
|
1121 |
apply auto |
|
1122 |
apply (rule_tac x = "-u" in exI) |
|
1123 |
apply (rule_tac x = v in exI) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1124 |
apply (subst gcd_neg1_int [symmetric]) |
31706 | 1125 |
apply auto |
1126 |
done |
|
1127 |
moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis" |
|
1128 |
apply (insert bezout_aux [of "-x" "-y"]) |
|
1129 |
apply auto |
|
1130 |
apply (rule_tac x = "-u" in exI) |
|
1131 |
apply (rule_tac x = "-v" in exI) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1132 |
apply (subst gcd_neg1_int [symmetric]) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1133 |
apply (subst gcd_neg2_int [symmetric]) |
31706 | 1134 |
apply auto |
1135 |
done |
|
1136 |
ultimately show ?thesis by blast |
|
1137 |
qed |
|
1138 |
||
1139 |
text {* versions of Bezout for nat, by Amine Chaieb *} |
|
1140 |
||
1141 |
lemma ind_euclid: |
|
1142 |
assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" |
|
1143 |
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
|
1144 |
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
|
1145 |
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
|
1146 |
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
|
1147 |
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
|
1148 |
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
|
1149 |
moreover {assume eq: "a= b" |
31706 | 1150 |
from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq |
1151 |
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
|
1152 |
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
|
1153 |
{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
|
1154 |
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
|
1155 |
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
|
1156 |
{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
|
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 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
|
1159 |
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
|
1160 |
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
|
1161 |
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
|
1162 |
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
|
1163 |
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
|
1164 |
{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
|
1165 |
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
|
1166 |
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
|
1167 |
{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
|
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 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
|
1170 |
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
|
1171 |
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
|
1172 |
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
|
1173 |
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
|
1174 |
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
|
1175 |
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
|
1176 |
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
|
1177 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1178 |
lemma bezout_lemma_nat: |
31706 | 1179 |
assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> |
1180 |
(a * x = b * y + d \<or> b * x = a * y + d)" |
|
1181 |
shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and> |
|
1182 |
(a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)" |
|
1183 |
using ex |
|
1184 |
apply clarsimp |
|
1185 |
apply (rule_tac x="d" in exI, simp add: dvd_add) |
|
1186 |
apply (case_tac "a * x = b * y + d" , simp_all) |
|
1187 |
apply (rule_tac x="x + y" in exI) |
|
1188 |
apply (rule_tac x="y" in exI) |
|
1189 |
apply algebra |
|
1190 |
apply (rule_tac x="x" in exI) |
|
1191 |
apply (rule_tac x="x + y" in exI) |
|
1192 |
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
|
1193 |
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
|
1194 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1195 |
lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> |
31706 | 1196 |
(a * x = b * y + d \<or> b * x = a * y + d)" |
1197 |
apply(induct a b rule: ind_euclid) |
|
1198 |
apply blast |
|
1199 |
apply clarify |
|
1200 |
apply (rule_tac x="a" in exI, simp add: dvd_add) |
|
1201 |
apply clarsimp |
|
1202 |
apply (rule_tac x="d" in exI) |
|
1203 |
apply (case_tac "a * x = b * y + d", simp_all add: dvd_add) |
|
1204 |
apply (rule_tac x="x+y" in exI) |
|
1205 |
apply (rule_tac x="y" in exI) |
|
1206 |
apply algebra |
|
1207 |
apply (rule_tac x="x" in exI) |
|
1208 |
apply (rule_tac x="x+y" in exI) |
|
1209 |
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
|
1210 |
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
|
1211 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1212 |
lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> |
31706 | 1213 |
(a * x - b * y = d \<or> b * x - a * y = d)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1214 |
using bezout_add_nat[of a b] |
31706 | 1215 |
apply clarsimp |
1216 |
apply (rule_tac x="d" in exI, simp) |
|
1217 |
apply (rule_tac x="x" in exI) |
|
1218 |
apply (rule_tac x="y" in exI) |
|
1219 |
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
|
1220 |
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
|
1221 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1222 |
lemma bezout_add_strong_nat: 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
|
1223 |
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
|
1224 |
proof- |
31706 | 1225 |
from nz have ap: "a > 0" by simp |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1226 |
from bezout_add_nat[of a b] |
31706 | 1227 |
have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or> |
1228 |
(\<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
|
1229 |
moreover |
31706 | 1230 |
{fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d" |
1231 |
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
|
1232 |
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
|
1233 |
{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
|
1234 |
{assume b0: "b = 0" with H have ?thesis by simp} |
31706 | 1235 |
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
|
1236 |
{assume b: "b \<noteq> 0" hence bp: "b > 0" by simp |
31706 | 1237 |
from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b" |
1238 |
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
|
1239 |
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
|
1240 |
{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
|
1241 |
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
|
1242 |
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
|
1243 |
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
|
1244 |
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
|
1245 |
moreover |
31706 | 1246 |
{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
|
1247 |
{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
|
1248 |
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
|
1249 |
{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
|
1250 |
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
|
1251 |
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
|
1252 |
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
|
1253 |
have dble: "d*b \<le> x*b*(b - 1)" using bp by simp |
31706 | 1254 |
from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)" |
1255 |
by simp |
|
1256 |
hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x" |
|
1257 |
by (simp only: mult_assoc right_distrib) |
|
1258 |
hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" |
|
1259 |
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
|
1260 |
hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp |
31706 | 1261 |
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
|
1262 |
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
|
1263 |
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
|
1264 |
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
|
1265 |
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
|
1266 |
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
|
1267 |
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
|
1268 |
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
|
1269 |
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
|
1270 |
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
|
1271 |
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
|
1272 |
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
|
1273 |
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
|
1274 |
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
|
1275 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1276 |
lemma bezout_nat: 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
|
1277 |
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
|
1278 |
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
|
1279 |
let ?g = "gcd a b" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1280 |
from bezout_add_strong_nat[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
|
1281 |
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
|
1282 |
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
|
1283 |
then obtain k where k: "?g = d*k" unfolding dvd_def by blast |
31706 | 1284 |
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
|
1285 |
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
|
1286 |
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
|
1287 |
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
|
1288 |
|
31706 | 1289 |
|
1290 |
subsection {* LCM *} |
|
1291 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1292 |
lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b" |
31706 | 1293 |
by (simp add: lcm_int_def lcm_nat_def zdiv_int |
1294 |
zmult_int [symmetric] gcd_int_def) |
|
1295 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1296 |
lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n" |
31706 | 1297 |
unfolding lcm_nat_def |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1298 |
by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat]) |
31706 | 1299 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1300 |
lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n" |
31706 | 1301 |
unfolding lcm_int_def gcd_int_def |
1302 |
apply (subst int_mult [symmetric]) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1303 |
apply (subst prod_gcd_lcm_nat [symmetric]) |
31706 | 1304 |
apply (subst nat_abs_mult_distrib [symmetric]) |
1305 |
apply (simp, simp add: abs_mult) |
|
1306 |
done |
|
1307 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1308 |
lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0" |
31706 | 1309 |
unfolding lcm_nat_def by simp |
1310 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1311 |
lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0" |
31706 | 1312 |
unfolding lcm_int_def by simp |
1313 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1314 |
lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0" |
31706 | 1315 |
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
|
1316 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1317 |
lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0" |
31706 | 1318 |
unfolding lcm_int_def by simp |
1319 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1320 |
lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1321 |
unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps) |
31706 | 1322 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1323 |
lemma lcm_commute_int: "lcm (m::int) n = lcm n m" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1324 |
unfolding lcm_int_def by (subst lcm_commute_nat, rule refl) |
31706 | 1325 |
|
1326 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1327 |
lemma lcm_pos_nat: |
31798 | 1328 |
"(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1329 |
by (metis gr0I mult_is_0 prod_gcd_lcm_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
|
1330 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1331 |
lemma lcm_pos_int: |
31798 | 1332 |
"(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1333 |
apply (subst lcm_abs_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1334 |
apply (rule lcm_pos_nat [transferred]) |
31798 | 1335 |
apply auto |
31706 | 1336 |
done |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1337 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1338 |
lemma dvd_pos_nat: |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1339 |
fixes n m :: nat |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1340 |
assumes "n > 0" and "m dvd n" |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1341 |
shows "m > 0" |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1342 |
using assms by (cases m) auto |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1343 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1344 |
lemma lcm_least_nat: |
31706 | 1345 |
assumes "(m::nat) dvd k" and "n dvd k" |
27556 | 1346 |
shows "lcm m n dvd k" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1347 |
proof (cases k) |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1348 |
case 0 then show ?thesis by auto |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1349 |
next |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1350 |
case (Suc _) then have pos_k: "k > 0" by auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1351 |
from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1352 |
with gcd_zero_nat [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
|
1353 |
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
|
1354 |
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
|
1355 |
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
|
1356 |
from pos_k k_n have pos_q: "q > 0" by auto |
27556 | 1357 |
have "k * k * gcd q p = k * gcd (k * q) (k * p)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1358 |
by (simp add: mult_ac gcd_mult_distrib_nat) |
27556 | 1359 |
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
|
1360 |
by (simp add: k_m [symmetric] k_n [symmetric]) |
27556 | 1361 |
also have "\<dots> = k * p * q * gcd m n" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1362 |
by (simp add: mult_ac gcd_mult_distrib_nat) |
27556 | 1363 |
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
|
1364 |
by (simp only: k_m [symmetric] k_n [symmetric]) |
27556 | 1365 |
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
|
1366 |
by (simp add: mult_ac) |
27556 | 1367 |
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
|
1368 |
by simp |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1369 |
with prod_gcd_lcm_nat [of m n] |
27556 | 1370 |
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
|
1371 |
by (simp add: mult_ac) |
31706 | 1372 |
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
|
1373 |
then show ?thesis using dvd_def by auto |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1374 |
qed |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1375 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1376 |
lemma lcm_least_int: |
31798 | 1377 |
"(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1378 |
apply (subst lcm_abs_int) |
31798 | 1379 |
apply (rule dvd_trans) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1380 |
apply (rule lcm_least_nat [transferred, of _ "abs k" _]) |
31798 | 1381 |
apply auto |
31706 | 1382 |
done |
1383 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1384 |
lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n" |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1385 |
proof (cases m) |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1386 |
case 0 then show ?thesis by simp |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1387 |
next |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1388 |
case (Suc _) |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1389 |
then have mpos: "m > 0" by simp |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1390 |
show ?thesis |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1391 |
proof (cases n) |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1392 |
case 0 then show ?thesis by simp |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1393 |
next |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1394 |
case (Suc _) |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1395 |
then have npos: "n > 0" by simp |
27556 | 1396 |
have "gcd m n dvd n" by simp |
1397 |
then obtain k where "n = gcd m n * k" using dvd_def by auto |
|
31706 | 1398 |
then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" |
1399 |
by (simp add: mult_ac) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1400 |
also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp |
31706 | 1401 |
finally show ?thesis by (simp add: lcm_nat_def) |
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1402 |
qed |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1403 |
qed |
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1404 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1405 |
lemma lcm_dvd1_int: "(m::int) dvd lcm m n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1406 |
apply (subst lcm_abs_int) |
31706 | 1407 |
apply (rule dvd_trans) |
1408 |
prefer 2 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1409 |
apply (rule lcm_dvd1_nat [transferred]) |
31706 | 1410 |
apply auto |
1411 |
done |
|
1412 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1413 |
lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1414 |
by (subst lcm_commute_nat, rule lcm_dvd1_nat) |
31706 | 1415 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1416 |
lemma lcm_dvd2_int: "(n::int) dvd lcm m n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1417 |
by (subst lcm_commute_int, rule lcm_dvd1_int) |
31706 | 1418 |
|
31730 | 1419 |
lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1420 |
by(metis lcm_dvd1_nat dvd_trans) |
31729 | 1421 |
|
31730 | 1422 |
lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1423 |
by(metis lcm_dvd2_nat dvd_trans) |
31729 | 1424 |
|
31730 | 1425 |
lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1426 |
by(metis lcm_dvd1_int dvd_trans) |
31729 | 1427 |
|
31730 | 1428 |
lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1429 |
by(metis lcm_dvd2_int dvd_trans) |
31729 | 1430 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1431 |
lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and> |
31706 | 1432 |
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1433 |
by (auto intro: dvd_anti_sym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1434 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1435 |
lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and> |
31706 | 1436 |
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1437 |
by (auto intro: dvd_anti_sym [transferred] lcm_least_int) |
31706 | 1438 |
|
31798 | 1439 |
lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y" |
31706 | 1440 |
apply (rule sym) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1441 |
apply (subst lcm_unique_nat [symmetric]) |
31706 | 1442 |
apply auto |
1443 |
done |
|
1444 |
||
31798 | 1445 |
lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y" |
31706 | 1446 |
apply (rule sym) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1447 |
apply (subst lcm_unique_int [symmetric]) |
31706 | 1448 |
apply auto |
1449 |
done |
|
1450 |
||
31798 | 1451 |
lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1452 |
by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat) |
31706 | 1453 |
|
31798 | 1454 |
lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1455 |
by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int) |
31706 | 1456 |
|
31992 | 1457 |
lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m" |
1458 |
by (metis lcm_proj1_if_dvd_nat lcm_unique_nat) |
|
1459 |
||
1460 |
lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n" |
|
1461 |
by (metis lcm_proj2_if_dvd_nat lcm_unique_nat) |
|
1462 |
||
1463 |
lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m" |
|
1464 |
by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int) |
|
1465 |
||
1466 |
lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n" |
|
1467 |
by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int) |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1468 |
|
31766 | 1469 |
lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)" |
31992 | 1470 |
by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat) |
31766 | 1471 |
|
1472 |
lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)" |
|
31992 | 1473 |
by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int) |
31766 | 1474 |
|
31992 | 1475 |
lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat] |
1476 |
lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int] |
|
31766 | 1477 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1478 |
lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1479 |
lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int |
31766 | 1480 |
|
31992 | 1481 |
lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)" |
1482 |
proof qed (auto simp add: gcd_ac_nat) |
|
1483 |
||
1484 |
lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)" |
|
1485 |
proof qed (auto simp add: gcd_ac_int) |
|
1486 |
||
1487 |
lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)" |
|
1488 |
proof qed (auto simp add: lcm_ac_nat) |
|
1489 |
||
1490 |
lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)" |
|
1491 |
proof qed (auto simp add: lcm_ac_int) |
|
1492 |
||
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
1493 |
|
31995 | 1494 |
(* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *) |
1495 |
||
1496 |
lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0" |
|
1497 |
by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat) |
|
1498 |
||
1499 |
lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0" |
|
1500 |
by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le) |
|
1501 |
||
1502 |
lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1" |
|
1503 |
by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat) |
|
1504 |
||
1505 |
lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)" |
|
1506 |
by (metis abs_minus_one abs_mult_self lcm_proj1_if_dvd_int lcm_unique_int one_dvd zmult_eq_1_iff) |
|
1507 |
||
1508 |
||
31706 | 1509 |
subsection {* Primes *} |
22367 | 1510 |
|
31992 | 1511 |
(* FIXME Is there a better way to handle these, rather than making them elim rules? *) |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
1512 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1513 |
lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0" |
31706 | 1514 |
by (unfold prime_nat_def, auto) |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
1515 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1516 |
lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0" |
31706 | 1517 |
by (unfold prime_nat_def, auto) |
22367 | 1518 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1519 |
lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1" |
31706 | 1520 |
by (unfold prime_nat_def, auto) |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
1521 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1522 |
lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1" |
31706 | 1523 |
by (unfold prime_nat_def, auto) |
22367 | 1524 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1525 |
lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0" |
31706 | 1526 |
by (unfold prime_nat_def, auto) |
22367 | 1527 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1528 |
lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0" |
31706 | 1529 |
by (unfold prime_nat_def, auto) |
1530 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1531 |
lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2" |
31706 | 1532 |
by (unfold prime_nat_def, auto) |
1533 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1534 |
lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0" |
31992 | 1535 |
by (unfold prime_int_def prime_nat_def) auto |
22367 | 1536 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1537 |
lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0" |
31706 | 1538 |
by (unfold prime_int_def prime_nat_def, auto) |
1539 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1540 |
lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1" |
31706 | 1541 |
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
|
1542 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1543 |
lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1" |
31706 | 1544 |
by (unfold prime_int_def prime_nat_def, auto) |
1545 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1546 |
lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2" |
31706 | 1547 |
by (unfold prime_int_def prime_nat_def, auto) |
22367 | 1548 |
|
31706 | 1549 |
|
1550 |
lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow> |
|
1551 |
m = 1 \<or> m = p))" |
|
1552 |
using prime_nat_def [transferred] |
|
1553 |
apply (case_tac "p >= 0") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1554 |
by (blast, auto simp add: prime_ge_0_int) |
31706 | 1555 |
|
1556 |
(* To do: determine primality of any numeral *) |
|
1557 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1558 |
lemma zero_not_prime_nat [simp]: "~prime (0::nat)" |
31706 | 1559 |
by (simp add: prime_nat_def) |
1560 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1561 |
lemma zero_not_prime_int [simp]: "~prime (0::int)" |
31706 | 1562 |
by (simp add: prime_int_def) |
1563 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1564 |
lemma one_not_prime_nat [simp]: "~prime (1::nat)" |
31706 | 1565 |
by (simp add: prime_nat_def) |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
1566 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1567 |
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)" |
31706 | 1568 |
by (simp add: prime_nat_def One_nat_def) |
1569 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1570 |
lemma one_not_prime_int [simp]: "~prime (1::int)" |
31706 | 1571 |
by (simp add: prime_int_def) |
1572 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1573 |
lemma two_is_prime_nat [simp]: "prime (2::nat)" |
31706 | 1574 |
apply (auto simp add: prime_nat_def) |
1575 |
apply (case_tac m) |
|
1576 |
apply (auto dest!: dvd_imp_le) |
|
1577 |
done |
|
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
1578 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1579 |
lemma two_is_prime_int [simp]: "prime (2::int)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1580 |
by (rule two_is_prime_nat [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
|
1581 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1582 |
lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n" |
31706 | 1583 |
apply (unfold prime_nat_def) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1584 |
apply (metis gcd_dvd1_nat gcd_dvd2_nat) |
31706 | 1585 |
done |
1586 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1587 |
lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n" |
31706 | 1588 |
apply (unfold prime_int_altdef) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1589 |
apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1590 |
done |
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1591 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1592 |
lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1593 |
by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat) |
31706 | 1594 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1595 |
lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1596 |
by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int) |
31706 | 1597 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1598 |
lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow> |
31706 | 1599 |
p dvd m * n = (p dvd m \<or> p dvd n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1600 |
by (rule iffI, rule prime_dvd_mult_nat, auto) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1601 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1602 |
lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow> |
31706 | 1603 |
p dvd m * n = (p dvd m \<or> p dvd n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1604 |
by (rule iffI, rule prime_dvd_mult_int, auto) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1605 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1606 |
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow> |
31706 | 1607 |
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n" |
1608 |
unfolding prime_nat_def dvd_def apply auto |
|
31992 | 1609 |
by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1610 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1611 |
lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow> |
31706 | 1612 |
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n" |
1613 |
unfolding prime_int_altdef dvd_def |
|
1614 |
apply auto |
|
31992 | 1615 |
by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1616 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1617 |
lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) --> |
31706 | 1618 |
n > 0 --> (p dvd x^n --> p dvd x)" |
1619 |
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
|
1620 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1621 |
lemma prime_dvd_power_int [rule_format]: "prime (p::int) --> |
31706 | 1622 |
n > 0 --> (p dvd x^n --> p dvd x)" |
1623 |
apply (induct n rule: nat_induct, auto) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1624 |
apply (frule prime_ge_0_int) |
31706 | 1625 |
apply auto |
1626 |
done |
|
1627 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1628 |
lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> |
31706 | 1629 |
coprime a (p^m)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1630 |
apply (rule coprime_exp_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1631 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1632 |
apply (erule (1) prime_imp_coprime_nat) |
31706 | 1633 |
done |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1634 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1635 |
lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> |
31706 | 1636 |
coprime a (p^m)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1637 |
apply (rule coprime_exp_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1638 |
apply (subst gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1639 |
apply (erule (1) prime_imp_coprime_int) |
31706 | 1640 |
done |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1641 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1642 |
lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1643 |
apply (rule prime_imp_coprime_nat, assumption) |
31706 | 1644 |
apply (unfold prime_nat_def, auto) |
1645 |
done |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1646 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1647 |
lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1648 |
apply (rule prime_imp_coprime_int, assumption) |
31706 | 1649 |
apply (unfold prime_int_altdef, clarify) |
1650 |
apply (drule_tac x = q in spec) |
|
1651 |
apply (drule_tac x = p in spec) |
|
1652 |
apply auto |
|
1653 |
done |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1654 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1655 |
lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> |
31706 | 1656 |
coprime (p^m) (q^n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1657 |
by (rule coprime_exp2_nat, rule primes_coprime_nat) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1658 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1659 |
lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> |
31706 | 1660 |
coprime (p^m) (q^n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1661 |
by (rule coprime_exp2_int, rule primes_coprime_int) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
1662 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1663 |
lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n" |
31706 | 1664 |
apply (induct n rule: nat_less_induct) |
1665 |
apply (case_tac "n = 0") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1666 |
using two_is_prime_nat apply blast |
31706 | 1667 |
apply (case_tac "prime n") |
1668 |
apply blast |
|
1669 |
apply (subgoal_tac "n > 1") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1670 |
apply (frule (1) not_prime_eq_prod_nat) |
31706 | 1671 |
apply (auto intro: dvd_mult dvd_mult2) |
1672 |
done |
|
23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset
|
1673 |
|
31706 | 1674 |
(* An Isar version: |
1675 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1676 |
lemma prime_factor_b_nat: |
31706 | 1677 |
fixes n :: nat |
1678 |
assumes "n \<noteq> 1" |
|
1679 |
shows "\<exists>p. prime p \<and> p dvd n" |
|
23983 | 1680 |
|
31706 | 1681 |
using `n ~= 1` |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1682 |
proof (induct n rule: less_induct_nat) |
31706 | 1683 |
fix n :: nat |
1684 |
assume "n ~= 1" and |
|
1685 |
ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)" |
|
1686 |
thus "\<exists>p. prime p \<and> p dvd n" |
|
1687 |
proof - |
|
1688 |
{ |
|
1689 |
assume "n = 0" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1690 |
moreover note two_is_prime_nat |
31706 | 1691 |
ultimately have ?thesis |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1692 |
by (auto simp del: two_is_prime_nat) |
31706 | 1693 |
} |
1694 |
moreover |
|
1695 |
{ |
|
1696 |
assume "prime n" |
|
1697 |
hence ?thesis by auto |
|
1698 |
} |
|
1699 |
moreover |
|
1700 |
{ |
|
1701 |
assume "n ~= 0" and "~ prime n" |
|
1702 |
with `n ~= 1` have "n > 1" by auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1703 |
with `~ prime n` and not_prime_eq_prod_nat obtain m k where |
31706 | 1704 |
"n = m * k" and "1 < m" and "m < n" by blast |
1705 |
with ih obtain p where "prime p" and "p dvd m" by blast |
|
1706 |
with `n = m * k` have ?thesis by auto |
|
1707 |
} |
|
1708 |
ultimately show ?thesis by blast |
|
1709 |
qed |
|
23983 | 1710 |
qed |
1711 |
||
31706 | 1712 |
*) |
1713 |
||
1714 |
text {* One property of coprimality is easier to prove via prime factors. *} |
|
1715 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1716 |
lemma prime_divprod_pow_nat: |
31706 | 1717 |
assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b" |
1718 |
shows "p^n dvd a \<or> p^n dvd b" |
|
1719 |
proof- |
|
1720 |
{assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis |
|
1721 |
apply (cases "n=0", simp_all) |
|
1722 |
apply (cases "a=1", simp_all) done} |
|
1723 |
moreover |
|
1724 |
{assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1" |
|
1725 |
then obtain m where m: "n = Suc m" by (cases n, auto) |
|
1726 |
from n have "p dvd p^n" by (intro dvd_power, auto) |
|
1727 |
also note pab |
|
1728 |
finally have pab': "p dvd a * b". |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1729 |
from prime_dvd_mult_nat[OF p pab'] |
31706 | 1730 |
have "p dvd a \<or> p dvd b" . |
1731 |
moreover |
|
1732 |
{assume pa: "p dvd a" |
|
1733 |
have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1734 |
from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto |
31706 | 1735 |
with p have "coprime b p" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1736 |
by (subst gcd_commute_nat, intro prime_imp_coprime_nat) |
31706 | 1737 |
hence pnb: "coprime (p^n) b" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1738 |
by (subst gcd_commute_nat, rule coprime_exp_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1739 |
from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast } |
31706 | 1740 |
moreover |
1741 |
{assume pb: "p dvd b" |
|
1742 |
have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1743 |
from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a" |
31706 | 1744 |
by auto |
1745 |
with p have "coprime a p" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1746 |
by (subst gcd_commute_nat, intro prime_imp_coprime_nat) |
31706 | 1747 |
hence pna: "coprime (p^n) a" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1748 |
by (subst gcd_commute_nat, rule coprime_exp_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
1749 |
from coprime_divprod_nat[OF pab pna] have ?thesis by blast } |
31706 | 1750 |
ultimately have ?thesis by blast} |
1751 |
ultimately show ?thesis by blast |
|
23983 | 1752 |
qed |
1753 |
||
21256 | 1754 |
end |