src/HOL/Old_Number_Theory/Factorization.thy
author haftmann
Tue Sep 01 15:39:33 2009 +0200 (2009-09-01)
changeset 32479 521cc9bf2958
parent 27368 src/HOL/NumberTheory/Factorization.thy@9f90ac19e32b
child 38159 e9b4835a54ee
permissions -rw-r--r--
some reorganization of number theory
     1 (*  Author:     Thomas Marthedal Rasmussen
     2     Copyright   2000  University of Cambridge
     3 *)
     4 
     5 header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
     6 
     7 theory Factorization
     8 imports Main "~~/src/HOL/Old_Number_Theory/Primes" Permutation
     9 begin
    10 
    11 
    12 subsection {* Definitions *}
    13 
    14 definition
    15   primel :: "nat list => bool" where
    16   "primel xs = (\<forall>p \<in> set xs. prime p)"
    17 
    18 consts
    19   nondec :: "nat list => bool "
    20   prod :: "nat list => nat"
    21   oinsert :: "nat => nat list => nat list"
    22   sort :: "nat list => nat list"
    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 (cases 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 (cases 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 (cases 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: "prime n ==> primel [n] \<and> prod [n] = n"
    87   apply (unfold primel_def)
    88   apply auto
    89   done
    90 
    91 lemma prime_nd_one: "prime p ==> \<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   by (metis dvd_mult_left dvd_refl prod.simps(2))
    98 
    99 lemma primel_tl: "primel (x # xs) ==> primel xs"
   100   apply (unfold primel_def)
   101   apply auto
   102   done
   103 
   104 lemma primel_hd_tl: "(primel (x # xs)) = (prime x \<and> primel xs)"
   105   apply (unfold primel_def)
   106   apply auto
   107   done
   108 
   109 lemma primes_eq: "prime p ==> prime q ==> p dvd q ==> p = q"
   110   apply (unfold prime_def)
   111   apply auto
   112   done
   113 
   114 lemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []"
   115   apply (cases xs)
   116    apply (simp_all add: primel_def prime_def)
   117   done
   118 
   119 lemma prime_g_one: "prime p ==> Suc 0 < p"
   120   apply (unfold prime_def)
   121   apply auto
   122   done
   123 
   124 lemma prime_g_zero: "prime p ==> 0 < p"
   125   apply (unfold prime_def)
   126   apply auto
   127   done
   128 
   129 lemma primel_nempty_g_one:
   130     "primel xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> Suc 0 < prod xs"
   131   apply (induct xs)
   132    apply simp
   133   apply (fastsimp simp: primel_def prime_def elim: one_less_mult)
   134   done
   135 
   136 lemma primel_prod_gz: "primel xs ==> 0 < prod xs"
   137   apply (induct xs)
   138    apply (auto simp: primel_def prime_def)
   139   done
   140 
   141 
   142 subsection {* Sorting *}
   143 
   144 lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
   145   apply (induct xs)
   146    apply simp
   147    apply (case_tac xs)
   148     apply (simp_all cong del: list.weak_case_cong)
   149   done
   150 
   151 lemma nondec_sort: "nondec (sort xs)"
   152   apply (induct xs)
   153    apply simp_all
   154   apply (erule nondec_oinsert)
   155   done
   156 
   157 lemma x_less_y_oinsert: "x \<le> y ==> l = y # ys ==> x # l = oinsert x l"
   158   apply simp_all
   159   done
   160 
   161 lemma nondec_sort_eq [rule_format]: "nondec xs \<longrightarrow> xs = sort xs"
   162   apply (induct xs)
   163    apply safe
   164     apply simp_all
   165    apply (case_tac xs)
   166     apply simp_all
   167   apply (case_tac xs)
   168    apply simp
   169   apply (rule_tac y = aa and ys = list in x_less_y_oinsert)
   170    apply simp_all
   171   done
   172 
   173 lemma oinsert_x_y: "oinsert x (oinsert y l) = oinsert y (oinsert x l)"
   174   apply (induct l)
   175   apply auto
   176   done
   177 
   178 
   179 subsection {* Permutation *}
   180 
   181 lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
   182   apply (unfold primel_def)
   183   apply (induct set: perm)
   184      apply simp
   185     apply simp
   186    apply (simp (no_asm))
   187    apply blast
   188   apply blast
   189   done
   190 
   191 lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
   192   apply (induct set: perm)
   193      apply (simp_all add: mult_ac)
   194   done
   195 
   196 lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
   197   apply (induct set: perm)
   198      apply auto
   199   done
   200 
   201 lemma perm_oinsert: "x # xs <~~> oinsert x xs"
   202   apply (induct xs)
   203    apply auto
   204   done
   205 
   206 lemma perm_sort: "xs <~~> sort xs"
   207   apply (induct xs)
   208   apply (auto intro: perm_oinsert elim: perm_subst_oinsert)
   209   done
   210 
   211 lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys"
   212   apply (induct set: perm)
   213      apply (simp_all add: oinsert_x_y)
   214   done
   215 
   216 
   217 subsection {* Existence *}
   218 
   219 lemma ex_nondec_lemma:
   220     "primel xs ==> \<exists>ys. primel ys \<and> nondec ys \<and> prod ys = prod xs"
   221   apply (blast intro: nondec_sort perm_prod perm_primel perm_sort perm_sym)
   222   done
   223 
   224 lemma not_prime_ex_mk:
   225   "Suc 0 < n \<and> \<not> prime n ==>
   226     \<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
   227   apply (unfold prime_def dvd_def)
   228   apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
   229   done
   230 
   231 lemma split_primel:
   232   "primel xs \<Longrightarrow> primel ys \<Longrightarrow> \<exists>l. primel l \<and> prod l = prod xs * prod ys"
   233   apply (rule exI)
   234   apply safe
   235    apply (rule_tac [2] prod_append)
   236   apply (simp add: primel_append)
   237   done
   238 
   239 lemma factor_exists [rule_format]: "Suc 0 < n --> (\<exists>l. primel l \<and> prod l = n)"
   240   apply (induct n rule: nat_less_induct)
   241   apply (rule impI)
   242   apply (case_tac "prime n")
   243    apply (rule exI)
   244    apply (erule prime_primel)
   245   apply (cut_tac n = n in not_prime_ex_mk)
   246    apply (auto intro!: split_primel)
   247   done
   248 
   249 lemma nondec_factor_exists: "Suc 0 < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
   250   apply (erule factor_exists [THEN exE])
   251   apply (blast intro!: ex_nondec_lemma)
   252   done
   253 
   254 
   255 subsection {* Uniqueness *}
   256 
   257 lemma prime_dvd_mult_list [rule_format]:
   258     "prime p ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
   259   apply (induct xs)
   260    apply (force simp add: prime_def)
   261    apply (force dest: prime_dvd_mult)
   262   done
   263 
   264 lemma hd_xs_dvd_prod:
   265   "primel (x # xs) ==> primel ys ==> prod (x # xs) = prod ys
   266     ==> \<exists>m. m \<in> set ys \<and> x dvd m"
   267   apply (rule prime_dvd_mult_list)
   268    apply (simp add: primel_hd_tl)
   269   apply (erule hd_dvd_prod)
   270   done
   271 
   272 lemma prime_dvd_eq: "primel (x # xs) ==> primel ys ==> m \<in> set ys ==> x dvd m ==> x = m"
   273   apply (rule primes_eq)
   274     apply (auto simp add: primel_def primel_hd_tl)
   275   done
   276 
   277 lemma hd_xs_eq_prod:
   278   "primel (x # xs) ==>
   279     primel ys ==> prod (x # xs) = prod ys ==> x \<in> set ys"
   280   apply (frule hd_xs_dvd_prod)
   281     apply auto
   282   apply (drule prime_dvd_eq)
   283      apply auto
   284   done
   285 
   286 lemma perm_primel_ex:
   287   "primel (x # xs) ==>
   288     primel ys ==> prod (x # xs) = prod ys ==> \<exists>l. ys <~~> (x # l)"
   289   apply (rule exI)
   290   apply (rule perm_remove)
   291   apply (erule hd_xs_eq_prod)
   292    apply simp_all
   293   done
   294 
   295 lemma primel_prod_less:
   296   "primel (x # xs) ==>
   297     primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys"
   298   by (metis less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff
   299     nat_less_le nat_mult_1 prime_def primel_hd_tl primel_prod_gz prod.simps(2))
   300 
   301 lemma prod_one_empty:
   302     "primel xs ==> p * prod xs = p ==> prime p ==> xs = []"
   303   apply (auto intro: primel_one_empty simp add: prime_def)
   304   done
   305 
   306 lemma uniq_ex_aux:
   307   "\<forall>m. m < prod ys --> (\<forall>xs ys. primel xs \<and> primel ys \<and>
   308       prod xs = prod ys \<and> prod xs = m --> xs <~~> ys) ==>
   309     primel list ==> primel x ==> prod list = prod x ==> prod x < prod ys
   310     ==> x <~~> list"
   311   apply simp
   312   done
   313 
   314 lemma factor_unique [rule_format]:
   315   "\<forall>xs ys. primel xs \<and> primel ys \<and> prod xs = prod ys \<and> prod xs = n
   316     --> xs <~~> ys"
   317   apply (induct n rule: nat_less_induct)
   318   apply safe
   319   apply (case_tac xs)
   320    apply (force intro: primel_one_empty)
   321   apply (rule perm_primel_ex [THEN exE])
   322      apply simp_all
   323   apply (rule perm.trans [THEN perm_sym])
   324   apply assumption
   325   apply (rule perm.Cons)
   326   apply (case_tac "x = []")
   327    apply (metis perm_prod perm_refl prime_primel primel_hd_tl primel_tl prod_one_empty)
   328   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))
   329   done
   330 
   331 lemma perm_nondec_unique:
   332     "xs <~~> ys ==> nondec xs ==> nondec ys ==> xs = ys"
   333   by (metis nondec_sort_eq perm_sort_eq)
   334 
   335 theorem unique_prime_factorization [rule_format]:
   336     "\<forall>n. Suc 0 < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
   337   by (metis factor_unique nondec_factor_exists perm_nondec_unique)
   338 
   339 end