author paulson Wed Sep 13 18:46:45 2000 +0200 (2000-09-13) changeset 9944 2a705d1af4dc parent 9943 55c82decf3f4 child 9945 a0efbd7c88dc
moved Primes, Fib, Factorization from HOL/ex
 src/HOL/NumberTheory/Factorization.ML file | annotate | diff | revisions src/HOL/NumberTheory/Factorization.thy file | annotate | diff | revisions src/HOL/NumberTheory/Fib.ML file | annotate | diff | revisions src/HOL/NumberTheory/Fib.thy file | annotate | diff | revisions src/HOL/NumberTheory/Primes.thy file | annotate | diff | revisions src/HOL/NumberTheory/ROOT.ML file | annotate | diff | revisions
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/NumberTheory/Factorization.ML	Wed Sep 13 18:46:45 2000 +0200
1.3 @@ -0,0 +1,312 @@
1.4 +(*  Title:      HOL/ex/Factorization.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Thomas Marthedal Rasmussen
1.7 +    Copyright   2000  University of Cambridge
1.8 +
1.9 +Fundamental Theorem of Arithmetic (unique factorization into primes)
1.10 +*)
1.11 +
1.12 +val prime_def = thm "prime_def";
1.13 +val prime_dvd_mult = thm "prime_dvd_mult";
1.14 +
1.15 +
1.16 +(* --- Arithmetic --- *)
1.17 +
1.18 +Goal "!!m::nat. [| m ~= m*k; m ~= 1 |] ==> 1<m";
1.19 +by (case_tac "m" 1);
1.20 +by Auto_tac;
1.21 +qed "one_less_m";
1.22 +
1.23 +Goal "!!m::nat. [| m ~= m*k; 1<m*k |] ==> 1<k";
1.24 +by (case_tac "k" 1);
1.25 +by Auto_tac;
1.26 +qed "one_less_k";
1.27 +
1.28 +Goal "!!m::nat. [| 0<k; k*n=k*m |] ==> n=m";
1.29 +by Auto_tac;
1.30 +qed "mult_left_cancel";
1.31 +
1.32 +Goal "!!m::nat. [| 0<m; m*n = m |] ==> n=1";
1.33 +by (case_tac "n" 1);
1.34 +by Auto_tac;
1.35 +qed "mn_eq_m_one";
1.36 +
1.37 +Goal "!!m::nat. [| 0<n; 0<k |] ==> 1<m --> m*n = k --> n<k";
1.38 +by (induct_tac "m" 1);
1.39 +by Auto_tac;
1.40 +qed_spec_mp "prod_mn_less_k";
1.41 +
1.42 +
1.43 +(* --- Prime List & Product --- *)
1.44 +
1.45 +Goal "prod (xs @ ys) = prod xs * prod ys";
1.46 +by (induct_tac "xs" 1);
1.47 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [mult_assoc])));
1.48 +qed "prod_append";
1.49 +
1.50 +Goal "prod (x#xs) = prod (y#ys) ==> x*prod xs = y*prod ys";
1.51 +by Auto_tac;
1.52 +qed "prod_xy_prod";
1.53 +
1.54 +Goalw [primel_def] "primel (xs @ ys) = (primel xs & primel ys)";
1.55 +by Auto_tac;
1.56 +qed "primel_append";
1.57 +
1.58 +Goalw [primel_def] "n:prime ==> primel [n] & prod [n] = n";
1.59 +by Auto_tac;
1.60 +qed "prime_primel";
1.61 +
1.62 +Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)";
1.63 +by Auto_tac;
1.64 +by (case_tac "k" 1);
1.65 +by Auto_tac;
1.66 +qed "prime_nd_one";
1.67 +
1.68 +Goalw [dvd_def] "[| prod (x#xs) = prod ys |] ==> x dvd (prod ys)";
1.69 +by (rtac exI 1);
1.70 +by (rtac sym 1);
1.71 +by (Asm_full_simp_tac 1);
1.72 +qed "hd_dvd_prod";
1.73 +
1.74 +Goalw [primel_def] "primel (x#xs) ==> primel xs";
1.75 +by Auto_tac;
1.76 +qed "primel_tl";
1.77 +
1.78 +Goalw [primel_def] "(primel (x#xs)) = (x:prime & primel xs)";
1.79 +by Auto_tac;
1.80 +qed "primel_hd_tl";
1.81 +
1.82 +Goalw [prime_def] "[| p:prime; q:prime; p dvd q |] ==> p=q";
1.83 +by Auto_tac;
1.84 +qed "primes_eq";
1.85 +
1.86 +Goalw [primel_def,prime_def] "[| primel xs; prod xs = 1 |] ==> xs = []";
1.87 +by (case_tac "xs" 1);
1.88 +by (ALLGOALS Asm_full_simp_tac);
1.89 +qed "primel_one_empty";
1.90 +
1.91 +Goalw [prime_def] "p:prime ==> 1<p";
1.92 +by Auto_tac;
1.93 +qed "prime_g_one";
1.94 +
1.95 +Goalw [prime_def] "p:prime ==> 0<p";
1.96 +by Auto_tac;
1.97 +qed "prime_g_zero";
1.98 +
1.99 +Goalw [primel_def,prime_def] "primel xs --> xs ~= [] --> 1 < prod xs";
1.100 +by (induct_tac "xs" 1);
1.101 +by (auto_tac (claset() addEs [one_less_mult], simpset()));
1.102 +qed_spec_mp "primel_nempty_g_one";
1.103 +
1.104 +Goalw [primel_def,prime_def] "primel xs --> 0 < prod xs";
1.105 +by (induct_tac "xs" 1);
1.106 +by Auto_tac;
1.107 +qed_spec_mp "primel_prod_gz";
1.108 +
1.109 +
1.110 +(* --- Sorting --- *)
1.111 +
1.112 +Goal "nondec xs --> nondec (oinsert x xs)";
1.113 +by (induct_tac "xs" 1);
1.114 +by (case_tac "list" 2);
1.115 +by (ALLGOALS(asm_full_simp_tac (simpset()delcongs[thm"list.weak_case_cong"])));
1.116 +qed_spec_mp "nondec_oinsert";
1.117 +
1.118 +Goal "nondec (sort xs)";
1.119 +by (induct_tac "xs" 1);
1.120 +by (ALLGOALS (Asm_full_simp_tac));
1.121 +by (etac nondec_oinsert 1);
1.122 +qed "nondec_sort";
1.123 +
1.124 +Goal "[| x<=y; l=y#ys |]  ==> x#l = oinsert x l";
1.125 +by (ALLGOALS Asm_full_simp_tac);
1.126 +qed "x_less_y_oinsert";
1.127 +
1.128 +Goal "nondec xs --> xs = sort xs";
1.129 +by (induct_tac "xs" 1);
1.130 +by Safe_tac;
1.131 +by (ALLGOALS Asm_full_simp_tac);
1.132 +by (case_tac "list" 1);
1.133 +by (ALLGOALS Asm_full_simp_tac);
1.134 +by (case_tac "list" 1);
1.135 +by (Asm_full_simp_tac 1);
1.136 +by (res_inst_tac [("y","aa"),("ys","lista")] x_less_y_oinsert 1);
1.137 +by (ALLGOALS Asm_full_simp_tac);
1.138 +qed_spec_mp "nondec_sort_eq";
1.139 +
1.140 +Goal "oinsert x (oinsert y l) = oinsert y (oinsert x l)";
1.141 +by (induct_tac "l" 1);
1.142 +by Auto_tac;
1.143 +qed "oinsert_x_y";
1.144 +
1.145 +
1.146 +(* --- Permutation --- *)
1.147 +
1.148 +Goalw [primel_def] "xs <~~> ys ==> primel xs --> primel ys";
1.149 +by (etac perm.induct 1);
1.150 +by (ALLGOALS Asm_simp_tac);
1.151 +qed_spec_mp "perm_primel";
1.152 +
1.153 +Goal "xs <~~> ys ==> prod xs = prod ys";
1.154 +by (etac perm.induct 1);
1.155 +by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));
1.156 +qed_spec_mp "perm_prod";
1.157 +
1.158 +Goal "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys";
1.159 +by (etac perm.induct 1);
1.160 +by Auto_tac;
1.161 +qed "perm_subst_oinsert";
1.162 +
1.163 +Goal "x#xs <~~> oinsert x xs";
1.164 +by (induct_tac "xs" 1);
1.165 +by Auto_tac;
1.166 +qed "perm_oinsert";
1.167 +
1.168 +Goal "xs <~~> sort xs";
1.169 +by (induct_tac "xs" 1);
1.170 +by (auto_tac (claset() addIs [perm_oinsert]
1.172 +              simpset()));
1.173 +qed "perm_sort";
1.174 +
1.175 +Goal "xs <~~> ys ==> sort xs = sort ys";
1.176 +by (etac perm.induct 1);
1.177 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [oinsert_x_y])));
1.178 +qed "perm_sort_eq";
1.179 +
1.180 +
1.181 +(* --- Existence --- *)
1.182 +
1.183 +Goal "primel xs ==> EX ys. primel ys & nondec ys & prod ys = prod xs";
1.184 +by (blast_tac (claset() addIs [nondec_sort, perm_prod,perm_primel,perm_sort,
1.185 +			       perm_sym]) 1);
1.186 +qed "ex_nondec_lemma";
1.187 +
1.188 +Goalw [prime_def,dvd_def]
1.189 +     "1<n & n~:prime --> (EX m k.1<m & 1<k & m<n & k<n & n=m*k)";
1.190 +by (auto_tac (claset() addIs [n_less_m_mult_n, n_less_n_mult_m,
1.191 +			      one_less_m, one_less_k],
1.192 +	      simpset()));
1.193 +qed_spec_mp "not_prime_ex_mk";
1.194 +
1.195 +Goal "[| primel xs; primel ys |] \
1.196 +\     ==> EX l. primel l & prod l = prod xs * prod ys";
1.197 +by (rtac exI 1);
1.198 +by Safe_tac;
1.199 +by (rtac prod_append 2);
1.200 +by (asm_simp_tac (simpset() addsimps [primel_append]) 1);
1.201 +qed "split_primel";
1.202 +
1.203 +Goal "1<n --> (EX l. primel l & prod l = n)";
1.204 +by (induct_thm_tac nat_less_induct "n" 1);
1.205 +by (rtac impI 1);
1.206 +by (case_tac "n:prime" 1);
1.207 +by (rtac exI 1);
1.208 +by (etac prime_primel 1);
1.209 +by (cut_inst_tac [("n","n")] not_prime_ex_mk 1);
1.210 +by (auto_tac (claset() addSIs [split_primel], simpset()));
1.211 +qed_spec_mp "factor_exists";
1.212 +
1.213 +Goal "1<n ==> (EX l. primel l & nondec l & prod l = n)";
1.214 +by (etac (factor_exists RS exE) 1);
1.215 +by (blast_tac (claset() addSIs [ex_nondec_lemma]) 1);
1.216 +qed "nondec_factor_exists";
1.217 +
1.218 +
1.219 +(* --- Uniqueness --- *)
1.220 +
1.221 +Goal "p:prime ==> p dvd (prod xs) --> (EX m. m:set xs & p dvd m)";
1.222 +by (induct_tac "xs" 1);
1.223 +by (ALLGOALS Asm_full_simp_tac);
1.224 +by (etac prime_nd_one 1);
1.225 +by (rtac impI 1);
1.226 +by (dtac prime_dvd_mult 1);
1.227 +by Auto_tac;
1.228 +qed_spec_mp "prime_dvd_mult_list";
1.229 +
1.230 +Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
1.231 +\     ==> EX m. m :set ys & x dvd m";
1.232 +by (rtac prime_dvd_mult_list 1);
1.233 +by (etac hd_dvd_prod 2);
1.234 +by (asm_full_simp_tac (simpset() addsimps [primel_hd_tl]) 1);
1.235 +qed "hd_xs_dvd_prod";
1.236 +
1.237 +Goal "[| primel (x#xs); primel ys; m:set ys; x dvd m |] ==> x=m";
1.238 +by (rtac primes_eq 1);
1.239 +by (auto_tac (claset(), simpset() addsimps [primel_def,primel_hd_tl]));
1.240 +qed "prime_dvd_eq";
1.241 +
1.242 +Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] ==> x:set ys";
1.243 +by (ftac hd_xs_dvd_prod 1);
1.244 +by Auto_tac;
1.245 +by (dtac prime_dvd_eq 1);
1.246 +by Auto_tac;
1.247 +qed "hd_xs_eq_prod";
1.248 +
1.249 +Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
1.250 +\     ==> EX l. ys <~~> (x#l)";
1.251 +by (rtac exI 1);
1.252 +by (rtac perm_remove 1);
1.253 +by (etac hd_xs_eq_prod 1);
1.254 +by (ALLGOALS assume_tac);
1.255 +qed "perm_primel_ex";
1.256 +
1.257 +Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
1.258 +\     ==> prod xs < prod ys";
1.259 +by (auto_tac (claset() addIs [prod_mn_less_k,prime_g_one,primel_prod_gz],
1.261 +qed "primel_prod_less";
1.262 +
1.263 +Goal "[| primel xs; p*prod xs = p; p:prime |] ==> xs=[]";
1.264 +by (auto_tac (claset() addIs [primel_one_empty,mn_eq_m_one,prime_g_zero],
1.265 +	      simpset()));
1.266 +qed "prod_one_empty";
1.267 +
1.268 +Goal "[| ALL m. m < prod ys --> (ALL xs ys. primel xs & primel ys & \
1.269 +\        prod xs = prod ys & prod xs = m --> xs <~~> ys); primel list; \
1.270 +\        primel x; prod list = prod x; prod x < prod ys |] ==> x <~~> list";
1.271 +by (Asm_full_simp_tac 1);
1.272 +qed "uniq_ex_lemma";
1.273 +
1.274 +Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \
1.275 +\     --> xs <~~> ys)";
1.276 +by (induct_thm_tac nat_less_induct "n" 1);
1.277 +by Safe_tac;
1.278 +by (case_tac "xs" 1);
1.279 +by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);
1.280 +by (rtac (perm_primel_ex RS exE) 1);
1.281 +by (ALLGOALS Asm_full_simp_tac);
1.282 +by (rtac (perm.trans RS perm_sym) 1);
1.283 +by (assume_tac 1);
1.284 +by (rtac perm.Cons 1);
1.285 +by (case_tac "x=[]" 1);
1.286 +by (asm_full_simp_tac (simpset() addsimps [perm_sing_eq,primel_hd_tl]) 1);
1.287 +by (res_inst_tac [("p","a")] prod_one_empty 1);
1.288 +by (ALLGOALS Asm_full_simp_tac);
1.289 +by (etac uniq_ex_lemma 1);
1.290 +by (auto_tac (claset() addIs [primel_tl,perm_primel],
1.292 +by (res_inst_tac [("k","a"),("n","prod list"),("m","prod x")] mult_left_cancel 1);
1.293 +by (res_inst_tac [("x","a")] primel_prod_less 3);
1.294 +by (rtac prod_xy_prod 2);
1.295 +by (res_inst_tac [("s","prod ys")] trans 2);
1.296 +by (etac perm_prod 3);
1.297 +by (etac (perm_prod RS sym) 5);
1.298 +by (auto_tac (claset() addIs [perm_primel,prime_g_zero], simpset()));
1.299 +qed_spec_mp "factor_unique";
1.300 +
1.301 +Goal "[| xs <~~> ys; nondec xs; nondec ys |] ==> xs = ys";
1.302 +by (rtac trans 1);
1.303 +by (rtac trans 1);
1.304 +by (etac nondec_sort_eq 1);
1.305 +by (etac perm_sort_eq 1);
1.306 +by (etac (nondec_sort_eq RS sym) 1);
1.307 +qed "perm_nondec_unique";
1.308 +
1.309 +Goal "ALL n. 1<n --> (EX! l. primel l & nondec l & prod l = n)";
1.310 +by Safe_tac;
1.311 +by (etac nondec_factor_exists 1);
1.312 +by (rtac perm_nondec_unique 1);
1.313 +by (rtac factor_unique 1);
1.314 +by (ALLGOALS Asm_full_simp_tac);
1.315 +qed_spec_mp "unique_prime_factorization";
```
```     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/NumberTheory/Factorization.thy	Wed Sep 13 18:46:45 2000 +0200
2.3 @@ -0,0 +1,38 @@
2.4 +(*  Title:      HOL/ex/Factorization.thy
2.5 +    ID:         \$Id\$
2.6 +    Author:     Thomas Marthedal Rasmussen
2.7 +    Copyright   2000  University of Cambridge
2.8 +
2.9 +Fundamental Theorem of Arithmetic (unique factorization into primes)
2.10 +*)
2.11 +
2.12 +
2.13 +Factorization = Primes + Perm +
2.14 +
2.15 +consts
2.16 +  primel  :: nat list => bool
2.17 +  nondec  :: nat list => bool
2.18 +  prod    :: nat list => nat
2.19 +  oinsert :: [nat, nat list] => nat list
2.20 +  sort    :: nat list => nat list
2.21 +
2.22 +defs
2.23 +  primel_def "primel xs == set xs <= prime"
2.24 +
2.25 +primrec
2.26 +  "nondec []     = True"
2.27 +  "nondec (x#xs) = (case xs of [] => True | y#ys => x<=y & nondec xs)"
2.28 +
2.29 +primrec
2.30 +  "prod []     = 1"
2.31 +  "prod (x#xs) = x * prod xs"
2.32 +
2.33 +primrec
2.34 +  "oinsert x []     = [x]"
2.35 +  "oinsert x (y#ys) = (if x<=y then x#y#ys else y#oinsert x ys)"
2.36 +
2.37 +primrec
2.38 +  "sort []     = []"
2.39 +  "sort (x#xs) = oinsert x (sort xs)"
2.40 +
2.41 +end
2.42 \ No newline at end of file
```
```     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/NumberTheory/Fib.ML	Wed Sep 13 18:46:45 2000 +0200
3.3 @@ -0,0 +1,113 @@
3.4 +(*  Title:      HOL/ex/Fib
3.5 +    ID:         \$Id\$
3.6 +    Author:     Lawrence C Paulson
3.7 +    Copyright   1997  University of Cambridge
3.8 +
3.9 +Fibonacci numbers: proofs of laws taken from
3.10 +
3.11 +  R. L. Graham, D. E. Knuth, O. Patashnik.
3.12 +  Concrete Mathematics.
3.14 +*)
3.15 +
3.16 +
3.17 +(** The difficulty in these proofs is to ensure that the induction hypotheses
3.18 +    are applied before the definition of "fib".  Towards this end, the
3.19 +    "fib" equations are not added to the simpset and are applied very
3.20 +    selectively at first.
3.21 +**)
3.22 +
3.23 +Delsimps fib.Suc_Suc;
3.24 +
3.25 +val [fib_Suc_Suc] = fib.Suc_Suc;
3.26 +val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc;
3.27 +
3.28 +(*Concrete Mathematics, page 280*)
3.29 +Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
3.30 +by (induct_thm_tac fib.induct "n" 1);
3.31 +(*Simplify the LHS just enough to apply the induction hypotheses*)
3.32 +by (asm_full_simp_tac
3.33 +    (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3);
3.34 +by (ALLGOALS
3.38 +
3.39 +
3.40 +Goal "fib (Suc n) ~= 0";
3.41 +by (induct_thm_tac fib.induct "n" 1);
3.42 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc])));
3.43 +qed "fib_Suc_neq_0";
3.44 +
3.45 +(* Also add  0 < fib (Suc n) *)
3.46 +Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1];
3.47 +
3.48 +Goal "0<n ==> 0 < fib n";
3.49 +by (rtac (not0_implies_Suc RS exE) 1);
3.50 +by Auto_tac;
3.51 +qed "fib_gr_0";
3.52 +
3.53 +(*Concrete Mathematics, page 278: Cassini's identity.
3.54 +  It is much easier to prove using integers!*)
3.55 +Goal "int (fib (Suc (Suc n)) * fib n) = \
3.56 +\     (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \
3.57 +\                     else int (fib(Suc n) * fib(Suc n)) + #1)";
3.58 +by (induct_thm_tac fib.induct "n" 1);
3.59 +by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2);
3.60 +by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1);
3.61 +by (asm_full_simp_tac
3.63 +			  mod_Suc, zmult_int RS sym] @ zmult_ac) 1);
3.64 +qed "fib_Cassini";
3.65 +
3.66 +
3.67 +
3.68 +(** Towards Law 6.111 of Concrete Mathematics **)
3.69 +
3.70 +val gcd_induct = thm "gcd_induct";
3.71 +val gcd_commute = thm "gcd_commute";
3.73 +val gcd_non_0 = thm "gcd_non_0";
3.74 +val gcd_mult_cancel = thm "gcd_mult_cancel";
3.75 +
3.76 +
3.77 +Goal "gcd(fib n, fib (Suc n)) = 1";
3.78 +by (induct_thm_tac fib.induct "n" 1);
3.79 +by (asm_simp_tac (simpset() addsimps [gcd_commute, fib_Suc3]) 3);
3.80 +by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
3.81 +qed "gcd_fib_Suc_eq_1";
3.82 +
3.83 +val gcd_fib_commute =
3.84 +    read_instantiate_sg (sign_of thy) [("m", "fib m")] gcd_commute;
3.85 +
3.86 +Goal "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)";
3.87 +by (simp_tac (simpset() addsimps [gcd_fib_commute]) 1);
3.88 +by (case_tac "m=0" 1);
3.89 +by (Asm_simp_tac 1);
3.90 +by (clarify_tac (claset() addSDs [not0_implies_Suc]) 1);
3.93 +by (asm_simp_tac (simpset() addsimps [gcd_non_0 RS sym]) 1);
3.94 +by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1);
3.96 +
3.97 +Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
3.98 +by (rtac (gcd_fib_add RS sym RS trans) 1);
3.99 +by (Asm_simp_tac 1);
3.100 +qed "gcd_fib_diff";
3.101 +
3.102 +Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
3.103 +by (induct_thm_tac nat_less_induct "n" 1);
3.104 +by (stac mod_if 1);
3.105 +by (Asm_simp_tac 1);
3.106 +by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq,
3.107 +				      not_less_iff_le, diff_less]) 1);
3.108 +qed "gcd_fib_mod";
3.109 +
3.110 +(*Law 6.111*)
3.111 +Goal "fib(gcd(m,n)) = gcd(fib m, fib n)";
3.112 +by (induct_thm_tac gcd_induct "m n" 1);
3.113 +by (Asm_simp_tac 1);
3.114 +by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
3.115 +by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1);
3.116 +qed "fib_gcd";
```
```     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/NumberTheory/Fib.thy	Wed Sep 13 18:46:45 2000 +0200
4.3 @@ -0,0 +1,17 @@
4.4 +(*  Title:      ex/Fib
4.5 +    ID:         \$Id\$
4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4.7 +    Copyright   1997  University of Cambridge
4.8 +
4.9 +The Fibonacci function.  Demonstrates the use of recdef.
4.10 +*)
4.11 +
4.12 +Fib = Divides + Primes +
4.13 +
4.14 +consts fib  :: "nat => nat"
4.15 +recdef fib "less_than"
4.16 +  zero    "fib 0 = 0"
4.17 +  one     "fib 1 = 1"
4.18 +  Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)"
4.19 +
4.20 +end
```
```     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/NumberTheory/Primes.thy	Wed Sep 13 18:46:45 2000 +0200
5.3 @@ -0,0 +1,208 @@
5.4 +(*  Title:      HOL/ex/Primes.thy
5.5 +    ID:         \$Id\$
5.6 +    Author:     Christophe Tabacznyj and Lawrence C Paulson
5.7 +    Copyright   1996  University of Cambridge
5.8 +
5.9 +The Greatest Common Divisor and Euclid's algorithm
5.10 +
5.11 +See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992)
5.12 +*)
5.13 +
5.14 +theory Primes = Main:
5.15 +consts
5.16 +  gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
5.17 +
5.18 +recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
5.19 +    "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
5.20 +
5.21 +constdefs
5.22 +  is_gcd  :: "[nat,nat,nat]=>bool"        (*gcd as a relation*)
5.23 +    "is_gcd p m n == p dvd m  &  p dvd n  &
5.24 +                     (ALL d. d dvd m & d dvd n --> d dvd p)"
5.25 +
5.26 +  coprime :: "[nat,nat]=>bool"
5.27 +    "coprime m n == gcd(m,n) = 1"
5.28 +
5.29 +  prime   :: "nat set"
5.30 +    "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
5.31 +
5.32 +
5.33 +(************************************************)
5.34 +(** Greatest Common Divisor                    **)
5.35 +(************************************************)
5.36 +
5.37 +(*** Euclid's Algorithm ***)
5.38 +
5.39 +
5.40 +lemma gcd_induct:
5.41 +     "[| !!m. P m 0;
5.42 +         !!m n. [| 0<n;  P n (m mod n) |] ==> P m n
5.43 +      |] ==> P (m::nat) (n::nat)"
5.44 +  apply (induct_tac m n rule: gcd.induct)
5.45 +  apply (case_tac "n=0")
5.46 +  apply (simp_all)
5.47 +  done
5.48 +
5.49 +
5.50 +lemma gcd_0 [simp]: "gcd(m,0) = m"
5.51 +  apply (simp);
5.52 +  done
5.53 +
5.54 +lemma gcd_non_0: "0<n ==> gcd(m,n) = gcd (n, m mod n)"
5.55 +  apply (simp)
5.56 +  done;
5.57 +
5.58 +declare gcd.simps [simp del];
5.59 +
5.60 +lemma gcd_1 [simp]: "gcd(m,1) = 1"
5.61 +  apply (simp add: gcd_non_0)
5.62 +  done
5.63 +
5.64 +(*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
5.65 +lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"
5.66 +  apply (induct_tac m n rule: gcd_induct)
5.67 +  apply (simp_all add: gcd_non_0)
5.68 +  apply (blast dest: dvd_mod_imp_dvd)
5.69 +  done
5.70 +
5.71 +lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
5.72 +lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2];
5.73 +
5.74 +
5.75 +(*Maximality: for all m,n,k naturals,
5.76 +                if k divides m and k divides n then k divides gcd(m,n)*)
5.77 +lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
5.78 +  apply (induct_tac m n rule: gcd_induct)
5.79 +  apply (simp_all add: gcd_non_0 dvd_mod);
5.80 +  done;
5.81 +
5.82 +lemma gcd_greatest_iff [iff]: "k dvd gcd(m,n) = (k dvd m & k dvd n)"
5.83 +  apply (blast intro!: gcd_greatest intro: dvd_trans);
5.84 +  done;
5.85 +
5.86 +(*Function gcd yields the Greatest Common Divisor*)
5.87 +lemma is_gcd: "is_gcd (gcd(m,n)) m n"
5.88 +  apply (simp add: is_gcd_def gcd_greatest)
5.89 +  done
5.90 +
5.91 +(*uniqueness of GCDs*)
5.92 +lemma is_gcd_unique: "[| is_gcd m a b; is_gcd n a b |] ==> m=n"
5.93 +  apply (simp add: is_gcd_def);
5.94 +  apply (blast intro: dvd_anti_sym)
5.95 +  done
5.96 +
5.97 +lemma is_gcd_dvd: "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"
5.98 +  apply (auto simp add: is_gcd_def);
5.99 +  done
5.100 +
5.101 +(** Commutativity **)
5.102 +
5.103 +lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
5.104 +  apply (auto simp add: is_gcd_def);
5.105 +  done
5.106 +
5.107 +lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
5.108 +  apply (rule is_gcd_unique)
5.109 +  apply (rule is_gcd)
5.110 +  apply (subst is_gcd_commute)
5.111 +  apply (simp add: is_gcd)
5.112 +  done
5.113 +
5.114 +lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"
5.115 +  apply (rule is_gcd_unique)
5.116 +  apply (rule is_gcd)
5.117 +  apply (simp add: is_gcd_def);
5.118 +  apply (blast intro: dvd_trans);
5.119 +  done
5.120 +
5.121 +lemma gcd_0_left [simp]: "gcd(0,m) = m"
5.122 +  apply (simp add: gcd_commute [of 0])
5.123 +  done
5.124 +
5.125 +lemma gcd_1_left [simp]: "gcd(1,m) = 1"
5.126 +  apply (simp add: gcd_commute [of 1])
5.127 +  done
5.128 +
5.129 +
5.130 +(** Multiplication laws **)
5.131 +
5.132 +(*Davenport, page 27*)
5.133 +lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)"
5.134 +  apply (induct_tac m n rule: gcd_induct)
5.135 +  apply (simp)
5.136 +  apply (case_tac "k=0")
5.137 +  apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
5.138 +  done
5.139 +
5.140 +lemma gcd_mult [simp]: "gcd(k, k*n) = k"
5.141 +  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, THEN sym])
5.142 +  done
5.143 +
5.144 +lemma gcd_self [simp]: "gcd(k,k) = k"
5.145 +  apply (rule gcd_mult [of k 1, simplified])
5.146 +  done
5.147 +
5.148 +lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
5.149 +  apply (insert gcd_mult_distrib2 [of m k n])
5.150 +  apply (simp)
5.151 +  apply (erule_tac t="m" in ssubst);
5.152 +  apply (simp)
5.153 +  done
5.154 +
5.155 +lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> k dvd (m*n) = k dvd m";
5.156 +  apply (blast intro: relprime_dvd_mult dvd_trans)
5.157 +  done
5.158 +
5.159 +lemma prime_imp_relprime: "[| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1"
5.160 +  apply (auto simp add: prime_def)
5.161 +  apply (drule_tac x="gcd(p,n)" in spec)
5.162 +  apply auto
5.163 +  apply (insert gcd_dvd2 [of p n])
5.164 +  apply (simp)
5.165 +  done
5.166 +
5.167 +(*This theorem leads immediately to a proof of the uniqueness of factorization.
5.168 +  If p divides a product of primes then it is one of those primes.*)
5.169 +lemma prime_dvd_mult: "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"
5.170 +  apply (blast intro: relprime_dvd_mult prime_imp_relprime)
5.171 +  done
5.172 +
5.173 +
5.175 +
5.176 +lemma gcd_add1 [simp]: "gcd(m+n, n) = gcd(m,n)"
5.177 +  apply (case_tac "n=0")
5.178 +  apply (simp_all add: gcd_non_0)
5.179 +  done
5.180 +
5.181 +lemma gcd_add2 [simp]: "gcd(m, m+n) = gcd(m,n)"
5.182 +  apply (rule gcd_commute [THEN trans])
5.185 +  apply (rule gcd_commute)
5.186 +  done
5.187 +
5.188 +lemma gcd_add2' [simp]: "gcd(m, n+m) = gcd(m,n)"
5.191 +  done
5.192 +
5.193 +lemma gcd_add_mult: "gcd(m, k*m+n) = gcd(m,n)"
5.194 +  apply (induct_tac "k")
5.196 +  done
5.197 +
5.198 +
5.199 +(** More multiplication laws **)
5.200 +
5.201 +lemma gcd_mult_cancel: "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"
5.202 +  apply (rule dvd_anti_sym)
5.203 +   apply (rule gcd_greatest)
5.204 +    apply (rule_tac n="k" in relprime_dvd_mult)
5.205 +     apply (simp add: gcd_assoc)
5.206 +     apply (simp add: gcd_commute)
5.207 +    apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
5.208 +  apply (blast intro: gcd_dvd1 dvd_trans);
5.209 +  done
5.210 +
5.211 +end
```
```     6.1 --- a/src/HOL/NumberTheory/ROOT.ML	Wed Sep 13 18:46:09 2000 +0200
6.2 +++ b/src/HOL/NumberTheory/ROOT.ML	Wed Sep 13 18:46:45 2000 +0200
6.3 @@ -6,7 +6,10 @@
6.4  Number theory developments by Thomas M Rasmussen
6.5  *)
6.6
6.7 -use_thy "Chinese";
6.8 -use_thy "EulerFermat";
6.9 -use_thy "WilsonRuss";
6.10 -use_thy "WilsonBij";
6.11 +time_use_thy "Primes";
6.12 +time_use_thy "Fib";
6.13 +with_path "../Induct" time_use_thy "Factorization";
6.14 +time_use_thy "Chinese";
6.15 +time_use_thy "EulerFermat";
6.16 +time_use_thy "WilsonRuss";
6.17 +time_use_thy "WilsonBij";
```