equal
deleted
inserted
replaced
1 (* Title: ZF/UNITY/MultusetSum.thy |
1 (* Title: ZF/UNITY/MultusetSum.thy |
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety |
2 Author: Sidi O Ehmety |
4 *) |
3 *) |
5 |
4 |
6 header {*Setsum for Multisets*} |
5 header {*Setsum for Multisets*} |
7 |
6 |
120 |
119 |
121 lemma msetsum_UN_disjoint [rule_format (no_asm)]: |
120 lemma msetsum_UN_disjoint [rule_format (no_asm)]: |
122 "[| I \<in> Fin(K); \<forall>i \<in> K. C(i) \<in> Fin(A) |] ==> |
121 "[| I \<in> Fin(K); \<forall>i \<in> K. C(i) \<in> Fin(A) |] ==> |
123 (\<forall>x \<in> A. multiset(f(x)) & mset_of(f(x))\<subseteq>B) --> |
122 (\<forall>x \<in> A. multiset(f(x)) & mset_of(f(x))\<subseteq>B) --> |
124 (\<forall>i \<in> I. \<forall>j \<in> I. i\<noteq>j --> C(i) Int C(j) = 0) --> |
123 (\<forall>i \<in> I. \<forall>j \<in> I. i\<noteq>j --> C(i) Int C(j) = 0) --> |
125 msetsum(f, \<Union>i \<in> I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)" |
124 msetsum(f, \<Union>i \<in> I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)" |
126 apply (erule Fin_induct, auto) |
125 apply (erule Fin_induct, auto) |
127 apply (subgoal_tac "\<forall>i \<in> y. x \<noteq> i") |
126 apply (subgoal_tac "\<forall>i \<in> y. x \<noteq> i") |
128 prefer 2 apply blast |
127 prefer 2 apply blast |
129 apply (subgoal_tac "C(x) Int (\<Union>i \<in> y. C (i)) = 0") |
128 apply (subgoal_tac "C(x) Int (\<Union>i \<in> y. C (i)) = 0") |
130 prefer 2 apply blast |
129 prefer 2 apply blast |