58197
|
1 |
(* Author: Florian Haftmann, TU Muenchen *)
|
|
2 |
|
|
3 |
header \<open>Big sum and product over function bodies\<close>
|
|
4 |
|
|
5 |
theory Groups_Big_Fun
|
|
6 |
imports
|
|
7 |
Main
|
|
8 |
"~~/src/Tools/Permanent_Interpretation"
|
|
9 |
begin
|
|
10 |
|
|
11 |
subsection \<open>Abstract product\<close>
|
|
12 |
|
|
13 |
no_notation times (infixl "*" 70)
|
|
14 |
no_notation Groups.one ("1")
|
|
15 |
|
|
16 |
locale comm_monoid_fun = comm_monoid
|
|
17 |
begin
|
|
18 |
|
|
19 |
definition G :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
|
|
20 |
where
|
|
21 |
expand_set: "G g = comm_monoid_set.F f 1 g {a. g a \<noteq> 1}"
|
|
22 |
|
|
23 |
interpretation F!: comm_monoid_set f 1
|
|
24 |
..
|
|
25 |
|
|
26 |
lemma expand_superset:
|
|
27 |
assumes "finite A" and "{a. g a \<noteq> 1} \<subseteq> A"
|
|
28 |
shows "G g = F.F g A"
|
|
29 |
apply (simp add: expand_set)
|
|
30 |
apply (rule F.same_carrierI [of A])
|
|
31 |
apply (simp_all add: assms)
|
|
32 |
done
|
|
33 |
|
|
34 |
lemma conditionalize:
|
|
35 |
assumes "finite A"
|
|
36 |
shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else 1)"
|
|
37 |
using assms
|
|
38 |
apply (simp add: expand_set)
|
|
39 |
apply (rule F.same_carrierI [of A])
|
|
40 |
apply auto
|
|
41 |
done
|
|
42 |
|
|
43 |
lemma neutral [simp]:
|
|
44 |
"G (\<lambda>a. 1) = 1"
|
|
45 |
by (simp add: expand_set)
|
|
46 |
|
|
47 |
lemma update [simp]:
|
|
48 |
assumes "finite {a. g a \<noteq> 1}"
|
|
49 |
assumes "g a = 1"
|
|
50 |
shows "G (g(a := b)) = b * G g"
|
|
51 |
proof (cases "b = 1")
|
|
52 |
case True with `g a = 1` show ?thesis
|
|
53 |
by (simp add: expand_set) (rule F.cong, auto)
|
|
54 |
next
|
|
55 |
case False
|
|
56 |
moreover have "{a'. a' \<noteq> a \<longrightarrow> g a' \<noteq> 1} = insert a {a. g a \<noteq> 1}"
|
|
57 |
by auto
|
|
58 |
moreover from `g a = 1` have "a \<notin> {a. g a \<noteq> 1}"
|
|
59 |
by simp
|
|
60 |
moreover have "F.F (\<lambda>a'. if a' = a then b else g a') {a. g a \<noteq> 1} = F.F g {a. g a \<noteq> 1}"
|
|
61 |
by (rule F.cong) (auto simp add: `g a = 1`)
|
|
62 |
ultimately show ?thesis using `finite {a. g a \<noteq> 1}` by (simp add: expand_set)
|
|
63 |
qed
|
|
64 |
|
|
65 |
lemma infinite [simp]:
|
|
66 |
"\<not> finite {a. g a \<noteq> 1} \<Longrightarrow> G g = 1"
|
|
67 |
by (simp add: expand_set)
|
|
68 |
|
|
69 |
lemma cong:
|
|
70 |
assumes "\<And>a. g a = h a"
|
|
71 |
shows "G g = G h"
|
|
72 |
using assms by (simp add: expand_set)
|
|
73 |
|
|
74 |
lemma strong_cong [cong]:
|
|
75 |
assumes "\<And>a. g a = h a"
|
|
76 |
shows "G (\<lambda>a. g a) = G (\<lambda>a. h a)"
|
|
77 |
using assms by (fact cong)
|
|
78 |
|
|
79 |
lemma not_neutral_obtains_not_neutral:
|
|
80 |
assumes "G g \<noteq> 1"
|
|
81 |
obtains a where "g a \<noteq> 1"
|
|
82 |
using assms by (auto elim: F.not_neutral_contains_not_neutral simp add: expand_set)
|
|
83 |
|
|
84 |
lemma reindex_cong:
|
|
85 |
assumes "bij l"
|
|
86 |
assumes "g \<circ> l = h"
|
|
87 |
shows "G g = G h"
|
|
88 |
proof -
|
|
89 |
from assms have unfold: "h = g \<circ> l" by simp
|
|
90 |
from `bij l` have "inj l" by (rule bij_is_inj)
|
|
91 |
then have "inj_on l {a. h a \<noteq> 1}" by (rule subset_inj_on) simp
|
|
92 |
moreover from `bij l` have "{a. g a \<noteq> 1} = l ` {a. h a \<noteq> 1}"
|
|
93 |
by (auto simp add: image_Collect unfold elim: bij_pointE)
|
|
94 |
moreover have "\<And>x. x \<in> {a. h a \<noteq> 1} \<Longrightarrow> g (l x) = h x"
|
|
95 |
by (simp add: unfold)
|
|
96 |
ultimately have "F.F g {a. g a \<noteq> 1} = F.F h {a. h a \<noteq> 1}"
|
|
97 |
by (rule F.reindex_cong)
|
|
98 |
then show ?thesis by (simp add: expand_set)
|
|
99 |
qed
|
|
100 |
|
|
101 |
lemma distrib:
|
|
102 |
assumes "finite {a. g a \<noteq> 1}" and "finite {a. h a \<noteq> 1}"
|
|
103 |
shows "G (\<lambda>a. g a * h a) = G g * G h"
|
|
104 |
proof -
|
|
105 |
from assms have "finite ({a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1})" by simp
|
|
106 |
moreover have "{a. g a * h a \<noteq> 1} \<subseteq> {a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"
|
|
107 |
by auto (drule sym, simp)
|
|
108 |
ultimately show ?thesis
|
|
109 |
using assms
|
|
110 |
by (simp add: expand_superset [of "{a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"] F.distrib)
|
|
111 |
qed
|
|
112 |
|
|
113 |
lemma commute:
|
|
114 |
assumes "finite C"
|
|
115 |
assumes subset: "{a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
|
|
116 |
shows "G (\<lambda>a. G (g a)) = G (\<lambda>b. G (\<lambda>a. g a b))"
|
|
117 |
proof -
|
|
118 |
from `finite C` subset
|
|
119 |
have "finite ({a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1})"
|
|
120 |
by (rule rev_finite_subset)
|
|
121 |
then have fins:
|
|
122 |
"finite {b. \<exists>a. g a b \<noteq> 1}" "finite {a. \<exists>b. g a b \<noteq> 1}"
|
|
123 |
by (auto simp add: finite_cartesian_product_iff)
|
|
124 |
have subsets: "\<And>a. {b. g a b \<noteq> 1} \<subseteq> {b. \<exists>a. g a b \<noteq> 1}"
|
|
125 |
"\<And>b. {a. g a b \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
|
|
126 |
"{a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1} \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
|
|
127 |
"{a. F.F (\<lambda>aa. g aa a) {a. \<exists>b. g a b \<noteq> 1} \<noteq> 1} \<subseteq> {b. \<exists>a. g a b \<noteq> 1}"
|
|
128 |
by (auto elim: F.not_neutral_contains_not_neutral)
|
|
129 |
from F.commute have
|
|
130 |
"F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1} =
|
|
131 |
F.F (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> 1}) {b. \<exists>a. g a b \<noteq> 1}" .
|
|
132 |
with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) =
|
|
133 |
G (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> 1})"
|
|
134 |
by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
|
|
135 |
expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
|
|
136 |
with subsets fins show ?thesis
|
|
137 |
by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
|
|
138 |
expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
|
|
139 |
qed
|
|
140 |
|
|
141 |
lemma cartesian_product:
|
|
142 |
assumes "finite C"
|
|
143 |
assumes subset: "{a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
|
|
144 |
shows "G (\<lambda>a. G (g a)) = G (\<lambda>(a, b). g a b)"
|
|
145 |
proof -
|
|
146 |
from subset `finite C` have fin_prod: "finite (?A \<times> ?B)"
|
|
147 |
by (rule finite_subset)
|
|
148 |
from fin_prod have "finite ?A" and "finite ?B"
|
|
149 |
by (auto simp add: finite_cartesian_product_iff)
|
|
150 |
have *: "G (\<lambda>a. G (g a)) =
|
|
151 |
(F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1})"
|
|
152 |
apply (subst expand_superset [of "?B"])
|
|
153 |
apply (rule `finite ?B`)
|
|
154 |
apply auto
|
|
155 |
apply (subst expand_superset [of "?A"])
|
|
156 |
apply (rule `finite ?A`)
|
|
157 |
apply auto
|
|
158 |
apply (erule F.not_neutral_contains_not_neutral)
|
|
159 |
apply auto
|
|
160 |
done
|
|
161 |
have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> ?A \<times> ?B"
|
|
162 |
by auto
|
|
163 |
with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> C"
|
|
164 |
by blast
|
|
165 |
show ?thesis
|
|
166 |
apply (simp add: *)
|
|
167 |
apply (simp add: F.cartesian_product)
|
|
168 |
apply (subst expand_superset [of C])
|
|
169 |
apply (rule `finite C`)
|
|
170 |
apply (simp_all add: **)
|
|
171 |
apply (rule F.same_carrierI [of C])
|
|
172 |
apply (rule `finite C`)
|
|
173 |
apply (simp_all add: subset)
|
|
174 |
apply auto
|
|
175 |
done
|
|
176 |
qed
|
|
177 |
|
|
178 |
lemma cartesian_product2:
|
|
179 |
assumes fin: "finite D"
|
|
180 |
assumes subset: "{(a, b). \<exists>c. g a b c \<noteq> 1} \<times> {c. \<exists>a b. g a b c \<noteq> 1} \<subseteq> D" (is "?AB \<times> ?C \<subseteq> D")
|
|
181 |
shows "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>(a, b, c). g a b c)"
|
|
182 |
proof -
|
|
183 |
have bij: "bij (\<lambda>(a, b, c). ((a, b), c))"
|
|
184 |
by (auto intro!: bijI injI simp add: image_def)
|
|
185 |
have "{p. \<exists>c. g (fst p) (snd p) c \<noteq> 1} \<times> {c. \<exists>p. g (fst p) (snd p) c \<noteq> 1} \<subseteq> D"
|
|
186 |
by auto (insert subset, auto)
|
|
187 |
with fin have "G (\<lambda>p. G (g (fst p) (snd p))) = G (\<lambda>(p, c). g (fst p) (snd p) c)"
|
|
188 |
by (rule cartesian_product)
|
|
189 |
then have "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>((a, b), c). g a b c)"
|
|
190 |
by (auto simp add: split_def)
|
|
191 |
also have "G (\<lambda>((a, b), c). g a b c) = G (\<lambda>(a, b, c). g a b c)"
|
|
192 |
using bij by (rule reindex_cong [of "\<lambda>(a, b, c). ((a, b), c)"]) (simp add: fun_eq_iff)
|
|
193 |
finally show ?thesis .
|
|
194 |
qed
|
|
195 |
|
|
196 |
lemma delta [simp]:
|
|
197 |
"G (\<lambda>b. if b = a then g b else 1) = g a"
|
|
198 |
proof -
|
|
199 |
have "{b. (if b = a then g b else 1) \<noteq> 1} \<subseteq> {a}" by auto
|
|
200 |
then show ?thesis by (simp add: expand_superset [of "{a}"])
|
|
201 |
qed
|
|
202 |
|
|
203 |
lemma delta' [simp]:
|
|
204 |
"G (\<lambda>b. if a = b then g b else 1) = g a"
|
|
205 |
proof -
|
|
206 |
have "(\<lambda>b. if a = b then g b else 1) = (\<lambda>b. if b = a then g b else 1)"
|
|
207 |
by (simp add: fun_eq_iff)
|
|
208 |
then have "G (\<lambda>b. if a = b then g b else 1) = G (\<lambda>b. if b = a then g b else 1)"
|
|
209 |
by (simp cong del: strong_cong)
|
|
210 |
then show ?thesis by simp
|
|
211 |
qed
|
|
212 |
|
|
213 |
end
|
|
214 |
|
|
215 |
notation times (infixl "*" 70)
|
|
216 |
notation Groups.one ("1")
|
|
217 |
|
|
218 |
|
|
219 |
subsection \<open>Concrete sum\<close>
|
|
220 |
|
|
221 |
context comm_monoid_add
|
|
222 |
begin
|
|
223 |
|
|
224 |
definition Sum_any :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
|
|
225 |
where
|
|
226 |
"Sum_any = comm_monoid_fun.G plus 0"
|
|
227 |
|
|
228 |
permanent_interpretation Sum_any!: comm_monoid_fun plus 0
|
|
229 |
where
|
|
230 |
"comm_monoid_fun.G plus 0 = Sum_any" and
|
|
231 |
"comm_monoid_set.F plus 0 = setsum"
|
|
232 |
proof -
|
|
233 |
show "comm_monoid_fun plus 0" ..
|
|
234 |
then interpret Sum_any!: comm_monoid_fun plus 0 .
|
|
235 |
from Sum_any_def show "comm_monoid_fun.G plus 0 = Sum_any" by rule
|
|
236 |
from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
|
|
237 |
qed
|
|
238 |
|
|
239 |
end
|
|
240 |
|
|
241 |
syntax
|
|
242 |
"_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _. _)" [0, 10] 10)
|
|
243 |
syntax (xsymbols)
|
|
244 |
"_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_. _)" [0, 10] 10)
|
|
245 |
syntax (HTML output)
|
|
246 |
"_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_. _)" [0, 10] 10)
|
|
247 |
|
|
248 |
translations
|
|
249 |
"\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
|
|
250 |
|
|
251 |
lemma Sum_any_left_distrib:
|
|
252 |
fixes r :: "'a :: semiring_0"
|
|
253 |
assumes "finite {a. g a \<noteq> 0}"
|
|
254 |
shows "Sum_any g * r = (\<Sum>n. g n * r)"
|
|
255 |
proof -
|
|
256 |
note assms
|
|
257 |
moreover have "{a. g a * r \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
|
|
258 |
ultimately show ?thesis
|
|
259 |
by (simp add: setsum_left_distrib Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
|
|
260 |
qed
|
|
261 |
|
|
262 |
lemma Sum_any_right_distrib:
|
|
263 |
fixes r :: "'a :: semiring_0"
|
|
264 |
assumes "finite {a. g a \<noteq> 0}"
|
|
265 |
shows "r * Sum_any g = (\<Sum>n. r * g n)"
|
|
266 |
proof -
|
|
267 |
note assms
|
|
268 |
moreover have "{a. r * g a \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
|
|
269 |
ultimately show ?thesis
|
|
270 |
by (simp add: setsum_right_distrib Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
|
|
271 |
qed
|
|
272 |
|
|
273 |
lemma Sum_any_product:
|
|
274 |
fixes f g :: "'b \<Rightarrow> 'a::semiring_0"
|
|
275 |
assumes "finite {a. f a \<noteq> 0}" and "finite {b. g b \<noteq> 0}"
|
|
276 |
shows "Sum_any f * Sum_any g = (\<Sum>a. \<Sum>b. f a * g b)"
|
|
277 |
proof -
|
|
278 |
have subset_f: "{a. (\<Sum>b. f a * g b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}"
|
|
279 |
by rule (simp, rule, auto)
|
|
280 |
moreover have subset_g: "\<And>a. {b. f a * g b \<noteq> 0} \<subseteq> {b. g b \<noteq> 0}"
|
|
281 |
by rule (simp, rule, auto)
|
|
282 |
ultimately show ?thesis using assms
|
|
283 |
by (auto simp add: Sum_any.expand_set [of f] Sum_any.expand_set [of g]
|
|
284 |
Sum_any.expand_superset [of "{a. f a \<noteq> 0}"] Sum_any.expand_superset [of "{b. g b \<noteq> 0}"]
|
|
285 |
setsum_product)
|
|
286 |
qed
|
|
287 |
|
58437
|
288 |
lemma Sum_any_eq_zero_iff [simp]:
|
|
289 |
fixes f :: "'a \<Rightarrow> nat"
|
|
290 |
assumes "finite {a. f a \<noteq> 0}"
|
|
291 |
shows "Sum_any f = 0 \<longleftrightarrow> f = (\<lambda>_. 0)"
|
|
292 |
using assms by (simp add: Sum_any.expand_set fun_eq_iff)
|
|
293 |
|
58197
|
294 |
|
|
295 |
subsection \<open>Concrete product\<close>
|
|
296 |
|
|
297 |
context comm_monoid_mult
|
|
298 |
begin
|
|
299 |
|
|
300 |
definition Prod_any :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
|
|
301 |
where
|
|
302 |
"Prod_any = comm_monoid_fun.G times 1"
|
|
303 |
|
|
304 |
permanent_interpretation Prod_any!: comm_monoid_fun times 1
|
|
305 |
where
|
|
306 |
"comm_monoid_fun.G times 1 = Prod_any" and
|
|
307 |
"comm_monoid_set.F times 1 = setprod"
|
|
308 |
proof -
|
|
309 |
show "comm_monoid_fun times 1" ..
|
|
310 |
then interpret Prod_any!: comm_monoid_fun times 1 .
|
|
311 |
from Prod_any_def show "comm_monoid_fun.G times 1 = Prod_any" by rule
|
|
312 |
from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
|
|
313 |
qed
|
|
314 |
|
|
315 |
end
|
|
316 |
|
|
317 |
syntax
|
|
318 |
"_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3PROD _. _)" [0, 10] 10)
|
|
319 |
syntax (xsymbols)
|
|
320 |
"_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3\<Prod>_. _)" [0, 10] 10)
|
|
321 |
syntax (HTML output)
|
|
322 |
"_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3\<Prod>_. _)" [0, 10] 10)
|
|
323 |
|
|
324 |
translations
|
|
325 |
"\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
|
|
326 |
|
|
327 |
lemma Prod_any_zero:
|
|
328 |
fixes f :: "'b \<Rightarrow> 'a :: comm_semiring_1"
|
|
329 |
assumes "finite {a. f a \<noteq> 1}"
|
|
330 |
assumes "f a = 0"
|
|
331 |
shows "(\<Prod>a. f a) = 0"
|
|
332 |
proof -
|
|
333 |
from `f a = 0` have "f a \<noteq> 1" by simp
|
|
334 |
with `f a = 0` have "\<exists>a. f a \<noteq> 1 \<and> f a = 0" by blast
|
|
335 |
with `finite {a. f a \<noteq> 1}` show ?thesis
|
|
336 |
by (simp add: Prod_any.expand_set setprod_zero)
|
|
337 |
qed
|
|
338 |
|
|
339 |
lemma Prod_any_not_zero:
|
|
340 |
fixes f :: "'b \<Rightarrow> 'a :: comm_semiring_1"
|
|
341 |
assumes "finite {a. f a \<noteq> 1}"
|
|
342 |
assumes "(\<Prod>a. f a) \<noteq> 0"
|
|
343 |
shows "f a \<noteq> 0"
|
|
344 |
using assms Prod_any_zero [of f] by blast
|
|
345 |
|
58437
|
346 |
lemma power_Sum_any:
|
|
347 |
assumes "finite {a. f a \<noteq> 0}"
|
|
348 |
shows "c ^ (\<Sum>a. f a) = (\<Prod>a. c ^ f a)"
|
|
349 |
proof -
|
|
350 |
have "{a. c ^ f a \<noteq> 1} \<subseteq> {a. f a \<noteq> 0}"
|
|
351 |
by (auto intro: ccontr)
|
|
352 |
with assms show ?thesis
|
|
353 |
by (simp add: Sum_any.expand_set Prod_any.expand_superset power_setsum)
|
|
354 |
qed
|
|
355 |
|
58197
|
356 |
end
|
58437
|
357 |
|