9944

1 
(* Title: HOL/ex/Factorization.thy


2 
ID: $Id$


3 
Author: Thomas Marthedal Rasmussen


4 
Copyright 2000 University of Cambridge


5 


6 
Fundamental Theorem of Arithmetic (unique factorization into primes)


7 
*)


8 


9 
val prime_def = thm "prime_def";


10 
val prime_dvd_mult = thm "prime_dvd_mult";


11 


12 


13 
(*  Arithmetic  *)


14 


15 
Goal "!!m::nat. [ m ~= m*k; m ~= 1 ] ==> 1<m";


16 
by (case_tac "m" 1);


17 
by Auto_tac;


18 
qed "one_less_m";


19 


20 
Goal "!!m::nat. [ m ~= m*k; 1<m*k ] ==> 1<k";


21 
by (case_tac "k" 1);


22 
by Auto_tac;


23 
qed "one_less_k";


24 


25 
Goal "!!m::nat. [ 0<k; k*n=k*m ] ==> n=m";


26 
by Auto_tac;


27 
qed "mult_left_cancel";


28 


29 
Goal "!!m::nat. [ 0<m; m*n = m ] ==> n=1";


30 
by (case_tac "n" 1);


31 
by Auto_tac;


32 
qed "mn_eq_m_one";


33 


34 
Goal "!!m::nat. [ 0<n; 0<k ] ==> 1<m > m*n = k > n<k";


35 
by (induct_tac "m" 1);


36 
by Auto_tac;


37 
qed_spec_mp "prod_mn_less_k";


38 


39 


40 
(*  Prime List & Product  *)


41 


42 
Goal "prod (xs @ ys) = prod xs * prod ys";


43 
by (induct_tac "xs" 1);


44 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mult_assoc])));


45 
qed "prod_append";


46 


47 
Goal "prod (x#xs) = prod (y#ys) ==> x*prod xs = y*prod ys";


48 
by Auto_tac;


49 
qed "prod_xy_prod";


50 


51 
Goalw [primel_def] "primel (xs @ ys) = (primel xs & primel ys)";


52 
by Auto_tac;


53 
qed "primel_append";


54 


55 
Goalw [primel_def] "n:prime ==> primel [n] & prod [n] = n";


56 
by Auto_tac;


57 
qed "prime_primel";


58 


59 
Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)";


60 
by Auto_tac;


61 
by (case_tac "k" 1);


62 
by Auto_tac;


63 
qed "prime_nd_one";


64 


65 
Goalw [dvd_def] "[ prod (x#xs) = prod ys ] ==> x dvd (prod ys)";


66 
by (rtac exI 1);


67 
by (rtac sym 1);


68 
by (Asm_full_simp_tac 1);


69 
qed "hd_dvd_prod";


70 


71 
Goalw [primel_def] "primel (x#xs) ==> primel xs";


72 
by Auto_tac;


73 
qed "primel_tl";


74 


75 
Goalw [primel_def] "(primel (x#xs)) = (x:prime & primel xs)";


76 
by Auto_tac;


77 
qed "primel_hd_tl";


78 


79 
Goalw [prime_def] "[ p:prime; q:prime; p dvd q ] ==> p=q";


80 
by Auto_tac;


81 
qed "primes_eq";


82 


83 
Goalw [primel_def,prime_def] "[ primel xs; prod xs = 1 ] ==> xs = []";


84 
by (case_tac "xs" 1);


85 
by (ALLGOALS Asm_full_simp_tac);


86 
qed "primel_one_empty";


87 


88 
Goalw [prime_def] "p:prime ==> 1<p";


89 
by Auto_tac;


90 
qed "prime_g_one";


91 


92 
Goalw [prime_def] "p:prime ==> 0<p";


93 
by Auto_tac;


94 
qed "prime_g_zero";


95 


96 
Goalw [primel_def,prime_def] "primel xs > xs ~= [] > 1 < prod xs";


97 
by (induct_tac "xs" 1);


98 
by (auto_tac (claset() addEs [one_less_mult], simpset()));


99 
qed_spec_mp "primel_nempty_g_one";


100 


101 
Goalw [primel_def,prime_def] "primel xs > 0 < prod xs";


102 
by (induct_tac "xs" 1);


103 
by Auto_tac;


104 
qed_spec_mp "primel_prod_gz";


105 


106 


107 
(*  Sorting  *)


108 


109 
Goal "nondec xs > nondec (oinsert x xs)";


110 
by (induct_tac "xs" 1);


111 
by (case_tac "list" 2);


112 
by (ALLGOALS(asm_full_simp_tac (simpset()delcongs[thm"list.weak_case_cong"])));


113 
qed_spec_mp "nondec_oinsert";


114 


115 
Goal "nondec (sort xs)";


116 
by (induct_tac "xs" 1);


117 
by (ALLGOALS (Asm_full_simp_tac));


