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 @@ -36,42 +36,46 @@
     1.4     "ALL i :# M. P i"? 
     1.5  *)
     1.6  
     1.7 -definition (in comm_monoid_mult) msetprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
     1.8 +definition (in comm_monoid_mult) msetprod :: "'a multiset \<Rightarrow> 'a"
     1.9  where
    1.10 -  "msetprod f M = setprod (\<lambda>x. f x ^ count M x) (set_of M)"
    1.11 +  "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
    1.12 +
    1.13 +abbreviation (in comm_monoid_mult) msetprod_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
    1.14 +where
    1.15 +  "msetprod_image f M \<equiv> msetprod (image_mset f M)"
    1.16  
    1.17  syntax
    1.18 -  "_msetprod" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" 
    1.19 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" 
    1.20        ("(3PROD _:#_. _)" [0, 51, 10] 10)
    1.21  
    1.22  translations
    1.23 -  "PROD i :# A. b" == "CONST msetprod (\<lambda>i. b) A"
    1.24 +  "PROD i :# A. b" == "CONST msetprod_image (\<lambda>i. b) A"
    1.25  
    1.26 -lemma msetprod_empty: "msetprod f {#} = 1"
    1.27 +lemma msetprod_empty: "msetprod {#} = 1"
    1.28    by (simp add: msetprod_def)
    1.29  
    1.30 -lemma msetprod_singleton: "msetprod f {#x#} = f x"
    1.31 +lemma msetprod_singleton: "msetprod {#x#} = x"
    1.32    by (simp add: msetprod_def)
    1.33  
    1.34 -lemma msetprod_Un: "msetprod f (A + B) = msetprod f A * msetprod f B" 
    1.35 +lemma msetprod_Un: "msetprod (A + B) = msetprod A * msetprod B" 
    1.36    apply (simp add: msetprod_def power_add)
    1.37    apply (subst setprod_Un2)
    1.38    apply auto
    1.39    apply (subgoal_tac 
    1.40 -      "(PROD x:set_of A - set_of B. f x ^ count A x * f x ^ count B x) =
    1.41 -       (PROD x:set_of A - set_of B. f x ^ count A x)")
    1.42 +      "(PROD x:set_of A - set_of B. x ^ count A x * x ^ count B x) =
    1.43 +       (PROD x:set_of A - set_of B. x ^ count A x)")
    1.44    apply (erule ssubst)
    1.45    apply (subgoal_tac 
    1.46 -      "(PROD x:set_of B - set_of A. f x ^ count A x * f x ^ count B x) =
    1.47 -       (PROD x:set_of B - set_of A. f x ^ count B x)")
    1.48 +      "(PROD x:set_of B - set_of A. x ^ count A x * x ^ count B x) =
    1.49 +       (PROD x:set_of B - set_of A. x ^ count B x)")
    1.50    apply (erule ssubst)
    1.51 -  apply (subgoal_tac "(PROD x:set_of A. f x ^ count A x) = 
    1.52 -    (PROD x:set_of A - set_of B. f x ^ count A x) *
    1.53 -    (PROD x:set_of A Int set_of B. f x ^ count A x)")
    1.54 +  apply (subgoal_tac "(PROD x:set_of A. x ^ count A x) = 
    1.55 +    (PROD x:set_of A - set_of B. x ^ count A x) *
    1.56 +    (PROD x:set_of A Int set_of B. x ^ count A x)")
    1.57    apply (erule ssubst)
    1.58 -  apply (subgoal_tac "(PROD x:set_of B. f x ^ count B x) = 
    1.59 -    (PROD x:set_of B - set_of A. f x ^ count B x) *
    1.60 -    (PROD x:set_of A Int set_of B. f x ^ count B x)")
    1.61 +  apply (subgoal_tac "(PROD x:set_of B. x ^ count B x) = 
    1.62 +    (PROD x:set_of B - set_of A. x ^ count B x) *
    1.63 +    (PROD x:set_of A Int set_of B. x ^ count B x)")
    1.64    apply (erule ssubst)
    1.65    apply (subst setprod_timesf)
    1.66    apply (force simp add: mult_ac)
    1.67 @@ -198,7 +202,8 @@
    1.68    apply (frule multiset_prime_factorization_exists)
    1.69    apply clarify
    1.70    apply (rule theI)
    1.71 -  apply (insert multiset_prime_factorization_unique, blast)+
    1.72 +  apply (insert multiset_prime_factorization_unique)
    1.73 +  apply auto
    1.74  done
    1.75  
    1.76