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