src/HOL/Old_Number_Theory/Factorization.thy
changeset 32479 521cc9bf2958
parent 27368 9f90ac19e32b
child 38159 e9b4835a54ee
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Old_Number_Theory/Factorization.thy	Tue Sep 01 15:39:33 2009 +0200
     1.3 @@ -0,0 +1,339 @@
     1.4 +(*  Author:     Thomas Marthedal Rasmussen
     1.5 +    Copyright   2000  University of Cambridge
     1.6 +*)
     1.7 +
     1.8 +header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
     1.9 +
    1.10 +theory Factorization
    1.11 +imports Main "~~/src/HOL/Old_Number_Theory/Primes" Permutation
    1.12 +begin
    1.13 +
    1.14 +
    1.15 +subsection {* Definitions *}
    1.16 +
    1.17 +definition
    1.18 +  primel :: "nat list => bool" where
    1.19 +  "primel xs = (\<forall>p \<in> set xs. prime p)"
    1.20 +
    1.21 +consts
    1.22 +  nondec :: "nat list => bool "
    1.23 +  prod :: "nat list => nat"
    1.24 +  oinsert :: "nat => nat list => nat list"
    1.25 +  sort :: "nat list => nat list"
    1.26 +
    1.27 +primrec
    1.28 +  "nondec [] = True"
    1.29 +  "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
    1.30 +
    1.31 +primrec
    1.32 +  "prod [] = Suc 0"
    1.33 +  "prod (x # xs) = x * prod xs"
    1.34 +
    1.35 +primrec
    1.36 +  "oinsert x [] = [x]"
    1.37 +  "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
    1.38 +
    1.39 +primrec
    1.40 +  "sort [] = []"
    1.41 +  "sort (x # xs) = oinsert x (sort xs)"
    1.42 +
    1.43 +
    1.44 +subsection {* Arithmetic *}
    1.45 +
    1.46 +lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
    1.47 +  apply (cases m)
    1.48 +   apply auto
    1.49 +  done
    1.50 +
    1.51 +lemma one_less_k: "(m::nat) \<noteq> m * k ==> Suc 0 < m * k ==> Suc 0 < k"
    1.52 +  apply (cases k)
    1.53 +   apply auto
    1.54 +  done
    1.55 +
    1.56 +lemma mult_left_cancel: "(0::nat) < k ==> k * n = k * m ==> n = m"
    1.57 +  apply auto
    1.58 +  done
    1.59 +
    1.60 +lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = Suc 0"
    1.61 +  apply (cases n)
    1.62 +   apply auto
    1.63 +  done
    1.64 +
    1.65 +lemma prod_mn_less_k:
    1.66 +    "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k"
    1.67 +  apply (induct m)
    1.68 +   apply auto
    1.69 +  done
    1.70 +
    1.71 +
    1.72 +subsection {* Prime list and product *}
    1.73 +
    1.74 +lemma prod_append: "prod (xs @ ys) = prod xs * prod ys"
    1.75 +  apply (induct xs)
    1.76 +   apply (simp_all add: mult_assoc)
    1.77 +  done
    1.78 +
    1.79 +lemma prod_xy_prod:
    1.80 +    "prod (x # xs) = prod (y # ys) ==> x * prod xs = y * prod ys"
    1.81 +  apply auto
    1.82 +  done
    1.83 +
    1.84 +lemma primel_append: "primel (xs @ ys) = (primel xs \<and> primel ys)"
    1.85 +  apply (unfold primel_def)
    1.86 +  apply auto
    1.87 +  done
    1.88 +
    1.89 +lemma prime_primel: "prime n ==> primel [n] \<and> prod [n] = n"
    1.90 +  apply (unfold primel_def)
    1.91 +  apply auto
    1.92 +  done
    1.93 +
    1.94 +lemma prime_nd_one: "prime p ==> \<not> p dvd Suc 0"
    1.95 +  apply (unfold prime_def dvd_def)
    1.96 +  apply auto
    1.97 +  done
    1.98 +
    1.99 +lemma hd_dvd_prod: "prod (x # xs) = prod ys ==> x dvd (prod ys)" 
   1.100 +  by (metis dvd_mult_left dvd_refl prod.simps(2))
   1.101 +
   1.102 +lemma primel_tl: "primel (x # xs) ==> primel xs"
   1.103 +  apply (unfold primel_def)
   1.104 +  apply auto
   1.105 +  done
   1.106 +
   1.107 +lemma primel_hd_tl: "(primel (x # xs)) = (prime x \<and> primel xs)"
   1.108 +  apply (unfold primel_def)
   1.109 +  apply auto
   1.110 +  done
   1.111 +
   1.112 +lemma primes_eq: "prime p ==> prime q ==> p dvd q ==> p = q"
   1.113 +  apply (unfold prime_def)
   1.114 +  apply auto
   1.115 +  done
   1.116 +
   1.117 +lemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []"
   1.118 +  apply (cases xs)
   1.119 +   apply (simp_all add: primel_def prime_def)
   1.120 +  done
   1.121 +
   1.122 +lemma prime_g_one: "prime p ==> Suc 0 < p"
   1.123 +  apply (unfold prime_def)
   1.124 +  apply auto
   1.125 +  done
   1.126 +
   1.127 +lemma prime_g_zero: "prime p ==> 0 < p"
   1.128 +  apply (unfold prime_def)
   1.129 +  apply auto
   1.130 +  done
   1.131 +
   1.132 +lemma primel_nempty_g_one:
   1.133 +    "primel xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> Suc 0 < prod xs"
   1.134 +  apply (induct xs)
   1.135 +   apply simp
   1.136 +  apply (fastsimp simp: primel_def prime_def elim: one_less_mult)
   1.137 +  done
   1.138 +
   1.139 +lemma primel_prod_gz: "primel xs ==> 0 < prod xs"
   1.140 +  apply (induct xs)
   1.141 +   apply (auto simp: primel_def prime_def)
   1.142 +  done
   1.143 +
   1.144 +
   1.145 +subsection {* Sorting *}
   1.146 +
   1.147 +lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
   1.148 +  apply (induct xs)
   1.149 +   apply simp
   1.150 +   apply (case_tac xs)
   1.151 +    apply (simp_all cong del: list.weak_case_cong)
   1.152 +  done
   1.153 +
   1.154 +lemma nondec_sort: "nondec (sort xs)"
   1.155 +  apply (induct xs)
   1.156 +   apply simp_all
   1.157 +  apply (erule nondec_oinsert)
   1.158 +  done
   1.159 +
   1.160 +lemma x_less_y_oinsert: "x \<le> y ==> l = y # ys ==> x # l = oinsert x l"
   1.161 +  apply simp_all
   1.162 +  done
   1.163 +
   1.164 +lemma nondec_sort_eq [rule_format]: "nondec xs \<longrightarrow> xs = sort xs"
   1.165 +  apply (induct xs)
   1.166 +   apply safe
   1.167 +    apply simp_all
   1.168 +   apply (case_tac xs)
   1.169 +    apply simp_all
   1.170 +  apply (case_tac xs)
   1.171 +   apply simp
   1.172 +  apply (rule_tac y = aa and ys = list in x_less_y_oinsert)
   1.173 +   apply simp_all
   1.174 +  done
   1.175 +
   1.176 +lemma oinsert_x_y: "oinsert x (oinsert y l) = oinsert y (oinsert x l)"
   1.177 +  apply (induct l)
   1.178 +  apply auto
   1.179 +  done
   1.180 +
   1.181 +
   1.182 +subsection {* Permutation *}
   1.183 +
   1.184 +lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
   1.185 +  apply (unfold primel_def)
   1.186 +  apply (induct set: perm)
   1.187 +     apply simp
   1.188 +    apply simp
   1.189 +   apply (simp (no_asm))
   1.190 +   apply blast
   1.191 +  apply blast
   1.192 +  done
   1.193 +
   1.194 +lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
   1.195 +  apply (induct set: perm)
   1.196 +     apply (simp_all add: mult_ac)
   1.197 +  done
   1.198 +
   1.199 +lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
   1.200 +  apply (induct set: perm)
   1.201 +     apply auto
   1.202 +  done
   1.203 +
   1.204 +lemma perm_oinsert: "x # xs <~~> oinsert x xs"
   1.205 +  apply (induct xs)
   1.206 +   apply auto
   1.207 +  done
   1.208 +
   1.209 +lemma perm_sort: "xs <~~> sort xs"
   1.210 +  apply (induct xs)
   1.211 +  apply (auto intro: perm_oinsert elim: perm_subst_oinsert)
   1.212 +  done
   1.213 +
   1.214 +lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys"
   1.215 +  apply (induct set: perm)
   1.216 +     apply (simp_all add: oinsert_x_y)
   1.217 +  done
   1.218 +
   1.219 +
   1.220 +subsection {* Existence *}
   1.221 +
   1.222 +lemma ex_nondec_lemma:
   1.223 +    "primel xs ==> \<exists>ys. primel ys \<and> nondec ys \<and> prod ys = prod xs"
   1.224 +  apply (blast intro: nondec_sort perm_prod perm_primel perm_sort perm_sym)
   1.225 +  done
   1.226 +
   1.227 +lemma not_prime_ex_mk:
   1.228 +  "Suc 0 < n \<and> \<not> prime n ==>
   1.229 +    \<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
   1.230 +  apply (unfold prime_def dvd_def)
   1.231 +  apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
   1.232 +  done
   1.233 +
   1.234 +lemma split_primel:
   1.235 +  "primel xs \<Longrightarrow> primel ys \<Longrightarrow> \<exists>l. primel l \<and> prod l = prod xs * prod ys"
   1.236 +  apply (rule exI)
   1.237 +  apply safe
   1.238 +   apply (rule_tac [2] prod_append)
   1.239 +  apply (simp add: primel_append)
   1.240 +  done
   1.241 +
   1.242 +lemma factor_exists [rule_format]: "Suc 0 < n --> (\<exists>l. primel l \<and> prod l = n)"
   1.243 +  apply (induct n rule: nat_less_induct)
   1.244 +  apply (rule impI)
   1.245 +  apply (case_tac "prime n")
   1.246 +   apply (rule exI)
   1.247 +   apply (erule prime_primel)
   1.248 +  apply (cut_tac n = n in not_prime_ex_mk)
   1.249 +   apply (auto intro!: split_primel)
   1.250 +  done
   1.251 +
   1.252 +lemma nondec_factor_exists: "Suc 0 < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
   1.253 +  apply (erule factor_exists [THEN exE])
   1.254 +  apply (blast intro!: ex_nondec_lemma)
   1.255 +  done
   1.256 +
   1.257 +
   1.258 +subsection {* Uniqueness *}
   1.259 +
   1.260 +lemma prime_dvd_mult_list [rule_format]:
   1.261 +    "prime p ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
   1.262 +  apply (induct xs)
   1.263 +   apply (force simp add: prime_def)
   1.264 +   apply (force dest: prime_dvd_mult)
   1.265 +  done
   1.266 +
   1.267 +lemma hd_xs_dvd_prod:
   1.268 +  "primel (x # xs) ==> primel ys ==> prod (x # xs) = prod ys
   1.269 +    ==> \<exists>m. m \<in> set ys \<and> x dvd m"
   1.270 +  apply (rule prime_dvd_mult_list)
   1.271 +   apply (simp add: primel_hd_tl)
   1.272 +  apply (erule hd_dvd_prod)
   1.273 +  done
   1.274 +
   1.275 +lemma prime_dvd_eq: "primel (x # xs) ==> primel ys ==> m \<in> set ys ==> x dvd m ==> x = m"
   1.276 +  apply (rule primes_eq)
   1.277 +    apply (auto simp add: primel_def primel_hd_tl)
   1.278 +  done
   1.279 +
   1.280 +lemma hd_xs_eq_prod:
   1.281 +  "primel (x # xs) ==>
   1.282 +    primel ys ==> prod (x # xs) = prod ys ==> x \<in> set ys"
   1.283 +  apply (frule hd_xs_dvd_prod)
   1.284 +    apply auto
   1.285 +  apply (drule prime_dvd_eq)
   1.286 +     apply auto
   1.287 +  done
   1.288 +
   1.289 +lemma perm_primel_ex:
   1.290 +  "primel (x # xs) ==>
   1.291 +    primel ys ==> prod (x # xs) = prod ys ==> \<exists>l. ys <~~> (x # l)"
   1.292 +  apply (rule exI)
   1.293 +  apply (rule perm_remove)
   1.294 +  apply (erule hd_xs_eq_prod)
   1.295 +   apply simp_all
   1.296 +  done
   1.297 +
   1.298 +lemma primel_prod_less:
   1.299 +  "primel (x # xs) ==>
   1.300 +    primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys"
   1.301 +  by (metis less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff
   1.302 +    nat_less_le nat_mult_1 prime_def primel_hd_tl primel_prod_gz prod.simps(2))
   1.303 +
   1.304 +lemma prod_one_empty:
   1.305 +    "primel xs ==> p * prod xs = p ==> prime p ==> xs = []"
   1.306 +  apply (auto intro: primel_one_empty simp add: prime_def)
   1.307 +  done
   1.308 +
   1.309 +lemma uniq_ex_aux:
   1.310 +  "\<forall>m. m < prod ys --> (\<forall>xs ys. primel xs \<and> primel ys \<and>
   1.311 +      prod xs = prod ys \<and> prod xs = m --> xs <~~> ys) ==>
   1.312 +    primel list ==> primel x ==> prod list = prod x ==> prod x < prod ys
   1.313 +    ==> x <~~> list"
   1.314 +  apply simp
   1.315 +  done
   1.316 +
   1.317 +lemma factor_unique [rule_format]:
   1.318 +  "\<forall>xs ys. primel xs \<and> primel ys \<and> prod xs = prod ys \<and> prod xs = n
   1.319 +    --> xs <~~> ys"
   1.320 +  apply (induct n rule: nat_less_induct)
   1.321 +  apply safe
   1.322 +  apply (case_tac xs)
   1.323 +   apply (force intro: primel_one_empty)
   1.324 +  apply (rule perm_primel_ex [THEN exE])
   1.325 +     apply simp_all
   1.326 +  apply (rule perm.trans [THEN perm_sym])
   1.327 +  apply assumption
   1.328 +  apply (rule perm.Cons)
   1.329 +  apply (case_tac "x = []")
   1.330 +   apply (metis perm_prod perm_refl prime_primel primel_hd_tl primel_tl prod_one_empty)
   1.331 +  apply (metis nat_0_less_mult_iff nat_mult_eq_cancel1 perm_primel perm_prod primel_prod_gz primel_prod_less primel_tl prod.simps(2))
   1.332 +  done
   1.333 +
   1.334 +lemma perm_nondec_unique:
   1.335 +    "xs <~~> ys ==> nondec xs ==> nondec ys ==> xs = ys"
   1.336 +  by (metis nondec_sort_eq perm_sort_eq)
   1.337 +
   1.338 +theorem unique_prime_factorization [rule_format]:
   1.339 +    "\<forall>n. Suc 0 < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
   1.340 +  by (metis factor_unique nondec_factor_exists perm_nondec_unique)
   1.341 +
   1.342 +end