theory Primefactors
imports "~/isabelle/src/HOL/NumberTheory/Factorization"
begin

section {* Auxiliary Lemmas *}

(* FIXME: remove this? *)
(*
lemma insert_Diff_swap: "a \<notin> B \<Longrightarrow> insert a (A - B) = (insert a A) - B"
by blast
*)

(* FIXME: replace power_power with power_mult .*)
(*
lemma power_power: "((x::nat) ^ a)^b = x ^ (a * b)"
by (simp add: power_mult)
*)

section {* Primefactors *}

constdefs primefactors::"nat \<Rightarrow> nat list"
"primefactors n \<equiv> (if n \<le> 1 then [] 
                  else (SOME l. primel l \<and> nondec l \<and> prod l = n))"

lemma prod_le:
"\<And> x. x \<in> set xs \<and> 0 < prod xs \<Longrightarrow> x \<le> prod xs"
apply (induct xs)
apply simp

apply atomize
apply simp
apply (case_tac "x = a")
apply simp
apply (case_tac "prod xs")
apply simp
apply simp

apply simp
apply (erule_tac x="x" in allE)
apply simp
apply (erule conjE)+
apply (subgoal_tac "1 * x \<le> a * prod xs")
 prefer 2
 apply (rule mult_mono)
 apply simp
 apply simp
 apply simp
 apply simp
apply simp
done

lemma primefactors_upper_bound:
"q \<in> set (primefactors n) \<Longrightarrow> q \<le> n"
apply (simp add: primefactors_def linorder_not_le split add: split_if_asm)
apply (frule unique_prime_factorization)
apply (erule ex1E)
apply (frule unique_prime_factorization)
apply (drule_tac a="l" in some1_equality)
apply assumption

apply (erule_tac V="\<forall> y. ?P y" in thin_rl)
apply simp
apply (subgoal_tac "q \<le> prod l")
 prefer 2
 apply (rule prod_le)
 apply simp
apply simp
done


lemma primefactors_are_prime:
"q \<in> set (primefactors n) \<Longrightarrow> q \<in> prime"
apply (simp add: primefactors_def linorder_not_le split add: split_if_asm)
apply (frule unique_prime_factorization)
apply (erule ex1E)
apply (frule unique_prime_factorization)
apply (drule_tac a="l" in some1_equality)
apply assumption

apply (erule_tac V="\<forall> y. ?P y" in thin_rl)
apply (simp add: primel_def subset_def)
done


lemma primefactors_lower_bound:
"q \<in> set (primefactors n) \<Longrightarrow> 1 < q"
apply (drule primefactors_are_prime)
apply (drule prime_g_one)
apply simp
done

lemma prod_dvd: 
"\<And> x. x \<in> set xs \<Longrightarrow> x dvd (prod xs)"
apply (induct xs)
apply simp

apply atomize
apply simp
apply (case_tac "x=a")
apply simp

apply (erule_tac x="x" in allE)
apply simp
apply (rule dvd_mult)
apply assumption
done

lemma primefactors_are_factors:
"\<And> q. q \<in> set (primefactors n) \<Longrightarrow> q dvd n"
apply (simp add: primefactors_def linorder_not_le split add: split_if_asm)
apply (frule unique_prime_factorization)
apply (erule ex1E)
apply (frule unique_prime_factorization)
apply (drule_tac a="l" in some1_equality)
apply assumption

apply (erule_tac V="\<forall> y. ?P y" in thin_rl)
apply (simp add: primel_def subset_def)
apply (subgoal_tac "q dvd (prod l)")
 prefer 2
 apply (rule prod_dvd)
 apply assumption
apply simp
done

lemma primefactors_prod:
"0 < n \<Longrightarrow> prod (primefactors n) = n"
apply (case_tac "Suc 0 < n")
apply (frule unique_prime_factorization)
apply (erule ex1E)
apply (frule unique_prime_factorization)
apply (drule_tac a="l" in some1_equality)
apply assumption

apply (erule_tac V="\<forall> y. ?P y" in thin_rl)
apply (simp add: primefactors_def)

apply (case_tac "n")
apply simp
apply (simp add: primefactors_def)
done



