# Theory Factorization

theory Factorization
imports Primes Permutation
(*  Title:      HOL/Old_Number_Theory/Factorization.thy
Author:     Thomas Marthedal Rasmussen
*)

section ‹Fundamental Theorem of Arithmetic (unique factorization into primes)›

theory Factorization
imports Primes "~~/src/HOL/Library/Permutation"
begin

subsection ‹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
done

lemma one_less_k: "(m::nat) ≠ m * k ==> Suc 0 < m * k ==> Suc 0 < k"
apply (cases k)
apply auto
done

lemma mult_left_cancel: "(0::nat) < k ==> k * n = k * m ==> n = m"
apply auto
done

lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = Suc 0"
apply (cases n)
apply auto
done

lemma prod_mn_less_k:
"(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k"
apply (induct m)
apply auto
done

subsection ‹Prime list and product›

lemma prod_append: "prod (xs @ ys) = prod xs * prod ys"
apply (induct xs)
done

lemma prod_xy_prod:
"prod (x # xs) = prod (y # ys) ==> x * prod xs = y * prod ys"
apply auto
done

lemma primel_append: "primel (xs @ ys) = (primel xs ∧ primel ys)"
apply (unfold primel_def)
apply auto
done

lemma prime_primel: "prime n ==> primel [n] ∧ prod [n] = n"
apply (unfold primel_def)
apply auto
done

lemma prime_nd_one: "prime p ==> ¬ p dvd Suc 0"
apply (unfold prime_def dvd_def)
apply auto
done

lemma 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
done

lemma primel_hd_tl: "(primel (x # xs)) = (prime x ∧ primel xs)"
apply (unfold primel_def)
apply auto
done

lemma primes_eq: "prime p ==> prime q ==> p dvd q ==> p = q"
apply (unfold prime_def)
apply auto
done

lemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []"
apply (cases xs)
done

lemma prime_g_one: "prime p ==> Suc 0 < p"
apply (unfold prime_def)
apply auto
done

lemma prime_g_zero: "prime p ==> 0 < p"
apply (unfold prime_def)
apply auto
done

lemma primel_nempty_g_one:
"primel xs ⟹ xs ≠ [] ⟹ Suc 0 < prod xs"
apply (induct xs)
apply simp
apply (fastforce simp: primel_def prime_def elim: one_less_mult)
done

lemma primel_prod_gz: "primel xs ==> 0 < prod xs"
apply (induct xs)
apply (auto simp: primel_def prime_def)
done

subsection ‹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.case_cong_weak)
done

lemma nondec_sort: "nondec (sort xs)"
apply (induct xs)
apply simp_all
apply (erule nondec_oinsert)
done

lemma x_less_y_oinsert: "x ≤ y ==> l = y # ys ==> x # l = oinsert x l"
apply simp_all
done

lemma 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
done

lemma oinsert_x_y: "oinsert x (oinsert y l) = oinsert y (oinsert x l)"
apply (induct l)
apply auto
done

subsection ‹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
done

lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
apply (induct set: perm)
done

lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
apply (induct set: perm)
apply auto
done

lemma perm_oinsert: "x # xs <~~> oinsert x xs"
apply (induct xs)
apply auto
done

lemma perm_sort: "xs <~~> sort xs"
apply (induct xs)
apply (auto intro: perm_oinsert elim: perm_subst_oinsert)
done

lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys"
apply (induct set: perm)
done

subsection ‹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)
done

lemma 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)
done

lemma split_primel:
"primel xs ⟹ primel ys ⟹ ∃l. primel l ∧ prod l = prod xs * prod ys"
apply (rule exI)
apply safe
apply (rule_tac [2] prod_append)
done

lemma 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)
done

lemma 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)
done

subsection ‹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 dest: prime_dvd_mult)
done

lemma 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 (erule hd_dvd_prod)
done

lemma 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)
done

lemma 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
done

lemma 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
done

lemma 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)
done

lemma 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
done

lemma 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))
done

lemma 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