118 
by (etac nondec_oinsert 1);


119 
qed "nondec_sort";


120 


121 
Goal "[ x<=y; l=y#ys ] ==> x#l = oinsert x l";


122 
by (ALLGOALS Asm_full_simp_tac);


123 
qed "x_less_y_oinsert";


124 


125 
Goal "nondec xs > xs = sort xs";


126 
by (induct_tac "xs" 1);


127 
by Safe_tac;


128 
by (ALLGOALS Asm_full_simp_tac);


129 
by (case_tac "list" 1);


130 
by (ALLGOALS Asm_full_simp_tac);


131 
by (case_tac "list" 1);


132 
by (Asm_full_simp_tac 1);


133 
by (res_inst_tac [("y","aa"),("ys","lista")] x_less_y_oinsert 1);


134 
by (ALLGOALS Asm_full_simp_tac);


135 
qed_spec_mp "nondec_sort_eq";


136 


137 
Goal "oinsert x (oinsert y l) = oinsert y (oinsert x l)";


138 
by (induct_tac "l" 1);


139 
by Auto_tac;


140 
qed "oinsert_x_y";


141 


142 


143 
(*  Permutation  *)


144 


145 
Goalw [primel_def] "xs <~~> ys ==> primel xs > primel ys";


146 
by (etac perm.induct 1);


147 
by (ALLGOALS Asm_simp_tac);


148 
qed_spec_mp "perm_primel";


149 


150 
Goal "xs <~~> ys ==> prod xs = prod ys";


151 
by (etac perm.induct 1);


152 
by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));


153 
qed_spec_mp "perm_prod";


154 


155 
Goal "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys";


156 
by (etac perm.induct 1);


157 
by Auto_tac;


158 
qed "perm_subst_oinsert";


159 


160 
Goal "x#xs <~~> oinsert x xs";


161 
by (induct_tac "xs" 1);


162 
by Auto_tac;


163 
qed "perm_oinsert";


164 


165 
Goal "xs <~~> sort xs";


166 
by (induct_tac "xs" 1);


167 
by (auto_tac (claset() addIs [perm_oinsert]


168 
addEs [perm_subst_oinsert],


169 
simpset()));


170 
qed "perm_sort";


171 


172 
Goal "xs <~~> ys ==> sort xs = sort ys";


173 
by (etac perm.induct 1);


174 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [oinsert_x_y])));


175 
qed "perm_sort_eq";


176 


177 


178 
(*  Existence  *)


179 


180 
Goal "primel xs ==> EX ys. primel ys & nondec ys & prod ys = prod xs";


181 
by (blast_tac (claset() addIs [nondec_sort, perm_prod,perm_primel,perm_sort,


182 
perm_sym]) 1);


183 
qed "ex_nondec_lemma";


184 


185 
Goalw [prime_def,dvd_def]


186 
"1<n & n~:prime > (EX m k.1<m & 1<k & m<n & k<n & n=m*k)";


187 
by (auto_tac (claset() addIs [n_less_m_mult_n, n_less_n_mult_m,


188 
one_less_m, one_less_k],


189 
simpset()));


190 
qed_spec_mp "not_prime_ex_mk";


191 


192 
Goal "[ primel xs; primel ys ] \


193 
\ ==> EX l. primel l & prod l = prod xs * prod ys";


194 
by (rtac exI 1);


195 
by Safe_tac;


196 
by (rtac prod_append 2);


197 
by (asm_simp_tac (simpset() addsimps [primel_append]) 1);


198 
qed "split_primel";


199 


200 
Goal "1<n > (EX l. primel l & prod l = n)";


201 
by (induct_thm_tac nat_less_induct "n" 1);


202 
by (rtac impI 1);


203 
by (case_tac "n:prime" 1);


204 
by (rtac exI 1);


205 
by (etac prime_primel 1);


206 
by (cut_inst_tac [("n","n")] not_prime_ex_mk 1);


207 
by (auto_tac (claset() addSIs [split_primel], simpset()));


208 
qed_spec_mp "factor_exists";


209 


210 
Goal "1<n ==> (EX l. primel l & nondec l & prod l = n)";


211 
by (etac (factor_exists RS exE) 1);


212 
by (blast_tac (claset() addSIs [ex_nondec_lemma]) 1);


213 
qed "nondec_factor_exists";


214 


215 


216 
(*  Uniqueness  *)


217 


218 
Goal "p:prime ==> p dvd (prod xs) > (EX m. m:set xs & p dvd m)";


219 
by (induct_tac "xs" 1);


220 
by (ALLGOALS Asm_full_simp_tac);


221 
by (etac prime_nd_one 1);


222 
by (rtac impI 1);


223 
by (dtac prime_dvd_mult 1);


224 
by Auto_tac;


225 
qed_spec_mp "prime_dvd_mult_list";


