(* Title: ZF/UNITY/MultisetSum.thy
Author: Sidi O Ehmety
*)
section ‹Setsum
for Multisets
›
theory MultisetSum
imports "ZF-Induct.Multiset"
begin
definition
lcomm ::
"[i, i, [i,i]\i]\o" where
"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)
"
definition
general_setsum ::
"[i,i,i, [i,i]\i, i\i] \i" where
"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
"
definition
msetsum ::
"[i\i, i, i]\i" where
"msetsum(g, C, B) \ normalize(general_setsum(C, Mult(B), 0, (+#), g))"
definition (* sum for naturals *)
nsetsum ::
"[i\i, i] \i" where
"nsetsum(g, C) \ general_setsum(C, nat, 0, (#+), 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), (+#))"
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
∪ D, B) +# msetsum(g, C
∩ D, B)
= msetsum(g, C, B) +# msetsum(g, D, B)
"
apply (erule Fin_induct)
apply (subgoal_tac [2]
"cons (x, y) \ D = cons (x, y \ D) ")
apply (auto simp add: msetsum_multiset)
apply (subgoal_tac
"y \ D \ Fin (A) \ y \ D \ Fin (A) ")
apply clarify
apply (case_tac
"x \ D")
apply (subgoal_tac [2]
"cons (x, y) \ D = y \ D")
apply (subgoal_tac
"cons (x, y) \ D = cons (x, y \ 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 \ 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)
"
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)) \ (\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)
∩ C(j) = 0)
⟶
msetsum(f,
∪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) \ (\i \ y. C (i)) = 0")
prefer 2
apply blast
apply (subgoal_tac
" (\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
∪ D, B) =
msetsum(f, C, B) +# msetsum(f, D, B) -# msetsum(f, C
∩ D, B)
"
apply (subgoal_tac
"C \ D \ Fin (A) \ C \ 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
end
