moved Primes, Fib, Factorization to HOL/NumberTheory
authorpaulson
Wed Sep 13 18:45:10 2000 +0200 (2000-09-13)
changeset 994287f0809a06a9
parent 9941 fe05af7ec816
child 9943 55c82decf3f4
moved Primes, Fib, Factorization to HOL/NumberTheory
src/HOL/IsaMakefile
src/HOL/Isar_examples/ROOT.ML
src/HOL/ex/Factorization.ML
src/HOL/ex/Factorization.thy
src/HOL/ex/Fib.ML
src/HOL/ex/Fib.thy
src/HOL/ex/Primes.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Sep 12 22:13:23 2000 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Sep 13 18:45:10 2000 +0200
     1.3 @@ -173,6 +173,8 @@
     1.4  HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
     1.5  
     1.6  $(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \
     1.7 +  NumberTheory/Fib.ML NumberTheory/Fib.thy NumberTheory/Primes.thy \
     1.8 +  NumberTheory/Factorization.ML NumberTheory/Factorization.thy \
     1.9    NumberTheory/BijectionRel.ML NumberTheory/BijectionRel.thy \
    1.10    NumberTheory/Chinese.ML NumberTheory/Chinese.thy \
    1.11    NumberTheory/EulerFermat.ML NumberTheory/EulerFermat.thy \
    1.12 @@ -430,8 +432,6 @@
    1.13  
    1.14  $(LOG)/HOL-ex.gz: $(OUT)/HOL  ex/AVL.ML ex/AVL.thy ex/BT.ML ex/BT.thy \
    1.15    ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML ex/NatSum.thy \
    1.16 -  ex/Fib.ML ex/Fib.thy ex/Primes.thy \
    1.17 -  ex/Factorization.ML ex/Factorization.thy \
    1.18    ex/Primrec.ML ex/Primrec.thy \
    1.19    ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
    1.20    ex/ROOT.ML ex/Recdefs.ML ex/Recdefs.thy ex/cla.ML \
     2.1 --- a/src/HOL/Isar_examples/ROOT.ML	Tue Sep 12 22:13:23 2000 +0200
     2.2 +++ b/src/HOL/Isar_examples/ROOT.ML	Wed Sep 13 18:45:10 2000 +0200
     2.3 @@ -13,8 +13,8 @@
     2.4  time_use_thy "Summation";
     2.5  time_use_thy "KnasterTarski";
     2.6  time_use_thy "MutilatedCheckerboard";
     2.7 -with_path "../Induct" time_use_thy "MultisetOrder";
     2.8 -with_path "../W0" time_use_thy "W_correct";
     2.9 -with_path "../ex" time_use_thy "Fibonacci";
    2.10 +with_path "../Induct"       time_use_thy "MultisetOrder";
    2.11 +with_path "../W0"           time_use_thy "W_correct";
    2.12 +with_path "../NumberTheory" time_use_thy "Fibonacci";
    2.13  time_use_thy "Puzzle";
    2.14  time_use_thy "NestedDatatype";
     3.1 --- a/src/HOL/ex/Factorization.ML	Tue Sep 12 22:13:23 2000 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,312 +0,0 @@
     3.4 -(*  Title:      HOL/ex/Factorization.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Thomas Marthedal Rasmussen
     3.7 -    Copyright   2000  University of Cambridge
     3.8 -
     3.9 -Fundamental Theorem of Arithmetic (unique factorization into primes)
    3.10 -*)
    3.11 -
    3.12 -val prime_def = thm "prime_def";
    3.13 -val prime_dvd_mult = thm "prime_dvd_mult";
    3.14 -
    3.15 -
    3.16 -(* --- Arithmetic --- *)
    3.17 -
    3.18 -Goal "!!m::nat. [| m ~= m*k; m ~= 1 |] ==> 1<m";
    3.19 -by (case_tac "m" 1);
    3.20 -by Auto_tac;
    3.21 -qed "one_less_m";
    3.22 -
    3.23 -Goal "!!m::nat. [| m ~= m*k; 1<m*k |] ==> 1<k";
    3.24 -by (case_tac "k" 1);
    3.25 -by Auto_tac;
    3.26 -qed "one_less_k";
    3.27 -
    3.28 -Goal "!!m::nat. [| 0<k; k*n=k*m |] ==> n=m";
    3.29 -by Auto_tac;
    3.30 -qed "mult_left_cancel";
    3.31 -
    3.32 -Goal "!!m::nat. [| 0<m; m*n = m |] ==> n=1";
    3.33 -by (case_tac "n" 1);
    3.34 -by Auto_tac;
    3.35 -qed "mn_eq_m_one";
    3.36 -
    3.37 -Goal "!!m::nat. [| 0<n; 0<k |] ==> 1<m --> m*n = k --> n<k";
    3.38 -by (induct_tac "m" 1);
    3.39 -by Auto_tac;
    3.40 -qed_spec_mp "prod_mn_less_k";
    3.41 -
    3.42 -
    3.43 -(* --- Prime List & Product --- *)
    3.44 -
    3.45 -Goal "prod (xs @ ys) = prod xs * prod ys"; 
    3.46 -by (induct_tac "xs" 1);
    3.47 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [mult_assoc])));
    3.48 -qed "prod_append";
    3.49 -
    3.50 -Goal "prod (x#xs) = prod (y#ys) ==> x*prod xs = y*prod ys";
    3.51 -by Auto_tac;
    3.52 -qed "prod_xy_prod";
    3.53 -
    3.54 -Goalw [primel_def] "primel (xs @ ys) = (primel xs & primel ys)";
    3.55 -by Auto_tac;
    3.56 -qed "primel_append";
    3.57 -
    3.58 -Goalw [primel_def] "n:prime ==> primel [n] & prod [n] = n";
    3.59 -by Auto_tac;
    3.60 -qed "prime_primel";
    3.61 -
    3.62 -Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)";
    3.63 -by Auto_tac;
    3.64 -by (case_tac "k" 1);
    3.65 -by Auto_tac;
    3.66 -qed "prime_nd_one";
    3.67 -
    3.68 -Goalw [dvd_def] "[| prod (x#xs) = prod ys |] ==> x dvd (prod ys)";
    3.69 -by (rtac exI 1);
    3.70 -by (rtac sym 1);
    3.71 -by (Asm_full_simp_tac 1);
    3.72 -qed "hd_dvd_prod";
    3.73 -
    3.74 -Goalw [primel_def] "primel (x#xs) ==> primel xs";
    3.75 -by Auto_tac;
    3.76 -qed "primel_tl";
    3.77 -
    3.78 -Goalw [primel_def] "(primel (x#xs)) = (x:prime & primel xs)"; 
    3.79 -by Auto_tac;
    3.80 -qed "primel_hd_tl";
    3.81 -
    3.82 -Goalw [prime_def] "[| p:prime; q:prime; p dvd q |] ==> p=q";
    3.83 -by Auto_tac;
    3.84 -qed "primes_eq";
    3.85 -
    3.86 -Goalw [primel_def,prime_def] "[| primel xs; prod xs = 1 |] ==> xs = []";
    3.87 -by (case_tac "xs" 1);
    3.88 -by (ALLGOALS Asm_full_simp_tac);
    3.89 -qed "primel_one_empty";
    3.90 -
    3.91 -Goalw [prime_def] "p:prime ==> 1<p";
    3.92 -by Auto_tac;
    3.93 -qed "prime_g_one";
    3.94 -
    3.95 -Goalw [prime_def] "p:prime ==> 0<p";
    3.96 -by Auto_tac;
    3.97 -qed "prime_g_zero";
    3.98 -
    3.99 -Goalw [primel_def,prime_def] "primel xs --> xs ~= [] --> 1 < prod xs";
   3.100 -by (induct_tac "xs" 1);
   3.101 -by (auto_tac (claset() addEs [one_less_mult], simpset()));
   3.102 -qed_spec_mp "primel_nempty_g_one";
   3.103 -
   3.104 -Goalw [primel_def,prime_def] "primel xs --> 0 < prod xs"; 
   3.105 -by (induct_tac "xs" 1);
   3.106 -by Auto_tac;
   3.107 -qed_spec_mp "primel_prod_gz";
   3.108 -
   3.109 -
   3.110 -(* --- Sorting --- *)
   3.111 -
   3.112 -Goal "nondec xs --> nondec (oinsert x xs)";
   3.113 -by (induct_tac "xs" 1);
   3.114 -by (case_tac "list" 2);
   3.115 -by (ALLGOALS(asm_full_simp_tac (simpset()delcongs[thm"list.weak_case_cong"])));
   3.116 -qed_spec_mp "nondec_oinsert";
   3.117 -
   3.118 -Goal "nondec (sort xs)";
   3.119 -by (induct_tac "xs" 1);
   3.120 -by (ALLGOALS (Asm_full_simp_tac));
   3.121 -by (etac nondec_oinsert 1);
   3.122 -qed "nondec_sort";
   3.123 -
   3.124 -Goal "[| x<=y; l=y#ys |]  ==> x#l = oinsert x l";
   3.125 -by (ALLGOALS Asm_full_simp_tac);
   3.126 -qed "x_less_y_oinsert";
   3.127 -
   3.128 -Goal "nondec xs --> xs = sort xs";
   3.129 -by (induct_tac "xs" 1);
   3.130 -by Safe_tac;
   3.131 -by (ALLGOALS Asm_full_simp_tac);
   3.132 -by (case_tac "list" 1);
   3.133 -by (ALLGOALS Asm_full_simp_tac);
   3.134 -by (case_tac "list" 1);
   3.135 -by (Asm_full_simp_tac 1);
   3.136 -by (res_inst_tac [("y","aa"),("ys","lista")] x_less_y_oinsert 1); 
   3.137 -by (ALLGOALS Asm_full_simp_tac);
   3.138 -qed_spec_mp "nondec_sort_eq";
   3.139 -
   3.140 -Goal "oinsert x (oinsert y l) = oinsert y (oinsert x l)";
   3.141 -by (induct_tac "l" 1);
   3.142 -by Auto_tac;
   3.143 -qed "oinsert_x_y";
   3.144 -
   3.145 -
   3.146 -(* --- Permutation --- *)
   3.147 -
   3.148 -Goalw [primel_def] "xs <~~> ys ==> primel xs --> primel ys";
   3.149 -by (etac perm.induct 1);
   3.150 -by (ALLGOALS Asm_simp_tac);
   3.151 -qed_spec_mp "perm_primel";
   3.152 -
   3.153 -Goal "xs <~~> ys ==> prod xs = prod ys";
   3.154 -by (etac perm.induct 1);
   3.155 -by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));
   3.156 -qed_spec_mp "perm_prod";
   3.157 -
   3.158 -Goal "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"; 
   3.159 -by (etac perm.induct 1);
   3.160 -by Auto_tac;
   3.161 -qed "perm_subst_oinsert";
   3.162 -
   3.163 -Goal "x#xs <~~> oinsert x xs";
   3.164 -by (induct_tac "xs" 1);
   3.165 -by Auto_tac;
   3.166 -qed "perm_oinsert";
   3.167 -
   3.168 -Goal "xs <~~> sort xs";
   3.169 -by (induct_tac "xs" 1);
   3.170 -by (auto_tac (claset() addIs [perm_oinsert] 
   3.171 -	               addEs [perm_subst_oinsert],
   3.172 -              simpset()));
   3.173 -qed "perm_sort";
   3.174 -
   3.175 -Goal "xs <~~> ys ==> sort xs = sort ys";
   3.176 -by (etac perm.induct 1);
   3.177 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [oinsert_x_y])));
   3.178 -qed "perm_sort_eq";
   3.179 -
   3.180 -
   3.181 -(* --- Existence --- *)
   3.182 -
   3.183 -Goal "primel xs ==> EX ys. primel ys & nondec ys & prod ys = prod xs";
   3.184 -by (blast_tac (claset() addIs [nondec_sort, perm_prod,perm_primel,perm_sort,
   3.185 -			       perm_sym]) 1);
   3.186 -qed "ex_nondec_lemma";
   3.187 -
   3.188 -Goalw [prime_def,dvd_def]
   3.189 -     "1<n & n~:prime --> (EX m k.1<m & 1<k & m<n & k<n & n=m*k)";
   3.190 -by (auto_tac (claset() addIs [n_less_m_mult_n, n_less_n_mult_m,
   3.191 -			      one_less_m, one_less_k], 
   3.192 -	      simpset()));
   3.193 -qed_spec_mp "not_prime_ex_mk";
   3.194 -
   3.195 -Goal "[| primel xs; primel ys |] \
   3.196 -\     ==> EX l. primel l & prod l = prod xs * prod ys";
   3.197 -by (rtac exI 1);
   3.198 -by Safe_tac;
   3.199 -by (rtac prod_append 2);
   3.200 -by (asm_simp_tac (simpset() addsimps [primel_append]) 1);
   3.201 -qed "split_primel";
   3.202 -
   3.203 -Goal "1<n --> (EX l. primel l & prod l = n)"; 
   3.204 -by (induct_thm_tac nat_less_induct "n" 1);
   3.205 -by (rtac impI 1);
   3.206 -by (case_tac "n:prime" 1);
   3.207 -by (rtac exI 1);
   3.208 -by (etac prime_primel 1);
   3.209 -by (cut_inst_tac [("n","n")] not_prime_ex_mk 1);
   3.210 -by (auto_tac (claset() addSIs [split_primel], simpset()));
   3.211 -qed_spec_mp "factor_exists";
   3.212 -
   3.213 -Goal "1<n ==> (EX l. primel l & nondec l & prod l = n)"; 
   3.214 -by (etac (factor_exists RS exE) 1);
   3.215 -by (blast_tac (claset() addSIs [ex_nondec_lemma]) 1);
   3.216 -qed "nondec_factor_exists";
   3.217 -
   3.218 -
   3.219 -(* --- Uniqueness --- *)
   3.220 -
   3.221 -Goal "p:prime ==> p dvd (prod xs) --> (EX m. m:set xs & p dvd m)";
   3.222 -by (induct_tac "xs" 1);
   3.223 -by (ALLGOALS Asm_full_simp_tac);
   3.224 -by (etac prime_nd_one 1);
   3.225 -by (rtac impI 1);
   3.226 -by (dtac prime_dvd_mult 1);
   3.227 -by Auto_tac;
   3.228 -qed_spec_mp "prime_dvd_mult_list";
   3.229 -
   3.230 -Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
   3.231 -\     ==> EX m. m :set ys & x dvd m";
   3.232 -by (rtac prime_dvd_mult_list 1);
   3.233 -by (etac hd_dvd_prod 2);
   3.234 -by (asm_full_simp_tac (simpset() addsimps [primel_hd_tl]) 1);
   3.235 -qed "hd_xs_dvd_prod";
   3.236 -
   3.237 -Goal "[| primel (x#xs); primel ys; m:set ys; x dvd m |] ==> x=m";
   3.238 -by (rtac primes_eq 1);
   3.239 -by (auto_tac (claset(), simpset() addsimps [primel_def,primel_hd_tl]));
   3.240 -qed "prime_dvd_eq";
   3.241 -
   3.242 -Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] ==> x:set ys";
   3.243 -by (ftac hd_xs_dvd_prod 1);
   3.244 -by Auto_tac;
   3.245 -by (dtac prime_dvd_eq 1);
   3.246 -by Auto_tac;
   3.247 -qed "hd_xs_eq_prod";
   3.248 -
   3.249 -Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
   3.250 -\     ==> EX l. ys <~~> (x#l)";
   3.251 -by (rtac exI 1);
   3.252 -by (rtac perm_remove 1);
   3.253 -by (etac hd_xs_eq_prod 1);
   3.254 -by (ALLGOALS assume_tac);
   3.255 -qed "perm_primel_ex";
   3.256 -
   3.257 -Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
   3.258 -\     ==> prod xs < prod ys";
   3.259 -by (auto_tac (claset() addIs [prod_mn_less_k,prime_g_one,primel_prod_gz],
   3.260 -              simpset() addsimps [primel_hd_tl]));
   3.261 -qed "primel_prod_less";
   3.262 -
   3.263 -Goal "[| primel xs; p*prod xs = p; p:prime |] ==> xs=[]";
   3.264 -by (auto_tac (claset() addIs [primel_one_empty,mn_eq_m_one,prime_g_zero], 
   3.265 -	      simpset()));
   3.266 -qed "prod_one_empty";
   3.267 -
   3.268 -Goal "[| ALL m. m < prod ys --> (ALL xs ys. primel xs & primel ys & \
   3.269 -\        prod xs = prod ys & prod xs = m --> xs <~~> ys); primel list; \
   3.270 -\        primel x; prod list = prod x; prod x < prod ys |] ==> x <~~> list";
   3.271 -by (Asm_full_simp_tac 1);
   3.272 -qed "uniq_ex_lemma";
   3.273 -
   3.274 -Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \
   3.275 -\     --> xs <~~> ys)";
   3.276 -by (induct_thm_tac nat_less_induct "n" 1);
   3.277 -by Safe_tac;
   3.278 -by (case_tac "xs" 1);
   3.279 -by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);
   3.280 -by (rtac (perm_primel_ex RS exE) 1);
   3.281 -by (ALLGOALS Asm_full_simp_tac);
   3.282 -by (rtac (perm.trans RS perm_sym) 1);
   3.283 -by (assume_tac 1);
   3.284 -by (rtac perm.Cons 1);
   3.285 -by (case_tac "x=[]" 1);
   3.286 -by (asm_full_simp_tac (simpset() addsimps [perm_sing_eq,primel_hd_tl]) 1);
   3.287 -by (res_inst_tac [("p","a")] prod_one_empty 1);
   3.288 -by (ALLGOALS Asm_full_simp_tac);
   3.289 -by (etac uniq_ex_lemma 1);
   3.290 -by (auto_tac (claset() addIs [primel_tl,perm_primel],
   3.291 -	      simpset() addsimps [primel_hd_tl]));
   3.292 -by (res_inst_tac [("k","a"),("n","prod list"),("m","prod x")] mult_left_cancel 1);
   3.293 -by (res_inst_tac [("x","a")] primel_prod_less 3);
   3.294 -by (rtac prod_xy_prod 2);
   3.295 -by (res_inst_tac [("s","prod ys")] trans 2);
   3.296 -by (etac perm_prod 3);
   3.297 -by (etac (perm_prod RS sym) 5); 
   3.298 -by (auto_tac (claset() addIs [perm_primel,prime_g_zero], simpset()));
   3.299 -qed_spec_mp "factor_unique";
   3.300 -
   3.301 -Goal "[| xs <~~> ys; nondec xs; nondec ys |] ==> xs = ys"; 
   3.302 -by (rtac trans 1);
   3.303 -by (rtac trans 1);
   3.304 -by (etac nondec_sort_eq 1);
   3.305 -by (etac perm_sort_eq 1);
   3.306 -by (etac (nondec_sort_eq RS sym) 1);
   3.307 -qed "perm_nondec_unique";
   3.308 -
   3.309 -Goal "ALL n. 1<n --> (EX! l. primel l & nondec l & prod l = n)";
   3.310 -by Safe_tac;
   3.311 -by (etac nondec_factor_exists 1);
   3.312 -by (rtac perm_nondec_unique 1);
   3.313 -by (rtac factor_unique 1);
   3.314 -by (ALLGOALS Asm_full_simp_tac);
   3.315 -qed_spec_mp "unique_prime_factorization";
     4.1 --- a/src/HOL/ex/Factorization.thy	Tue Sep 12 22:13:23 2000 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,38 +0,0 @@
     4.4 -(*  Title:      HOL/ex/Factorization.thy
     4.5 -    ID:         $Id$
     4.6 -    Author:     Thomas Marthedal Rasmussen
     4.7 -    Copyright   2000  University of Cambridge
     4.8 -
     4.9 -Fundamental Theorem of Arithmetic (unique factorization into primes)
    4.10 -*)
    4.11 -
    4.12 -
    4.13 -Factorization = Primes + Perm +
    4.14 -
    4.15 -consts
    4.16 -  primel  :: nat list => bool 
    4.17 -  nondec  :: nat list => bool 
    4.18 -  prod    :: nat list => nat
    4.19 -  oinsert :: [nat, nat list] => nat list
    4.20 -  sort    :: nat list => nat list
    4.21 -
    4.22 -defs
    4.23 -  primel_def "primel xs == set xs <= prime"
    4.24 -
    4.25 -primrec
    4.26 -  "nondec []     = True"
    4.27 -  "nondec (x#xs) = (case xs of [] => True | y#ys => x<=y & nondec xs)"
    4.28 -
    4.29 -primrec
    4.30 -  "prod []     = 1"
    4.31 -  "prod (x#xs) = x * prod xs"
    4.32 -
    4.33 -primrec
    4.34 -  "oinsert x []     = [x]"
    4.35 -  "oinsert x (y#ys) = (if x<=y then x#y#ys else y#oinsert x ys)"
    4.36 -
    4.37 -primrec
    4.38 -  "sort []     = []"
    4.39 -  "sort (x#xs) = oinsert x (sort xs)"  
    4.40 -
    4.41 -end
    4.42 \ No newline at end of file
     5.1 --- a/src/HOL/ex/Fib.ML	Tue Sep 12 22:13:23 2000 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,113 +0,0 @@
     5.4 -(*  Title:      HOL/ex/Fib
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson
     5.7 -    Copyright   1997  University of Cambridge
     5.8 -
     5.9 -Fibonacci numbers: proofs of laws taken from
    5.10 -
    5.11 -  R. L. Graham, D. E. Knuth, O. Patashnik.
    5.12 -  Concrete Mathematics.
    5.13 -  (Addison-Wesley, 1989)
    5.14 -*)
    5.15 -
    5.16 -
    5.17 -(** The difficulty in these proofs is to ensure that the induction hypotheses
    5.18 -    are applied before the definition of "fib".  Towards this end, the 
    5.19 -    "fib" equations are not added to the simpset and are applied very 
    5.20 -    selectively at first.
    5.21 -**)
    5.22 -
    5.23 -Delsimps fib.Suc_Suc;
    5.24 -
    5.25 -val [fib_Suc_Suc] = fib.Suc_Suc;
    5.26 -val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc;
    5.27 -
    5.28 -(*Concrete Mathematics, page 280*)
    5.29 -Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
    5.30 -by (induct_thm_tac fib.induct "n" 1);
    5.31 -(*Simplify the LHS just enough to apply the induction hypotheses*)
    5.32 -by (asm_full_simp_tac
    5.33 -    (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3);
    5.34 -by (ALLGOALS 
    5.35 -    (asm_simp_tac (simpset() addsimps 
    5.36 -		   ([fib_Suc_Suc, add_mult_distrib, add_mult_distrib2]))));
    5.37 -qed "fib_add";
    5.38 -
    5.39 -
    5.40 -Goal "fib (Suc n) ~= 0";
    5.41 -by (induct_thm_tac fib.induct "n" 1);
    5.42 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc])));
    5.43 -qed "fib_Suc_neq_0";
    5.44 -
    5.45 -(* Also add  0 < fib (Suc n) *)
    5.46 -Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1];
    5.47 -
    5.48 -Goal "0<n ==> 0 < fib n";
    5.49 -by (rtac (not0_implies_Suc RS exE) 1);
    5.50 -by Auto_tac;
    5.51 -qed "fib_gr_0";
    5.52 -
    5.53 -(*Concrete Mathematics, page 278: Cassini's identity.
    5.54 -  It is much easier to prove using integers!*)
    5.55 -Goal "int (fib (Suc (Suc n)) * fib n) = \
    5.56 -\     (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \
    5.57 -\                     else int (fib(Suc n) * fib(Suc n)) + #1)";
    5.58 -by (induct_thm_tac fib.induct "n" 1);
    5.59 -by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2);
    5.60 -by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1);
    5.61 -by (asm_full_simp_tac
    5.62 -     (simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
    5.63 -			  mod_Suc, zmult_int RS sym] @ zmult_ac) 1);
    5.64 -qed "fib_Cassini";
    5.65 -
    5.66 -
    5.67 -
    5.68 -(** Towards Law 6.111 of Concrete Mathematics **)
    5.69 -
    5.70 -val gcd_induct = thm "gcd_induct";
    5.71 -val gcd_commute = thm "gcd_commute";
    5.72 -val gcd_add2 = thm "gcd_add2";
    5.73 -val gcd_non_0 = thm "gcd_non_0";
    5.74 -val gcd_mult_cancel = thm "gcd_mult_cancel";
    5.75 -
    5.76 -
    5.77 -Goal "gcd(fib n, fib (Suc n)) = 1";
    5.78 -by (induct_thm_tac fib.induct "n" 1);
    5.79 -by (asm_simp_tac (simpset() addsimps [gcd_commute, fib_Suc3]) 3);
    5.80 -by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
    5.81 -qed "gcd_fib_Suc_eq_1"; 
    5.82 -
    5.83 -val gcd_fib_commute = 
    5.84 -    read_instantiate_sg (sign_of thy) [("m", "fib m")] gcd_commute;
    5.85 -
    5.86 -Goal "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)";
    5.87 -by (simp_tac (simpset() addsimps [gcd_fib_commute]) 1);
    5.88 -by (case_tac "m=0" 1);
    5.89 -by (Asm_simp_tac 1);
    5.90 -by (clarify_tac (claset() addSDs [not0_implies_Suc]) 1);
    5.91 -by (simp_tac (simpset() addsimps [fib_add]) 1);
    5.92 -by (asm_simp_tac (simpset() addsimps [add_commute, gcd_non_0]) 1);
    5.93 -by (asm_simp_tac (simpset() addsimps [gcd_non_0 RS sym]) 1);
    5.94 -by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1);
    5.95 -qed "gcd_fib_add";
    5.96 -
    5.97 -Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
    5.98 -by (rtac (gcd_fib_add RS sym RS trans) 1);
    5.99 -by (Asm_simp_tac 1);
   5.100 -qed "gcd_fib_diff";
   5.101 -
   5.102 -Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
   5.103 -by (induct_thm_tac nat_less_induct "n" 1);
   5.104 -by (stac mod_if 1);
   5.105 -by (Asm_simp_tac 1);
   5.106 -by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq, 
   5.107 -				      not_less_iff_le, diff_less]) 1);
   5.108 -qed "gcd_fib_mod";
   5.109 -
   5.110 -(*Law 6.111*)
   5.111 -Goal "fib(gcd(m,n)) = gcd(fib m, fib n)";
   5.112 -by (induct_thm_tac gcd_induct "m n" 1);
   5.113 -by (Asm_simp_tac 1);
   5.114 -by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
   5.115 -by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1);
   5.116 -qed "fib_gcd";
     6.1 --- a/src/HOL/ex/Fib.thy	Tue Sep 12 22:13:23 2000 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,17 +0,0 @@
     6.4 -(*  Title:      ex/Fib
     6.5 -    ID:         $Id$
     6.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 -    Copyright   1997  University of Cambridge
     6.8 -
     6.9 -The Fibonacci function.  Demonstrates the use of recdef.
    6.10 -*)
    6.11 -
    6.12 -Fib = Divides + Primes +
    6.13 -
    6.14 -consts fib  :: "nat => nat"
    6.15 -recdef fib "less_than"
    6.16 -  zero    "fib 0 = 0"
    6.17 -  one     "fib 1 = 1"
    6.18 -  Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)"
    6.19 -
    6.20 -end
     7.1 --- a/src/HOL/ex/Primes.thy	Tue Sep 12 22:13:23 2000 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,208 +0,0 @@
     7.4 -(*  Title:      HOL/ex/Primes.thy
     7.5 -    ID:         $Id$
     7.6 -    Author:     Christophe Tabacznyj and Lawrence C Paulson
     7.7 -    Copyright   1996  University of Cambridge
     7.8 -
     7.9 -The Greatest Common Divisor and Euclid's algorithm
    7.10 -
    7.11 -See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992)
    7.12 -*)
    7.13 -
    7.14 -theory Primes = Main:
    7.15 -consts
    7.16 -  gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
    7.17 -
    7.18 -recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
    7.19 -    "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
    7.20 -
    7.21 -constdefs
    7.22 -  is_gcd  :: "[nat,nat,nat]=>bool"        (*gcd as a relation*)
    7.23 -    "is_gcd p m n == p dvd m  &  p dvd n  &
    7.24 -                     (ALL d. d dvd m & d dvd n --> d dvd p)"
    7.25 -
    7.26 -  coprime :: "[nat,nat]=>bool"
    7.27 -    "coprime m n == gcd(m,n) = 1"
    7.28 -
    7.29 -  prime   :: "nat set"
    7.30 -    "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
    7.31 -
    7.32 -
    7.33 -(************************************************)
    7.34 -(** Greatest Common Divisor                    **)
    7.35 -(************************************************)
    7.36 -
    7.37 -(*** Euclid's Algorithm ***)
    7.38 -
    7.39 -
    7.40 -lemma gcd_induct:
    7.41 -     "[| !!m. P m 0;     
    7.42 -         !!m n. [| 0<n;  P n (m mod n) |] ==> P m n  
    7.43 -      |] ==> P (m::nat) (n::nat)"
    7.44 -  apply (induct_tac m n rule: gcd.induct)
    7.45 -  apply (case_tac "n=0")
    7.46 -  apply (simp_all)
    7.47 -  done
    7.48 -
    7.49 -
    7.50 -lemma gcd_0 [simp]: "gcd(m,0) = m"
    7.51 -  apply (simp);
    7.52 -  done
    7.53 -
    7.54 -lemma gcd_non_0: "0<n ==> gcd(m,n) = gcd (n, m mod n)"
    7.55 -  apply (simp)
    7.56 -  done;
    7.57 -
    7.58 -declare gcd.simps [simp del];
    7.59 -
    7.60 -lemma gcd_1 [simp]: "gcd(m,1) = 1"
    7.61 -  apply (simp add: gcd_non_0)
    7.62 -  done
    7.63 -
    7.64 -(*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
    7.65 -lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"
    7.66 -  apply (induct_tac m n rule: gcd_induct)
    7.67 -  apply (simp_all add: gcd_non_0)
    7.68 -  apply (blast dest: dvd_mod_imp_dvd)
    7.69 -  done
    7.70 -
    7.71 -lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
    7.72 -lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2];
    7.73 -
    7.74 -
    7.75 -(*Maximality: for all m,n,k naturals, 
    7.76 -                if k divides m and k divides n then k divides gcd(m,n)*)
    7.77 -lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
    7.78 -  apply (induct_tac m n rule: gcd_induct)
    7.79 -  apply (simp_all add: gcd_non_0 dvd_mod);
    7.80 -  done;
    7.81 -
    7.82 -lemma gcd_greatest_iff [iff]: "k dvd gcd(m,n) = (k dvd m & k dvd n)"
    7.83 -  apply (blast intro!: gcd_greatest intro: dvd_trans);
    7.84 -  done;
    7.85 -
    7.86 -(*Function gcd yields the Greatest Common Divisor*)
    7.87 -lemma is_gcd: "is_gcd (gcd(m,n)) m n"
    7.88 -  apply (simp add: is_gcd_def gcd_greatest)
    7.89 -  done
    7.90 -
    7.91 -(*uniqueness of GCDs*)
    7.92 -lemma is_gcd_unique: "[| is_gcd m a b; is_gcd n a b |] ==> m=n"
    7.93 -  apply (simp add: is_gcd_def);
    7.94 -  apply (blast intro: dvd_anti_sym)
    7.95 -  done
    7.96 -
    7.97 -lemma is_gcd_dvd: "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"
    7.98 -  apply (auto simp add: is_gcd_def);
    7.99 -  done
   7.100 -
   7.101 -(** Commutativity **)
   7.102 -
   7.103 -lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
   7.104 -  apply (auto simp add: is_gcd_def);
   7.105 -  done
   7.106 -
   7.107 -lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
   7.108 -  apply (rule is_gcd_unique)
   7.109 -  apply (rule is_gcd)
   7.110 -  apply (subst is_gcd_commute)
   7.111 -  apply (simp add: is_gcd)
   7.112 -  done
   7.113 -
   7.114 -lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"
   7.115 -  apply (rule is_gcd_unique)
   7.116 -  apply (rule is_gcd)
   7.117 -  apply (simp add: is_gcd_def);
   7.118 -  apply (blast intro: dvd_trans);
   7.119 -  done 
   7.120 -
   7.121 -lemma gcd_0_left [simp]: "gcd(0,m) = m"
   7.122 -  apply (simp add: gcd_commute [of 0])
   7.123 -  done
   7.124 -
   7.125 -lemma gcd_1_left [simp]: "gcd(1,m) = 1"
   7.126 -  apply (simp add: gcd_commute [of 1])
   7.127 -  done
   7.128 -
   7.129 -
   7.130 -(** Multiplication laws **)
   7.131 -
   7.132 -(*Davenport, page 27*)
   7.133 -lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)"
   7.134 -  apply (induct_tac m n rule: gcd_induct)
   7.135 -  apply (simp)
   7.136 -  apply (case_tac "k=0")
   7.137 -  apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   7.138 -  done
   7.139 -
   7.140 -lemma gcd_self [simp]: "gcd(m,m) = m"
   7.141 -  apply (rule gcd_mult_distrib2 [of m 1 1, simplified, THEN sym])
   7.142 -  done
   7.143 -
   7.144 -lemma gcd_mult [simp]: "gcd(k, k*n) = k"
   7.145 -  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, THEN sym])
   7.146 -  done
   7.147 -
   7.148 -lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
   7.149 -   apply (subgoal_tac "gcd(m*k, m*n) = m")
   7.150 -   apply (erule_tac t="m" in subst);
   7.151 -   apply (simp)
   7.152 -   apply (simp add: gcd_mult_distrib2 [THEN sym]);
   7.153 -  done
   7.154 -
   7.155 -lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> k dvd (m*n) = k dvd m";
   7.156 -  apply (blast intro: relprime_dvd_mult dvd_trans)
   7.157 -  done
   7.158 -
   7.159 -lemma prime_imp_relprime: "[| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1"
   7.160 -  apply (auto simp add: prime_def)
   7.161 -  apply (drule_tac x="gcd(p,n)" in spec)
   7.162 -  apply auto
   7.163 -  apply (insert gcd_dvd2 [of p n])
   7.164 -  apply (simp)
   7.165 -  done
   7.166 -
   7.167 -(*This theorem leads immediately to a proof of the uniqueness of factorization.
   7.168 -  If p divides a product of primes then it is one of those primes.*)
   7.169 -lemma prime_dvd_mult: "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"
   7.170 -  apply (blast intro: relprime_dvd_mult prime_imp_relprime)
   7.171 -  done
   7.172 -
   7.173 -
   7.174 -(** Addition laws **)
   7.175 -
   7.176 -lemma gcd_add1 [simp]: "gcd(m+n, n) = gcd(m,n)"
   7.177 -  apply (case_tac "n=0")
   7.178 -  apply (simp_all add: gcd_non_0)
   7.179 -  done
   7.180 -
   7.181 -lemma gcd_add2 [simp]: "gcd(m, m+n) = gcd(m,n)"
   7.182 -  apply (rule gcd_commute [THEN trans])
   7.183 -  apply (subst add_commute)
   7.184 -  apply (simp add: gcd_add1)
   7.185 -  apply (rule gcd_commute)
   7.186 -  done
   7.187 -
   7.188 -lemma gcd_add2' [simp]: "gcd(m, n+m) = gcd(m,n)"
   7.189 -  apply (subst add_commute)
   7.190 -  apply (rule gcd_add2)
   7.191 -  done
   7.192 -
   7.193 -lemma gcd_add_mult: "gcd(m, k*m+n) = gcd(m,n)"
   7.194 -  apply (induct_tac "k")
   7.195 -  apply (simp_all add: gcd_add2 add_assoc)
   7.196 -  done
   7.197 -
   7.198 -
   7.199 -(** More multiplication laws **)
   7.200 -
   7.201 -lemma gcd_mult_cancel: "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"
   7.202 -  apply (rule dvd_anti_sym)
   7.203 -   apply (rule gcd_greatest)
   7.204 -    apply (rule_tac n="k" in relprime_dvd_mult)
   7.205 -     apply (simp add: gcd_assoc)
   7.206 -     apply (simp add: gcd_commute)
   7.207 -    apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
   7.208 -  apply (blast intro: gcd_dvd1 dvd_trans);
   7.209 -  done
   7.210 -
   7.211 -end
     8.1 --- a/src/HOL/ex/ROOT.ML	Tue Sep 12 22:13:23 2000 +0200
     8.2 +++ b/src/HOL/ex/ROOT.ML	Wed Sep 13 18:45:10 2000 +0200
     8.3 @@ -6,9 +6,6 @@
     8.4  
     8.5  (*some examples of recursive function definitions: the TFL package*)
     8.6  time_use_thy "Recdefs";
     8.7 -time_use_thy "Primes";
     8.8 -time_use_thy "Fib";
     8.9 -with_path "../Induct" time_use_thy "Factorization";
    8.10  time_use_thy "Primrec";
    8.11  
    8.12  time_use_thy "NatSum";