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: 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: A Int lessThan k. {#f i#})" |
76 apply (rule setsum_cong, auto) |
76 by (rule setsum_cong, auto) |
77 done |
|
78 |
77 |
79 lemma bag_of_sublist: |
78 lemma bag_of_sublist: |
80 "bag_of (sublist l A) = |
79 "bag_of (sublist l A) = |
81 (\<Sum>i: A Int lessThan (length l). {# l!i #})" |
80 (\\<Sum>i: A Int lessThan (length l). {# l!i #})" |
82 apply (rule_tac xs = l in rev_induct, simp) |
81 apply (rule_tac xs = l in rev_induct, simp) |
83 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 |
84 bag_of_sublist_lemma plus_ac0) |
83 bag_of_sublist_lemma plus_ac0) |
85 done |
84 done |
86 |
85 |
87 |
86 |
88 lemma bag_of_sublist_Un_Int: |
87 lemma bag_of_sublist_Un_Int: |
89 "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = |
88 "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = |
90 bag_of (sublist l A) + bag_of (sublist l B)" |
89 bag_of (sublist l A) + bag_of (sublist l B)" |
91 apply (subgoal_tac "A Int B Int {..length l (} = (A Int {..length l (}) Int (B Int {..length l (}) ") |
90 apply (subgoal_tac "A Int B Int {..length l (} = |
|
91 (A Int {..length l (}) Int (B Int {..length l (}) ") |
92 apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast) |
92 apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast) |
93 done |
93 done |
94 |
94 |
95 lemma bag_of_sublist_Un_disjoint: |
95 lemma bag_of_sublist_Un_disjoint: |
96 "A Int B = {} |
96 "A Int B = {} |
97 ==> bag_of (sublist l (A Un B)) = |
97 ==> bag_of (sublist l (A Un B)) = |
98 bag_of (sublist l A) + bag_of (sublist l B)" |
98 bag_of (sublist l A) + bag_of (sublist l B)" |
99 apply (simp add: bag_of_sublist_Un_Int [symmetric]) |
99 by (simp add: bag_of_sublist_Un_Int [symmetric]) |
100 done |
|
101 |
100 |
102 lemma bag_of_sublist_UN_disjoint [rule_format]: |
101 lemma bag_of_sublist_UN_disjoint [rule_format]: |
103 "[| 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 = {} |] |
104 ==> bag_of (sublist l (UNION I A)) = |
103 ==> bag_of (sublist l (UNION I A)) = |
105 (\<Sum>i:I. bag_of (sublist l (A i)))" |
104 (\\<Sum>i:I. bag_of (sublist l (A i)))" |
106 apply (simp del: UN_simps |
105 apply (simp del: UN_simps |
107 add: UN_simps [symmetric] add: bag_of_sublist) |
106 add: UN_simps [symmetric] add: bag_of_sublist) |
108 apply (subst setsum_UN_disjoint, auto) |
107 apply (subst setsum_UN_disjoint, auto) |
109 done |
108 done |
110 |
109 |