(* Title: ZF/UNITY/MultusetSum.thy ID: $Id: MultisetSum.thy,v 1.2 2004/09/19 14:51:10 paulson Exp $ Author: Sidi O Ehmety *) header {*Setsum for Multisets*} theory MultisetSum imports "../Induct/Multiset" begin constdefs lcomm :: "[i, i, [i,i]=>i]=>o" "lcomm(A, B, f) == (∀x ∈ A. ∀y ∈ A. ∀z ∈ B. f(x, f(y, z))= f(y, f(x, z))) & (∀x ∈ A. ∀y ∈ B. f(x, y) ∈ B)" general_setsum :: "[i,i,i, [i,i]=>i, i=>i] =>i" "general_setsum(C, B, e, f, g) == if Finite(C) then fold[cons(e, B)](%x y. f(g(x), y), e, C) else e" msetsum :: "[i=>i, i, i]=>i" "msetsum(g, C, B) == normalize(general_setsum(C, Mult(B), 0, op +#, g))" (* sum for naturals *) nsetsum :: "[i=>i, i] =>i" "nsetsum(g, C) == general_setsum(C, nat, 0, op #+, g)" lemma mset_of_normalize: "mset_of(normalize(M)) ⊆ mset_of(M)" by (auto simp add: mset_of_def normalize_def) lemma general_setsum_0 [simp]: "general_setsum(0, B, e, f, g) = e" by (simp add: general_setsum_def) lemma general_setsum_cons [simp]: "[| C ∈ Fin(A); a ∈ A; a∉C; e ∈ B; ∀x ∈ A. g(x) ∈ B; lcomm(B, B, f) |] ==> general_setsum(cons(a, C), B, e, f, g) = f(g(a), general_setsum(C, B, e, f,g))" apply (simp add: general_setsum_def) apply (auto simp add: Fin_into_Finite [THEN Finite_cons] cons_absorb) prefer 2 apply (blast dest: Fin_into_Finite) apply (rule fold_typing.fold_cons) apply (auto simp add: fold_typing_def lcomm_def) done (** lcomm **) lemma lcomm_mono: "[| C⊆A; lcomm(A, B, f) |] ==> lcomm(C, B,f)" by (auto simp add: lcomm_def, blast) lemma munion_lcomm [simp]: "lcomm(Mult(A), Mult(A), op +#)" by (auto simp add: lcomm_def Mult_iff_multiset munion_lcommute) (** msetsum **) lemma multiset_general_setsum: "[| C ∈ Fin(A); ∀x ∈ A. multiset(g(x))& mset_of(g(x))⊆B |] ==> multiset(general_setsum(C, B -||> nat - {0}, 0, λu v. u +# v, g))" apply (erule Fin_induct, auto) apply (subst general_setsum_cons) apply (auto simp add: Mult_iff_multiset) done lemma msetsum_0 [simp]: "msetsum(g, 0, B) = 0" by (simp add: msetsum_def) lemma msetsum_cons [simp]: "[| C ∈ Fin(A); a∉C; a ∈ A; ∀x ∈ A. multiset(g(x)) & mset_of(g(x))⊆B |] ==> msetsum(g, cons(a, C), B) = g(a) +# msetsum(g, C, B)" apply (simp add: msetsum_def) apply (subst general_setsum_cons) apply (auto simp add: multiset_general_setsum Mult_iff_multiset) done (* msetsum type *) lemma msetsum_multiset: "multiset(msetsum(g, C, B))" by (simp add: msetsum_def) lemma mset_of_msetsum: "[| C ∈ Fin(A); ∀x ∈ A. multiset(g(x)) & mset_of(g(x))⊆B |] ==> mset_of(msetsum(g, C, B))⊆B" by (erule Fin_induct, auto) (*The reversed orientation looks more natural, but LOOPS as a simprule!*) lemma msetsum_Un_Int: "[| C ∈ Fin(A); D ∈ Fin(A); ∀x ∈ A. multiset(g(x)) & mset_of(g(x))⊆B |] ==> msetsum(g, C Un D, B) +# msetsum(g, C Int D, B) = msetsum(g, C, B) +# msetsum(g, D, B)" apply (erule Fin_induct) apply (subgoal_tac [2] "cons (x, y) Un D = cons (x, y Un D) ") apply (auto simp add: msetsum_multiset) apply (subgoal_tac "y Un D ∈ Fin (A) & y Int D ∈ Fin (A) ") apply clarify apply (case_tac "x ∈ D") apply (subgoal_tac [2] "cons (x, y) Int D = y Int D") apply (subgoal_tac "cons (x, y) Int D = cons (x, y Int D) ") apply (simp_all (no_asm_simp) add: cons_absorb munion_assoc msetsum_multiset) apply (simp (no_asm_simp) add: munion_lcommute msetsum_multiset) apply auto done lemma msetsum_Un_disjoint: "[| C ∈ Fin(A); D ∈ Fin(A); C Int D = 0; ∀x ∈ A. multiset(g(x)) & mset_of(g(x))⊆B |] ==> msetsum(g, C Un D, B) = msetsum(g, C, B) +# msetsum(g,D, B)" apply (subst msetsum_Un_Int [symmetric]) apply (auto simp add: msetsum_multiset) done lemma UN_Fin_lemma [rule_format (no_asm)]: "I ∈ Fin(A) ==> (∀i ∈ I. C(i) ∈ Fin(B)) --> (\<Union>i ∈ I. C(i)):Fin(B)" by (erule Fin_induct, auto) lemma msetsum_UN_disjoint [rule_format (no_asm)]: "[| I ∈ Fin(K); ∀i ∈ K. C(i) ∈ Fin(A) |] ==> (∀x ∈ A. multiset(f(x)) & mset_of(f(x))⊆B) --> (∀i ∈ I. ∀j ∈ I. i≠j --> C(i) Int C(j) = 0) --> msetsum(f, \<Union>i ∈ I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)" apply (erule Fin_induct, auto) apply (subgoal_tac "∀i ∈ y. x ≠ i") prefer 2 apply blast apply (subgoal_tac "C(x) Int (\<Union>i ∈ y. C (i)) = 0") prefer 2 apply blast apply (subgoal_tac " (\<Union>i ∈ y. C (i)):Fin (A) & C(x) :Fin (A) ") prefer 2 apply (blast intro: UN_Fin_lemma dest: FinD, clarify) apply (simp (no_asm_simp) add: msetsum_Un_disjoint) apply (subgoal_tac "∀x ∈ K. multiset (msetsum (f, C(x), B)) & mset_of (msetsum (f, C(x), B)) ⊆ B") apply (simp (no_asm_simp)) apply clarify apply (drule_tac x = xa in bspec) apply (simp_all (no_asm_simp) add: msetsum_multiset mset_of_msetsum) done lemma msetsum_addf: "[| C ∈ Fin(A); ∀x ∈ A. multiset(f(x)) & mset_of(f(x))⊆B; ∀x ∈ A. multiset(g(x)) & mset_of(g(x))⊆B |] ==> msetsum(%x. f(x) +# g(x), C, B) = msetsum(f, C, B) +# msetsum(g, C, B)" apply (subgoal_tac "∀x ∈ A. multiset (f(x) +# g(x)) & mset_of (f(x) +# g(x)) ⊆ B") apply (erule Fin_induct) apply (auto simp add: munion_ac) done lemma msetsum_cong: "[| C=D; !!x. x ∈ D ==> f(x) = g(x) |] ==> msetsum(f, C, B) = msetsum(g, D, B)" by (simp add: msetsum_def general_setsum_def cong add: fold_cong) lemma multiset_union_diff: "[| multiset(M); multiset(N) |] ==> M +# N -# N = M" by (simp add: multiset_equality) lemma msetsum_Un: "[| C ∈ Fin(A); D ∈ Fin(A); ∀x ∈ A. multiset(f(x)) & mset_of(f(x)) ⊆ B |] ==> msetsum(f, C Un D, B) = msetsum(f, C, B) +# msetsum(f, D, B) -# msetsum(f, C Int D, B)" apply (subgoal_tac "C Un D ∈ Fin (A) & C Int D ∈ Fin (A) ") apply clarify apply (subst msetsum_Un_Int [symmetric]) apply (simp_all (no_asm_simp) add: msetsum_multiset multiset_union_diff) apply (blast dest: FinD) done lemma nsetsum_0 [simp]: "nsetsum(g, 0)=0" by (simp add: nsetsum_def) lemma nsetsum_cons [simp]: "[| Finite(C); x∉C |] ==> nsetsum(g, cons(x, C))= g(x) #+ nsetsum(g, C)" apply (simp add: nsetsum_def general_setsum_def) apply (rule_tac A = "cons (x, C)" in fold_typing.fold_cons) apply (auto intro: Finite_cons_lemma simp add: fold_typing_def) done lemma nsetsum_type [simp,TC]: "nsetsum(g, C) ∈ nat" apply (case_tac "Finite (C) ") prefer 2 apply (simp add: nsetsum_def general_setsum_def) apply (erule Finite_induct, auto) done ML {* val mset_of_normalize = thm "mset_of_normalize"; val general_setsum_0 = thm "general_setsum_0"; val general_setsum_cons = thm "general_setsum_cons"; val lcomm_mono = thm "lcomm_mono"; val munion_lcomm = thm "munion_lcomm"; val multiset_general_setsum = thm "multiset_general_setsum"; val msetsum_0 = thm "msetsum_0"; val msetsum_cons = thm "msetsum_cons"; val msetsum_multiset = thm "msetsum_multiset"; val mset_of_msetsum = thm "mset_of_msetsum"; val msetsum_Un_Int = thm "msetsum_Un_Int"; val msetsum_Un_disjoint = thm "msetsum_Un_disjoint"; val UN_Fin_lemma = thm "UN_Fin_lemma"; val msetsum_UN_disjoint = thm "msetsum_UN_disjoint"; val msetsum_addf = thm "msetsum_addf"; val msetsum_cong = thm "msetsum_cong"; val multiset_union_diff = thm "multiset_union_diff"; val msetsum_Un = thm "msetsum_Un"; val nsetsum_0 = thm "nsetsum_0"; val nsetsum_cons = thm "nsetsum_cons"; val nsetsum_type = thm "nsetsum_type"; *} end
lemma mset_of_normalize:
mset_of(normalize(M)) ⊆ mset_of(M)
lemma general_setsum_0:
general_setsum(0, B, e, f, g) = e
lemma general_setsum_cons:
[| C ∈ Fin(A); a ∈ A; a ∉ C; e ∈ B; ∀x∈A. g(x) ∈ B; lcomm(B, B, f) |] ==> general_setsum(cons(a, C), B, e, f, g) = f(g(a), general_setsum(C, B, e, f, g))
lemma lcomm_mono:
[| C ⊆ A; lcomm(A, B, f) |] ==> lcomm(C, B, f)
lemma munion_lcomm:
lcomm(A -||> nat - {0}, A -||> nat - {0}, op +#)
lemma multiset_general_setsum:
[| C ∈ Fin(A); ∀x∈A. multiset(g(x)) ∧ mset_of(g(x)) ⊆ B |] ==> multiset(general_setsum(C, B -||> nat - {0}, 0, %u v. u +# v, g))
lemma msetsum_0:
msetsum(g, 0, B) = 0
lemma msetsum_cons:
[| C ∈ Fin(A); a ∉ C; a ∈ A; ∀x∈A. multiset(g(x)) ∧ mset_of(g(x)) ⊆ B |] ==> msetsum(g, cons(a, C), B) = g(a) +# msetsum(g, C, B)
lemma msetsum_multiset:
multiset(msetsum(g, C, B))
lemma mset_of_msetsum:
[| C ∈ Fin(A); ∀x∈A. multiset(g(x)) ∧ mset_of(g(x)) ⊆ B |] ==> mset_of(msetsum(g, C, B)) ⊆ B
lemma msetsum_Un_Int:
[| C ∈ Fin(A); D ∈ Fin(A); ∀x∈A. multiset(g(x)) ∧ mset_of(g(x)) ⊆ B |] ==> msetsum(g, C ∪ D, B) +# msetsum(g, C ∩ D, B) = msetsum(g, C, B) +# msetsum(g, D, B)
lemma msetsum_Un_disjoint:
[| C ∈ Fin(A); D ∈ Fin(A); C ∩ D = 0; ∀x∈A. multiset(g(x)) ∧ mset_of(g(x)) ⊆ B |] ==> msetsum(g, C ∪ D, B) = msetsum(g, C, B) +# msetsum(g, D, B)
lemma UN_Fin_lemma:
[| I ∈ Fin(A); ∀i∈I. C(i) ∈ Fin(B) |] ==> \<Union>RepFun(I, C) ∈ Fin(B)
lemma msetsum_UN_disjoint:
[| I ∈ Fin(K); ∀i∈K. C(i) ∈ Fin(A); ∀x∈A. multiset(f(x)) ∧ mset_of(f(x)) ⊆ B; ∀i∈I. ∀j∈I. i ≠ j --> C(i) ∩ C(j) = 0 |] ==> msetsum(f, \<Union>RepFun(I, C), B) = msetsum(%i. msetsum(f, C(i), B), I, B)
lemma msetsum_addf:
[| C ∈ Fin(A); ∀x∈A. multiset(f(x)) ∧ mset_of(f(x)) ⊆ B; ∀x∈A. multiset(g(x)) ∧ mset_of(g(x)) ⊆ B |] ==> msetsum(%x. f(x) +# g(x), C, B) = msetsum(f, C, B) +# msetsum(g, C, B)
lemma msetsum_cong:
[| C = D; !!x. x ∈ D ==> f(x) = g(x) |] ==> msetsum(f, C, B) = msetsum(g, D, B)
lemma multiset_union_diff:
[| multiset(M); multiset(N) |] ==> M +# N -# N = M
lemma msetsum_Un:
[| C ∈ Fin(A); D ∈ Fin(A); ∀x∈A. multiset(f(x)) ∧ mset_of(f(x)) ⊆ B |] ==> msetsum(f, C ∪ D, B) = msetsum(f, C, B) +# msetsum(f, D, B) -# msetsum(f, C ∩ D, B)
lemma nsetsum_0:
nsetsum(g, 0) = 0
lemma nsetsum_cons:
[| Finite(C); x ∉ C |] ==> nsetsum(g, cons(x, C)) = g(x) #+ nsetsum(g, C)
lemma nsetsum_type:
nsetsum(g, C) ∈ nat