author | paulson |
Thu, 01 Oct 1998 18:30:05 +0200 | |
changeset 5601 | b6456ccd9e3e |
parent 5227 | e5a6ace920a0 |
child 6073 | fba734ba6894 |
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 |
(************************************************) |
|
14 |
(** Greatest Common Divisor **) |
|
15 |
(************************************************) |
|
16 |
||
3495
04739732b13e
New comments on how to deal with unproved termination conditions
paulson
parents:
3457
diff
changeset
|
17 |
(*** Euclid's Algorithm ***) |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
18 |
|
1804 | 19 |
|
3495
04739732b13e
New comments on how to deal with unproved termination conditions
paulson
parents:
3457
diff
changeset
|
20 |
(** 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
|
21 |
and induction rule **) |
04739732b13e
New comments on how to deal with unproved termination conditions
paulson
parents:
3457
diff
changeset
|
22 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
23 |
Tfl.tgoalw thy [] gcd.rules; |
4356 | 24 |
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
|
25 |
val tc = result(); |
1804 | 26 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
27 |
val gcd_eq = tc RS hd gcd.rules; |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
28 |
|
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
29 |
val prems = goal thy |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
30 |
"[| !!m. P m 0; \ |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
31 |
\ !!m n. [| 0<n; P n (m mod n) |] ==> P m n \ |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
32 |
\ |] ==> P m n"; |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
33 |
by (res_inst_tac [("u","m"),("v","n")] (tc RS gcd.induct) 1); |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
34 |
by (case_tac "n=0" 1); |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
35 |
by (asm_simp_tac (simpset() addsimps prems) 1); |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
36 |
by Safe_tac; |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
37 |
by (asm_simp_tac (simpset() addsimps prems) 1); |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
38 |
qed "gcd_induct"; |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
39 |
|
1804 | 40 |
|
5069 | 41 |
Goal "gcd(m,0) = m"; |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
42 |
by (rtac (gcd_eq RS trans) 1); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
43 |
by (Simp_tac 1); |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
44 |
qed "gcd_0"; |
4809 | 45 |
Addsimps [gcd_0]; |
1804 | 46 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
47 |
Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)"; |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
48 |
by (rtac (gcd_eq RS trans) 1); |
4686 | 49 |
by (Asm_simp_tac 1); |
4356 | 50 |
by (Blast_tac 1); |
4809 | 51 |
qed "gcd_non_0"; |
1804 | 52 |
|
5069 | 53 |
Goal "gcd(m,1) = 1"; |
4809 | 54 |
by (simp_tac (simpset() addsimps [gcd_non_0]) 1); |
55 |
qed "gcd_1"; |
|
56 |
Addsimps [gcd_1]; |
|
1804 | 57 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
58 |
(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) |
5069 | 59 |
Goal "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"; |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
60 |
by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); |
4809 | 61 |
by (ALLGOALS |
62 |
(asm_full_simp_tac (simpset() addsimps [gcd_non_0, mod_less_divisor]))); |
|
4089 | 63 |
by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1); |
4809 | 64 |
qed "gcd_dvd_both"; |
65 |
||
66 |
bind_thm ("gcd_dvd1", gcd_dvd_both RS conjunct1); |
|
67 |
bind_thm ("gcd_dvd2", gcd_dvd_both RS conjunct2); |
|
68 |
||
1804 | 69 |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
70 |
(*Maximality: for all m,n,f naturals, |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
71 |
if f divides m and f divides n then f divides gcd(m,n)*) |
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
72 |
Goal "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"; |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
73 |
by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); |
4809 | 74 |
by (ALLGOALS |
75 |
(asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod, |
|
76 |
mod_less_divisor]))); |
|
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
77 |
qed_spec_mp "gcd_greatest"; |
1804 | 78 |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
79 |
(*Function gcd yields the Greatest Common Divisor*) |
5069 | 80 |
Goalw [is_gcd_def] "is_gcd (gcd(m,n)) m n"; |
4809 | 81 |
by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_dvd_both]) 1); |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
2102
diff
changeset
|
82 |
qed "is_gcd"; |
1804 | 83 |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
84 |
(*uniqueness of GCDs*) |
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
85 |
Goalw [is_gcd_def] "[| is_gcd m a b; is_gcd n a b |] ==> m=n"; |
4089 | 86 |
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
|
87 |
qed "is_gcd_unique"; |
1804 | 88 |
|
4809 | 89 |
(*USED??*) |
5069 | 90 |
Goalw [is_gcd_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
91 |
"[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"; |
4809 | 92 |
by (Blast_tac 1); |
93 |
qed "is_gcd_dvd"; |
|
94 |
||
95 |
(** Commutativity **) |
|
96 |
||
5069 | 97 |
Goalw [is_gcd_def] "is_gcd k m n = is_gcd k n m"; |
4809 | 98 |
by (Blast_tac 1); |
99 |
qed "is_gcd_commute"; |
|
100 |
||
5069 | 101 |
Goal "gcd(m,n) = gcd(n,m)"; |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
102 |
by (rtac is_gcd_unique 1); |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
103 |
by (rtac is_gcd 2); |
4809 | 104 |
by (asm_simp_tac (simpset() addsimps [is_gcd, is_gcd_commute]) 1); |
105 |
qed "gcd_commute"; |
|
106 |
||
5069 | 107 |
Goal "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"; |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
108 |
by (rtac is_gcd_unique 1); |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
109 |
by (rtac is_gcd 2); |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
110 |
by (rewtac is_gcd_def); |
4809 | 111 |
by (blast_tac (claset() addSIs [gcd_dvd1, gcd_dvd2] |
112 |
addIs [gcd_greatest, dvd_trans]) 1); |
|
113 |
qed "gcd_assoc"; |
|
114 |
||
5069 | 115 |
Goal "gcd(0,m) = m"; |
4809 | 116 |
by (stac gcd_commute 1); |
117 |
by (rtac gcd_0 1); |
|
118 |
qed "gcd_0_left"; |
|
119 |
||
5069 | 120 |
Goal "gcd(1,m) = 1"; |
4809 | 121 |
by (stac gcd_commute 1); |
122 |
by (rtac gcd_1 1); |
|
123 |
qed "gcd_1_left"; |
|
124 |
Addsimps [gcd_0_left, gcd_1_left]; |
|
125 |
||
126 |
||
127 |
(** Multiplication laws **) |
|
128 |
||
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
129 |
(*Davenport, page 27*) |
5069 | 130 |
Goal "k * gcd(m,n) = gcd(k*m, k*n)"; |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
131 |
by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
132 |
by (Asm_full_simp_tac 1); |
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
133 |
by (case_tac "k=0" 1); |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
134 |
by (Asm_full_simp_tac 1); |
4809 | 135 |
by (asm_full_simp_tac |
136 |
(simpset() addsimps [mod_geq, gcd_non_0, mod_mult_distrib2]) 1); |
|
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
137 |
qed "gcd_mult_distrib2"; |
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
138 |
|
5069 | 139 |
Goal "gcd(m,m) = m"; |
4809 | 140 |
by (cut_inst_tac [("k","m"),("m","1"),("n","1")] gcd_mult_distrib2 1); |
141 |
by (Asm_full_simp_tac 1); |
|
142 |
qed "gcd_self"; |
|
143 |
Addsimps [gcd_self]; |
|
144 |
||
5069 | 145 |
Goal "gcd(k, k*n) = k"; |
4809 | 146 |
by (cut_inst_tac [("k","k"),("m","1"),("n","n")] gcd_mult_distrib2 1); |
147 |
by (Asm_full_simp_tac 1); |
|
148 |
qed "gcd_mult"; |
|
149 |
Addsimps [gcd_mult]; |
|
150 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
151 |
Goal "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m"; |
4809 | 152 |
by (subgoal_tac "m = gcd(m*k, m*n)" 1); |
153 |
by (etac ssubst 1 THEN rtac gcd_greatest 1); |
|
154 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym]))); |
|
155 |
qed "relprime_dvd_mult"; |
|
156 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
157 |
Goalw [prime_def] "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1"; |
4809 | 158 |
by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1); |
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
159 |
by Auto_tac; |
4809 | 160 |
qed "prime_imp_relprime"; |
161 |
||
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
162 |
(*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
|
163 |
If p divides a product of primes then it is one of those primes.*) |
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
164 |
Goal "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"; |
4809 | 165 |
by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime]) 1); |
3377
afa1fedef73f
New results including the basis for unique factorization
paulson
parents:
3359
diff
changeset
|
166 |
qed "prime_dvd_mult"; |
4809 | 167 |
|
168 |
||
169 |
(** Addition laws **) |
|
170 |
||
5069 | 171 |
Goal "gcd(m, m+n) = gcd(m,n)"; |
4809 | 172 |
by (res_inst_tac [("n1", "m+n")] (gcd_commute RS ssubst) 1); |
173 |
by (rtac (gcd_eq RS trans) 1); |
|
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
174 |
by Auto_tac; |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
175 |
by (asm_simp_tac (simpset() addsimps [mod_add_self1]) 1); |
4809 | 176 |
by (stac gcd_commute 1); |
177 |
by (stac gcd_non_0 1); |
|
178 |
by Safe_tac; |
|
179 |
qed "gcd_add"; |
|
180 |
||
5069 | 181 |
Goal "gcd(m, n+m) = gcd(m,n)"; |
4809 | 182 |
by (asm_simp_tac (simpset() addsimps [add_commute, gcd_add]) 1); |
183 |
qed "gcd_add2"; |
|
184 |
||
185 |
||
186 |
(** More multiplication laws **) |
|
187 |
||
5069 | 188 |
Goal "gcd(m,n) dvd gcd(k*m, n)"; |
4809 | 189 |
by (blast_tac (claset() addIs [gcd_greatest, dvd_trans, |
190 |
gcd_dvd1, gcd_dvd2]) 1); |
|
191 |
qed "gcd_dvd_gcd_mult"; |
|
192 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
193 |
Goal "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"; |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
194 |
by (rtac dvd_anti_sym 1); |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
195 |
by (rtac gcd_dvd_gcd_mult 2); |
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
196 |
by (rtac ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1); |
4809 | 197 |
by (stac mult_commute 2); |
4812
d65372e425e5
expandshort; new gcd_induct with inbuilt case analysis
paulson
parents:
4809
diff
changeset
|
198 |
by (rtac gcd_dvd1 2); |
4809 | 199 |
by (stac gcd_commute 1); |
200 |
by (asm_simp_tac (simpset() addsimps [gcd_assoc RS sym]) 1); |
|
201 |
qed "gcd_mult_cancel"; |