author | paulson |
Mon, 23 Jun 1997 10:42:03 +0200 | |
changeset 3457 | a8ab7c64817c |
parent 3377 | afa1fedef73f |
child 3495 | 04739732b13e |
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 |
||
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
19 |
(* Euclid's Algorithm *) |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
20 |
|
1804 | 21 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
22 |
Tfl.tgoalw thy [] gcd.rules; |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
23 |
by (simp_tac (!simpset addsimps [mod_less_divisor,zero_less_eq]) 1); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
24 |
val tc = result(); |
1804 | 25 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
26 |
val gcd_eq = tc RS hd gcd.rules; |
3270 | 27 |
val gcd_induct = tc RS gcd.induct; |
1804 | 28 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
29 |
goal thy "gcd(m,0) = m"; |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
30 |
by (rtac (gcd_eq RS trans) 1); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
31 |
by (Simp_tac 1); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
32 |
qed "gcd_0"; |
1804 | 33 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
34 |
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
|
35 |
by (rtac (gcd_eq RS trans) 1); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
36 |
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
37 |
qed "gcd_less_0"; |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
38 |
Addsimps [gcd_0, gcd_less_0]; |
1804 | 39 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
40 |
goal thy "gcd(m,0) dvd m"; |
1804 | 41 |
by (Simp_tac 1); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
42 |
qed "gcd_0_dvd_m"; |
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 0"; |
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_0"; |
1804 | 47 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
48 |
(*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
|
49 |
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
|
50 |
by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1); |
2102 | 51 |
by (case_tac "n=0" 1); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
52 |
by (ALLGOALS |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
53 |
(asm_simp_tac (!simpset addsimps [mod_less_divisor,zero_less_eq]))); |
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
54 |
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
|
55 |
qed "gcd_divides_both"; |
1804 | 56 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
57 |
(*Maximality: for all m,n,f naturals, |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
58 |
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
|
59 |
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
|
60 |
by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1); |
2102 | 61 |
by (case_tac "n=0" 1); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
62 |
by (ALLGOALS |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
63 |
(asm_simp_tac (!simpset addsimps [dvd_mod, mod_less_divisor, |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
64 |
zero_less_eq]))); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
65 |
qed_spec_mp "gcd_greatest"; |
1804 | 66 |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
67 |
(*Function gcd yields the Greatest Common Divisor*) |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
68 |
goalw thy [is_gcd_def] "is_gcd (gcd(m,n)) m n"; |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
69 |
by (asm_simp_tac (!simpset addsimps [gcd_greatest, gcd_divides_both]) 1); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
70 |
qed "is_gcd"; |
1804 | 71 |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
72 |
(*uniqueness of GCDs*) |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
73 |
goalw thy [is_gcd_def] "is_gcd m a b & is_gcd n a b --> m=n"; |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
74 |
by (blast_tac (!claset addIs [dvd_anti_sym]) 1); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
75 |
qed "is_gcd_unique"; |
1804 | 76 |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
77 |
(*Davenport, page 27*) |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
78 |
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
|
79 |
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
|
80 |
by (case_tac "k=0" 1); |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
81 |
by (case_tac "n=0" 2); |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
82 |
by (ALLGOALS |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
83 |
(asm_simp_tac (!simpset addsimps [mod_less_divisor, zero_less_eq, |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
84 |
mod_geq, mod_mult_distrib2]))); |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
85 |
qed "gcd_mult_distrib2"; |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
86 |
|
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
87 |
(*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
|
88 |
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
|
89 |
goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"; |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
90 |
by (Step_tac 1); |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
91 |
by (subgoal_tac "m = gcd(m*p, m*n)" 1); |
3457 | 92 |
by (etac ssubst 1); |
93 |
by (rtac gcd_greatest 1); |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
94 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [gcd_mult_distrib2 RS sym]))); |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
95 |
(*Now deduce gcd(p,n)=1 to finish the proof*) |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
96 |
by (cut_inst_tac [("m","p"),("n","n")] gcd_divides_both 1); |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
97 |
by (fast_tac (!claset addSss (!simpset)) 1); |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
98 |
qed "prime_dvd_mult"; |