author | nipkow |
Sat, 07 Mar 1998 16:29:29 +0100 | |
changeset 4686 | 74a12e86b20b |
parent 4356 | 0dfd34f0d33d |
child 4728 | b72dd6b2ba56 |
permissions | -rw-r--r-- |
1804 | 1 |
(* Title: HOL/ex/Primes.ML |
2 |
ID: $Id$ |
|
3 |
Author: Christophe Tabacznyj and Lawrence C Paulson |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
The "divides" relation, the greatest common divisor and Euclid's algorithm |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
7 |
|
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
8 |
See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992) |
1804 | 9 |
*) |
10 |
||
11 |
eta_contract:=false; |
|
12 |
||
13 |
open Primes; |
|
14 |
||
15 |
(************************************************) |
|
16 |
(** Greatest Common Divisor **) |
|
17 |
(************************************************) |
|
18 |
||
3495
04739732b13e
New comments on how to deal with unproved termination conditions
paulson
parents:
3457
diff
changeset
|
19 |
(*** Euclid's Algorithm ***) |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
20 |
|
1804 | 21 |
|
3495
04739732b13e
New comments on how to deal with unproved termination conditions
paulson
parents:
3457
diff
changeset
|
22 |
(** Prove the termination condition and remove it from the recursion equations |
04739732b13e
New comments on how to deal with unproved termination conditions
paulson
parents:
3457
diff
changeset
|
23 |
and induction rule **) |
04739732b13e
New comments on how to deal with unproved termination conditions
paulson
parents:
3457
diff
changeset
|
24 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
25 |
Tfl.tgoalw thy [] gcd.rules; |
4356 | 26 |
by (simp_tac (simpset() addsimps [mod_less_divisor]) 1); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
27 |
val tc = result(); |
1804 | 28 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
29 |
val gcd_eq = tc RS hd gcd.rules; |
3270 | 30 |
val gcd_induct = tc RS gcd.induct; |
1804 | 31 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
32 |
goal thy "gcd(m,0) = m"; |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
33 |
by (rtac (gcd_eq RS trans) 1); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
34 |
by (Simp_tac 1); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
35 |
qed "gcd_0"; |
1804 | 36 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
37 |
goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)"; |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
38 |
by (rtac (gcd_eq RS trans) 1); |
4686 | 39 |
by (Asm_simp_tac 1); |
4356 | 40 |
by (Blast_tac 1); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
41 |
qed "gcd_less_0"; |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
42 |
Addsimps [gcd_0, gcd_less_0]; |
1804 | 43 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
44 |
goal thy "gcd(m,0) dvd m"; |
1804 | 45 |
by (Simp_tac 1); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
46 |
qed "gcd_0_dvd_m"; |
1804 | 47 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
48 |
goal thy "gcd(m,0) dvd 0"; |
1804 | 49 |
by (Simp_tac 1); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
50 |
qed "gcd_0_dvd_0"; |
1804 | 51 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
52 |
(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
53 |
goal thy "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"; |
3301
cdcc4d5602b6
Now the recdef induction rule variables are named u, v, ...
paulson
parents:
3270
diff
changeset
|
54 |
by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1); |
2102 | 55 |
by (case_tac "n=0" 1); |
4356 | 56 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mod_less_divisor]))); |
4089 | 57 |
by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
58 |
qed "gcd_divides_both"; |
1804 | 59 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
60 |
(*Maximality: for all m,n,f naturals, |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
61 |
if f divides m and f divides n then f divides gcd(m,n)*) |
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
62 |
goal thy "!!k. (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"; |
3301
cdcc4d5602b6
Now the recdef induction rule variables are named u, v, ...
paulson
parents:
3270
diff
changeset
|
63 |
by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1); |
2102 | 64 |
by (case_tac "n=0" 1); |
4356 | 65 |
by (ALLGOALS(asm_full_simp_tac(simpset() addsimps[dvd_mod,mod_less_divisor]))); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
66 |
qed_spec_mp "gcd_greatest"; |
1804 | 67 |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
68 |
(*Function gcd yields the Greatest Common Divisor*) |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
69 |
goalw thy [is_gcd_def] "is_gcd (gcd(m,n)) m n"; |
4089 | 70 |
by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_divides_both]) 1); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
71 |
qed "is_gcd"; |
1804 | 72 |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
73 |
(*uniqueness of GCDs*) |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
74 |
goalw thy [is_gcd_def] "is_gcd m a b & is_gcd n a b --> m=n"; |
4089 | 75 |
by (blast_tac (claset() addIs [dvd_anti_sym]) 1); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
76 |
qed "is_gcd_unique"; |
1804 | 77 |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
78 |
(*Davenport, page 27*) |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
79 |
goal thy "k * gcd(m,n) = gcd(k*m, k*n)"; |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
80 |
by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1); |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
81 |
by (case_tac "k=0" 1); |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
82 |
by (case_tac "n=0" 2); |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
83 |
by (ALLGOALS |
4356 | 84 |
(asm_full_simp_tac (simpset() addsimps |
85 |
[mod_less_divisor, mod_geq, mod_mult_distrib2]))); |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
86 |
qed "gcd_mult_distrib2"; |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
87 |
|
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
88 |
(*This theorem leads immediately to a proof of the uniqueness of factorization. |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
89 |
If p divides a product of primes then it is one of those primes.*) |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
90 |
goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"; |
3718 | 91 |
by (Clarify_tac 1); |
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
92 |
by (subgoal_tac "m = gcd(m*p, m*n)" 1); |
3457 | 93 |
by (etac ssubst 1); |
94 |
by (rtac gcd_greatest 1); |
|
4089 | 95 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym]))); |
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
96 |
(*Now deduce gcd(p,n)=1 to finish the proof*) |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
97 |
by (cut_inst_tac [("m","p"),("n","n")] gcd_divides_both 1); |
4089 | 98 |
by (fast_tac (claset() addSss (simpset())) 1); |
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
99 |
qed "prime_dvd_mult"; |