equal
deleted
inserted
replaced
69 (** setsum **) |
69 (** setsum **) |
70 |
70 |
71 declare setsum_cong [cong] |
71 declare setsum_cong [cong] |
72 |
72 |
73 lemma bag_of_sublist_lemma: |
73 lemma bag_of_sublist_lemma: |
74 "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) = |
74 "(\<Sum>i\<in> A Int lessThan k. {#if i<k then f i else g i#}) = |
75 (\<Sum>i: A Int lessThan k. {#f i#})" |
75 (\<Sum>i\<in> A Int lessThan k. {#f i#})" |
76 by (rule setsum_cong, auto) |
76 by (rule setsum_cong, auto) |
77 |
77 |
78 lemma bag_of_sublist: |
78 lemma bag_of_sublist: |
79 "bag_of (sublist l A) = |
79 "bag_of (sublist l A) = |
80 (\<Sum>i: A Int lessThan (length l). {# l!i #})" |
80 (\<Sum>i\<in> A Int lessThan (length l). {# l!i #})" |
81 apply (rule_tac xs = l in rev_induct, simp) |
81 apply (rule_tac xs = l in rev_induct, simp) |
82 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append |
82 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append |
83 bag_of_sublist_lemma add_ac) |
83 bag_of_sublist_lemma add_ac) |
84 done |
84 done |
85 |
85 |
99 by (simp add: bag_of_sublist_Un_Int [symmetric]) |
99 by (simp add: bag_of_sublist_Un_Int [symmetric]) |
100 |
100 |
101 lemma bag_of_sublist_UN_disjoint [rule_format]: |
101 lemma bag_of_sublist_UN_disjoint [rule_format]: |
102 "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] |
102 "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] |
103 ==> bag_of (sublist l (UNION I A)) = |
103 ==> bag_of (sublist l (UNION I A)) = |
104 (\<Sum>i:I. bag_of (sublist l (A i)))" |
104 (\<Sum>i\<in>I. bag_of (sublist l (A i)))" |
105 apply (simp del: UN_simps |
105 apply (simp del: UN_simps |
106 add: UN_simps [symmetric] add: bag_of_sublist) |
106 add: UN_simps [symmetric] add: bag_of_sublist) |
107 apply (subst setsum_UN_disjoint, auto) |
107 apply (subst setsum_UN_disjoint, auto) |
108 done |
108 done |
109 |
109 |