lemma primefactors_primel:
"primel (primefactors n)"
apply (case_tac "Suc 0 < n")
apply (frule unique_prime_factorization)
apply (erule ex1E)
apply (frule unique_prime_factorization)
apply (drule_tac a="l" in some1_equality)
apply assumption

apply (erule_tac V="\<forall> y. ?P y" in thin_rl)
apply (simp add: primefactors_def)

apply (case_tac "n")
apply (simp add: primefactors_def primel_def)
apply (simp add: primefactors_def primel_def)
done


lemma primefactors_nondec:
"nondec (primefactors n)"
apply (case_tac "Suc 0 < n")
apply (frule unique_prime_factorization)
apply (erule ex1E)
apply (frule unique_prime_factorization)
apply (drule_tac a="l" in some1_equality)
apply assumption

apply (erule_tac V="\<forall> y. ?P y" in thin_rl)
apply (simp add: primefactors_def)

apply (case_tac "n")
apply (simp add: primefactors_def primel_def)
apply (simp add: primefactors_def primel_def)
done

lemma nondec_split: "nondec l \<Longrightarrow> (\<exists> n. (\<forall> x \<in> set (take n l). x \<le> a) \<and> (\<forall> x \<in> set (drop n l). a < x))"
apply (induct l)
apply simp

apply simp
apply (case_tac "l")
apply simp
apply (case_tac "aa \<le> a")
apply (rule_tac x="Suc 0" in exI)
apply simp

apply (rule_tac x="0" in exI)
apply simp

apply (simp only: list.cases)
apply (drule_tac t="aaa # list" in sym)
apply simp

apply (erule exE | erule conjE)+
apply (case_tac "aa \<le> a")
apply (rule_tac x="Suc n" in exI)
apply simp

apply (rule_tac x="0" in exI)
apply simp

apply (case_tac "n")
apply simp

apply simp
apply (drule_tac s="aaa # list" in sym)
apply simp
done

lemma nondec_hd_tl: 
"nondec xs \<Longrightarrow> \<forall> x\<in> set (tl xs). hd xs \<le> x"
apply (induct xs)
apply simp

apply simp
apply (case_tac "xs")
apply simp

apply (simp only: list.cases tl.simps hd.simps)
apply (rule ballI)
apply simp
apply (case_tac "x=aa")
apply simp

apply simp
apply (erule conjE)+
apply (erule_tac x="x" in ballE)
 prefer 2
 apply simp
apply simp
done

lemma nondec_append:
"\<And> ys. nondec (xs@ys) = (nondec xs \<and> nondec ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x \<le> y))"
apply (induct xs)
apply simp

apply atomize
apply simp
apply (case_tac "xs")
apply simp
apply (case_tac "ys")
apply simp
apply (simp only: list.cases)
apply (case_tac "a \<le> aa")
apply (case_tac "nondec ys")
apply (frule nondec_hd_tl)
apply (simp add: Ball_def del: nondec.simps)
apply (rule allI)
apply (erule_tac x="x" in allE)
apply (rule impI)
apply simp

apply simp

apply simp

apply (simp del: nondec.simps)
apply (case_tac "a \<le> aa")
apply (case_tac "nondec (aa # list)")
apply (case_tac "nondec ys")
apply (simp add: Ball_def del: nondec.simps)
apply (case_tac "(\<forall>x. x \<in> set list \<longrightarrow> (\<forall>xa. xa \<in> set ys \<longrightarrow> x \<le> xa))")
apply simp
apply (rule iffI)
apply (rule conjI)
apply (rule allI, rule impI)
apply (erule_tac x="x" in allE)+
apply simp

apply (rule allI, rule impI)
apply (erule_tac x="x" in allE)+
apply simp

apply (rule allI, rule impI)
apply (erule conjE)+
apply (erule_tac x="x" in allE)+
apply simp

apply (simp only: simp_thms)

apply simp

apply simp

apply simp
done


lemma nondec_last_butlast: 
"nondec xs \<Longrightarrow> \<forall> x\<in> set (butlast xs). x \<le> last xs"
apply (induct xs rule: rev_induct)
apply simp

apply (simp add: nondec_append)
done

