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