converting UNITY/MultisetSum.ML to Isar script
authorpaulson
Sun Sep 19 16:51:10 2004 +0200 (2004-09-19)
changeset 15202d14a6e421a65
parent 15201 d73f9d49d835
child 15203 4481ada46cbb
converting UNITY/MultisetSum.ML to Isar script
src/ZF/IsaMakefile
src/ZF/UNITY/MultisetSum.ML
src/ZF/UNITY/MultisetSum.thy
     1.1 --- a/src/ZF/IsaMakefile	Fri Sep 17 16:08:52 2004 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Sun Sep 19 16:51:10 2004 +0200
     1.3 @@ -122,8 +122,7 @@
     1.4    UNITY/AllocBase.thy UNITY/AllocImpl.thy\
     1.5    UNITY/ClientImpl.thy UNITY/Distributor.thy\
     1.6    UNITY/Follows.thy UNITY/Increasing.thy UNITY/Merge.thy\
     1.7 -  UNITY/Monotonicity.thy\
     1.8 -  UNITY/MultisetSum.ML UNITY/MultisetSum.thy\
     1.9 +  UNITY/Monotonicity.thy UNITY/MultisetSum.thy\
    1.10    UNITY/WFair.ML UNITY/WFair.thy
    1.11  	@$(ISATOOL) usedir $(OUT)/ZF UNITY
    1.12  
     2.1 --- a/src/ZF/UNITY/MultisetSum.ML	Fri Sep 17 16:08:52 2004 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,201 +0,0 @@
     2.4 -(*  Title:      ZF/UNITY/MultusetSum.thy
     2.5 -    ID:         $Id \\<in> MultisetSum.ML,v 1.2 2003/06/24 14:33:00 paulson Exp $
     2.6 -    Author:     Sidi O Ehmety
     2.7 -    Copyright:  2002 University of Cambridge
     2.8 -Setsum for multisets.
     2.9 -*)
    2.10 -
    2.11 -Goal "mset_of(normalize(M)) <= mset_of(M)";
    2.12 -by (auto_tac (claset(), simpset() addsimps [mset_of_def,normalize_def])); 
    2.13 -qed "mset_of_normalize";
    2.14 -
    2.15 -Goalw [general_setsum_def]
    2.16 -"general_setsum(0, B, e, f, g) = e";
    2.17 -by Auto_tac;
    2.18 -qed "general_setsum_0";
    2.19 -Addsimps [general_setsum_0];
    2.20 -
    2.21 -Goalw [general_setsum_def] 
    2.22 -"[| C \\<in> Fin(A); a \\<in> A; a\\<notin>C; e \\<in> B; \\<forall>x \\<in> A. g(x):B; lcomm(B, B, f) |] ==> \
    2.23 -\ general_setsum(cons(a, C), B, e, f, g) = \
    2.24 -\   f(g(a), general_setsum(C, B, e, f,g))";
    2.25 -by  (auto_tac (claset(), simpset() addsimps [Fin_into_Finite RS Finite_cons, 
    2.26 -                                             cons_absorb]));
    2.27 -by (blast_tac (claset() addDs [Fin_into_Finite]) 2);
    2.28 -by (resolve_tac [thm"fold_typing.fold_cons"] 1);
    2.29 -by (auto_tac (claset(), simpset() addsimps [thm "fold_typing_def", lcomm_def]));
    2.30 -qed "general_setsum_cons";
    2.31 -Addsimps [general_setsum_cons];
    2.32 -
    2.33 -(** lcomm **)
    2.34 -
    2.35 -Goalw [lcomm_def]
    2.36 -"[| C<=A; lcomm(A, B, f) |] ==> lcomm(C, B,f)";
    2.37 -by Auto_tac;
    2.38 -by (Blast_tac 1);
    2.39 -qed "lcomm_mono";
    2.40 -
    2.41 -Goalw [lcomm_def]
    2.42 -  "lcomm(Mult(A), Mult(A), op +#)";
    2.43 -by (auto_tac (claset(), simpset() 
    2.44 -    addsimps [Mult_iff_multiset, munion_lcommute]));
    2.45 -qed "munion_lcomm";
    2.46 -Addsimps [munion_lcomm];
    2.47 -
    2.48 -(** msetsum **)
    2.49 -
    2.50 -Goal
    2.51 -"[| C \\<in> Fin(A); \\<forall>x \\<in> A. multiset(g(x))& mset_of(g(x))<=B  |]  \
    2.52 -\  ==> multiset(general_setsum(C, B -||> nat - {0}, 0, \\<lambda>u v. u +# v, g))";
    2.53 -by (etac Fin_induct 1);
    2.54 -by Auto_tac;
    2.55 -by (stac general_setsum_cons 1); 
    2.56 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
    2.57 -qed "multiset_general_setsum";
    2.58 -
    2.59 -Goalw [msetsum_def] "msetsum(g, 0, B) = 0";
    2.60 -by Auto_tac;
    2.61 -qed "msetsum_0";
    2.62 -Addsimps [msetsum_0];
    2.63 -
    2.64 -Goalw [msetsum_def]
    2.65 -"[| C \\<in> Fin(A); a\\<notin>C; a \\<in> A; \\<forall>x \\<in> A. multiset(g(x)) & mset_of(g(x))<=B  |]  \
    2.66 -\  ==> msetsum(g, cons(a, C), B) = g(a) +#  msetsum(g, C, B)";
    2.67 -by (stac general_setsum_cons 1); 
    2.68 -by (auto_tac (claset(), simpset() addsimps [multiset_general_setsum, Mult_iff_multiset]));
    2.69 -qed "msetsum_cons";
    2.70 -Addsimps [msetsum_cons];
    2.71 -
    2.72 -(* msetsum type *)
    2.73 -
    2.74 -Goal "multiset(msetsum(g, C, B))";
    2.75 -by (asm_full_simp_tac (simpset() addsimps [msetsum_def]) 1); 
    2.76 -qed "msetsum_multiset";
    2.77 -
    2.78 -Goal 
    2.79 -"[| C \\<in> Fin(A); \\<forall>x \\<in> A. multiset(g(x)) & mset_of(g(x))<=B |] \ 
    2.80 -\ ==> mset_of(msetsum(g, C, B))<=B";
    2.81 -by (etac Fin_induct 1);
    2.82 -by Auto_tac;
    2.83 -qed "mset_of_msetsum";
    2.84 -
    2.85 -
    2.86 -
    2.87 -(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
    2.88 -Goal 
    2.89 -"[| C \\<in> Fin(A); D \\<in> Fin(A); \\<forall>x \\<in> A. multiset(g(x)) & mset_of(g(x))<=B |] \
    2.90 -\     ==> msetsum(g, C Un D, B) +# msetsum(g, C Int D, B) \
    2.91 -\       = msetsum(g, C, B) +# msetsum(g, D, B)";
    2.92 -by (etac Fin_induct 1);
    2.93 -by (subgoal_tac "cons(x, y) Un D = cons(x, y Un D)" 2);
    2.94 -by (auto_tac (claset(), simpset() addsimps [msetsum_multiset]));
    2.95 -by (subgoal_tac "y Un D \\<in> Fin(A) & y Int D \\<in> Fin(A)" 1);
    2.96 -by (Clarify_tac 1);
    2.97 -by (case_tac "x \\<in> D" 1);
    2.98 -by (subgoal_tac "cons(x, y) Int D = y Int D" 2);
    2.99 -by (subgoal_tac "cons(x, y) Int D = cons(x, y Int D)" 1);
   2.100 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [cons_absorb,
   2.101 -                munion_assoc, msetsum_multiset])));
   2.102 -by (asm_simp_tac (simpset() addsimps [munion_lcommute, msetsum_multiset]) 1);
   2.103 -by Auto_tac;
   2.104 -qed "msetsum_Un_Int";
   2.105 -
   2.106 -
   2.107 -Goal "[| C \\<in> Fin(A); D \\<in> Fin(A); C Int D = 0; \
   2.108 -\  \\<forall>x \\<in> A. multiset(g(x)) & mset_of(g(x))<=B |] \
   2.109 -\     ==> msetsum(g, C Un D, B) = msetsum(g, C, B) +# msetsum(g,D, B)";  
   2.110 -by (stac (msetsum_Un_Int RS sym) 1);
   2.111 -by (auto_tac (claset(),  simpset() addsimps [msetsum_multiset]));
   2.112 -qed "msetsum_Un_disjoint";
   2.113 -
   2.114 -Goal "I \\<in> Fin(A) ==> (\\<forall>i \\<in> I. C(i):Fin(B)) --> (\\<Union>i \\<in> I. C(i)):Fin(B)";
   2.115 -by (etac Fin_induct 1);
   2.116 -by Auto_tac;
   2.117 -qed_spec_mp "UN_Fin_lemma";
   2.118 - 
   2.119 -Goal "!!I. [| I \\<in> Fin(K); \\<forall>i \\<in> K. C(i):Fin(A) |] ==> \
   2.120 -\ (\\<forall>x \\<in> A. multiset(f(x)) & mset_of(f(x))<=B) -->  \
   2.121 -\ (\\<forall>i \\<in> I. \\<forall>j \\<in> I. i\\<noteq>j --> C(i) Int C(j) = 0) --> \
   2.122 -\   msetsum(f, \\<Union>i \\<in> I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)"; 
   2.123 -by (etac Fin_induct 1);
   2.124 -by (ALLGOALS(Clarify_tac));
   2.125 -by Auto_tac;
   2.126 -by (subgoal_tac "\\<forall>i \\<in> y. x \\<noteq> i" 1);
   2.127 - by (Blast_tac 2); 
   2.128 -by (subgoal_tac "C(x) Int (\\<Union>i \\<in> y. C(i)) = 0" 1);
   2.129 - by (Blast_tac 2);
   2.130 -by (subgoal_tac " (\\<Union>i \\<in> y. C(i)):Fin(A) & C(x):Fin(A)" 1);
   2.131 -by (blast_tac (claset() addIs [UN_Fin_lemma] addDs [FinD]) 2);
   2.132 -by (Clarify_tac 1);
   2.133 -by (asm_simp_tac (simpset() addsimps [msetsum_Un_disjoint]) 1);
   2.134 -by (subgoal_tac "\\<forall>x \\<in> K. multiset(msetsum(f, C(x), B)) &\
   2.135 -                \ mset_of(msetsum(f, C(x), B)) <= B" 1);
   2.136 -by (Asm_simp_tac 1);
   2.137 -by (Clarify_tac 1);
   2.138 -by (dres_inst_tac [("x", "xa")] bspec 1);
   2.139 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [msetsum_multiset, mset_of_msetsum])));
   2.140 -qed_spec_mp "msetsum_UN_disjoint";
   2.141 -
   2.142 -Goal 
   2.143 -"[| C \\<in> Fin(A); \
   2.144 -\ \\<forall>x \\<in> A. multiset(f(x)) & mset_of(f(x))<=B; \
   2.145 -\ \\<forall>x \\<in> A. multiset(g(x)) & mset_of(g(x))<=B |] ==>\
   2.146 -\ msetsum(%x. f(x) +# g(x), C, B) = msetsum(f, C, B) +# msetsum(g, C, B)";
   2.147 -by (subgoal_tac "\\<forall>x \\<in> A. multiset(f(x) +# g(x)) & mset_of(f(x) +# g(x))<=B" 1);
   2.148 -by (etac Fin_induct 1);
   2.149 -by (ALLGOALS(Asm_simp_tac));
   2.150 -by (resolve_tac [trans] 1);
   2.151 -by (resolve_tac [msetsum_cons] 1);
   2.152 -by (assume_tac 1);
   2.153 -by (auto_tac (claset(), simpset() addsimps [msetsum_multiset, munion_assoc]));
   2.154 -by (asm_simp_tac (simpset() addsimps [msetsum_multiset, munion_lcommute]) 1);
   2.155 -qed "msetsum_addf";
   2.156 -
   2.157 -
   2.158 -val prems = Goal
   2.159 - "[| C=D; !!x. x \\<in> D ==> f(x) = g(x) |] ==> \
   2.160 -\    msetsum(f, C, B) = msetsum(g, D, B)";
   2.161 -by (asm_full_simp_tac (simpset() addsimps [msetsum_def, general_setsum_def]@prems addcongs [fold_cong]) 1);
   2.162 -qed  "msetsum_cong";
   2.163 -
   2.164 -Goal "[| multiset(M); multiset(N) |] ==> M +# N -# N = M";
   2.165 -by (asm_simp_tac (simpset() addsimps [multiset_equality]) 1);
   2.166 -qed "multiset_union_diff";
   2.167 -
   2.168 -
   2.169 -Goal "[| C \\<in> Fin(A); D \\<in> Fin(A); \
   2.170 -\ \\<forall>x \\<in> A. multiset(f(x)) & mset_of(f(x))<=B  |] \
   2.171 -\  ==> msetsum(f, C Un D, B) = \
   2.172 -\         msetsum(f, C, B) +# msetsum(f, D, B) -# msetsum(f, C Int D, B)";
   2.173 -by (subgoal_tac "C Un D \\<in> Fin(A) & C Int D \\<in> Fin(A)" 1);
   2.174 -by (Clarify_tac 1);
   2.175 -by (stac (msetsum_Un_Int RS sym) 1);
   2.176 -by (ALLGOALS(asm_simp_tac (simpset() addsimps 
   2.177 -         [msetsum_multiset,multiset_union_diff])));
   2.178 -by (blast_tac (claset() addDs [FinD]) 1);
   2.179 -qed "msetsum_Un";
   2.180 -
   2.181 -
   2.182 -Goalw [nsetsum_def] "nsetsum(g, 0)=0";
   2.183 -by Auto_tac;
   2.184 -qed "nsetsum_0";
   2.185 -Addsimps [nsetsum_0];
   2.186 -
   2.187 -Goalw [nsetsum_def, general_setsum_def] 
   2.188 -"[| Finite(C); x\\<notin>C |] \
   2.189 -\  ==> nsetsum(g, cons(x, C))= g(x) #+ nsetsum(g, C)";
   2.190 -by (auto_tac (claset(), simpset() addsimps [Finite_cons]));
   2.191 -by (res_inst_tac [("A", "cons(x, C)")] (thm"fold_typing.fold_cons") 1);
   2.192 -by (auto_tac (claset() addIs [thm"Finite_cons_lemma"], 
   2.193 -              simpset() addsimps [thm "fold_typing_def"]));
   2.194 -qed "nsetsum_cons";
   2.195 -Addsimps [nsetsum_cons];
   2.196 -
   2.197 -Goal "nsetsum(g, C):nat";
   2.198 -by (case_tac "Finite(C)" 1);
   2.199 -by (asm_simp_tac (simpset() addsimps [nsetsum_def, general_setsum_def]) 2);
   2.200 -by (etac Finite_induct 1);
   2.201 -by Auto_tac;
   2.202 -qed "nsetsum_type";
   2.203 -Addsimps [nsetsum_type];  
   2.204 -AddTCs [nsetsum_type];
     3.1 --- a/src/ZF/UNITY/MultisetSum.thy	Fri Sep 17 16:08:52 2004 +0200
     3.2 +++ b/src/ZF/UNITY/MultisetSum.thy	Sun Sep 19 16:51:10 2004 +0200
     3.3 @@ -1,17 +1,20 @@
     3.4  (*  Title:      ZF/UNITY/MultusetSum.thy
     3.5      ID:         $Id$
     3.6      Author:     Sidi O Ehmety
     3.7 -
     3.8 -Setsum for multisets.
     3.9  *)
    3.10  
    3.11 -MultisetSum = Multiset +
    3.12 +header {*Setsum for Multisets*}
    3.13 +
    3.14 +theory MultisetSum
    3.15 +imports "../Induct/Multiset"
    3.16 +begin
    3.17 +
    3.18  constdefs
    3.19  
    3.20    lcomm :: "[i, i, [i,i]=>i]=>o"
    3.21    "lcomm(A, B, f) ==
    3.22 -   (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))= f(y, f(x, z)))  &
    3.23 -   (ALL x:A. ALL y:B. f(x, y):B)"
    3.24 +   (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> B. f(x, f(y, z))= f(y, f(x, z)))  &
    3.25 +   (\<forall>x \<in> A. \<forall>y \<in> B. f(x, y) \<in> B)"
    3.26  
    3.27    general_setsum :: "[i,i,i, [i,i]=>i, i=>i] =>i"
    3.28     "general_setsum(C, B, e, f, g) ==
    3.29 @@ -23,4 +26,184 @@
    3.30    (* sum for naturals *)
    3.31    nsetsum :: "[i=>i, i] =>i"
    3.32    "nsetsum(g, C) == general_setsum(C, nat, 0, op #+, g)"
    3.33 +
    3.34 +
    3.35 +lemma mset_of_normalize: "mset_of(normalize(M)) \<subseteq> mset_of(M)"
    3.36 +by (auto simp add: mset_of_def normalize_def)
    3.37 +
    3.38 +lemma general_setsum_0 [simp]: "general_setsum(0, B, e, f, g) = e"
    3.39 +by (simp add: general_setsum_def)
    3.40 +
    3.41 +lemma general_setsum_cons [simp]: 
    3.42 +"[| 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) |] ==>  
    3.43 +  general_setsum(cons(a, C), B, e, f, g) =  
    3.44 +    f(g(a), general_setsum(C, B, e, f,g))"
    3.45 +apply (simp add: general_setsum_def)
    3.46 +apply  (auto simp add: Fin_into_Finite [THEN Finite_cons] cons_absorb)
    3.47 +prefer 2 apply (blast dest: Fin_into_Finite)
    3.48 +apply (rule fold_typing.fold_cons)
    3.49 +apply (auto simp add: fold_typing_def lcomm_def)
    3.50 +done
    3.51 +
    3.52 +(** lcomm **)
    3.53 +
    3.54 +lemma lcomm_mono: "[| C\<subseteq>A; lcomm(A, B, f) |] ==> lcomm(C, B,f)"
    3.55 +by (auto simp add: lcomm_def, blast)
    3.56 +
    3.57 +lemma munion_lcomm [simp]: "lcomm(Mult(A), Mult(A), op +#)"
    3.58 +by (auto simp add: lcomm_def Mult_iff_multiset munion_lcommute)
    3.59 +
    3.60 +(** msetsum **)
    3.61 +
    3.62 +lemma multiset_general_setsum: 
    3.63 +     "[| C \<in> Fin(A); \<forall>x \<in> A. multiset(g(x))& mset_of(g(x))\<subseteq>B  |]   
    3.64 +      ==> multiset(general_setsum(C, B -||> nat - {0}, 0, \<lambda>u v. u +# v, g))"
    3.65 +apply (erule Fin_induct, auto)
    3.66 +apply (subst general_setsum_cons)
    3.67 +apply (auto simp add: Mult_iff_multiset)
    3.68 +done
    3.69 +
    3.70 +lemma msetsum_0 [simp]: "msetsum(g, 0, B) = 0"
    3.71 +by (simp add: msetsum_def)
    3.72 +
    3.73 +lemma msetsum_cons [simp]: 
    3.74 +  "[| C \<in> Fin(A); a\<notin>C; a \<in> A; \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B  |]   
    3.75 +   ==> msetsum(g, cons(a, C), B) = g(a) +#  msetsum(g, C, B)"
    3.76 +apply (simp add: msetsum_def)
    3.77 +apply (subst general_setsum_cons)
    3.78 +apply (auto simp add: multiset_general_setsum Mult_iff_multiset)
    3.79 +done
    3.80 +
    3.81 +(* msetsum type *)
    3.82 +
    3.83 +lemma msetsum_multiset: "multiset(msetsum(g, C, B))"
    3.84 +by (simp add: msetsum_def)
    3.85 +
    3.86 +lemma mset_of_msetsum: 
    3.87 +     "[| C \<in> Fin(A); \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B |]   
    3.88 +      ==> mset_of(msetsum(g, C, B))\<subseteq>B"
    3.89 +by (erule Fin_induct, auto)
    3.90 +
    3.91 +
    3.92 +(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
    3.93 +lemma msetsum_Un_Int: 
    3.94 +     "[| C \<in> Fin(A); D \<in> Fin(A); \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B |]
    3.95 +      ==> msetsum(g, C Un D, B) +# msetsum(g, C Int D, B)  
    3.96 +        = msetsum(g, C, B) +# msetsum(g, D, B)"
    3.97 +apply (erule Fin_induct)
    3.98 +apply (subgoal_tac [2] "cons (x, y) Un D = cons (x, y Un D) ")
    3.99 +apply (auto simp add: msetsum_multiset)
   3.100 +apply (subgoal_tac "y Un D \<in> Fin (A) & y Int D \<in> Fin (A) ")
   3.101 +apply clarify
   3.102 +apply (case_tac "x \<in> D")
   3.103 +apply (subgoal_tac [2] "cons (x, y) Int D = y Int D")
   3.104 +apply (subgoal_tac "cons (x, y) Int D = cons (x, y Int D) ")
   3.105 +apply (simp_all (no_asm_simp) add: cons_absorb munion_assoc msetsum_multiset)
   3.106 +apply (simp (no_asm_simp) add: munion_lcommute msetsum_multiset)
   3.107 +apply auto
   3.108 +done
   3.109 +
   3.110 +
   3.111 +lemma msetsum_Un_disjoint:
   3.112 +     "[| C \<in> Fin(A); D \<in> Fin(A); C Int D = 0;  
   3.113 +         \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B |]  
   3.114 +      ==> msetsum(g, C Un D, B) = msetsum(g, C, B) +# msetsum(g,D, B)"
   3.115 +apply (subst msetsum_Un_Int [symmetric])
   3.116 +apply (auto simp add: msetsum_multiset)
   3.117 +done
   3.118 +
   3.119 +lemma UN_Fin_lemma [rule_format (no_asm)]:
   3.120 +     "I \<in> Fin(A) ==> (\<forall>i \<in> I. C(i) \<in> Fin(B)) --> (\<Union>i \<in> I. C(i)):Fin(B)"
   3.121 +by (erule Fin_induct, auto)
   3.122 + 
   3.123 +lemma msetsum_UN_disjoint [rule_format (no_asm)]:
   3.124 +     "[| I \<in> Fin(K); \<forall>i \<in> K. C(i) \<in> Fin(A) |] ==>  
   3.125 +      (\<forall>x \<in> A. multiset(f(x)) & mset_of(f(x))\<subseteq>B) -->   
   3.126 +      (\<forall>i \<in> I. \<forall>j \<in> I. i\<noteq>j --> C(i) Int C(j) = 0) -->  
   3.127 +	msetsum(f, \<Union>i \<in> I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)"
   3.128 +apply (erule Fin_induct, auto)
   3.129 +apply (subgoal_tac "\<forall>i \<in> y. x \<noteq> i")
   3.130 + prefer 2 apply blast
   3.131 +apply (subgoal_tac "C(x) Int (\<Union>i \<in> y. C (i)) = 0")
   3.132 + prefer 2 apply blast
   3.133 +apply (subgoal_tac " (\<Union>i \<in> y. C (i)):Fin (A) & C(x) :Fin (A) ")
   3.134 +prefer 2 apply (blast intro: UN_Fin_lemma dest: FinD, clarify)
   3.135 +apply (simp (no_asm_simp) add: msetsum_Un_disjoint)
   3.136 +apply (subgoal_tac "\<forall>x \<in> K. multiset (msetsum (f, C(x), B)) & mset_of (msetsum (f, C(x), B)) \<subseteq> B")
   3.137 +apply (simp (no_asm_simp))
   3.138 +apply clarify
   3.139 +apply (drule_tac x = xa in bspec)
   3.140 +apply (simp_all (no_asm_simp) add: msetsum_multiset mset_of_msetsum)
   3.141 +done
   3.142 +
   3.143 +lemma msetsum_addf: 
   3.144 +    "[| C \<in> Fin(A);  
   3.145 +      \<forall>x \<in> A. multiset(f(x)) & mset_of(f(x))\<subseteq>B;  
   3.146 +      \<forall>x \<in> A. multiset(g(x)) & mset_of(g(x))\<subseteq>B |] ==> 
   3.147 +      msetsum(%x. f(x) +# g(x), C, B) = msetsum(f, C, B) +# msetsum(g, C, B)"
   3.148 +apply (subgoal_tac "\<forall>x \<in> A. multiset (f(x) +# g(x)) & mset_of (f(x) +# g(x)) \<subseteq> B")
   3.149 +apply (erule Fin_induct)
   3.150 +apply (auto simp add: munion_ac) 
   3.151 +done
   3.152 +
   3.153 +lemma msetsum_cong: 
   3.154 +    "[| C=D; !!x. x \<in> D ==> f(x) = g(x) |]
   3.155 +     ==> msetsum(f, C, B) = msetsum(g, D, B)"
   3.156 +by (simp add: msetsum_def general_setsum_def cong add: fold_cong)
   3.157 +
   3.158 +lemma multiset_union_diff: "[| multiset(M); multiset(N) |] ==> M +# N -# N = M"
   3.159 +by (simp add: multiset_equality)
   3.160 +
   3.161 +lemma msetsum_Un: "[| C \<in> Fin(A); D \<in> Fin(A);  
   3.162 +  \<forall>x \<in> A. multiset(f(x)) & mset_of(f(x)) \<subseteq> B  |]  
   3.163 +   ==> msetsum(f, C Un D, B) =  
   3.164 +          msetsum(f, C, B) +# msetsum(f, D, B) -# msetsum(f, C Int D, B)"
   3.165 +apply (subgoal_tac "C Un D \<in> Fin (A) & C Int D \<in> Fin (A) ")
   3.166 +apply clarify
   3.167 +apply (subst msetsum_Un_Int [symmetric])
   3.168 +apply (simp_all (no_asm_simp) add: msetsum_multiset multiset_union_diff)
   3.169 +apply (blast dest: FinD)
   3.170 +done
   3.171 +
   3.172 +lemma nsetsum_0 [simp]: "nsetsum(g, 0)=0"
   3.173 +by (simp add: nsetsum_def)
   3.174 +
   3.175 +lemma nsetsum_cons [simp]: 
   3.176 +     "[| Finite(C); x\<notin>C |] ==> nsetsum(g, cons(x, C))= g(x) #+ nsetsum(g, C)"
   3.177 +apply (simp add: nsetsum_def general_setsum_def)
   3.178 +apply (rule_tac A = "cons (x, C)" in fold_typing.fold_cons)
   3.179 +apply (auto intro: Finite_cons_lemma simp add: fold_typing_def)
   3.180 +done
   3.181 +
   3.182 +lemma nsetsum_type [simp,TC]: "nsetsum(g, C) \<in> nat"
   3.183 +apply (case_tac "Finite (C) ")
   3.184 + prefer 2 apply (simp add: nsetsum_def general_setsum_def)
   3.185 +apply (erule Finite_induct, auto)
   3.186 +done
   3.187 +
   3.188 +ML
   3.189 +{*
   3.190 +val mset_of_normalize = thm "mset_of_normalize";
   3.191 +val general_setsum_0 = thm "general_setsum_0";
   3.192 +val general_setsum_cons = thm "general_setsum_cons";
   3.193 +val lcomm_mono = thm "lcomm_mono";
   3.194 +val munion_lcomm = thm "munion_lcomm";
   3.195 +val multiset_general_setsum = thm "multiset_general_setsum";
   3.196 +val msetsum_0 = thm "msetsum_0";
   3.197 +val msetsum_cons = thm "msetsum_cons";
   3.198 +val msetsum_multiset = thm "msetsum_multiset";
   3.199 +val mset_of_msetsum = thm "mset_of_msetsum";
   3.200 +val msetsum_Un_Int = thm "msetsum_Un_Int";
   3.201 +val msetsum_Un_disjoint = thm "msetsum_Un_disjoint";
   3.202 +val UN_Fin_lemma = thm "UN_Fin_lemma";
   3.203 +val msetsum_UN_disjoint = thm "msetsum_UN_disjoint";
   3.204 +val msetsum_addf = thm "msetsum_addf";
   3.205 +val msetsum_cong = thm "msetsum_cong";
   3.206 +val multiset_union_diff = thm "multiset_union_diff";
   3.207 +val msetsum_Un = thm "msetsum_Un";
   3.208 +val nsetsum_0 = thm "nsetsum_0";
   3.209 +val nsetsum_cons = thm "nsetsum_cons";
   3.210 +val nsetsum_type = thm "nsetsum_type";
   3.211 +*}
   3.212 +
   3.213  end
   3.214 \ No newline at end of file