lemma prime_primefactors:
"p \<in> prime \<Longrightarrow> primefactors p  = [p]"
apply (frule prime_g_one)
apply (frule unique_prime_factorization)
apply (subgoal_tac "primel [p] \<and> nondec [p] \<and> prod [p] = p")
 prefer 2
 apply simp
 apply (drule prime_primel)
 apply simp
apply (drule_tac a="[p]" in some1_equality)
apply simp

apply (simp add: primefactors_def)
done

lemma primefactors_mult:
"\<lbrakk> 0 < n; p \<in> prime \<rbrakk> \<Longrightarrow> \<exists> ps ps'. primefactors (n * p) = ps@[p]@ps' \<and> primefactors n = ps@ps'"
apply (case_tac "Suc 0 < n")
--{* 1 < n *}
apply (frule nondec_factor_exists)
apply (erule exE)
apply (frule unique_prime_factorization)
apply (drule_tac a="l" in some1_equality)
apply assumption
apply (erule conjE)+
apply (frule_tac a="p" in nondec_split)
apply (erule exE | erule conjE)+
apply (rule_tac x="take na l" in exI)
apply (rule_tac x="drop na l" in exI)
apply (subgoal_tac "primel (take na l @ [p] @ drop na l)")
 prefer 2
 apply (subgoal_tac "primel (take na l @ drop na l)")
  prefer 2
  apply simp
 apply (simp only: primel_append)
 apply (subgoal_tac "primel [p]")
  prefer 2
  apply (drule prime_primel)
  apply simp
 apply simp
apply (subgoal_tac "nondec (take na l @ [p] @ drop na l)")
 prefer 2
 apply (subgoal_tac "nondec (take na l @ drop na l)")
  prefer 2
  apply simp
 apply (simp only: nondec_append simp_thms)
 apply (erule conjE)+
 apply (rule conjI)
 apply (rule conjI)
 apply (simp (no_asm))

 apply (rule ballI)
 apply (simp only: Ball_def)
 apply (rule allI, rule impI)
 apply (erule_tac x="xa" in allE)+
 apply simp

 apply (simp only: Ball_def)
 apply (rule allI, rule impI)+
 apply (erule_tac x="x" in allE)
 apply (erule_tac x="x" in allE)
 apply (erule_tac x="x" in allE)
 apply (drule mp, assumption)+
 apply (erule_tac x="xa" in allE)
 apply simp
 apply (case_tac "xa = p")
 apply simp

 apply simp
apply (subgoal_tac "prod (take na l @ [p] @ drop na l) = n * p")
 prefer 2
 apply (subgoal_tac "prod (take na l @ drop na l) = n")
  prefer 2
  apply simp
 apply (drule_tac prime_g_one)
 apply (simp add: prod_append prod.simps)
  apply (subgoal_tac "prod (take na l @ drop na l) = n")
   prefer 2
   apply simp
  apply (simp only: prod_append)
apply (subgoal_tac "Suc 0 < n * p")
 prefer 2
 apply (drule_tac prime_g_one)
 apply (subgoal_tac "Suc 0 * (Suc 0) < n * p")
  prefer 2
  apply (rule mult_strict_mono)
  apply assumption+
  apply simp
  apply simp
 apply simp
apply (frule_tac n="n * p" in unique_prime_factorization)
apply (drule_tac a="take na l @ [p] @ drop na l" in some1_equality)
apply  simp

apply (simp add: primefactors_def)

apply (case_tac "n")
apply simp

apply (case_tac "nat")
apply simp
apply (rule_tac x="[]" in exI)
apply (rule_tac x="[]" in exI)
apply (drule prime_primefactors)
apply simp
apply (simp add: primefactors_def)

apply simp
done

lemma prod_non_empty:
"1 < prod xs \<Longrightarrow> xs \<noteq> []"
apply (induct xs)
apply simp

apply simp
done

theorem primefactors_exist:
"1 < (n::nat) \<Longrightarrow> primefactors n \<noteq> []"
apply (subgoal_tac "prod (primefactors n) = n")
 prefer 2
 apply (rule primefactors_prod)
 apply simp
apply (case_tac "n")
apply simp

apply (case_tac "nat")
apply (simp add: primefactors_def)

apply (rule prod_non_empty)
apply simp
done

