src/HOL/NumberTheory/Factorization.thy
changeset 11049 7eef34adb852
parent 9944 2a705d1af4dc
child 11364 01020b10c0a7
     1.1 --- a/src/HOL/NumberTheory/Factorization.thy	Sat Feb 03 17:43:34 2001 +0100
     1.2 +++ b/src/HOL/NumberTheory/Factorization.thy	Sun Feb 04 19:31:13 2001 +0100
     1.3 @@ -1,38 +1,363 @@
     1.4 -(*  Title:      HOL/ex/Factorization.thy
     1.5 +(*  Title:      HOL/NumberTheory/Factorization.thy
     1.6      ID:         $Id$
     1.7      Author:     Thomas Marthedal Rasmussen
     1.8      Copyright   2000  University of Cambridge
     1.9 +*)
    1.10  
    1.11 -Fundamental Theorem of Arithmetic (unique factorization into primes)
    1.12 -*)
    1.13 +header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
    1.14 +
    1.15 +theory Factorization = Primes + Permutation:
    1.16  
    1.17  
    1.18 -Factorization = Primes + Perm +
    1.19 +subsection {* Definitions *}
    1.20  
    1.21  consts
    1.22 -  primel  :: nat list => bool 
    1.23 -  nondec  :: nat list => bool 
    1.24 -  prod    :: nat list => nat
    1.25 -  oinsert :: [nat, nat list] => nat list
    1.26 -  sort    :: nat list => nat list
    1.27 +  primel :: "nat list => bool "
    1.28 +  nondec :: "nat list => bool "
    1.29 +  prod :: "nat list => nat"
    1.30 +  oinsert :: "nat => nat list => nat list"
    1.31 +  sort :: "nat list => nat list"
    1.32  
    1.33  defs
    1.34 -  primel_def "primel xs == set xs <= prime"
    1.35 +  primel_def: "primel xs == set xs \<subseteq> prime"
    1.36 +
    1.37 +primrec
    1.38 +  "nondec [] = True"
    1.39 +  "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
    1.40  
    1.41  primrec
    1.42 -  "nondec []     = True"
    1.43 -  "nondec (x#xs) = (case xs of [] => True | y#ys => x<=y & nondec xs)"
    1.44 +  "prod [] = 1"
    1.45 +  "prod (x # xs) = x * prod xs"
    1.46 +
    1.47 +primrec
    1.48 +  "oinsert x [] = [x]"
    1.49 +  "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
    1.50  
    1.51  primrec
    1.52 -  "prod []     = 1"
    1.53 -  "prod (x#xs) = x * prod xs"
    1.54 +  "sort [] = []"
    1.55 +  "sort (x # xs) = oinsert x (sort xs)"
    1.56 +
    1.57 +
    1.58 +subsection {* Arithmetic *}
    1.59 +
    1.60 +lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> 1 ==> 1 < m"
    1.61 +  apply (case_tac m)
    1.62 +   apply auto
    1.63 +  done
    1.64 +
    1.65 +lemma one_less_k: "(m::nat) \<noteq> m * k ==> 1 < m * k ==> 1 < k"
    1.66 +  apply (case_tac k)
    1.67 +   apply auto
    1.68 +  done
    1.69 +
    1.70 +lemma mult_left_cancel: "(0::nat) < k ==> k * n = k * m ==> n = m"
    1.71 +  apply auto
    1.72 +  done
    1.73 +
    1.74 +lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = 1"
    1.75 +  apply (case_tac n)
    1.76 +   apply auto
    1.77 +  done
    1.78 +
    1.79 +lemma prod_mn_less_k:
    1.80 +    "(0::nat) < n ==> 0 < k ==> 1 < m ==> m * n = k ==> n < k"
    1.81 +  apply (induct m)
    1.82 +   apply auto
    1.83 +  done
    1.84 +
    1.85 +
    1.86 +subsection {* Prime list and product *}
    1.87 +
    1.88 +lemma prod_append: "prod (xs @ ys) = prod xs * prod ys"
    1.89 +  apply (induct xs)
    1.90 +   apply (simp_all add: mult_assoc)
    1.91 +  done
    1.92 +
    1.93 +lemma prod_xy_prod:
    1.94 +    "prod (x # xs) = prod (y # ys) ==> x * prod xs = y * prod ys"
    1.95 +  apply auto
    1.96 +  done
    1.97 +
    1.98 +lemma primel_append: "primel (xs @ ys) = (primel xs \<and> primel ys)"
    1.99 +  apply (unfold primel_def)
   1.100 +  apply auto
   1.101 +  done
   1.102 +
   1.103 +lemma prime_primel: "n \<in> prime ==> primel [n] \<and> prod [n] = n"
   1.104 +  apply (unfold primel_def)
   1.105 +  apply auto
   1.106 +  done
   1.107 +
   1.108 +lemma prime_nd_one: "p \<in> prime ==> \<not> p dvd 1"
   1.109 +  apply (unfold prime_def dvd_def)
   1.110 +  apply auto
   1.111 +  done
   1.112 +
   1.113 +lemma hd_dvd_prod: "prod (x # xs) = prod ys ==> x dvd (prod ys)"
   1.114 +  apply (unfold dvd_def)
   1.115 +  apply (rule exI)
   1.116 +  apply (rule sym)
   1.117 +  apply simp
   1.118 +  done
   1.119 +
   1.120 +lemma primel_tl: "primel (x # xs) ==> primel xs"
   1.121 +  apply (unfold primel_def)
   1.122 +  apply auto
   1.123 +  done
   1.124 +
   1.125 +lemma primel_hd_tl: "(primel (x # xs)) = (x \<in> prime \<and> primel xs)"
   1.126 +  apply (unfold primel_def)
   1.127 +  apply auto
   1.128 +  done
   1.129 +
   1.130 +lemma primes_eq: "p \<in> prime ==> q \<in> prime ==> p dvd q ==> p = q"
   1.131 +  apply (unfold prime_def)
   1.132 +  apply auto
   1.133 +  done
   1.134 +
   1.135 +lemma primel_one_empty: "primel xs ==> prod xs = 1 ==> xs = []"
   1.136 +  apply (unfold primel_def prime_def)
   1.137 +  apply (case_tac xs)
   1.138 +   apply simp_all
   1.139 +  done
   1.140 +
   1.141 +lemma prime_g_one: "p \<in> prime ==> 1 < p"
   1.142 +  apply (unfold prime_def)
   1.143 +  apply auto
   1.144 +  done
   1.145 +
   1.146 +lemma prime_g_zero: "p \<in> prime ==> 0 < p"
   1.147 +  apply (unfold prime_def)
   1.148 +  apply auto
   1.149 +  done
   1.150 +
   1.151 +lemma primel_nempty_g_one [rule_format]:
   1.152 +    "primel xs --> xs \<noteq> [] --> 1 < prod xs"
   1.153 +  apply (unfold primel_def prime_def)
   1.154 +  apply (induct xs)
   1.155 +   apply (auto elim: one_less_mult)
   1.156 +  done
   1.157 +
   1.158 +lemma primel_prod_gz: "primel xs ==> 0 < prod xs"
   1.159 +  apply (unfold primel_def prime_def)
   1.160 +  apply (induct xs)
   1.161 +   apply auto
   1.162 +  done
   1.163 +
   1.164 +
   1.165 +subsection {* Sorting *}
   1.166 +
   1.167 +lemma nondec_oinsert [rule_format]: "nondec xs --> nondec (oinsert x xs)"
   1.168 +  apply (induct xs)
   1.169 +   apply (case_tac [2] list)
   1.170 +    apply (simp_all cong del: list.weak_case_cong)
   1.171 +  done
   1.172 +
   1.173 +lemma nondec_sort: "nondec (sort xs)"
   1.174 +  apply (induct xs)
   1.175 +   apply simp_all
   1.176 +  apply (erule nondec_oinsert)
   1.177 +  done
   1.178 +
   1.179 +lemma x_less_y_oinsert: "x \<le> y ==> l = y # ys ==> x # l = oinsert x l"
   1.180 +  apply simp_all
   1.181 +  done
   1.182 +
   1.183 +lemma nondec_sort_eq [rule_format]: "nondec xs --> xs = sort xs"
   1.184 +  apply (induct xs)
   1.185 +   apply safe
   1.186 +    apply simp_all
   1.187 +   apply (case_tac list)
   1.188 +    apply simp_all
   1.189 +  apply (case_tac list)
   1.190 +   apply simp
   1.191 +  apply (rule_tac y = aa and ys = lista in x_less_y_oinsert)
   1.192 +   apply simp_all
   1.193 +  done
   1.194 +
   1.195 +lemma oinsert_x_y: "oinsert x (oinsert y l) = oinsert y (oinsert x l)"
   1.196 +  apply (induct l)
   1.197 +  apply auto
   1.198 +  done
   1.199 +
   1.200 +
   1.201 +subsection {* Permutation *}
   1.202 +
   1.203 +lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
   1.204 +  apply (unfold primel_def)
   1.205 +  apply (erule perm.induct)
   1.206 +     apply simp_all
   1.207 +  done
   1.208 +
   1.209 +lemma perm_prod [rule_format]: "xs <~~> ys ==> prod xs = prod ys"
   1.210 +  apply (erule perm.induct)
   1.211 +     apply (simp_all add: mult_ac)
   1.212 +  done
   1.213  
   1.214 -primrec
   1.215 -  "oinsert x []     = [x]"
   1.216 -  "oinsert x (y#ys) = (if x<=y then x#y#ys else y#oinsert x ys)"
   1.217 +lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
   1.218 +  apply (erule perm.induct)
   1.219 +     apply auto
   1.220 +  done
   1.221 +
   1.222 +lemma perm_oinsert: "x # xs <~~> oinsert x xs"
   1.223 +  apply (induct xs)
   1.224 +   apply auto
   1.225 +  done
   1.226 +
   1.227 +lemma perm_sort: "xs <~~> sort xs"
   1.228 +  apply (induct xs)
   1.229 +  apply (auto intro: perm_oinsert elim: perm_subst_oinsert)
   1.230 +  done
   1.231 +
   1.232 +lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys"
   1.233 +  apply (erule perm.induct)
   1.234 +     apply (simp_all add: oinsert_x_y)
   1.235 +  done
   1.236 +
   1.237 +
   1.238 +subsection {* Existence *}
   1.239 +
   1.240 +lemma ex_nondec_lemma:
   1.241 +    "primel xs ==> \<exists>ys. primel ys \<and> nondec ys \<and> prod ys = prod xs"
   1.242 +  apply (blast intro: nondec_sort perm_prod perm_primel perm_sort perm_sym)
   1.243 +  done
   1.244 +
   1.245 +lemma not_prime_ex_mk:
   1.246 +  "1 < n \<and> n \<notin> prime ==>
   1.247 +    \<exists>m k. 1 < m \<and> 1 < k \<and> m < n \<and> k < n \<and> n = m * k"
   1.248 +  apply (unfold prime_def dvd_def)
   1.249 +  apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
   1.250 +  done
   1.251 +
   1.252 +lemma split_primel:
   1.253 +    "primel xs ==> primel ys ==> \<exists>l. primel l \<and> prod l = prod xs * prod ys"
   1.254 +  apply (rule exI)
   1.255 +  apply safe
   1.256 +   apply (rule_tac [2] prod_append)
   1.257 +  apply (simp add: primel_append)
   1.258 +  done
   1.259 +
   1.260 +lemma factor_exists [rule_format]: "1 < n --> (\<exists>l. primel l \<and> prod l = n)"
   1.261 +  apply (induct n rule: nat_less_induct)
   1.262 +  apply (rule impI)
   1.263 +  apply (case_tac "n \<in> prime")
   1.264 +   apply (rule exI)
   1.265 +   apply (erule prime_primel)
   1.266 +  apply (cut_tac n = n in not_prime_ex_mk)
   1.267 +   apply (auto intro!: split_primel)
   1.268 +  done
   1.269 +
   1.270 +lemma nondec_factor_exists: "1 < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
   1.271 +  apply (erule factor_exists [THEN exE])
   1.272 +  apply (blast intro!: ex_nondec_lemma)
   1.273 +  done
   1.274 +
   1.275 +
   1.276 +subsection {* Uniqueness *}
   1.277 +
   1.278 +lemma prime_dvd_mult_list [rule_format]:
   1.279 +    "p \<in> prime ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
   1.280 +  apply (induct xs)
   1.281 +   apply simp_all
   1.282 +   apply (erule prime_nd_one)
   1.283 +  apply (rule impI)
   1.284 +  apply (drule prime_dvd_mult)
   1.285 +   apply auto
   1.286 +  done
   1.287 +
   1.288 +lemma hd_xs_dvd_prod:
   1.289 +  "primel (x # xs) ==> primel ys ==> prod (x # xs) = prod ys
   1.290 +    ==> \<exists>m. m \<in> set ys \<and> x dvd m"
   1.291 +  apply (rule prime_dvd_mult_list)
   1.292 +   apply (simp add: primel_hd_tl)
   1.293 +  apply (erule hd_dvd_prod)
   1.294 +  done
   1.295 +
   1.296 +lemma prime_dvd_eq: "primel (x # xs) ==> primel ys ==> m \<in> set ys ==> x dvd m ==> x = m"
   1.297 +  apply (rule primes_eq)
   1.298 +    apply (auto simp add: primel_def primel_hd_tl)
   1.299 +  done
   1.300  
   1.301 -primrec
   1.302 -  "sort []     = []"
   1.303 -  "sort (x#xs) = oinsert x (sort xs)"  
   1.304 +lemma hd_xs_eq_prod:
   1.305 +  "primel (x # xs) ==>
   1.306 +    primel ys ==> prod (x # xs) = prod ys ==> x \<in> set ys"
   1.307 +  apply (frule hd_xs_dvd_prod)
   1.308 +    apply auto
   1.309 +  apply (drule prime_dvd_eq)
   1.310 +     apply auto
   1.311 +  done
   1.312 +
   1.313 +lemma perm_primel_ex:
   1.314 +  "primel (x # xs) ==>
   1.315 +    primel ys ==> prod (x # xs) = prod ys ==> \<exists>l. ys <~~> (x # l)"
   1.316 +  apply (rule exI)
   1.317 +  apply (rule perm_remove)
   1.318 +  apply (erule hd_xs_eq_prod)
   1.319 +   apply simp_all
   1.320 +  done
   1.321 +
   1.322 +lemma primel_prod_less:
   1.323 +  "primel (x # xs) ==>
   1.324 +    primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys"
   1.325 +  apply (auto intro: prod_mn_less_k prime_g_one primel_prod_gz simp add: primel_hd_tl)
   1.326 +  done
   1.327 +
   1.328 +lemma prod_one_empty:
   1.329 +    "primel xs ==> p * prod xs = p ==> p \<in> prime ==> xs = []"
   1.330 +  apply (auto intro: primel_one_empty simp add: prime_def)
   1.331 +  done
   1.332 +
   1.333 +lemma uniq_ex_aux:
   1.334 +  "\<forall>m. m < prod ys --> (\<forall>xs ys. primel xs \<and> primel ys \<and>
   1.335 +      prod xs = prod ys \<and> prod xs = m --> xs <~~> ys) ==>
   1.336 +    primel list ==> primel x ==> prod list = prod x ==> prod x < prod ys
   1.337 +    ==> x <~~> list"
   1.338 +  apply simp
   1.339 +  done
   1.340  
   1.341 -end
   1.342 \ No newline at end of file
   1.343 +lemma factor_unique [rule_format]:
   1.344 +  "\<forall>xs ys. primel xs \<and> primel ys \<and> prod xs = prod ys \<and> prod xs = n
   1.345 +    --> xs <~~> ys"
   1.346 +  apply (induct n rule: nat_less_induct)
   1.347 +  apply safe
   1.348 +  apply (case_tac xs)
   1.349 +   apply (force intro: primel_one_empty)
   1.350 +  apply (rule perm_primel_ex [THEN exE])
   1.351 +     apply simp_all
   1.352 +  apply (rule perm.trans [THEN perm_sym])
   1.353 +  apply assumption
   1.354 +  apply (rule perm.Cons)
   1.355 +  apply (case_tac "x = []")
   1.356 +   apply (simp add: perm_sing_eq primel_hd_tl)
   1.357 +   apply (rule_tac p = a in prod_one_empty)
   1.358 +     apply simp_all
   1.359 +  apply (erule uniq_ex_aux)
   1.360 +     apply (auto intro: primel_tl perm_primel simp add: primel_hd_tl)
   1.361 +   apply (rule_tac k = a and n = "prod list" and m = "prod x" in mult_left_cancel)
   1.362 +    apply (rule_tac [3] x = a in primel_prod_less)
   1.363 +      apply (rule_tac [2] prod_xy_prod)
   1.364 +      apply (rule_tac [2] s = "prod ys" in HOL.trans)
   1.365 +       apply (erule_tac [3] perm_prod)
   1.366 +      apply (erule_tac [5] perm_prod [symmetric])
   1.367 +     apply (auto intro: perm_primel prime_g_zero)
   1.368 +  done
   1.369 +
   1.370 +lemma perm_nondec_unique:
   1.371 +    "xs <~~> ys ==> nondec xs ==> nondec ys ==> xs = ys"
   1.372 +  apply (rule HOL.trans)
   1.373 +   apply (rule HOL.trans)
   1.374 +    apply (erule nondec_sort_eq)
   1.375 +   apply (erule perm_sort_eq)
   1.376 +  apply (erule nondec_sort_eq [symmetric])
   1.377 +  done
   1.378 +
   1.379 +lemma unique_prime_factorization [rule_format]:
   1.380 +    "\<forall>n. 1 < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
   1.381 +  apply safe
   1.382 +   apply (erule nondec_factor_exists)
   1.383 +  apply (rule perm_nondec_unique)
   1.384 +    apply (rule factor_unique)
   1.385 +    apply simp_all
   1.386 +  done
   1.387 +
   1.388 +end