226 


227 
Goal "[ primel (x#xs); primel ys; prod (x#xs) = prod ys ] \


228 
\ ==> EX m. m :set ys & x dvd m";


229 
by (rtac prime_dvd_mult_list 1);


230 
by (etac hd_dvd_prod 2);


231 
by (asm_full_simp_tac (simpset() addsimps [primel_hd_tl]) 1);


232 
qed "hd_xs_dvd_prod";


233 


234 
Goal "[ primel (x#xs); primel ys; m:set ys; x dvd m ] ==> x=m";


235 
by (rtac primes_eq 1);


236 
by (auto_tac (claset(), simpset() addsimps [primel_def,primel_hd_tl]));


237 
qed "prime_dvd_eq";


238 


239 
Goal "[ primel (x#xs); primel ys; prod (x#xs) = prod ys ] ==> x:set ys";


240 
by (ftac hd_xs_dvd_prod 1);


241 
by Auto_tac;


242 
by (dtac prime_dvd_eq 1);


243 
by Auto_tac;


244 
qed "hd_xs_eq_prod";


245 


246 
Goal "[ primel (x#xs); primel ys; prod (x#xs) = prod ys ] \


247 
\ ==> EX l. ys <~~> (x#l)";


248 
by (rtac exI 1);


249 
by (rtac perm_remove 1);


250 
by (etac hd_xs_eq_prod 1);


251 
by (ALLGOALS assume_tac);


252 
qed "perm_primel_ex";


253 


254 
Goal "[ primel (x#xs); primel ys; prod (x#xs) = prod ys ] \


255 
\ ==> prod xs < prod ys";


256 
by (auto_tac (claset() addIs [prod_mn_less_k,prime_g_one,primel_prod_gz],


257 
simpset() addsimps [primel_hd_tl]));


258 
qed "primel_prod_less";


259 


260 
Goal "[ primel xs; p*prod xs = p; p:prime ] ==> xs=[]";


261 
by (auto_tac (claset() addIs [primel_one_empty,mn_eq_m_one,prime_g_zero],


262 
simpset()));


263 
qed "prod_one_empty";


264 


265 
Goal "[ ALL m. m < prod ys > (ALL xs ys. primel xs & primel ys & \


266 
\ prod xs = prod ys & prod xs = m > xs <~~> ys); primel list; \


267 
\ primel x; prod list = prod x; prod x < prod ys ] ==> x <~~> list";


268 
by (Asm_full_simp_tac 1);


269 
qed "uniq_ex_lemma";


270 


271 
Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \


272 
\ > xs <~~> ys)";


273 
by (induct_thm_tac nat_less_induct "n" 1);


274 
by Safe_tac;


275 
by (case_tac "xs" 1);


276 
by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);


277 
by (rtac (perm_primel_ex RS exE) 1);


278 
by (ALLGOALS Asm_full_simp_tac);


279 
by (rtac (perm.trans RS perm_sym) 1);


280 
by (assume_tac 1);


281 
by (rtac perm.Cons 1);


282 
by (case_tac "x=[]" 1);


283 
by (asm_full_simp_tac (simpset() addsimps [perm_sing_eq,primel_hd_tl]) 1);


284 
by (res_inst_tac [("p","a")] prod_one_empty 1);


285 
by (ALLGOALS Asm_full_simp_tac);


286 
by (etac uniq_ex_lemma 1);


287 
by (auto_tac (claset() addIs [primel_tl,perm_primel],


288 
simpset() addsimps [primel_hd_tl]));


289 
by (res_inst_tac [("k","a"),("n","prod list"),("m","prod x")] mult_left_cancel 1);


290 
by (res_inst_tac [("x","a")] primel_prod_less 3);


291 
by (rtac prod_xy_prod 2);


292 
by (res_inst_tac [("s","prod ys")] trans 2);


293 
by (etac perm_prod 3);


294 
by (etac (perm_prod RS sym) 5);


295 
by (auto_tac (claset() addIs [perm_primel,prime_g_zero], simpset()));


296 
qed_spec_mp "factor_unique";


297 


298 
Goal "[ xs <~~> ys; nondec xs; nondec ys ] ==> xs = ys";


299 
by (rtac trans 1);


300 
by (rtac trans 1);


301 
by (etac nondec_sort_eq 1);


302 
by (etac perm_sort_eq 1);


303 
by (etac (nondec_sort_eq RS sym) 1);


304 
qed "perm_nondec_unique";


305 


306 
Goal "ALL n. 1<n > (EX! l. primel l & nondec l & prod l = n)";


307 
by Safe_tac;


308 
by (etac nondec_factor_exists 1);


309 
by (rtac perm_nondec_unique 1);


310 
by (rtac factor_unique 1);


311 
by (ALLGOALS Asm_full_simp_tac);


312 
qed_spec_mp "unique_prime_factorization";
