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