author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
37936  1 
(* Title: ZF/UNITY/MultisetSum.thy 
14052  2 
Author: Sidi O Ehmety 
3 
*) 

4 

15202  5 
header {*Setsum for Multisets*} 
6 

7 
theory MultisetSum 

8 
imports "../Induct/Multiset" 

9 
begin 

10 

24893  11 
definition 
12 
lcomm :: "[i, i, [i,i]=>i]=>o" where 

14052  13 
"lcomm(A, B, f) == 
15202  14 
(\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> B. f(x, f(y, z))= f(y, f(x, z))) & 
15 
(\<forall>x \<in> A. \<forall>y \<in> B. f(x, y) \<in> B)" 

14052  16 

24893  17 
definition 
18 
general_setsum :: "[i,i,i, [i,i]=>i, i=>i] =>i" where 

14052  19 
"general_setsum(C, B, e, f, g) == 
20 
if Finite(C) then fold[cons(e, B)](%x y. f(g(x), y), e, C) else e" 

21 

24893  22 
definition 
23 
msetsum :: "[i=>i, i, i]=>i" where 

14052  24 
"msetsum(g, C, B) == normalize(general_setsum(C, Mult(B), 0, op +#, g))" 
25 

24893  26 

27 
definition (* sum for naturals *) 

28 
nsetsum :: "[i=>i, i] =>i" where 

14052  29 
"nsetsum(g, C) == general_setsum(C, nat, 0, op #+, g)" 
15202  30 

31 

32 
lemma mset_of_normalize: "mset_of(normalize(M)) \<subseteq> mset_of(M)" 

33 
by (auto simp add: mset_of_def normalize_def) 

34 

35 
lemma general_setsum_0 [simp]: "general_setsum(0, B, e, f, g) = e" 

36 
by (simp add: general_setsum_def) 

37 

38 
lemma general_setsum_cons [simp]: 

39 
"[ C \<in> Fin(A); a \<in> A; a\<notin>C; e \<in> B; \<forall>x \<in> A. g(x) \<in> B; lcomm(B, B, f) ] ==> 

40 
general_setsum(cons(a, C), B, e, f, g) = 

41 
f(g(a), general_setsum(C, B, e, f,g))" 

42 
apply (simp add: general_setsum_def) 

43 
apply (auto simp add: Fin_into_Finite [THEN Finite_cons] cons_absorb) 

44 
prefer 2 apply (blast dest: Fin_into_Finite) 

45 
apply (rule fold_typing.fold_cons) 

46 
apply (auto simp add: fold_typing_def lcomm_def) 

47 
done 

48 

49 
(** lcomm **) 

50 

51 
lemma lcomm_mono: "[ C\<subseteq>A; lcomm(A, B, f) ] ==> lcomm(C, B,f)" 

52 
by (auto simp add: lcomm_def, blast) 

53 

54 
lemma munion_lcomm [simp]: "lcomm(Mult(A), Mult(A), op +#)" 

55 
by (auto simp add: lcomm_def Mult_iff_multiset munion_lcommute) 

56 

57 
(** msetsum **) 

58 

59 
lemma multiset_general_setsum: 

60 
"[ C \<in> Fin(A); \<forall>x \<in> A. multiset(g(x))& mset_of(g(x))\<subseteq>B ] 

