69 bind_thm ("gcd_dvd2", gcd_dvd_both RS conjunct2); |
69 bind_thm ("gcd_dvd2", gcd_dvd_both RS conjunct2); |
70 |
70 |
71 |
71 |
72 (*Maximality: for all m,n,f naturals, |
72 (*Maximality: for all m,n,f naturals, |
73 if f divides m and f divides n then f divides gcd(m,n)*) |
73 if f divides m and f divides n then f divides gcd(m,n)*) |
74 Goal "!!k. (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"; |
74 Goal "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"; |
75 by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); |
75 by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); |
76 by (ALLGOALS |
76 by (ALLGOALS |
77 (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod, |
77 (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod, |
78 mod_less_divisor]))); |
78 mod_less_divisor]))); |
79 qed_spec_mp "gcd_greatest"; |
79 qed_spec_mp "gcd_greatest"; |
82 Goalw [is_gcd_def] "is_gcd (gcd(m,n)) m n"; |
82 Goalw [is_gcd_def] "is_gcd (gcd(m,n)) m n"; |
83 by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_dvd_both]) 1); |
83 by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_dvd_both]) 1); |
84 qed "is_gcd"; |
84 qed "is_gcd"; |
85 |
85 |
86 (*uniqueness of GCDs*) |
86 (*uniqueness of GCDs*) |
87 Goalw [is_gcd_def] "!!m n. [| is_gcd m a b; is_gcd n a b |] ==> m=n"; |
87 Goalw [is_gcd_def] "[| is_gcd m a b; is_gcd n a b |] ==> m=n"; |
88 by (blast_tac (claset() addIs [dvd_anti_sym]) 1); |
88 by (blast_tac (claset() addIs [dvd_anti_sym]) 1); |
89 qed "is_gcd_unique"; |
89 qed "is_gcd_unique"; |
90 |
90 |
91 (*USED??*) |
91 (*USED??*) |
92 Goalw [is_gcd_def] |
92 Goalw [is_gcd_def] |
148 by (cut_inst_tac [("k","k"),("m","1"),("n","n")] gcd_mult_distrib2 1); |
148 by (cut_inst_tac [("k","k"),("m","1"),("n","n")] gcd_mult_distrib2 1); |
149 by (Asm_full_simp_tac 1); |
149 by (Asm_full_simp_tac 1); |
150 qed "gcd_mult"; |
150 qed "gcd_mult"; |
151 Addsimps [gcd_mult]; |
151 Addsimps [gcd_mult]; |
152 |
152 |
153 Goal "!!k. [| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m"; |
153 Goal "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m"; |
154 by (subgoal_tac "m = gcd(m*k, m*n)" 1); |
154 by (subgoal_tac "m = gcd(m*k, m*n)" 1); |
155 by (etac ssubst 1 THEN rtac gcd_greatest 1); |
155 by (etac ssubst 1 THEN rtac gcd_greatest 1); |
156 by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym]))); |
156 by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym]))); |
157 qed "relprime_dvd_mult"; |
157 qed "relprime_dvd_mult"; |
158 |
158 |
159 Goalw [prime_def] "!!p. [| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1"; |
159 Goalw [prime_def] "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1"; |
160 by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1); |
160 by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1); |
161 by (fast_tac (claset() addss (simpset())) 1); |
161 by Auto_tac; |
162 qed "prime_imp_relprime"; |
162 qed "prime_imp_relprime"; |
163 |
163 |
164 (*This theorem leads immediately to a proof of the uniqueness of factorization. |
164 (*This theorem leads immediately to a proof of the uniqueness of factorization. |
165 If p divides a product of primes then it is one of those primes.*) |
165 If p divides a product of primes then it is one of those primes.*) |
166 Goal "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"; |
166 Goal "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"; |
167 by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime]) 1); |
167 by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime]) 1); |
168 qed "prime_dvd_mult"; |
168 qed "prime_dvd_mult"; |
169 |
169 |
170 |
170 |
171 (** Addition laws **) |
171 (** Addition laws **) |
190 Goal "gcd(m,n) dvd gcd(k*m, n)"; |
190 Goal "gcd(m,n) dvd gcd(k*m, n)"; |
191 by (blast_tac (claset() addIs [gcd_greatest, dvd_trans, |
191 by (blast_tac (claset() addIs [gcd_greatest, dvd_trans, |
192 gcd_dvd1, gcd_dvd2]) 1); |
192 gcd_dvd1, gcd_dvd2]) 1); |
193 qed "gcd_dvd_gcd_mult"; |
193 qed "gcd_dvd_gcd_mult"; |
194 |
194 |
195 Goal "!!n. gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"; |
195 Goal "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"; |
196 by (rtac dvd_anti_sym 1); |
196 by (rtac dvd_anti_sym 1); |
197 by (rtac gcd_dvd_gcd_mult 2); |
197 by (rtac gcd_dvd_gcd_mult 2); |
198 by (rtac ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1); |
198 by (rtac ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1); |
199 by (stac mult_commute 2); |
199 by (stac mult_commute 2); |
200 by (rtac gcd_dvd1 2); |
200 by (rtac gcd_dvd1 2); |