moved Primes, Fib, Factorization from HOL/ex
authorpaulson
Wed Sep 13 18:46:45 2000 +0200 (2000-09-13)
changeset 99442a705d1af4dc
parent 9943 55c82decf3f4
child 9945 a0efbd7c88dc
moved Primes, Fib, Factorization from HOL/ex
src/HOL/NumberTheory/Factorization.ML
src/HOL/NumberTheory/Factorization.thy
src/HOL/NumberTheory/Fib.ML
src/HOL/NumberTheory/Fib.thy
src/HOL/NumberTheory/Primes.thy
src/HOL/NumberTheory/ROOT.ML
     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.171 +	               addEs [perm_subst_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.260 +              simpset() addsimps [primel_hd_tl]));
   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.291 +	      simpset() addsimps [primel_hd_tl]));
   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.13 +  (Addison-Wesley, 1989)
    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.35 +    (asm_simp_tac (simpset() addsimps 
    3.36 +		   ([fib_Suc_Suc, add_mult_distrib, add_mult_distrib2]))));
    3.37 +qed "fib_add";
    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.62 +     (simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
    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.72 +val gcd_add2 = thm "gcd_add2";
    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.91 +by (simp_tac (simpset() addsimps [fib_add]) 1);
    3.92 +by (asm_simp_tac (simpset() addsimps [add_commute, gcd_non_0]) 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.95 +qed "gcd_fib_add";
    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.174 +(** Addition laws **)
   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.183 +  apply (subst add_commute)
   5.184 +  apply (simp add: gcd_add1)
   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.189 +  apply (subst add_commute)
   5.190 +  apply (rule gcd_add2)
   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.195 +  apply (simp_all add: gcd_add2 add_assoc)
   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";