# Theory Factorization

Up to index of Isabelle/HOL/Old_Number_Theory

theory Factorization
imports Primes Permutation
`(*  Title:      HOL/Old_Number_Theory/Factorization.thy    Author:     Thomas Marthedal Rasmussen    Copyright   2000  University of Cambridge*)header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}theory Factorizationimports Primes "~~/src/HOL/Library/Permutation"beginsubsection {* Definitions *}definition primel :: "nat list => bool"  where "primel xs = (∀p ∈ set xs. prime p)"primrec nondec :: "nat list => bool"where  "nondec [] = True"| "nondec (x # xs) = (case xs of [] => True | y # ys => x ≤ y ∧ nondec xs)"primrec prod :: "nat list => nat"where  "prod [] = Suc 0"| "prod (x # xs) = x * prod xs"primrec oinsert :: "nat => nat list => nat list"where  "oinsert x [] = [x]"| "oinsert x (y # ys) = (if x ≤ y then x # y # ys else y # oinsert x ys)"primrec sort :: "nat list => nat list"where  "sort [] = []"| "sort (x # xs) = oinsert x (sort xs)"subsection {* Arithmetic *}lemma one_less_m: "(m::nat) ≠ m * k ==> m ≠ Suc 0 ==> Suc 0 < m"  apply (cases m)   apply auto  donelemma one_less_k: "(m::nat) ≠ m * k ==> Suc 0 < m * k ==> Suc 0 < k"  apply (cases k)   apply auto  donelemma mult_left_cancel: "(0::nat) < k ==> k * n = k * m ==> n = m"  apply auto  donelemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = Suc 0"  apply (cases n)   apply auto  donelemma prod_mn_less_k:    "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k"  apply (induct m)   apply auto  donesubsection {* Prime list and product *}lemma prod_append: "prod (xs @ ys) = prod xs * prod ys"  apply (induct xs)   apply (simp_all add: mult_assoc)  donelemma prod_xy_prod:    "prod (x # xs) = prod (y # ys) ==> x * prod xs = y * prod ys"  apply auto  donelemma primel_append: "primel (xs @ ys) = (primel xs ∧ primel ys)"  apply (unfold primel_def)  apply auto  donelemma prime_primel: "prime n ==> primel [n] ∧ prod [n] = n"  apply (unfold primel_def)  apply auto  donelemma prime_nd_one: "prime p ==> ¬ p dvd Suc 0"  apply (unfold prime_def dvd_def)  apply auto  donelemma hd_dvd_prod: "prod (x # xs) = prod ys ==> x dvd (prod ys)"   by (metis dvd_mult_left dvd_refl prod.simps(2))lemma primel_tl: "primel (x # xs) ==> primel xs"  apply (unfold primel_def)  apply auto  donelemma primel_hd_tl: "(primel (x # xs)) = (prime x ∧ primel xs)"  apply (unfold primel_def)  apply auto  donelemma primes_eq: "prime p ==> prime q ==> p dvd q ==> p = q"  apply (unfold prime_def)  apply auto  donelemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []"  apply (cases xs)   apply (simp_all add: primel_def prime_def)  donelemma prime_g_one: "prime p ==> Suc 0 < p"  apply (unfold prime_def)  apply auto  donelemma prime_g_zero: "prime p ==> 0 < p"  apply (unfold prime_def)  apply auto  donelemma primel_nempty_g_one:    "primel xs ==> xs ≠ [] ==> Suc 0 < prod xs"  apply (induct xs)   apply simp  apply (fastsimp simp: primel_def prime_def elim: one_less_mult)  donelemma primel_prod_gz: "primel xs ==> 0 < prod xs"  apply (induct xs)   apply (auto simp: primel_def prime_def)  donesubsection {* Sorting *}lemma nondec_oinsert: "nondec xs ==> nondec (oinsert x xs)"  apply (induct xs)   apply simp   apply (case_tac xs)    apply (simp_all cong del: list.weak_case_cong)  donelemma nondec_sort: "nondec (sort xs)"  apply (induct xs)   apply simp_all  apply (erule nondec_oinsert)  donelemma x_less_y_oinsert: "x ≤ y ==> l = y # ys ==> x # l = oinsert x l"  apply simp_all  donelemma nondec_sort_eq [rule_format]: "nondec xs --> xs = sort xs"  apply (induct xs)   apply safe    apply simp_all   apply (case_tac xs)    apply simp_all  apply (case_tac xs)   apply simp  apply (rule_tac y = aa and ys = list in x_less_y_oinsert)   apply simp_all  donelemma oinsert_x_y: "oinsert x (oinsert y l) = oinsert y (oinsert x l)"  apply (induct l)  apply auto  donesubsection {* Permutation *}lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"  apply (unfold primel_def)  apply (induct set: perm)     apply simp    apply simp   apply (simp (no_asm))   apply blast  apply blast  donelemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"  apply (induct set: perm)     apply (simp_all add: mult_ac)  donelemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"  apply (induct set: perm)     apply auto  donelemma perm_oinsert: "x # xs <~~> oinsert x xs"  apply (induct xs)   apply auto  donelemma perm_sort: "xs <~~> sort xs"  apply (induct xs)  apply (auto intro: perm_oinsert elim: perm_subst_oinsert)  donelemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys"  apply (induct set: perm)     apply (simp_all add: oinsert_x_y)  donesubsection {* Existence *}lemma ex_nondec_lemma:    "primel xs ==> ∃ys. primel ys ∧ nondec ys ∧ prod ys = prod xs"  apply (blast intro: nondec_sort perm_prod perm_primel perm_sort perm_sym)  donelemma not_prime_ex_mk:  "Suc 0 < n ∧ ¬ prime n ==>    ∃m k. Suc 0 < m ∧ Suc 0 < k ∧ m < n ∧ k < n ∧ n = m * k"  apply (unfold prime_def dvd_def)  apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)  donelemma split_primel:  "primel xs ==> primel ys ==> ∃l. primel l ∧ prod l = prod xs * prod ys"  apply (rule exI)  apply safe   apply (rule_tac  prod_append)  apply (simp add: primel_append)  donelemma factor_exists [rule_format]: "Suc 0 < n --> (∃l. primel l ∧ prod l = n)"  apply (induct n rule: nat_less_induct)  apply (rule impI)  apply (case_tac "prime n")   apply (rule exI)   apply (erule prime_primel)  apply (cut_tac n = n in not_prime_ex_mk)   apply (auto intro!: split_primel)  donelemma nondec_factor_exists: "Suc 0 < n ==> ∃l. primel l ∧ nondec l ∧ prod l = n"  apply (erule factor_exists [THEN exE])  apply (blast intro!: ex_nondec_lemma)  donesubsection {* Uniqueness *}lemma prime_dvd_mult_list [rule_format]:    "prime p ==> p dvd (prod xs) --> (∃m. m:set xs ∧ p dvd m)"  apply (induct xs)   apply (force simp add: prime_def)   apply (force dest: prime_dvd_mult)  donelemma hd_xs_dvd_prod:  "primel (x # xs) ==> primel ys ==> prod (x # xs) = prod ys    ==> ∃m. m ∈ set ys ∧ x dvd m"  apply (rule prime_dvd_mult_list)   apply (simp add: primel_hd_tl)  apply (erule hd_dvd_prod)  donelemma prime_dvd_eq: "primel (x # xs) ==> primel ys ==> m ∈ set ys ==> x dvd m ==> x = m"  apply (rule primes_eq)    apply (auto simp add: primel_def primel_hd_tl)  donelemma hd_xs_eq_prod:  "primel (x # xs) ==>    primel ys ==> prod (x # xs) = prod ys ==> x ∈ set ys"  apply (frule hd_xs_dvd_prod)    apply auto  apply (drule prime_dvd_eq)     apply auto  donelemma perm_primel_ex:  "primel (x # xs) ==>    primel ys ==> prod (x # xs) = prod ys ==> ∃l. ys <~~> (x # l)"  apply (rule exI)  apply (rule perm_remove)  apply (erule hd_xs_eq_prod)   apply simp_all  donelemma primel_prod_less:  "primel (x # xs) ==>    primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys"  by (metis less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff    nat_less_le nat_mult_1 prime_def primel_hd_tl primel_prod_gz prod.simps(2))lemma prod_one_empty:    "primel xs ==> p * prod xs = p ==> prime p ==> xs = []"  apply (auto intro: primel_one_empty simp add: prime_def)  donelemma uniq_ex_aux:  "∀m. m < prod ys --> (∀xs ys. primel xs ∧ primel ys ∧      prod xs = prod ys ∧ prod xs = m --> xs <~~> ys) ==>    primel list ==> primel x ==> prod list = prod x ==> prod x < prod ys    ==> x <~~> list"  apply simp  donelemma factor_unique [rule_format]:  "∀xs ys. primel xs ∧ primel ys ∧ prod xs = prod ys ∧ prod xs = n    --> xs <~~> ys"  apply (induct n rule: nat_less_induct)  apply safe  apply (case_tac xs)   apply (force intro: primel_one_empty)  apply (rule perm_primel_ex [THEN exE])     apply simp_all  apply (rule perm.trans [THEN perm_sym])  apply assumption  apply (rule perm.Cons)  apply (case_tac "x = []")   apply (metis perm_prod perm_refl prime_primel primel_hd_tl primel_tl prod_one_empty)  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))  donelemma perm_nondec_unique:    "xs <~~> ys ==> nondec xs ==> nondec ys ==> xs = ys"  by (metis nondec_sort_eq perm_sort_eq)theorem unique_prime_factorization [rule_format]:    "∀n. Suc 0 < n --> (∃!l. primel l ∧ nondec l ∧ prod l = n)"  by (metis factor_unique nondec_factor_exists perm_nondec_unique)end`