src/HOL/Number_Theory/UniqueFactorization.thy
changeset 35416 d8d7d1b785af
parent 35054 a5db9779b026
child 35644 d20cf282342e
equal deleted inserted replaced
35342:4dc65845eab3 35416:d8d7d1b785af
    65    to multiset.thy? If so, one should similarly define msetsum for abelian 
    65    to multiset.thy? If so, one should similarly define msetsum for abelian 
    66    semirings, using of_nat. Also, is it worth developing bounded quantifiers 
    66    semirings, using of_nat. Also, is it worth developing bounded quantifiers 
    67    "ALL i :# M. P i"? 
    67    "ALL i :# M. P i"? 
    68 *)
    68 *)
    69 
    69 
    70 constdefs
    70 definition msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b" where
    71   msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b"
       
    72   "msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)"
    71   "msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)"
    73 
    72 
    74 syntax
    73 syntax
    75   "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" 
    74   "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" 
    76       ("(3PROD _:#_. _)" [0, 51, 10] 10)
    75       ("(3PROD _:#_. _)" [0, 51, 10] 10)
   212       by auto
   211       by auto
   213   }
   212   }
   214   thus ?thesis by (simp add:multiset_eq_conv_count_eq)
   213   thus ?thesis by (simp add:multiset_eq_conv_count_eq)
   215 qed
   214 qed
   216 
   215 
   217 constdefs
   216 definition multiset_prime_factorization :: "nat => nat multiset" where
   218   multiset_prime_factorization :: "nat => nat multiset"
       
   219   "multiset_prime_factorization n ==
   217   "multiset_prime_factorization n ==
   220      if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 
   218      if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 
   221        n = (PROD i :# M. i)))
   219        n = (PROD i :# M. i)))
   222      else {#}"
   220      else {#}"
   223 
   221