new theory ex/Factorization
authorpaulson
Wed Mar 08 16:14:12 2000 +0100 (2000-03-08)
changeset 835357a163920480
parent 8352 0fda5ba36934
child 8354 c02e3c131eca
new theory ex/Factorization
src/HOL/IsaMakefile
src/HOL/ex/Factorization.ML
src/HOL/ex/Factorization.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Mar 08 16:13:19 2000 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Mar 08 16:14:12 2000 +0100
     1.3 @@ -413,8 +413,10 @@
     1.4  
     1.5  $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/BT.ML ex/BT.thy ex/Fib.ML ex/Fib.thy \
     1.6    ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML \
     1.7 -  ex/NatSum.thy ex/Primes.ML ex/Primes.thy ex/Primrec.ML \
     1.8 -  ex/Primrec.thy ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
     1.9 +  ex/NatSum.thy ex/Primes.ML ex/Primes.thy \
    1.10 +  ex/Factorization.ML ex/Factorization.thy \
    1.11 +  ex/Primrec.ML ex/Primrec.thy \
    1.12 +  ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
    1.13    ex/ROOT.ML ex/Recdefs.ML ex/Recdefs.thy ex/cla.ML ex/meson.ML \
    1.14    ex/mesontest.ML ex/set.ML ex/Group.ML ex/Group.thy ex/IntRing.ML \
    1.15    ex/IntRing.thy ex/IntRingDefs.ML ex/IntRingDefs.thy ex/Lagrange.ML \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Factorization.ML	Wed Mar 08 16:14:12 2000 +0100
     2.3 @@ -0,0 +1,309 @@
     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 +(* --- Arithmetic --- *)
    2.14 +
    2.15 +Goal "[| m ~= m*k; m ~= 1 |] ==> 1<m";
    2.16 +by (exhaust_tac "m" 1);
    2.17 +by Auto_tac;
    2.18 +qed "one_less_m";
    2.19 +
    2.20 +Goal "[| m ~= m*k; 1<m*k |] ==> 1<k";
    2.21 +by (exhaust_tac "k" 1);
    2.22 +by Auto_tac;
    2.23 +qed "one_less_k";
    2.24 +
    2.25 +Goal "[| 0<k; k*n=k*m |] ==> n=m";
    2.26 +by Auto_tac;
    2.27 +qed "mult_left_cancel";
    2.28 +
    2.29 +Goal "[| 0<m; m*n = m |] ==> n=1";
    2.30 +by (exhaust_tac "n" 1);
    2.31 +by Auto_tac;
    2.32 +qed "mn_eq_m_one";
    2.33 +
    2.34 +Goal "[| 0<n; 0<k |] ==> 1<m --> m*n = k --> n<k";
    2.35 +by (induct_tac "m" 1);
    2.36 +by Auto_tac;
    2.37 +qed_spec_mp "prod_mn_less_k";
    2.38 +
    2.39 +
    2.40 +(* --- Prime List & Product --- *)
    2.41 +
    2.42 +Goal "prod (xs @ ys) = prod xs * prod ys"; 
    2.43 +by (induct_tac "xs" 1);
    2.44 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [mult_assoc])));
    2.45 +qed "prod_append";
    2.46 +
    2.47 +Goal "prod (x#xs) = prod (y#ys) ==> x*prod xs = y*prod ys";
    2.48 +by Auto_tac;
    2.49 +qed "prod_xy_prod";
    2.50 +
    2.51 +Goalw [primel_def] "primel (xs @ ys) = (primel xs & primel ys)";
    2.52 +by Auto_tac;
    2.53 +qed "primel_append";
    2.54 +
    2.55 +Goalw [primel_def] "n:prime ==> primel [n] & prod [n] = n";
    2.56 +by Auto_tac;
    2.57 +qed "prime_primel";
    2.58 +
    2.59 +Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)";
    2.60 +by Auto_tac;
    2.61 +by (exhaust_tac "k" 1);
    2.62 +by Auto_tac;
    2.63 +qed "prime_nd_one";
    2.64 +
    2.65 +Goalw [dvd_def] "[| prod (x#xs) = prod ys |] ==> x dvd (prod ys)";
    2.66 +by (rtac exI 1);
    2.67 +by (rtac sym 1);
    2.68 +by (Asm_full_simp_tac 1);
    2.69 +qed "hd_dvd_prod";
    2.70 +
    2.71 +Goalw [primel_def] "primel (x#xs) ==> primel xs";
    2.72 +by Auto_tac;
    2.73 +qed "primel_tl";
    2.74 +
    2.75 +Goalw [primel_def] "(primel (x#xs)) = (x:prime & primel xs)"; 
    2.76 +by Auto_tac;
    2.77 +qed "primel_hd_tl";
    2.78 +
    2.79 +Goalw [prime_def] "[| p:prime; q:prime; p dvd q |] ==> p=q";
    2.80 +by Auto_tac;
    2.81 +qed "primes_eq";
    2.82 +
    2.83 +Goalw [primel_def,prime_def] "[| primel xs; prod xs = 1 |] ==> xs = []";
    2.84 +by (exhaust_tac "xs" 1);
    2.85 +by (ALLGOALS Asm_full_simp_tac);
    2.86 +qed "primel_one_empty";
    2.87 +
    2.88 +Goalw [prime_def] "p:prime ==> 1<p";
    2.89 +by Auto_tac;
    2.90 +qed "prime_g_one";
    2.91 +
    2.92 +Goalw [prime_def] "p:prime ==> 0<p";
    2.93 +by Auto_tac;
    2.94 +qed "prime_g_zero";
    2.95 +
    2.96 +Goalw [primel_def,prime_def] "primel xs --> xs ~= [] --> 1 < prod xs";
    2.97 +by (induct_tac "xs" 1);
    2.98 +by (auto_tac (claset() addEs [one_less_mult], simpset()));
    2.99 +qed_spec_mp "primel_nempty_g_one";
   2.100 +
   2.101 +Goalw [primel_def,prime_def] "primel xs --> 0 < prod xs"; 
   2.102 +by (induct_tac "xs" 1);
   2.103 +by Auto_tac;
   2.104 +qed_spec_mp "primel_prod_gz";
   2.105 +
   2.106 +
   2.107 +(* --- Sorting --- *)
   2.108 +
   2.109 +Goal "nondec xs --> nondec (oinsert x xs)";
   2.110 +by (induct_tac "xs" 1);
   2.111 +by (exhaust_tac "list" 2);
   2.112 +by (ALLGOALS (Asm_full_simp_tac));
   2.113 +qed_spec_mp "nondec_oinsert";
   2.114 +
   2.115 +Goal "nondec (sort xs)";
   2.116 +by (induct_tac "xs" 1);
   2.117 +by (ALLGOALS (Asm_full_simp_tac));
   2.118 +by (etac nondec_oinsert 1);
   2.119 +qed "nondec_sort";
   2.120 +
   2.121 +Goal "[| x<=y; l=y#ys |]  ==> x#l = oinsert x l";
   2.122 +by (ALLGOALS Asm_full_simp_tac);
   2.123 +qed "x_less_y_oinsert";
   2.124 +
   2.125 +Goal "nondec xs --> xs = sort xs";
   2.126 +by (induct_tac "xs" 1);
   2.127 +by Safe_tac;
   2.128 +by (ALLGOALS Asm_full_simp_tac);
   2.129 +by (exhaust_tac "list" 1);
   2.130 +by (ALLGOALS Asm_full_simp_tac);
   2.131 +by (exhaust_tac "list" 1);
   2.132 +by (Asm_full_simp_tac 1);
   2.133 +by (res_inst_tac [("y","aa"),("ys","lista")] x_less_y_oinsert 1); 
   2.134 +by (ALLGOALS Asm_full_simp_tac);
   2.135 +qed_spec_mp "nondec_sort_eq";
   2.136 +
   2.137 +Goal "oinsert x (oinsert y l) = oinsert y (oinsert x l)";
   2.138 +by (induct_tac "l" 1);
   2.139 +by (ALLGOALS Asm_full_simp_tac);
   2.140 +qed "oinsert_x_y";
   2.141 +
   2.142 +
   2.143 +(* --- Permutation --- *)
   2.144 +
   2.145 +Goalw [primel_def] "xs <~~> ys ==> primel xs --> primel ys";
   2.146 +by (etac perm.induct 1);
   2.147 +by (ALLGOALS Asm_simp_tac);
   2.148 +qed_spec_mp "perm_primel";
   2.149 +
   2.150 +Goal "xs <~~> ys ==> prod xs = prod ys";
   2.151 +by (etac perm.induct 1);
   2.152 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_left_commute])));
   2.153 +qed_spec_mp "perm_prod";
   2.154 +
   2.155 +Goal "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"; 
   2.156 +by (etac perm.induct 1);
   2.157 +by (auto_tac (claset() addIs perm_rules, simpset()));
   2.158 +qed "perm_subst_oinsert";
   2.159 +
   2.160 +Goal "x#xs <~~> oinsert x xs";
   2.161 +by (induct_tac "xs" 1);
   2.162 +by (auto_tac (claset() addIs perm_rules, simpset()));
   2.163 +qed "perm_oinsert";
   2.164 +
   2.165 +Goal "xs <~~> sort xs";
   2.166 +by (induct_tac "xs" 1);
   2.167 +by (auto_tac (claset() addIs [perm.trans,perm_oinsert] 
   2.168 +	               addEs [perm_subst_oinsert],
   2.169 +              simpset() addsimps [perm_refl]));
   2.170 +qed "perm_sort";
   2.171 +
   2.172 +Goal "xs <~~> ys ==> sort xs = sort ys";
   2.173 +by (etac perm.induct 1);
   2.174 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [oinsert_x_y])));
   2.175 +qed "perm_sort_eq";
   2.176 +
   2.177 +
   2.178 +(* --- Existence --- *)
   2.179 +
   2.180 +Goal "primel xs ==> EX ys. primel ys & nondec ys & prod ys = prod xs";
   2.181 +by (blast_tac (claset() addIs [nondec_sort, perm_prod,perm_primel,perm_sort,
   2.182 +			       perm_sym]) 1);
   2.183 +qed "ex_nondec_lemma";
   2.184 +
   2.185 +Goalw [prime_def,dvd_def]
   2.186 +     "1<n & n~:prime --> (EX m k.1<m & 1<k & m<n & k<n & n=m*k)";
   2.187 +by (auto_tac (claset() addIs [n_less_m_mult_n, n_less_n_mult_m,
   2.188 +			      one_less_m, one_less_k], 
   2.189 +	      simpset()));
   2.190 +qed_spec_mp "not_prime_ex_mk";
   2.191 +
   2.192 +Goal "[| primel xs; primel ys |] \
   2.193 +\     ==> EX l. primel l & prod l = prod xs * prod ys";
   2.194 +by (rtac exI 1);
   2.195 +by Safe_tac;
   2.196 +by (rtac prod_append 2);
   2.197 +by (asm_simp_tac (simpset() addsimps [primel_append]) 1);
   2.198 +qed "split_primel";
   2.199 +
   2.200 +Goal "1<n --> (EX l. primel l & prod l = n)"; 
   2.201 +by (res_inst_tac [("n","n")] less_induct 1);
   2.202 +by (rtac impI 1);
   2.203 +by (case_tac "n:prime" 1);
   2.204 +by (rtac exI 1);
   2.205 +by (etac prime_primel 1);
   2.206 +by (cut_inst_tac [("n","n")] not_prime_ex_mk 1);
   2.207 +by (auto_tac (claset() addSIs [split_primel], simpset()));
   2.208 +qed_spec_mp "factor_exists";
   2.209 +
   2.210 +Goal "1<n ==> (EX l. primel l & nondec l & prod l = n)"; 
   2.211 +by (etac (factor_exists RS exE) 1);
   2.212 +by (blast_tac (claset() addSIs [ex_nondec_lemma]) 1);
   2.213 +qed "nondec_factor_exists";
   2.214 +
   2.215 +
   2.216 +(* --- Uniqueness --- *)
   2.217 +
   2.218 +Goal "p:prime ==> p dvd (prod xs) --> (EX m. m:set xs & p dvd m)";
   2.219 +by (induct_tac "xs" 1);
   2.220 +by (ALLGOALS Asm_full_simp_tac);
   2.221 +by (etac prime_nd_one 1);
   2.222 +by (rtac impI 1);
   2.223 +by (dtac prime_dvd_mult 1);
   2.224 +by Auto_tac;
   2.225 +qed_spec_mp "prime_dvd_mult_list";
   2.226 +
   2.227 +Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
   2.228 +\     ==> EX m. m :set ys & x dvd m";
   2.229 +by (rtac prime_dvd_mult_list 1);
   2.230 +by (etac hd_dvd_prod 2);
   2.231 +by (asm_full_simp_tac (simpset() addsimps [primel_hd_tl]) 1);
   2.232 +qed "hd_xs_dvd_prod";
   2.233 +
   2.234 +Goal "[| primel (x#xs); primel ys; m:set ys; x dvd m |] ==> x=m";
   2.235 +by (rtac primes_eq 1);
   2.236 +by (auto_tac (claset(), simpset() addsimps [primel_def,primel_hd_tl]));
   2.237 +qed "prime_dvd_eq";
   2.238 +
   2.239 +Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] ==> x:set ys";
   2.240 +by (ftac hd_xs_dvd_prod 1);
   2.241 +by Auto_tac;
   2.242 +by (dtac prime_dvd_eq 1);
   2.243 +by Auto_tac;
   2.244 +qed "hd_xs_eq_prod";
   2.245 +
   2.246 +Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
   2.247 +\     ==> EX l. ys <~~> (x#l)";
   2.248 +by (rtac exI 1);
   2.249 +by (rtac perm_remove 1);
   2.250 +by (etac hd_xs_eq_prod 1);
   2.251 +by (ALLGOALS assume_tac);
   2.252 +qed "perm_primel_ex";
   2.253 +
   2.254 +Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
   2.255 +\     ==> prod xs < prod ys";
   2.256 +by (auto_tac (claset() addIs [prod_mn_less_k,prime_g_one,primel_prod_gz],
   2.257 +              simpset() addsimps [primel_hd_tl]));
   2.258 +qed "primel_prod_less";
   2.259 +
   2.260 +Goal "[| primel xs; p*prod xs = p; p:prime |] ==> xs=[]";
   2.261 +by (auto_tac (claset() addIs [primel_one_empty,mn_eq_m_one,prime_g_zero], 
   2.262 +	      simpset()));
   2.263 +qed "prod_one_empty";
   2.264 +
   2.265 +Goal "[| ALL m. m < prod ys --> (ALL xs ys. primel xs & primel ys & \
   2.266 +\        prod xs = prod ys & prod xs = m --> xs <~~> ys); primel list; \
   2.267 +\        primel x; prod list = prod x; prod x < prod ys |] ==> x <~~> list";
   2.268 +by (Asm_full_simp_tac 1);
   2.269 +qed "uniq_ex_lemma";
   2.270 +
   2.271 +Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \
   2.272 +\     --> xs <~~> ys)";
   2.273 +by (res_inst_tac [("n","n")] less_induct 1);
   2.274 +by Safe_tac;
   2.275 +by (exhaust_tac "xs" 1);
   2.276 +by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);
   2.277 +by (rtac (perm_primel_ex RS exE) 1);
   2.278 +by (ALLGOALS Asm_full_simp_tac);
   2.279 +by (rtac (perm.trans RS perm_sym) 1);
   2.280 +by (assume_tac 1);
   2.281 +by (rtac perm.Cons 1);
   2.282 +by (case_tac "x=[]" 1);
   2.283 +by (asm_full_simp_tac (simpset() addsimps [perm_sing_eq,primel_hd_tl]) 1);
   2.284 +by (res_inst_tac [("p","a")] prod_one_empty 1);
   2.285 +by (ALLGOALS Asm_full_simp_tac);
   2.286 +by (etac uniq_ex_lemma 1);
   2.287 +by (auto_tac (claset() addIs [primel_tl,perm_primel],
   2.288 +	      simpset() addsimps [primel_hd_tl]));
   2.289 +by (res_inst_tac [("k","a"),("n","prod list"),("m","prod x")] mult_left_cancel 1);
   2.290 +by (res_inst_tac [("x","a")] primel_prod_less 3);
   2.291 +by (rtac prod_xy_prod 2);
   2.292 +by (res_inst_tac [("s","prod ys")] trans 2);
   2.293 +by (etac perm_prod 3);
   2.294 +by (etac (perm_prod RS sym) 5); 
   2.295 +by (auto_tac (claset() addIs [perm_primel,prime_g_zero], simpset()));
   2.296 +qed_spec_mp "factor_unique";
   2.297 +
   2.298 +Goal "[| xs <~~> ys; nondec xs; nondec ys |] ==> xs = ys"; 
   2.299 +by (rtac trans 1);
   2.300 +by (rtac trans 1);
   2.301 +by (etac nondec_sort_eq 1);
   2.302 +by (etac perm_sort_eq 1);
   2.303 +by (etac (nondec_sort_eq RS sym) 1);
   2.304 +qed "perm_nondec_unique";
   2.305 +
   2.306 +Goal "ALL n. 1<n --> (EX! l. primel l & nondec l & prod l = n)";
   2.307 +by Safe_tac;
   2.308 +by (etac nondec_factor_exists 1);
   2.309 +by (rtac perm_nondec_unique 1);
   2.310 +by (rtac factor_unique 1);
   2.311 +by (ALLGOALS Asm_full_simp_tac);
   2.312 +qed_spec_mp "unique_prime_factorization";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Factorization.thy	Wed Mar 08 16:14:12 2000 +0100
     3.3 @@ -0,0 +1,38 @@
     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 +
    3.13 +Factorization = Primes + Perm +
    3.14 +
    3.15 +consts
    3.16 +  primel  :: nat list => bool 
    3.17 +  nondec  :: nat list => bool 
    3.18 +  prod    :: nat list => nat
    3.19 +  oinsert :: [nat, nat list] => nat list
    3.20 +  sort    :: nat list => nat list
    3.21 +
    3.22 +defs
    3.23 +  primel_def "primel xs == set xs <= prime"
    3.24 +
    3.25 +primrec
    3.26 +  "nondec []     = True"
    3.27 +  "nondec (x#xs) = (case xs of [] => True | y#ys => x<=y & nondec xs)"
    3.28 +
    3.29 +primrec
    3.30 +  "prod []     = 1"
    3.31 +  "prod (x#xs) = x * prod xs"
    3.32 +
    3.33 +primrec
    3.34 +  "oinsert x []     = [x]"
    3.35 +  "oinsert x (y#ys) = (if x<=y then x#y#ys else y#oinsert x ys)"
    3.36 +
    3.37 +primrec
    3.38 +  "sort []     = []"
    3.39 +  "sort (x#xs) = oinsert x (sort xs)"  
    3.40 +
    3.41 +end
    3.42 \ No newline at end of file
     4.1 --- a/src/HOL/ex/ROOT.ML	Wed Mar 08 16:13:19 2000 +0100
     4.2 +++ b/src/HOL/ex/ROOT.ML	Wed Mar 08 16:14:12 2000 +0100
     4.3 @@ -14,6 +14,7 @@
     4.4  time_use_thy "Recdefs";
     4.5  time_use_thy "Primes";
     4.6  time_use_thy "Fib";
     4.7 +with_path "../Induct" use_thy "Factorization";
     4.8  time_use_thy "Primrec";
     4.9  
    4.10  time_use_thy "NatSum";