lemma no_primefactors:
"primefactors n = [] \<Longrightarrow> n = 0 \<or> n = 1"
apply (case_tac "n")
apply simp

apply (case_tac "nat")
apply  simp

apply (subgoal_tac "primefactors n \<noteq> []")
 prefer 2
 apply (rule primefactors_exist)
 apply simp
apply simp
done


(* FIXME: Move to standard library ?*)
lemma singleton_replicate:
"set xs \<subseteq> {x} = (\<exists> n. xs = replicate n x)"
apply (induct xs)
apply simp
apply (rule_tac x="0" in exI)
apply simp

apply simp
apply (rule iffI)
apply (erule conjE)+
apply (erule exE)
apply (rule_tac x="Suc n" in exI)
apply simp

apply (erule exE)
apply (case_tac "n")
apply simp

apply simp
apply (rule_tac x="nat" in exI)
apply simp
done

lemma primefactors_mult_sorted:
"primefactors (n * q) = ns @ [q] \<Longrightarrow> primefactors n = ns"
apply (subgoal_tac "q \<in> prime")
 prefer 2
 apply (rule_tac n="n * q" in primefactors_are_prime)
 apply simp
apply (subgoal_tac "0 < n")
 prefer 2
 apply (case_tac "n")
 apply (simp add: primefactors_def)

 apply simp
apply (subgoal_tac "\<exists> ps ps'. primefactors (n * q) = ps@[q]@ps' \<and> primefactors n = ps@ps'")
 prefer 2
 apply (rule primefactors_mult)
 apply assumption
 apply assumption
apply (erule exE | erule conjE)+

apply (rule_tac xs="ps'" in rev_cases)
apply simp

apply simp
apply (erule conjE)+
apply (drule_tac t="ns" in sym)
apply simp

apply (subgoal_tac "set ys \<subseteq> {q}")
 prefer 2
 apply (subgoal_tac "nondec (q # ys @ [q])")
  prefer 2
  apply (subgoal_tac "nondec (primefactors (n * q))")
   prefer 2
   apply (rule primefactors_nondec)
  apply (simp add: nondec_append)
  apply (subgoal_tac "\<forall> x \<in> set (ys @ [q]). q \<le> x")
   prefer 2
   apply (drule nondec_hd_tl)
   apply simp
  apply (subgoal_tac "\<forall> x \<in> set (q # ys). x \<le> q")
   prefer 2
   apply (drule nondec_last_butlast)
   apply simp
  apply (simp only: subset_def)
  apply (rule ballI)
  apply (erule_tac x="x" in ballE)
   prefer 2
   apply simp
  apply (erule_tac x="x" in ballE)
   prefer 2
   apply simp
  apply simp
apply (simp add: singleton_replicate)
apply (erule exE)
apply (simp add: replicate_app_Cons_same)
done

lemma primefactors_complete:
"\<lbrakk> n \<in> prime; n dvd m; 0 < m \<rbrakk> \<Longrightarrow> n \<in> set (primefactors m)"
apply (simp only: dvd_def)
apply (erule exE)
apply (simp add: primefactors_mult)
apply (subgoal_tac "0 < n")
 prefer 2
 apply(rule prime_g_zero)
 apply assumption
apply (subgoal_tac "\<exists>ps ps'. primefactors (k * n) = ps @ [n] @ ps' \<and> primefactors k = ps @ ps'")
 prefer 2
 apply (rule primefactors_mult)
 apply simp
 apply assumption
apply (erule exE | erule conjE)+
apply (simp add: ring_eq_simps)
done

lemma common_primefactors:
"\<lbrakk> n dvd m; 0 < m \<rbrakk> \<Longrightarrow> set (primefactors n) \<subseteq> set (primefactors m)"
apply (simp only: subset_def)
apply (rule ballI)
apply (subgoal_tac "x \<in> prime")
 prefer 2
 apply (rule primefactors_are_prime)
 apply simp
apply (subgoal_tac "x dvd n")
 prefer 2
 apply (rule primefactors_are_factors)
 apply simp
apply (rule primefactors_complete)
apply simp

apply (rule dvd_trans)
apply simp
apply simp

apply simp
done

end