1.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Oct 04 23:19:02 2012 +0200
     1.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Oct 04 23:19:02 2012 +0200
     1.3 @@ -339,29 +339,32 @@
     1.4    by auto
     1.5  
     1.6  lemma prime_factorization_unique_nat: 
     1.7 -    "S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
     1.8 -      n = (PROD p : S. p^(f p)) \<Longrightarrow>
     1.9 -        S = prime_factors n & (ALL p. f p = multiplicity p n)"
    1.10 -  apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset f")
    1.11 -  apply (unfold prime_factors_nat_def multiplicity_nat_def)
    1.12 -  apply (simp add: set_of_def Abs_multiset_inverse multiset_def)
    1.13 -  apply (unfold multiset_prime_factorization_def)
    1.14 -  apply (subgoal_tac "n > 0")
    1.15 -  prefer 2
    1.16 -  apply force
    1.17 -  apply (subst if_P, assumption)
    1.18 -  apply (rule the1_equality)
    1.19 -  apply (rule ex_ex1I)
    1.20 -  apply (rule multiset_prime_factorization_exists, assumption)
    1.21 -  apply (rule multiset_prime_factorization_unique)
    1.22 -  apply force
    1.23 -  apply force
    1.24 -  apply force
    1.25 -  unfolding set_of_def msetprod_def
    1.26 -  apply (subgoal_tac "f : multiset")
    1.27 -  apply (auto simp only: Abs_multiset_inverse)
    1.28 -  unfolding multiset_def apply force 
    1.29 -  done
    1.30 +  fixes f :: "nat \<Rightarrow> _"
    1.31 +  assumes S_eq: "S = {p. 0 < f p}" and "finite S"
    1.32 +    and "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
    1.33 +  shows "S = prime_factors n \<and> (\<forall>p. f p = multiplicity p n)"
    1.34 +proof -
    1.35 +  from assms have "f \<in> multiset"
    1.36 +    by (auto simp add: multiset_def)
    1.37 +  moreover from assms have "n > 0" by force
    1.38 +  ultimately have "multiset_prime_factorization n = Abs_multiset f"
    1.39 +    apply (unfold multiset_prime_factorization_def)
    1.40 +    apply (subst if_P, assumption)
    1.41 +    apply (rule the1_equality)
    1.42 +    apply (rule ex_ex1I)
    1.43 +    apply (rule multiset_prime_factorization_exists, assumption)
    1.44 +    apply (rule multiset_prime_factorization_unique)
    1.45 +    apply force
    1.46 +    apply force
    1.47 +    apply force
    1.48 +    using assms
    1.49 +    apply (simp add: Abs_multiset_inverse set_of_def msetprod_def)
    1.50 +    done
    1.51 +  with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
    1.52 +    by (simp add: Abs_multiset_inverse)
    1.53 +  with S_eq show ?thesis
    1.54 +    by (simp add: set_of_def multiset_def prime_factors_nat_def multiplicity_nat_def)
    1.55 +qed
    1.56  
    1.57  lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
    1.58      finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
    1.59 @@ -874,3 +877,4 @@
    1.60    done
    1.61  
    1.62  end
    1.63 +