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 |
|
7 |
|
8 See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992) |
|
9 *) |
|
10 |
|
11 eta_contract:=false; |
|
12 |
|
13 (************************************************) |
|
14 (** Greatest Common Divisor **) |
|
15 (************************************************) |
|
16 |
|
17 (*** Euclid's Algorithm ***) |
|
18 |
|
19 |
|
20 val [gcd_eq] = gcd.simps; |
|
21 |
|
22 |
|
23 val prems = goal thy |
|
24 "[| !!m. P m 0; \ |
|
25 \ !!m n. [| 0<n; P n (m mod n) |] ==> P m n \ |
|
26 \ |] ==> P (m::nat) (n::nat)"; |
|
27 by (induct_thm_tac gcd.induct "m n" 1); |
|
28 by (case_tac "n=0" 1); |
|
29 by (asm_simp_tac (simpset() addsimps prems) 1); |
|
30 by Safe_tac; |
|
31 by (asm_simp_tac (simpset() addsimps prems) 1); |
|
32 qed "gcd_induct"; |
|
33 |
|
34 |
|
35 Goal "gcd(m,0) = m"; |
|
36 by (Simp_tac 1); |
|
37 qed "gcd_0"; |
|
38 Addsimps [gcd_0]; |
|
39 |
|
40 Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)"; |
|
41 by (Asm_simp_tac 1); |
|
42 qed "gcd_non_0"; |
|
43 |
|
44 Delsimps gcd.simps; |
|
45 |
|
46 Goal "gcd(m,1) = 1"; |
|
47 by (simp_tac (simpset() addsimps [gcd_non_0]) 1); |
|
48 qed "gcd_1"; |
|
49 Addsimps [gcd_1]; |
|
50 |
|
51 (*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) |
|
52 Goal "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"; |
|
53 by (induct_thm_tac gcd_induct "m n" 1); |
|
54 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [gcd_non_0]))); |
|
55 by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1); |
|
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 |
|
61 |
|
62 (*Maximality: for all m,n,f naturals, |
|
63 if f divides m and f divides n then f divides gcd(m,n)*) |
|
64 Goal "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"; |
|
65 by (induct_thm_tac gcd_induct "m n" 1); |
|
66 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod]))); |
|
67 qed_spec_mp "gcd_greatest"; |
|
68 |
|
69 (*Function gcd yields the Greatest Common Divisor*) |
|
70 Goalw [is_gcd_def] "is_gcd (gcd(m,n)) m n"; |
|
71 by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_dvd_both]) 1); |
|
72 qed "is_gcd"; |
|
73 |
|
74 (*uniqueness of GCDs*) |
|
75 Goalw [is_gcd_def] "[| is_gcd m a b; is_gcd n a b |] ==> m=n"; |
|
76 by (blast_tac (claset() addIs [dvd_anti_sym]) 1); |
|
77 qed "is_gcd_unique"; |
|
78 |
|
79 (*USED??*) |
|
80 Goalw [is_gcd_def] |
|
81 "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"; |
|
82 by (Blast_tac 1); |
|
83 qed "is_gcd_dvd"; |
|
84 |
|
85 (** Commutativity **) |
|
86 |
|
87 Goalw [is_gcd_def] "is_gcd k m n = is_gcd k n m"; |
|
88 by (Blast_tac 1); |
|
89 qed "is_gcd_commute"; |
|
90 |
|
91 Goal "gcd(m,n) = gcd(n,m)"; |
|
92 by (rtac is_gcd_unique 1); |
|
93 by (rtac is_gcd 2); |
|
94 by (asm_simp_tac (simpset() addsimps [is_gcd, is_gcd_commute]) 1); |
|
95 qed "gcd_commute"; |
|
96 |
|
97 Goal "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"; |
|
98 by (rtac is_gcd_unique 1); |
|
99 by (rtac is_gcd 2); |
|
100 by (rewtac is_gcd_def); |
|
101 by (blast_tac (claset() addSIs [gcd_dvd1, gcd_dvd2] |
|
102 addIs [gcd_greatest, dvd_trans]) 1); |
|
103 qed "gcd_assoc"; |
|
104 |
|
105 Goal "gcd(0,m) = m"; |
|
106 by (stac gcd_commute 1); |
|
107 by (rtac gcd_0 1); |
|
108 qed "gcd_0_left"; |
|
109 |
|
110 Goal "gcd(1,m) = 1"; |
|
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 |
|
119 (*Davenport, page 27*) |
|
120 Goal "k * gcd(m,n) = gcd(k*m, k*n)"; |
|
121 by (induct_thm_tac gcd_induct "m n" 1); |
|
122 by (Asm_full_simp_tac 1); |
|
123 by (case_tac "k=0" 1); |
|
124 by (Asm_full_simp_tac 1); |
|
125 by (asm_full_simp_tac |
|
126 (simpset() addsimps [mod_geq, gcd_non_0, mod_mult_distrib2]) 1); |
|
127 qed "gcd_mult_distrib2"; |
|
128 |
|
129 Goal "gcd(m,m) = m"; |
|
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 |
|
135 Goal "gcd(k, k*n) = k"; |
|
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 |
|
141 Goal "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m"; |
|
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 |
|
147 Goalw [prime_def] "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1"; |
|
148 by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1); |
|
149 by Auto_tac; |
|
150 qed "prime_imp_relprime"; |
|
151 |
|
152 (*This theorem leads immediately to a proof of the uniqueness of factorization. |
|
153 If p divides a product of primes then it is one of those primes.*) |
|
154 Goal "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"; |
|
155 by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime]) 1); |
|
156 qed "prime_dvd_mult"; |
|
157 |
|
158 |
|
159 (** Addition laws **) |
|
160 |
|
161 Goal "gcd(m, m+n) = gcd(m,n)"; |
|
162 by (res_inst_tac [("n1", "m+n")] (gcd_commute RS ssubst) 1); |
|
163 by (rtac (gcd_eq RS trans) 1); |
|
164 by Auto_tac; |
|
165 by (asm_simp_tac (simpset() addsimps [mod_add_self1]) 1); |
|
166 by (stac gcd_commute 1); |
|
167 by (stac gcd_non_0 1); |
|
168 by Safe_tac; |
|
169 qed "gcd_add"; |
|
170 |
|
171 Goal "gcd(m, n+m) = gcd(m,n)"; |
|
172 by (asm_simp_tac (simpset() addsimps [add_commute, gcd_add]) 1); |
|
173 qed "gcd_add2"; |
|
174 |
|
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 |
|
181 |
|
182 (** More multiplication laws **) |
|
183 |
|
184 Goal "gcd(m,n) dvd gcd(k*m, n)"; |
|
185 by (blast_tac (claset() addIs [gcd_greatest, dvd_trans, |
|
186 gcd_dvd1, gcd_dvd2]) 1); |
|
187 qed "gcd_dvd_gcd_mult"; |
|
188 |
|
189 Goal "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"; |
|
190 by (rtac dvd_anti_sym 1); |
|
191 by (rtac gcd_dvd_gcd_mult 2); |
|
192 by (rtac ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1); |
|
193 by (stac mult_commute 2); |
|
194 by (rtac gcd_dvd1 2); |
|
195 by (stac gcd_commute 1); |
|
196 by (asm_simp_tac (simpset() addsimps [gcd_assoc RS sym]) 1); |
|
197 qed "gcd_mult_cancel"; |
|