src/HOL/Old_Number_Theory/Factorization.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 44890 22f665a2e91c
child 57512 cc97b347b301
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
     1 (*  Title:      HOL/Old_Number_Theory/Factorization.thy
     2     Author:     Thomas Marthedal Rasmussen
     3     Copyright   2000  University of Cambridge
     4 *)
     5 
     6 header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
     7 
     8 theory Factorization
     9 imports Primes "~~/src/HOL/Library/Permutation"
    10 begin
    11 
    12 
    13 subsection {* Definitions *}
    14 
    15 definition primel :: "nat list => bool"
    16   where "primel xs = (\<forall>p \<in> set xs. prime p)"
    17 
    18 primrec nondec :: "nat list => bool"
    19 where
    20   "nondec [] = True"
    21 | "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
    22 
    23 primrec prod :: "nat list => nat"
    24 where
    25   "prod [] = Suc 0"
    26 | "prod (x # xs) = x * prod xs"
    27 
    28 primrec oinsert :: "nat => nat list => nat list"
    29 where
    30   "oinsert x [] = [x]"
    31 | "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
    32 
    33 primrec sort :: "nat list => nat list"
    34 where
    35   "sort [] = []"
    36 | "sort (x # xs) = oinsert x (sort xs)"
    37 
    38 
    39 subsection {* Arithmetic *}
    40 
    41 lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
    42   apply (cases m)
    43    apply auto
    44   done
    45 
    46 lemma one_less_k: "(m::nat) \<noteq> m * k ==> Suc 0 < m * k ==> Suc 0 < k"
    47   apply (cases k)
    48    apply auto
    49   done
    50 
    51 lemma mult_left_cancel: "(0::nat) < k ==> k * n = k * m ==> n = m"
    52   apply auto
    53   done
    54 
    55 lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = Suc 0"
    56   apply (cases n)
    57    apply auto
    58   done
    59 
    60 lemma prod_mn_less_k:
    61     "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k"
    62   apply (induct m)
    63    apply auto
    64   done
    65 
    66 
    67 subsection {* Prime list and product *}
    68 
    69 lemma prod_append: "prod (xs @ ys) = prod xs * prod ys"
    70   apply (induct xs)
    71    apply (simp_all add: mult_assoc)
    72   done
    73 
    74 lemma prod_xy_prod:
    75     "prod (x # xs) = prod (y # ys) ==> x * prod xs = y * prod ys"
    76   apply auto
    77   done
    78 
    79 lemma primel_append: "primel (xs @ ys) = (primel xs \<and> primel ys)"
    80   apply (unfold primel_def)
    81   apply auto
    82   done
    83 
    84 lemma prime_primel: "prime n ==> primel [n] \<and> prod [n] = n"
    85   apply (unfold primel_def)
    86   apply auto
    87   done
    88 
    89 lemma prime_nd_one: "prime p ==> \<not> p dvd Suc 0"
    90   apply (unfold prime_def dvd_def)
    91   apply auto
    92   done
    93 
    94 lemma hd_dvd_prod: "prod (x # xs) = prod ys ==> x dvd (prod ys)" 
    95   by (metis dvd_mult_left dvd_refl prod.simps(2))
    96 
    97 lemma primel_tl: "primel (x # xs) ==> primel xs"
    98   apply (unfold primel_def)
    99   apply auto
   100   done
   101 
   102 lemma primel_hd_tl: "(primel (x # xs)) = (prime x \<and> primel xs)"
   103   apply (unfold primel_def)
   104   apply auto
   105   done
   106 
   107 lemma primes_eq: "prime p ==> prime q ==> p dvd q ==> p = q"
   108   apply (unfold prime_def)
   109   apply auto
   110   done
   111 
   112 lemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []"
   113   apply (cases xs)
   114    apply (simp_all add: primel_def prime_def)
   115   done
   116 
   117 lemma prime_g_one: "prime p ==> Suc 0 < p"
   118   apply (unfold prime_def)
   119   apply auto
   120   done
   121 
   122 lemma prime_g_zero: "prime p ==> 0 < p"
   123   apply (unfold prime_def)
   124   apply auto
   125   done
   126 
   127 lemma primel_nempty_g_one:
   128     "primel xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> Suc 0 < prod xs"
   129   apply (induct xs)
   130    apply simp
   131   apply (fastforce simp: primel_def prime_def elim: one_less_mult)
   132   done
   133 
   134 lemma primel_prod_gz: "primel xs ==> 0 < prod xs"
   135   apply (induct xs)
   136    apply (auto simp: primel_def prime_def)
   137   done
   138 
   139 
   140 subsection {* Sorting *}
   141 
   142 lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
   143   apply (induct xs)
   144    apply simp
   145    apply (case_tac xs)
   146     apply (simp_all cong del: list.weak_case_cong)
   147   done
   148 
   149 lemma nondec_sort: "nondec (sort xs)"
   150   apply (induct xs)
   151    apply simp_all
   152   apply (erule nondec_oinsert)
   153   done
   154 
   155 lemma x_less_y_oinsert: "x \<le> y ==> l = y # ys ==> x # l = oinsert x l"
   156   apply simp_all
   157   done
   158 
   159 lemma nondec_sort_eq [rule_format]: "nondec xs \<longrightarrow> xs = sort xs"
   160   apply (induct xs)
   161    apply safe
   162     apply simp_all
   163    apply (case_tac xs)
   164     apply simp_all
   165   apply (case_tac xs)
   166    apply simp
   167   apply (rule_tac y = aa and ys = list in x_less_y_oinsert)
   168    apply simp_all
   169   done
   170 
   171 lemma oinsert_x_y: "oinsert x (oinsert y l) = oinsert y (oinsert x l)"
   172   apply (induct l)
   173   apply auto
   174   done
   175 
   176 
   177 subsection {* Permutation *}
   178 
   179 lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
   180   apply (unfold primel_def)
   181   apply (induct set: perm)
   182      apply simp
   183     apply simp
   184    apply (simp (no_asm))
   185    apply blast
   186   apply blast
   187   done
   188 
   189 lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
   190   apply (induct set: perm)
   191      apply (simp_all add: mult_ac)
   192   done
   193 
   194 lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
   195   apply (induct set: perm)
   196      apply auto
   197   done
   198 
   199 lemma perm_oinsert: "x # xs <~~> oinsert x xs"
   200   apply (induct xs)
   201    apply auto
   202   done
   203 
   204 lemma perm_sort: "xs <~~> sort xs"
   205   apply (induct xs)
   206   apply (auto intro: perm_oinsert elim: perm_subst_oinsert)
   207   done
   208 
   209 lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys"
   210   apply (induct set: perm)
   211      apply (simp_all add: oinsert_x_y)
   212   done
   213 
   214 
   215 subsection {* Existence *}
   216 
   217 lemma ex_nondec_lemma:
   218     "primel xs ==> \<exists>ys. primel ys \<and> nondec ys \<and> prod ys = prod xs"
   219   apply (blast intro: nondec_sort perm_prod perm_primel perm_sort perm_sym)
   220   done
   221 
   222 lemma not_prime_ex_mk:
   223   "Suc 0 < n \<and> \<not> prime n ==>
   224     \<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
   225   apply (unfold prime_def dvd_def)
   226   apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
   227   done
   228 
   229 lemma split_primel:
   230   "primel xs \<Longrightarrow> primel ys \<Longrightarrow> \<exists>l. primel l \<and> prod l = prod xs * prod ys"
   231   apply (rule exI)
   232   apply safe
   233    apply (rule_tac [2] prod_append)
   234   apply (simp add: primel_append)
   235   done
   236 
   237 lemma factor_exists [rule_format]: "Suc 0 < n --> (\<exists>l. primel l \<and> prod l = n)"
   238   apply (induct n rule: nat_less_induct)
   239   apply (rule impI)
   240   apply (case_tac "prime n")
   241    apply (rule exI)
   242    apply (erule prime_primel)
   243   apply (cut_tac n = n in not_prime_ex_mk)
   244    apply (auto intro!: split_primel)
   245   done
   246 
   247 lemma nondec_factor_exists: "Suc 0 < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
   248   apply (erule factor_exists [THEN exE])
   249   apply (blast intro!: ex_nondec_lemma)
   250   done
   251 
   252 
   253 subsection {* Uniqueness *}
   254 
   255 lemma prime_dvd_mult_list [rule_format]:
   256     "prime p ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
   257   apply (induct xs)
   258    apply (force simp add: prime_def)
   259    apply (force dest: prime_dvd_mult)
   260   done
   261 
   262 lemma hd_xs_dvd_prod:
   263   "primel (x # xs) ==> primel ys ==> prod (x # xs) = prod ys
   264     ==> \<exists>m. m \<in> set ys \<and> x dvd m"
   265   apply (rule prime_dvd_mult_list)
   266    apply (simp add: primel_hd_tl)
   267   apply (erule hd_dvd_prod)
   268   done
   269 
   270 lemma prime_dvd_eq: "primel (x # xs) ==> primel ys ==> m \<in> set ys ==> x dvd m ==> x = m"
   271   apply (rule primes_eq)
   272     apply (auto simp add: primel_def primel_hd_tl)
   273   done
   274 
   275 lemma hd_xs_eq_prod:
   276   "primel (x # xs) ==>
   277     primel ys ==> prod (x # xs) = prod ys ==> x \<in> set ys"
   278   apply (frule hd_xs_dvd_prod)
   279     apply auto
   280   apply (drule prime_dvd_eq)
   281      apply auto
   282   done
   283 
   284 lemma perm_primel_ex:
   285   "primel (x # xs) ==>
   286     primel ys ==> prod (x # xs) = prod ys ==> \<exists>l. ys <~~> (x # l)"
   287   apply (rule exI)
   288   apply (rule perm_remove)
   289   apply (erule hd_xs_eq_prod)
   290    apply simp_all
   291   done
   292 
   293 lemma primel_prod_less:
   294   "primel (x # xs) ==>
   295     primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys"
   296   by (metis less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff
   297     nat_less_le nat_mult_1 prime_def primel_hd_tl primel_prod_gz prod.simps(2))
   298 
   299 lemma prod_one_empty:
   300     "primel xs ==> p * prod xs = p ==> prime p ==> xs = []"
   301   apply (auto intro: primel_one_empty simp add: prime_def)
   302   done
   303 
   304 lemma uniq_ex_aux:
   305   "\<forall>m. m < prod ys --> (\<forall>xs ys. primel xs \<and> primel ys \<and>
   306       prod xs = prod ys \<and> prod xs = m --> xs <~~> ys) ==>
   307     primel list ==> primel x ==> prod list = prod x ==> prod x < prod ys
   308     ==> x <~~> list"
   309   apply simp
   310   done
   311 
   312 lemma factor_unique [rule_format]:
   313   "\<forall>xs ys. primel xs \<and> primel ys \<and> prod xs = prod ys \<and> prod xs = n
   314     --> xs <~~> ys"
   315   apply (induct n rule: nat_less_induct)
   316   apply safe
   317   apply (case_tac xs)
   318    apply (force intro: primel_one_empty)
   319   apply (rule perm_primel_ex [THEN exE])
   320      apply simp_all
   321   apply (rule perm.trans [THEN perm_sym])
   322   apply assumption
   323   apply (rule perm.Cons)
   324   apply (case_tac "x = []")
   325    apply (metis perm_prod perm_refl prime_primel primel_hd_tl primel_tl prod_one_empty)
   326   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))
   327   done
   328 
   329 lemma perm_nondec_unique:
   330     "xs <~~> ys ==> nondec xs ==> nondec ys ==> xs = ys"
   331   by (metis nondec_sort_eq perm_sort_eq)
   332 
   333 theorem unique_prime_factorization [rule_format]:
   334     "\<forall>n. Suc 0 < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
   335   by (metis factor_unique nondec_factor_exists perm_nondec_unique)
   336 
   337 end