61 
==> multiset(general_setsum(C, B > nat  {0}, 0, \<lambda>u v. u +# v, g))" 

62 
apply (erule Fin_induct, auto) 

63 
apply (subst general_setsum_cons) 

64 
apply (auto simp add: Mult_iff_multiset) 

65 
done 

66 

67 
lemma msetsum_0 [simp]: "msetsum(g, 0, B) = 0" 

68 
by (simp add: msetsum_def) 

69 

70 
lemma msetsum_cons [simp]: 

71 
"[ C \<in> Fin(A); a\<notin>C; a \<in> A; \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B ] 

72 
==> msetsum(g, cons(a, C), B) = g(a) +# msetsum(g, C, B)" 

73 
apply (simp add: msetsum_def) 

74 
apply (subst general_setsum_cons) 

75 
apply (auto simp add: multiset_general_setsum Mult_iff_multiset) 

76 
done 

77 

78 
(* msetsum type *) 

79 

80 
lemma msetsum_multiset: "multiset(msetsum(g, C, B))" 

81 
by (simp add: msetsum_def) 

82 

83 
lemma mset_of_msetsum: 

84 
"[ C \<in> Fin(A); \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B ] 

85 
==> mset_of(msetsum(g, C, B))\<subseteq>B" 

86 
by (erule Fin_induct, auto) 

87 

88 

89 
(*The reversed orientation looks more natural, but LOOPS as a simprule!*) 

90 
lemma msetsum_Un_Int: 

91 
"[ C \<in> Fin(A); D \<in> Fin(A); \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B ] 

46823  92 
==> msetsum(g, C \<union> D, B) +# msetsum(g, C \<inter> D, B) 
15202  93 
= msetsum(g, C, B) +# msetsum(g, D, B)" 
94 
apply (erule Fin_induct) 

46823  95 
apply (subgoal_tac [2] "cons (x, y) \<union> D = cons (x, y \<union> D) ") 
15202  96 
apply (auto simp add: msetsum_multiset) 
46823  97 
apply (subgoal_tac "y \<union> D \<in> Fin (A) & y \<inter> D \<in> Fin (A) ") 
15202  98 
apply clarify 
99 
apply (case_tac "x \<in> D") 

46823  100 
apply (subgoal_tac [2] "cons (x, y) \<inter> D = y \<inter> D") 
101 
apply (subgoal_tac "cons (x, y) \<inter> D = cons (x, y \<inter> D) ") 

15202  102 
apply (simp_all (no_asm_simp) add: cons_absorb munion_assoc msetsum_multiset) 
103 
apply (simp (no_asm_simp) add: munion_lcommute msetsum_multiset) 

104 
apply auto 

105 
done 

106 

107 

108 
lemma msetsum_Un_disjoint: 

46823  109 
"[ C \<in> Fin(A); D \<in> Fin(A); C \<inter> D = 0; 
15202  110 
\<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B ] 
46823  111 
==> msetsum(g, C \<union> D, B) = msetsum(g, C, B) +# msetsum(g,D, B)" 
15202  112 
apply (subst msetsum_Un_Int [symmetric]) 
113 
apply (auto simp add: msetsum_multiset) 

114 
done 

115 

116 
lemma UN_Fin_lemma [rule_format (no_asm)]: 

46823  117 
"I \<in> Fin(A) ==> (\<forall>i \<in> I. C(i) \<in> Fin(B)) \<longrightarrow> (\<Union>i \<in> I. C(i)):Fin(B)" 
15202  118 
by (erule Fin_induct, auto) 
119 

120 
lemma msetsum_UN_disjoint [rule_format (no_asm)]: 

121 
"[ I \<in> Fin(K); \<forall>i \<in> K. C(i) \<in> Fin(A) ] ==> 

46823  122 
(\<forall>x \<in> A. multiset(f(x)) & mset_of(f(x))\<subseteq>B) \<longrightarrow> 
123 
(\<forall>i \<in> I. \<forall>j \<in> I. i\<noteq>j \<longrightarrow> C(i) \<inter> C(j) = 0) \<longrightarrow> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

124 
msetsum(f, \<Union>i \<in> I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)" 
15202  125 
apply (erule Fin_induct, auto) 
126 
apply (subgoal_tac "\<forall>i \<in> y. x \<noteq> i") 

127 
prefer 2 apply blast 

46823  128 
apply (subgoal_tac "C(x) \<inter> (\<Union>i \<in> y. C (i)) = 0") 
15202  129 
prefer 2 apply blast 
130 
apply (subgoal_tac " (\<Union>i \<in> y. C (i)):Fin (A) & C(x) :Fin (A) ") 

131 
prefer 2 apply (blast intro: UN_Fin_lemma dest: FinD, clarify) 

132 
apply (simp (no_asm_simp) add: msetsum_Un_disjoint) 

133 
apply (subgoal_tac "\<forall>x \<in> K. multiset (msetsum (f, C(x), B)) & mset_of (msetsum (f, C(x), B)) \<subseteq> B") 

134 
apply (simp (no_asm_simp)) 

135 
apply clarify 

136 
apply (drule_tac x = xa in bspec) 

137 
apply (simp_all (no_asm_simp) add: msetsum_multiset mset_of_msetsum) 

138 
done 

139 

140 
lemma msetsum_addf: 

141 
"[ C \<in> Fin(A); 

142 
\<forall>x \<in> A. multiset(f(x)) & mset_of(f(x))\<subseteq>B; 

143 
\<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B ] ==> 

144 
msetsum(%x. f(x) +# g(x), C, B) = msetsum(f, C, B) +# msetsum(g, C, B)" 

145 
apply (subgoal_tac "\<forall>x \<in> A. multiset (f(x) +# g(x)) & mset_of (f(x) +# g(x)) \<subseteq> B") 

146 
apply (erule Fin_induct) 

147 
apply (auto simp add: munion_ac) 

148 
done 

149 

150 
lemma msetsum_cong: 

151 
"[ C=D; !!x. x \<in> D ==> f(x) = g(x) ] 

152 
==> msetsum(f, C, B) = msetsum(g, D, B)" 

153 
by (simp add: msetsum_def general_setsum_def cong add: fold_cong) 

154 

155 
lemma multiset_union_diff: "[ multiset(M); multiset(N) ] ==> M +# N # N = M" 

156 
by (simp add: multiset_equality) 

157 

158 
lemma msetsum_Un: "[ C \<in> Fin(A); D \<in> Fin(A); 

159 
\<forall>x \<in> A. multiset(f(x)) & mset_of(f(x)) \<subseteq> B ] 

46823  160 
==> msetsum(f, C \<union> D, B) = 
161 
msetsum(f, C, B) +# msetsum(f, D, B) # msetsum(f, C \<inter> D, B)" 

162 
apply (subgoal_tac "C \<union> D \<in> Fin (A) & C \<inter> D \<in> Fin (A) ") 

15202  163 
apply clarify 
164 
apply (subst msetsum_Un_Int [symmetric]) 

165 
apply (simp_all (no_asm_simp) add: msetsum_multiset multiset_union_diff) 

166 
apply (blast dest: FinD) 

167 
done 

168 

169 
lemma nsetsum_0 [simp]: "nsetsum(g, 0)=0" 

170 
by (simp add: nsetsum_def) 

171 

172 
lemma nsetsum_cons [simp]: 

173 
"[ Finite(C); x\<notin>C ] ==> nsetsum(g, cons(x, C))= g(x) #+ nsetsum(g, C)" 

174 
apply (simp add: nsetsum_def general_setsum_def) 

175 
apply (rule_tac A = "cons (x, C)" in fold_typing.fold_cons) 

176 
apply (auto intro: Finite_cons_lemma simp add: fold_typing_def) 

177 
done 

178 

179 
lemma nsetsum_type [simp,TC]: "nsetsum(g, C) \<in> nat" 

180 
apply (case_tac "Finite (C) ") 

181 
prefer 2 apply (simp add: nsetsum_def general_setsum_def) 

182 
apply (erule Finite_induct, auto) 

183 
done 

184 

14052  185 
end 