author | nipkow |
Sat, 08 Aug 2020 18:20:09 +0200 | |
changeset 72122 | 2dcb6523f6af |
parent 67399 | eab6ce8368fa |
child 76213 | e44d86131648 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: ZF/UNITY/MultisetSum.thy |
14052 | 2 |
Author: Sidi O Ehmety |
3 |
*) |
|
4 |
||
60770 | 5 |
section \<open>Setsum for Multisets\<close> |
15202 | 6 |
|
7 |
theory MultisetSum |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
60770
diff
changeset
|
8 |
imports "ZF-Induct.Multiset" |
15202 | 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 |
|
67399 | 24 |
"msetsum(g, C, B) == normalize(general_setsum(C, Mult(B), 0, (+#), g))" |
14052 | 25 |
|
24893 | 26 |
|
27 |
definition (* sum for naturals *) |
|
28 |
nsetsum :: "[i=>i, i] =>i" where |
|
67399 | 29 |
"nsetsum(g, C) == general_setsum(C, nat, 0, (#+), 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 |
||
67399 | 54 |
lemma munion_lcomm [simp]: "lcomm(Mult(A), Mult(A), (+#))" |
15202 | 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 tab-width;
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 |
||
67399 | 185 |
end |