author | wenzelm |
Wed, 26 Jul 2006 00:44:44 +0200 | |
changeset 20207 | 4c57e850e8d5 |
parent 16417 | 9bc16273c2d4 |
child 24893 | b8ef7afe3a6b |
permissions | -rw-r--r-- |
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
1 |
(* Title: ZF/ex/Primes.thy |
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
3 |
Author: Christophe Tabacznyj and Lawrence C Paulson |
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
4 |
Copyright 1996 University of Cambridge |
15863 | 5 |
*) |
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
6 |
|
15863 | 7 |
header{*The Divides Relation and Euclid's algorithm for the GCD*} |
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
8 |
|
16417 | 9 |
theory Primes imports Main begin |
12867 | 10 |
constdefs |
11 |
divides :: "[i,i]=>o" (infixl "dvd" 50) |
|
12 |
"m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)" |
|
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
13 |
|
15863 | 14 |
is_gcd :: "[i,i,i]=>o" --{*definition of great common divisor*} |
12867 | 15 |
"is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) & |
16 |
(\<forall>d\<in>nat. (d dvd m) & (d dvd n) --> d dvd p)" |
|
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
17 |
|
15863 | 18 |
gcd :: "[i,i]=>i" --{*Euclid's algorithm for the gcd*} |
12867 | 19 |
"gcd(m,n) == transrec(natify(n), |
20 |
%n f. \<lambda>m \<in> nat. |
|
11382
a816fead971a
now more like the HOL versions, and with the Square Root example added
paulson
parents:
11316
diff
changeset
|
21 |
if n=0 then m else f`(m mod n)`n) ` natify(m)" |
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
22 |
|
15863 | 23 |
coprime :: "[i,i]=>o" --{*the coprime relation*} |
11382
a816fead971a
now more like the HOL versions, and with the Square Root example added
paulson
parents:
11316
diff
changeset
|
24 |
"coprime(m,n) == gcd(m,n) = 1" |
a816fead971a
now more like the HOL versions, and with the Square Root example added
paulson
parents:
11316
diff
changeset
|
25 |
|
15863 | 26 |
prime :: i --{*the set of prime numbers*} |
12867 | 27 |
"prime == {p \<in> nat. 1<p & (\<forall>m \<in> nat. m dvd p --> m=1 | m=p)}" |
28 |
||
15863 | 29 |
|
30 |
subsection{*The Divides Relation*} |
|
12867 | 31 |
|
32 |
lemma dvdD: "m dvd n ==> m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
33 |
by (unfold divides_def, assumption) |
12867 | 34 |
|
35 |
lemma dvdE: |
|
36 |
"[|m dvd n; !!k. [|m \<in> nat; n \<in> nat; k \<in> nat; n = m#*k|] ==> P|] ==> P" |
|
37 |
by (blast dest!: dvdD) |
|
38 |
||
39 |
lemmas dvd_imp_nat1 = dvdD [THEN conjunct1, standard] |
|
40 |
lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1, standard] |
|
41 |
||
42 |
||
43 |
lemma dvd_0_right [simp]: "m \<in> nat ==> m dvd 0" |
|
15863 | 44 |
apply (simp add: divides_def) |
12867 | 45 |
apply (fast intro: nat_0I mult_0_right [symmetric]) |
46 |
done |
|
47 |
||
48 |
lemma dvd_0_left: "0 dvd m ==> m = 0" |
|
15863 | 49 |
by (simp add: divides_def) |
12867 | 50 |
|
51 |
lemma dvd_refl [simp]: "m \<in> nat ==> m dvd m" |
|
15863 | 52 |
apply (simp add: divides_def) |
12867 | 53 |
apply (fast intro: nat_1I mult_1_right [symmetric]) |
54 |
done |
|
55 |
||
56 |
lemma dvd_trans: "[| m dvd n; n dvd p |] ==> m dvd p" |
|
15863 | 57 |
by (auto simp add: divides_def intro: mult_assoc mult_type) |
12867 | 58 |
|
59 |
lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m=n" |
|
15863 | 60 |
apply (simp add: divides_def) |
12867 | 61 |
apply (force dest: mult_eq_self_implies_10 |
62 |
simp add: mult_assoc mult_eq_1_iff) |
|
63 |
done |
|
64 |
||
65 |
lemma dvd_mult_left: "[|(i#*j) dvd k; i \<in> nat|] ==> i dvd k" |
|
15863 | 66 |
by (auto simp add: divides_def mult_assoc) |
12867 | 67 |
|
68 |
lemma dvd_mult_right: "[|(i#*j) dvd k; j \<in> nat|] ==> j dvd k" |
|
15863 | 69 |
apply (simp add: divides_def, clarify) |
12867 | 70 |
apply (rule_tac x = "i#*k" in bexI) |
71 |
apply (simp add: mult_ac) |
|
72 |
apply (rule mult_type) |
|
73 |
done |
|
74 |
||
75 |
||
15863 | 76 |
subsection{*Euclid's Algorithm for the GCD*} |
12867 | 77 |
|
78 |
lemma gcd_0 [simp]: "gcd(m,0) = natify(m)" |
|
15863 | 79 |
apply (simp add: gcd_def) |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
80 |
apply (subst transrec, simp) |
12867 | 81 |
done |
82 |
||
83 |
lemma gcd_natify1 [simp]: "gcd(natify(m),n) = gcd(m,n)" |
|
84 |
by (simp add: gcd_def) |
|
85 |
||
86 |
lemma gcd_natify2 [simp]: "gcd(m, natify(n)) = gcd(m,n)" |
|
87 |
by (simp add: gcd_def) |
|
88 |
||
89 |
lemma gcd_non_0_raw: |
|
90 |
"[| 0<n; n \<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)" |
|
15863 | 91 |
apply (simp add: gcd_def) |
12867 | 92 |
apply (rule_tac P = "%z. ?left (z) = ?right" in transrec [THEN ssubst]) |
93 |
apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym] |
|
94 |
mod_less_divisor [THEN ltD]) |
|
95 |
done |
|
96 |
||
97 |
lemma gcd_non_0: "0 < natify(n) ==> gcd(m,n) = gcd(n, m mod n)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
98 |
apply (cut_tac m = m and n = "natify (n) " in gcd_non_0_raw) |
12867 | 99 |
apply auto |
100 |
done |
|
101 |
||
102 |
lemma gcd_1 [simp]: "gcd(m,1) = 1" |
|
103 |
by (simp (no_asm_simp) add: gcd_non_0) |
|
104 |
||
105 |
lemma dvd_add: "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)" |
|
15863 | 106 |
apply (simp add: divides_def) |
12867 | 107 |
apply (fast intro: add_mult_distrib_left [symmetric] add_type) |
108 |
done |
|
109 |
||
110 |
lemma dvd_mult: "k dvd n ==> k dvd (m #* n)" |
|
15863 | 111 |
apply (simp add: divides_def) |
12867 | 112 |
apply (fast intro: mult_left_commute mult_type) |
113 |
done |
|
114 |
||
115 |
lemma dvd_mult2: "k dvd m ==> k dvd (m #* n)" |
|
116 |
apply (subst mult_commute) |
|
117 |
apply (blast intro: dvd_mult) |
|
118 |
done |
|
119 |
||
120 |
(* k dvd (m*k) *) |
|
121 |
lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult, standard] |
|
122 |
lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2, standard] |
|
123 |
||
124 |
lemma dvd_mod_imp_dvd_raw: |
|
125 |
"[| a \<in> nat; b \<in> nat; k dvd b; k dvd (a mod b) |] ==> k dvd a" |
|
15863 | 126 |
apply (case_tac "b=0") |
13259 | 127 |
apply (simp add: DIVISION_BY_ZERO_MOD) |
12867 | 128 |
apply (blast intro: mod_div_equality [THEN subst] |
129 |
elim: dvdE |
|
130 |
intro!: dvd_add dvd_mult mult_type mod_type div_type) |
|
131 |
done |
|
132 |
||
133 |
lemma dvd_mod_imp_dvd: "[| k dvd (a mod b); k dvd b; a \<in> nat |] ==> k dvd a" |
|
13259 | 134 |
apply (cut_tac b = "natify (b)" in dvd_mod_imp_dvd_raw) |
12867 | 135 |
apply auto |
136 |
apply (simp add: divides_def) |
|
137 |
done |
|
138 |
||
139 |
(*Imitating TFL*) |
|
140 |
lemma gcd_induct_lemma [rule_format (no_asm)]: "[| n \<in> nat; |
|
141 |
\<forall>m \<in> nat. P(m,0); |
|
142 |
\<forall>m \<in> nat. \<forall>n \<in> nat. 0<n --> P(n, m mod n) --> P(m,n) |] |
|
143 |
==> \<forall>m \<in> nat. P (m,n)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
144 |
apply (erule_tac i = n in complete_induct) |
12867 | 145 |
apply (case_tac "x=0") |
146 |
apply (simp (no_asm_simp)) |
|
147 |
apply clarify |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
148 |
apply (drule_tac x1 = m and x = x in bspec [THEN bspec]) |
12867 | 149 |
apply (simp_all add: Ord_0_lt_iff) |
150 |
apply (blast intro: mod_less_divisor [THEN ltD]) |
|
151 |
done |
|
152 |
||
153 |
lemma gcd_induct: "!!P. [| m \<in> nat; n \<in> nat; |
|
154 |
!!m. m \<in> nat ==> P(m,0); |
|
155 |
!!m n. [|m \<in> nat; n \<in> nat; 0<n; P(n, m mod n)|] ==> P(m,n) |] |
|
156 |
==> P (m,n)" |
|
157 |
by (blast intro: gcd_induct_lemma) |
|
158 |
||
159 |
||
15863 | 160 |
subsection{*Basic Properties of @{term gcd}*} |
12867 | 161 |
|
15863 | 162 |
text{*type of gcd*} |
12867 | 163 |
lemma gcd_type [simp,TC]: "gcd(m, n) \<in> nat" |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
164 |
apply (subgoal_tac "gcd (natify (m), natify (n)) \<in> nat") |
12867 | 165 |
apply simp |
13259 | 166 |
apply (rule_tac m = "natify (m)" and n = "natify (n)" in gcd_induct) |
12867 | 167 |
apply auto |
168 |
apply (simp add: gcd_non_0) |
|
169 |
done |
|
170 |
||
171 |
||
15863 | 172 |
text{* Property 1: gcd(a,b) divides a and b *} |
12867 | 173 |
|
174 |
lemma gcd_dvd_both: |
|
175 |
"[| m \<in> nat; n \<in> nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
176 |
apply (rule_tac m = m and n = n in gcd_induct) |
12867 | 177 |
apply (simp_all add: gcd_non_0) |
178 |
apply (blast intro: dvd_mod_imp_dvd_raw nat_into_Ord [THEN Ord_0_lt]) |
|
179 |
done |
|
180 |
||
181 |
lemma gcd_dvd1 [simp]: "m \<in> nat ==> gcd(m,n) dvd m" |
|
13259 | 182 |
apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both) |
12867 | 183 |
apply auto |
184 |
done |
|
185 |
||
186 |
lemma gcd_dvd2 [simp]: "n \<in> nat ==> gcd(m,n) dvd n" |
|
13259 | 187 |
apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both) |
12867 | 188 |
apply auto |
189 |
done |
|
190 |
||
15863 | 191 |
text{* if f divides a and b then f divides gcd(a,b) *} |
12867 | 192 |
|
193 |
lemma dvd_mod: "[| f dvd a; f dvd b |] ==> f dvd (a mod b)" |
|
15863 | 194 |
apply (simp add: divides_def) |
13259 | 195 |
apply (case_tac "b=0") |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
196 |
apply (simp add: DIVISION_BY_ZERO_MOD, auto) |
12867 | 197 |
apply (blast intro: mod_mult_distrib2 [symmetric]) |
198 |
done |
|
199 |
||
15863 | 200 |
text{* Property 2: for all a,b,f naturals, |
201 |
if f divides a and f divides b then f divides gcd(a,b)*} |
|
12867 | 202 |
|
203 |
lemma gcd_greatest_raw [rule_format]: |
|
204 |
"[| m \<in> nat; n \<in> nat; f \<in> nat |] |
|
205 |
==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
206 |
apply (rule_tac m = m and n = n in gcd_induct) |
12867 | 207 |
apply (simp_all add: gcd_non_0 dvd_mod) |
208 |
done |
|
209 |
||
210 |
lemma gcd_greatest: "[| f dvd m; f dvd n; f \<in> nat |] ==> f dvd gcd(m,n)" |
|
211 |
apply (rule gcd_greatest_raw) |
|
212 |
apply (auto simp add: divides_def) |
|
213 |
done |
|
214 |
||
215 |
lemma gcd_greatest_iff [simp]: "[| k \<in> nat; m \<in> nat; n \<in> nat |] |
|
216 |
==> (k dvd gcd (m, n)) <-> (k dvd m & k dvd n)" |
|
217 |
by (blast intro!: gcd_greatest gcd_dvd1 gcd_dvd2 intro: dvd_trans) |
|
218 |
||
219 |
||
15863 | 220 |
subsection{*The Greatest Common Divisor*} |
221 |
||
222 |
text{*The GCD exists and function gcd computes it.*} |
|
12867 | 223 |
|
224 |
lemma is_gcd: "[| m \<in> nat; n \<in> nat |] ==> is_gcd(gcd(m,n), m, n)" |
|
225 |
by (simp add: is_gcd_def) |
|
226 |
||
15863 | 227 |
text{*The GCD is unique*} |
12867 | 228 |
|
229 |
lemma is_gcd_unique: "[|is_gcd(m,a,b); is_gcd(n,a,b); m\<in>nat; n\<in>nat|] ==> m=n" |
|
15863 | 230 |
apply (simp add: is_gcd_def) |
12867 | 231 |
apply (blast intro: dvd_anti_sym) |
232 |
done |
|
233 |
||
234 |
lemma is_gcd_commute: "is_gcd(k,m,n) <-> is_gcd(k,n,m)" |
|
15863 | 235 |
by (simp add: is_gcd_def, blast) |
12867 | 236 |
|
237 |
lemma gcd_commute_raw: "[| m \<in> nat; n \<in> nat |] ==> gcd(m,n) = gcd(n,m)" |
|
238 |
apply (rule is_gcd_unique) |
|
239 |
apply (rule is_gcd) |
|
240 |
apply (rule_tac [3] is_gcd_commute [THEN iffD1]) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
241 |
apply (rule_tac [3] is_gcd, auto) |
12867 | 242 |
done |
243 |
||
244 |
lemma gcd_commute: "gcd(m,n) = gcd(n,m)" |
|
13259 | 245 |
apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_commute_raw) |
12867 | 246 |
apply auto |
247 |
done |
|
248 |
||
249 |
lemma gcd_assoc_raw: "[| k \<in> nat; m \<in> nat; n \<in> nat |] |
|
250 |
==> gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" |
|
251 |
apply (rule is_gcd_unique) |
|
252 |
apply (rule is_gcd) |
|
253 |
apply (simp_all add: is_gcd_def) |
|
254 |
apply (blast intro: gcd_dvd1 gcd_dvd2 gcd_type intro: dvd_trans) |
|
255 |
done |
|
256 |
||
257 |
lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" |
|
13259 | 258 |
apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) " |
12867 | 259 |
in gcd_assoc_raw) |
260 |
apply auto |
|
261 |
done |
|
262 |
||
263 |
lemma gcd_0_left [simp]: "gcd (0, m) = natify(m)" |
|
264 |
by (simp add: gcd_commute [of 0]) |
|
265 |
||
266 |
lemma gcd_1_left [simp]: "gcd (1, m) = 1" |
|
267 |
by (simp add: gcd_commute [of 1]) |
|
268 |
||
269 |
||
15863 | 270 |
subsection{*Addition laws*} |
271 |
||
272 |
lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)" |
|
273 |
apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))") |
|
274 |
apply simp |
|
275 |
apply (case_tac "natify (n) = 0") |
|
276 |
apply (auto simp add: Ord_0_lt_iff gcd_non_0) |
|
277 |
done |
|
278 |
||
279 |
lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)" |
|
280 |
apply (rule gcd_commute [THEN trans]) |
|
281 |
apply (subst add_commute, simp) |
|
282 |
apply (rule gcd_commute) |
|
283 |
done |
|
284 |
||
285 |
lemma gcd_add2' [simp]: "gcd (m, n #+ m) = gcd (m, n)" |
|
286 |
by (subst add_commute, rule gcd_add2) |
|
287 |
||
288 |
lemma gcd_add_mult_raw: "k \<in> nat ==> gcd (m, k #* m #+ n) = gcd (m, n)" |
|
289 |
apply (erule nat_induct) |
|
290 |
apply (auto simp add: gcd_add2 add_assoc) |
|
291 |
done |
|
292 |
||
293 |
lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)" |
|
294 |
apply (cut_tac k = "natify (k)" in gcd_add_mult_raw) |
|
295 |
apply auto |
|
296 |
done |
|
297 |
||
298 |
||
299 |
subsection{* Multiplication Laws*} |
|
12867 | 300 |
|
301 |
lemma gcd_mult_distrib2_raw: |
|
302 |
"[| k \<in> nat; m \<in> nat; n \<in> nat |] |
|
303 |
==> k #* gcd (m, n) = gcd (k #* m, k #* n)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
304 |
apply (erule_tac m = m and n = n in gcd_induct, assumption) |
12867 | 305 |
apply simp |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
306 |
apply (case_tac "k = 0", simp) |
12867 | 307 |
apply (simp add: mod_geq gcd_non_0 mod_mult_distrib2 Ord_0_lt_iff) |
308 |
done |
|
309 |
||
310 |
lemma gcd_mult_distrib2: "k #* gcd (m, n) = gcd (k #* m, k #* n)" |
|
13259 | 311 |
apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) " |
12867 | 312 |
in gcd_mult_distrib2_raw) |
313 |
apply auto |
|
314 |
done |
|
315 |
||
316 |
lemma gcd_mult [simp]: "gcd (k, k #* n) = natify(k)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
317 |
by (cut_tac k = k and m = 1 and n = n in gcd_mult_distrib2, auto) |
12867 | 318 |
|
319 |
lemma gcd_self [simp]: "gcd (k, k) = natify(k)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
320 |
by (cut_tac k = k and n = 1 in gcd_mult, auto) |
12867 | 321 |
|
322 |
lemma relprime_dvd_mult: |
|
323 |
"[| gcd (k,n) = 1; k dvd (m #* n); m \<in> nat |] ==> k dvd m" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
324 |
apply (cut_tac k = m and m = k and n = n in gcd_mult_distrib2, auto) |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
325 |
apply (erule_tac b = m in ssubst) |
12867 | 326 |
apply (simp add: dvd_imp_nat1) |
327 |
done |
|
328 |
||
329 |
lemma relprime_dvd_mult_iff: |
|
330 |
"[| gcd (k,n) = 1; m \<in> nat |] ==> k dvd (m #* n) <-> k dvd m" |
|
331 |
by (blast intro: dvdI2 relprime_dvd_mult dvd_trans) |
|
332 |
||
333 |
lemma prime_imp_relprime: |
|
334 |
"[| p \<in> prime; ~ (p dvd n); n \<in> nat |] ==> gcd (p, n) = 1" |
|
15863 | 335 |
apply (simp add: prime_def, clarify) |
13259 | 336 |
apply (drule_tac x = "gcd (p,n)" in bspec) |
12867 | 337 |
apply auto |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
338 |
apply (cut_tac m = p and n = n in gcd_dvd2, auto) |
12867 | 339 |
done |
340 |
||
341 |
lemma prime_into_nat: "p \<in> prime ==> p \<in> nat" |
|
15863 | 342 |
by (simp add: prime_def) |
12867 | 343 |
|
344 |
lemma prime_nonzero: "p \<in> prime \<Longrightarrow> p\<noteq>0" |
|
15863 | 345 |
by (auto simp add: prime_def) |
12867 | 346 |
|
347 |
||
15863 | 348 |
text{*This theorem leads immediately to a proof of the uniqueness of |
349 |
factorization. If @{term p} divides a product of primes then it is |
|
350 |
one of those primes.*} |
|
12867 | 351 |
|
352 |
lemma prime_dvd_mult: |
|
353 |
"[|p dvd m #* n; p \<in> prime; m \<in> nat; n \<in> nat |] ==> p dvd m \<or> p dvd n" |
|
354 |
by (blast intro: relprime_dvd_mult prime_imp_relprime prime_into_nat) |
|
355 |
||
356 |
||
357 |
lemma gcd_mult_cancel_raw: |
|
358 |
"[|gcd (k,n) = 1; m \<in> nat; n \<in> nat|] ==> gcd (k #* m, n) = gcd (m, n)" |
|
359 |
apply (rule dvd_anti_sym) |
|
360 |
apply (rule gcd_greatest) |
|
361 |
apply (rule relprime_dvd_mult [of _ k]) |
|
362 |
apply (simp add: gcd_assoc) |
|
363 |
apply (simp add: gcd_commute) |
|
364 |
apply (simp_all add: mult_commute) |
|
365 |
apply (blast intro: dvdI1 gcd_dvd1 dvd_trans) |
|
366 |
done |
|
367 |
||
368 |
lemma gcd_mult_cancel: "gcd (k,n) = 1 ==> gcd (k #* m, n) = gcd (m, n)" |
|
13259 | 369 |
apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_mult_cancel_raw) |
12867 | 370 |
apply auto |
371 |
done |
|
372 |
||
373 |
||
15863 | 374 |
subsection{*The Square Root of a Prime is Irrational: Key Lemma*} |
12867 | 375 |
|
376 |
lemma prime_dvd_other_side: |
|
377 |
"\<lbrakk>n#*n = p#*(k#*k); p \<in> prime; n \<in> nat\<rbrakk> \<Longrightarrow> p dvd n" |
|
378 |
apply (subgoal_tac "p dvd n#*n") |
|
379 |
apply (blast dest: prime_dvd_mult) |
|
380 |
apply (rule_tac j = "k#*k" in dvd_mult_left) |
|
381 |
apply (auto simp add: prime_def) |
|
382 |
done |
|
383 |
||
384 |
lemma reduction: |
|
385 |
"\<lbrakk>k#*k = p#*(j#*j); p \<in> prime; 0 < k; j \<in> nat; k \<in> nat\<rbrakk> |
|
386 |
\<Longrightarrow> k < p#*j & 0 < j" |
|
387 |
apply (rule ccontr) |
|
388 |
apply (simp add: not_lt_iff_le prime_into_nat) |
|
389 |
apply (erule disjE) |
|
390 |
apply (frule mult_le_mono, assumption+) |
|
391 |
apply (simp add: mult_ac) |
|
392 |
apply (auto dest!: natify_eqE |
|
393 |
simp add: not_lt_iff_le prime_into_nat mult_le_cancel_le1) |
|
394 |
apply (simp add: prime_def) |
|
395 |
apply (blast dest: lt_trans1) |
|
396 |
done |
|
397 |
||
398 |
lemma rearrange: "j #* (p#*j) = k#*k \<Longrightarrow> k#*k = p#*(j#*j)" |
|
399 |
by (simp add: mult_ac) |
|
400 |
||
401 |
lemma prime_not_square: |
|
402 |
"\<lbrakk>m \<in> nat; p \<in> prime\<rbrakk> \<Longrightarrow> \<forall>k \<in> nat. 0<k \<longrightarrow> m#*m \<noteq> p#*(k#*k)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
403 |
apply (erule complete_induct, clarify) |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13259
diff
changeset
|
404 |
apply (frule prime_dvd_other_side, assumption) |
12867 | 405 |
apply assumption |
406 |
apply (erule dvdE) |
|
407 |
apply (simp add: mult_assoc mult_cancel1 prime_nonzero prime_into_nat) |
|
408 |
apply (blast dest: rearrange reduction ltD) |
|
409 |
done |
|
1792
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
410 |
|
75c54074cd8c
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson
parents:
diff
changeset
|
411 |
end |