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