# HG changeset patch
# User haftmann
# Date 1349385542 -7200
# Node ID 741dd8efff5ba3c6d2742347e9c67a4eca30a4cb
# Parent  56494eedf4933c5de394d1b6ab0d62dd3e7b2705
tuned proof

diff -r 56494eedf493 -r 741dd8efff5b src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Oct 04 23:19:02 2012 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Oct 04 23:19:02 2012 +0200
@@ -339,29 +339,32 @@
   by auto
 
 lemma prime_factorization_unique_nat: 
-    "S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
-      n = (PROD p : S. p^(f p)) \<Longrightarrow>
-        S = prime_factors n & (ALL p. f p = multiplicity p n)"
-  apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset f")
-  apply (unfold prime_factors_nat_def multiplicity_nat_def)
-  apply (simp add: set_of_def Abs_multiset_inverse multiset_def)
-  apply (unfold multiset_prime_factorization_def)
-  apply (subgoal_tac "n > 0")
-  prefer 2
-  apply force
-  apply (subst if_P, assumption)
-  apply (rule the1_equality)
-  apply (rule ex_ex1I)
-  apply (rule multiset_prime_factorization_exists, assumption)
-  apply (rule multiset_prime_factorization_unique)
-  apply force
-  apply force
-  apply force
-  unfolding set_of_def msetprod_def
-  apply (subgoal_tac "f : multiset")
-  apply (auto simp only: Abs_multiset_inverse)
-  unfolding multiset_def apply force 
-  done
+  fixes f :: "nat \<Rightarrow> _"
+  assumes S_eq: "S = {p. 0 < f p}" and "finite S"
+    and "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
+  shows "S = prime_factors n \<and> (\<forall>p. f p = multiplicity p n)"
+proof -
+  from assms have "f \<in> multiset"
+    by (auto simp add: multiset_def)
+  moreover from assms have "n > 0" by force
+  ultimately have "multiset_prime_factorization n = Abs_multiset f"
+    apply (unfold multiset_prime_factorization_def)
+    apply (subst if_P, assumption)
+    apply (rule the1_equality)
+    apply (rule ex_ex1I)
+    apply (rule multiset_prime_factorization_exists, assumption)
+    apply (rule multiset_prime_factorization_unique)
+    apply force
+    apply force
+    apply force
+    using assms
+    apply (simp add: Abs_multiset_inverse set_of_def msetprod_def)
+    done
+  with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
+    by (simp add: Abs_multiset_inverse)
+  with S_eq show ?thesis
+    by (simp add: set_of_def multiset_def prime_factors_nat_def multiplicity_nat_def)
+qed
 
 lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
@@ -874,3 +877,4 @@
   done
 
 end
+