author | Manuel Eberl <eberlm@in.tum.de> |
Tue, 19 Jan 2016 11:19:25 +0100 | |
changeset 62201 | eca7b38c8ee5 |
parent 61955 | e96292f32c3c |
child 63099 | af0e964aad7b |
permissions | -rw-r--r-- |
58101 | 1 |
(* Author: Tobias Nipkow, TU Muenchen *) |
2 |
||
60758 | 3 |
section \<open>Sum and product over lists\<close> |
58101 | 4 |
|
5 |
theory Groups_List |
|
6 |
imports List |
|
7 |
begin |
|
8 |
||
58320 | 9 |
no_notation times (infixl "*" 70) |
10 |
no_notation Groups.one ("1") |
|
11 |
||
12 |
locale monoid_list = monoid |
|
13 |
begin |
|
14 |
||
15 |
definition F :: "'a list \<Rightarrow> 'a" |
|
16 |
where |
|
17 |
eq_foldr [code]: "F xs = foldr f xs 1" |
|
18 |
||
19 |
lemma Nil [simp]: |
|
20 |
"F [] = 1" |
|
21 |
by (simp add: eq_foldr) |
|
22 |
||
23 |
lemma Cons [simp]: |
|
24 |
"F (x # xs) = x * F xs" |
|
25 |
by (simp add: eq_foldr) |
|
26 |
||
27 |
lemma append [simp]: |
|
28 |
"F (xs @ ys) = F xs * F ys" |
|
29 |
by (induct xs) (simp_all add: assoc) |
|
30 |
||
31 |
end |
|
58101 | 32 |
|
58320 | 33 |
locale comm_monoid_list = comm_monoid + monoid_list |
34 |
begin |
|
35 |
||
36 |
lemma rev [simp]: |
|
37 |
"F (rev xs) = F xs" |
|
38 |
by (simp add: eq_foldr foldr_fold fold_rev fun_eq_iff assoc left_commute) |
|
39 |
||
40 |
end |
|
41 |
||
42 |
locale comm_monoid_list_set = list: comm_monoid_list + set: comm_monoid_set |
|
43 |
begin |
|
58101 | 44 |
|
58320 | 45 |
lemma distinct_set_conv_list: |
46 |
"distinct xs \<Longrightarrow> set.F g (set xs) = list.F (map g xs)" |
|
47 |
by (induct xs) simp_all |
|
58101 | 48 |
|
58320 | 49 |
lemma set_conv_list [code]: |
50 |
"set.F g (set xs) = list.F (map g (remdups xs))" |
|
51 |
by (simp add: distinct_set_conv_list [symmetric]) |
|
52 |
||
53 |
end |
|
54 |
||
55 |
notation times (infixl "*" 70) |
|
56 |
notation Groups.one ("1") |
|
57 |
||
58 |
||
60758 | 59 |
subsection \<open>List summation\<close> |
58320 | 60 |
|
61 |
context monoid_add |
|
62 |
begin |
|
63 |
||
61605 | 64 |
sublocale listsum: monoid_list plus 0 |
61776 | 65 |
defines |
66 |
listsum = listsum.F .. |
|
58320 | 67 |
|
68 |
end |
|
69 |
||
70 |
context comm_monoid_add |
|
71 |
begin |
|
72 |
||
61605 | 73 |
sublocale listsum: comm_monoid_list plus 0 |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset
|
74 |
rewrites |
58320 | 75 |
"monoid_list.F plus 0 = listsum" |
76 |
proof - |
|
77 |
show "comm_monoid_list plus 0" .. |
|
61605 | 78 |
then interpret listsum: comm_monoid_list plus 0 . |
61776 | 79 |
from listsum_def show "monoid_list.F plus 0 = listsum" by simp |
58101 | 80 |
qed |
81 |
||
61605 | 82 |
sublocale setsum: comm_monoid_list_set plus 0 |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset
|
83 |
rewrites |
58320 | 84 |
"monoid_list.F plus 0 = listsum" |
85 |
and "comm_monoid_set.F plus 0 = setsum" |
|
86 |
proof - |
|
87 |
show "comm_monoid_list_set plus 0" .. |
|
61605 | 88 |
then interpret setsum: comm_monoid_list_set plus 0 . |
61776 | 89 |
from listsum_def show "monoid_list.F plus 0 = listsum" by simp |
90 |
from setsum_def show "comm_monoid_set.F plus 0 = setsum" by (auto intro: sym) |
|
58320 | 91 |
qed |
92 |
||
93 |
end |
|
94 |
||
60758 | 95 |
text \<open>Some syntactic sugar for summing a function over a list:\<close> |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
96 |
syntax (ASCII) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
97 |
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) |
58101 | 98 |
syntax |
99 |
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) |
|
61799 | 100 |
translations \<comment> \<open>Beware of argument permutation!\<close> |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
101 |
"\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (\<lambda>x. b) xs)" |
58101 | 102 |
|
60758 | 103 |
text \<open>TODO duplicates\<close> |
58320 | 104 |
lemmas listsum_simps = listsum.Nil listsum.Cons |
105 |
lemmas listsum_append = listsum.append |
|
106 |
lemmas listsum_rev = listsum.rev |
|
107 |
||
108 |
lemma (in monoid_add) fold_plus_listsum_rev: |
|
109 |
"fold plus xs = plus (listsum (rev xs))" |
|
110 |
proof |
|
111 |
fix x |
|
112 |
have "fold plus xs x = listsum (rev xs @ [x])" |
|
113 |
by (simp add: foldr_conv_fold listsum.eq_foldr) |
|
114 |
also have "\<dots> = listsum (rev xs) + x" |
|
115 |
by simp |
|
116 |
finally show "fold plus xs x = listsum (rev xs) + x" |
|
117 |
. |
|
118 |
qed |
|
119 |
||
58101 | 120 |
lemma (in comm_monoid_add) listsum_map_remove1: |
121 |
"x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))" |
|
122 |
by (induct xs) (auto simp add: ac_simps) |
|
123 |
||
124 |
lemma (in monoid_add) size_list_conv_listsum: |
|
125 |
"size_list f xs = listsum (map f xs) + size xs" |
|
126 |
by (induct xs) auto |
|
127 |
||
128 |
lemma (in monoid_add) length_concat: |
|
129 |
"length (concat xss) = listsum (map length xss)" |
|
130 |
by (induct xss) simp_all |
|
131 |
||
132 |
lemma (in monoid_add) length_product_lists: |
|
133 |
"length (product_lists xss) = foldr op * (map length xss) 1" |
|
134 |
proof (induct xss) |
|
135 |
case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def) |
|
136 |
qed simp |
|
137 |
||
138 |
lemma (in monoid_add) listsum_map_filter: |
|
139 |
assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0" |
|
140 |
shows "listsum (map f (filter P xs)) = listsum (map f xs)" |
|
141 |
using assms by (induct xs) auto |
|
142 |
||
143 |
lemma (in comm_monoid_add) distinct_listsum_conv_Setsum: |
|
144 |
"distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)" |
|
145 |
by (induct xs) simp_all |
|
146 |
||
58995 | 147 |
lemma listsum_upt[simp]: |
148 |
"m \<le> n \<Longrightarrow> listsum [m..<n] = \<Sum> {m..<n}" |
|
149 |
by(simp add: distinct_listsum_conv_Setsum) |
|
150 |
||
58101 | 151 |
lemma listsum_eq_0_nat_iff_nat [simp]: |
152 |
"listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)" |
|
153 |
by (induct ns) simp_all |
|
154 |
||
155 |
lemma member_le_listsum_nat: |
|
156 |
"(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns" |
|
157 |
by (induct ns) auto |
|
158 |
||
159 |
lemma elem_le_listsum_nat: |
|
160 |
"k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)" |
|
161 |
by (rule member_le_listsum_nat) simp |
|
162 |
||
163 |
lemma listsum_update_nat: |
|
164 |
"k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k" |
|
165 |
apply(induct ns arbitrary:k) |
|
166 |
apply (auto split:nat.split) |
|
167 |
apply(drule elem_le_listsum_nat) |
|
168 |
apply arith |
|
169 |
done |
|
170 |
||
171 |
lemma (in monoid_add) listsum_triv: |
|
172 |
"(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" |
|
173 |
by (induct xs) (simp_all add: distrib_right) |
|
174 |
||
175 |
lemma (in monoid_add) listsum_0 [simp]: |
|
176 |
"(\<Sum>x\<leftarrow>xs. 0) = 0" |
|
177 |
by (induct xs) (simp_all add: distrib_right) |
|
178 |
||
61799 | 179 |
text\<open>For non-Abelian groups \<open>xs\<close> needs to be reversed on one side:\<close> |
58101 | 180 |
lemma (in ab_group_add) uminus_listsum_map: |
181 |
"- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)" |
|
182 |
by (induct xs) simp_all |
|
183 |
||
184 |
lemma (in comm_monoid_add) listsum_addf: |
|
185 |
"(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)" |
|
186 |
by (induct xs) (simp_all add: algebra_simps) |
|
187 |
||
188 |
lemma (in ab_group_add) listsum_subtractf: |
|
189 |
"(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)" |
|
190 |
by (induct xs) (simp_all add: algebra_simps) |
|
191 |
||
192 |
lemma (in semiring_0) listsum_const_mult: |
|
193 |
"(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)" |
|
194 |
by (induct xs) (simp_all add: algebra_simps) |
|
195 |
||
196 |
lemma (in semiring_0) listsum_mult_const: |
|
197 |
"(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c" |
|
198 |
by (induct xs) (simp_all add: algebra_simps) |
|
199 |
||
200 |
lemma (in ordered_ab_group_add_abs) listsum_abs: |
|
201 |
"\<bar>listsum xs\<bar> \<le> listsum (map abs xs)" |
|
202 |
by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq]) |
|
203 |
||
204 |
lemma listsum_mono: |
|
205 |
fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}" |
|
206 |
shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)" |
|
207 |
by (induct xs) (simp, simp add: add_mono) |
|
208 |
||
209 |
lemma (in monoid_add) listsum_distinct_conv_setsum_set: |
|
210 |
"distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)" |
|
211 |
by (induct xs) simp_all |
|
212 |
||
213 |
lemma (in monoid_add) interv_listsum_conv_setsum_set_nat: |
|
214 |
"listsum (map f [m..<n]) = setsum f (set [m..<n])" |
|
215 |
by (simp add: listsum_distinct_conv_setsum_set) |
|
216 |
||
217 |
lemma (in monoid_add) interv_listsum_conv_setsum_set_int: |
|
218 |
"listsum (map f [k..l]) = setsum f (set [k..l])" |
|
219 |
by (simp add: listsum_distinct_conv_setsum_set) |
|
220 |
||
60758 | 221 |
text \<open>General equivalence between @{const listsum} and @{const setsum}\<close> |
58101 | 222 |
lemma (in monoid_add) listsum_setsum_nth: |
223 |
"listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)" |
|
224 |
using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth) |
|
225 |
||
59728 | 226 |
lemma listsum_map_eq_setsum_count: |
60541 | 227 |
"listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) (set xs)" |
59728 | 228 |
proof(induction xs) |
229 |
case (Cons x xs) |
|
230 |
show ?case (is "?l = ?r") |
|
231 |
proof cases |
|
232 |
assume "x \<in> set xs" |
|
60541 | 233 |
have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH) |
60758 | 234 |
also have "set xs = insert x (set xs - {x})" using \<open>x \<in> set xs\<close>by blast |
60541 | 235 |
also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). count_list xs x * f x) = ?r" |
59728 | 236 |
by (simp add: setsum.insert_remove eq_commute) |
237 |
finally show ?thesis . |
|
238 |
next |
|
239 |
assume "x \<notin> set xs" |
|
240 |
hence "\<And>xa. xa \<in> set xs \<Longrightarrow> x \<noteq> xa" by blast |
|
60758 | 241 |
thus ?thesis by (simp add: Cons.IH \<open>x \<notin> set xs\<close>) |
59728 | 242 |
qed |
243 |
qed simp |
|
244 |
||
245 |
lemma listsum_map_eq_setsum_count2: |
|
246 |
assumes "set xs \<subseteq> X" "finite X" |
|
60541 | 247 |
shows "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X" |
59728 | 248 |
proof- |
60541 | 249 |
let ?F = "\<lambda>x. count_list xs x * f x" |
59728 | 250 |
have "setsum ?F X = setsum ?F (set xs \<union> (X - set xs))" |
251 |
using Un_absorb1[OF assms(1)] by(simp) |
|
252 |
also have "\<dots> = setsum ?F (set xs)" |
|
253 |
using assms(2) |
|
254 |
by(simp add: setsum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel) |
|
255 |
finally show ?thesis by(simp add:listsum_map_eq_setsum_count) |
|
256 |
qed |
|
257 |
||
58101 | 258 |
|
60758 | 259 |
subsection \<open>Further facts about @{const List.n_lists}\<close> |
58101 | 260 |
|
261 |
lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n" |
|
262 |
by (induct n) (auto simp add: comp_def length_concat listsum_triv) |
|
263 |
||
264 |
lemma distinct_n_lists: |
|
265 |
assumes "distinct xs" |
|
266 |
shows "distinct (List.n_lists n xs)" |
|
267 |
proof (rule card_distinct) |
|
268 |
from assms have card_length: "card (set xs) = length xs" by (rule distinct_card) |
|
269 |
have "card (set (List.n_lists n xs)) = card (set xs) ^ n" |
|
270 |
proof (induct n) |
|
271 |
case 0 then show ?case by simp |
|
272 |
next |
|
273 |
case (Suc n) |
|
274 |
moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs) |
|
275 |
= (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))" |
|
276 |
by (rule card_UN_disjoint) auto |
|
277 |
moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)" |
|
278 |
by (rule card_image) (simp add: inj_on_def) |
|
279 |
ultimately show ?case by auto |
|
280 |
qed |
|
281 |
also have "\<dots> = length xs ^ n" by (simp add: card_length) |
|
282 |
finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)" |
|
283 |
by (simp add: length_n_lists) |
|
284 |
qed |
|
285 |
||
286 |
||
60758 | 287 |
subsection \<open>Tools setup\<close> |
58101 | 288 |
|
58320 | 289 |
lemmas setsum_code = setsum.set_conv_list |
290 |
||
58101 | 291 |
lemma setsum_set_upto_conv_listsum_int [code_unfold]: |
292 |
"setsum f (set [i..j::int]) = listsum (map f [i..j])" |
|
293 |
by (simp add: interv_listsum_conv_setsum_set_int) |
|
294 |
||
295 |
lemma setsum_set_upt_conv_listsum_nat [code_unfold]: |
|
296 |
"setsum f (set [m..<n]) = listsum (map f [m..<n])" |
|
297 |
by (simp add: interv_listsum_conv_setsum_set_nat) |
|
298 |
||
299 |
context |
|
300 |
begin |
|
301 |
||
302 |
interpretation lifting_syntax . |
|
303 |
||
304 |
lemma listsum_transfer[transfer_rule]: |
|
305 |
assumes [transfer_rule]: "A 0 0" |
|
306 |
assumes [transfer_rule]: "(A ===> A ===> A) op + op +" |
|
307 |
shows "(list_all2 A ===> A) listsum listsum" |
|
58320 | 308 |
unfolding listsum.eq_foldr [abs_def] |
58101 | 309 |
by transfer_prover |
310 |
||
311 |
end |
|
312 |
||
58368 | 313 |
|
60758 | 314 |
subsection \<open>List product\<close> |
58368 | 315 |
|
316 |
context monoid_mult |
|
317 |
begin |
|
318 |
||
61605 | 319 |
sublocale listprod: monoid_list times 1 |
61776 | 320 |
defines |
321 |
listprod = listprod.F .. |
|
58368 | 322 |
|
58320 | 323 |
end |
58368 | 324 |
|
325 |
context comm_monoid_mult |
|
326 |
begin |
|
327 |
||
61605 | 328 |
sublocale listprod: comm_monoid_list times 1 |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset
|
329 |
rewrites |
58368 | 330 |
"monoid_list.F times 1 = listprod" |
331 |
proof - |
|
332 |
show "comm_monoid_list times 1" .. |
|
61605 | 333 |
then interpret listprod: comm_monoid_list times 1 . |
61776 | 334 |
from listprod_def show "monoid_list.F times 1 = listprod" by simp |
58368 | 335 |
qed |
336 |
||
61605 | 337 |
sublocale setprod: comm_monoid_list_set times 1 |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset
|
338 |
rewrites |
58368 | 339 |
"monoid_list.F times 1 = listprod" |
340 |
and "comm_monoid_set.F times 1 = setprod" |
|
341 |
proof - |
|
342 |
show "comm_monoid_list_set times 1" .. |
|
61605 | 343 |
then interpret setprod: comm_monoid_list_set times 1 . |
61776 | 344 |
from listprod_def show "monoid_list.F times 1 = listprod" by simp |
345 |
from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym) |
|
58368 | 346 |
qed |
347 |
||
348 |
end |
|
349 |
||
60758 | 350 |
text \<open>Some syntactic sugar:\<close> |
58368 | 351 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
352 |
syntax (ASCII) |
58368 | 353 |
"_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10) |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
354 |
syntax |
58368 | 355 |
"_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10) |
61799 | 356 |
translations \<comment> \<open>Beware of argument permutation!\<close> |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
357 |
"\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST listprod (CONST map (\<lambda>x. b) xs)" |
58368 | 358 |
|
359 |
end |