equal
deleted
inserted
replaced
69 "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" |
69 "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" |
70 ("(3PROD _:#_. _)" [0, 51, 10] 10) |
70 ("(3PROD _:#_. _)" [0, 51, 10] 10) |
71 |
71 |
72 translations |
72 translations |
73 "PROD i :# A. b" == "CONST msetprod (%i. b) A" |
73 "PROD i :# A. b" == "CONST msetprod (%i. b) A" |
|
74 |
|
75 lemma msetprod_empty: |
|
76 "msetprod f {#} = 1" |
|
77 by (simp add: msetprod_def) |
|
78 |
|
79 lemma msetprod_singleton: |
|
80 "msetprod f {#x#} = f x" |
|
81 by (simp add: msetprod_def) |
74 |
82 |
75 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" |
83 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" |
76 apply (simp add: msetprod_def power_add) |
84 apply (simp add: msetprod_def power_add) |
77 apply (subst setprod_Un2) |
85 apply (subst setprod_Un2) |
78 apply auto |
86 apply auto |