equal
deleted
inserted
replaced
74 ==> bag_of (nths l (A Un B)) = |
74 ==> bag_of (nths l (A Un B)) = |
75 bag_of (nths l A) + bag_of (nths l B)" |
75 bag_of (nths l A) + bag_of (nths l B)" |
76 by (simp add: bag_of_nths_Un_Int [symmetric]) |
76 by (simp add: bag_of_nths_Un_Int [symmetric]) |
77 |
77 |
78 lemma bag_of_nths_UN_disjoint [rule_format]: |
78 lemma bag_of_nths_UN_disjoint [rule_format]: |
79 "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] |
79 "[| finite I; \<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j \<longrightarrow> A i Int A j = {} |] |
80 ==> bag_of (nths l (UNION I A)) = |
80 ==> bag_of (nths l (UNION I A)) = |
81 (\<Sum>i\<in>I. bag_of (nths l (A i)))" |
81 (\<Sum>i\<in>I. bag_of (nths l (A i)))" |
82 apply (auto simp add: bag_of_nths) |
82 apply (auto simp add: bag_of_nths) |
83 unfolding UN_simps [symmetric] |
83 unfolding UN_simps [symmetric] |
84 apply (subst sum.UNION_disjoint) |
84 apply (subst sum.UNION_disjoint) |