author | wenzelm |
Mon, 28 Dec 2015 01:26:34 +0100 | |
changeset 61944 | 5d06ecfdb472 |
parent 61799 | 4cf66f21b764 |
child 61955 | e96292f32c3c |
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> |
58101 | 96 |
|
97 |
syntax |
|
98 |
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) |
|
99 |
syntax (xsymbols) |
|
100 |
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) |
|
101 |
||
61799 | 102 |
translations \<comment> \<open>Beware of argument permutation!\<close> |
58101 | 103 |
"SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)" |
104 |
"\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)" |
|
105 |
||
60758 | 106 |
text \<open>TODO duplicates\<close> |
58320 | 107 |
lemmas listsum_simps = listsum.Nil listsum.Cons |
108 |
lemmas listsum_append = listsum.append |
|
109 |
lemmas listsum_rev = listsum.rev |
|
110 |
||
111 |
lemma (in monoid_add) fold_plus_listsum_rev: |
|
112 |
"fold plus xs = plus (listsum (rev xs))" |
|
113 |
proof |
|
114 |
fix x |
|
115 |
have "fold plus xs x = listsum (rev xs @ [x])" |
|
116 |
by (simp add: foldr_conv_fold listsum.eq_foldr) |
|
117 |
also have "\<dots> = listsum (rev xs) + x" |
|
118 |
by simp |
|
119 |
finally show "fold plus xs x = listsum (rev xs) + x" |
|
120 |
. |
|
121 |
qed |
|
122 |
||
58101 | 123 |
lemma (in comm_monoid_add) listsum_map_remove1: |
124 |
"x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))" |
|
125 |
by (induct xs) (auto simp add: ac_simps) |
|
126 |
||
127 |
lemma (in monoid_add) size_list_conv_listsum: |
|
128 |
"size_list f xs = listsum (map f xs) + size xs" |
|
129 |
by (induct xs) auto |
|
130 |
||
131 |
lemma (in monoid_add) length_concat: |
|
132 |
"length (concat xss) = listsum (map length xss)" |
|
133 |
by (induct xss) simp_all |
|
134 |
||
135 |
lemma (in monoid_add) length_product_lists: |
|
136 |
"length (product_lists xss) = foldr op * (map length xss) 1" |
|
137 |
proof (induct xss) |
|
138 |
case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def) |
|
139 |
qed simp |
|
140 |
||
141 |
lemma (in monoid_add) listsum_map_filter: |
|
142 |
assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0" |
|
143 |
shows "listsum (map f (filter P xs)) = listsum (map f xs)" |
|
144 |
using assms by (induct xs) auto |
|
145 |
||
146 |
lemma (in comm_monoid_add) distinct_listsum_conv_Setsum: |
|
147 |
"distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)" |
|
148 |
by (induct xs) simp_all |
|
149 |
||
58995 | 150 |
lemma listsum_upt[simp]: |
151 |
"m \<le> n \<Longrightarrow> listsum [m..<n] = \<Sum> {m..<n}" |
|
152 |
by(simp add: distinct_listsum_conv_Setsum) |
|
153 |
||
58101 | 154 |
lemma listsum_eq_0_nat_iff_nat [simp]: |
155 |
"listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)" |
|
156 |
by (induct ns) simp_all |
|
157 |
||
158 |
lemma member_le_listsum_nat: |
|
159 |
"(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns" |
|
160 |
by (induct ns) auto |
|
161 |
||
162 |
lemma elem_le_listsum_nat: |
|
163 |
"k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)" |
|
164 |
by (rule member_le_listsum_nat) simp |
|
165 |
||
166 |
lemma listsum_update_nat: |
|
167 |
"k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k" |
|
168 |
apply(induct ns arbitrary:k) |
|
169 |
apply (auto split:nat.split) |
|
170 |
apply(drule elem_le_listsum_nat) |
|
171 |
apply arith |
|
172 |
done |
|
173 |
||
174 |
lemma (in monoid_add) listsum_triv: |
|
175 |
"(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" |
|
176 |
by (induct xs) (simp_all add: distrib_right) |
|
177 |
||
178 |
lemma (in monoid_add) listsum_0 [simp]: |
|
179 |
"(\<Sum>x\<leftarrow>xs. 0) = 0" |
|
180 |
by (induct xs) (simp_all add: distrib_right) |
|
181 |
||
61799 | 182 |
text\<open>For non-Abelian groups \<open>xs\<close> needs to be reversed on one side:\<close> |
58101 | 183 |
lemma (in ab_group_add) uminus_listsum_map: |
184 |
"- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)" |
|
185 |
by (induct xs) simp_all |
|
186 |
||
187 |
lemma (in comm_monoid_add) listsum_addf: |
|
188 |
"(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)" |
|
189 |
by (induct xs) (simp_all add: algebra_simps) |
|
190 |
||
191 |
lemma (in ab_group_add) listsum_subtractf: |
|
192 |
"(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)" |
|
193 |
by (induct xs) (simp_all add: algebra_simps) |
|
194 |
||
195 |
lemma (in semiring_0) listsum_const_mult: |
|
196 |
"(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)" |
|
197 |
by (induct xs) (simp_all add: algebra_simps) |
|
198 |
||
199 |
lemma (in semiring_0) listsum_mult_const: |
|
200 |
"(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c" |
|
201 |
by (induct xs) (simp_all add: algebra_simps) |
|
202 |
||
203 |
lemma (in ordered_ab_group_add_abs) listsum_abs: |
|
204 |
"\<bar>listsum xs\<bar> \<le> listsum (map abs xs)" |
|
205 |
by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq]) |
|
206 |
||
207 |
lemma listsum_mono: |
|
208 |
fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}" |
|
209 |
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)" |
|
210 |
by (induct xs) (simp, simp add: add_mono) |
|
211 |
||
212 |
lemma (in monoid_add) listsum_distinct_conv_setsum_set: |
|
213 |
"distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)" |
|
214 |
by (induct xs) simp_all |
|
215 |
||
216 |
lemma (in monoid_add) interv_listsum_conv_setsum_set_nat: |
|
217 |
"listsum (map f [m..<n]) = setsum f (set [m..<n])" |
|
218 |
by (simp add: listsum_distinct_conv_setsum_set) |
|
219 |
||
220 |
lemma (in monoid_add) interv_listsum_conv_setsum_set_int: |
|
221 |
"listsum (map f [k..l]) = setsum f (set [k..l])" |
|
222 |
by (simp add: listsum_distinct_conv_setsum_set) |
|
223 |
||
60758 | 224 |
text \<open>General equivalence between @{const listsum} and @{const setsum}\<close> |
58101 | 225 |
lemma (in monoid_add) listsum_setsum_nth: |
226 |
"listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)" |
|
227 |
using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth) |
|
228 |
||
59728 | 229 |
lemma listsum_map_eq_setsum_count: |
60541 | 230 |
"listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) (set xs)" |
59728 | 231 |
proof(induction xs) |
232 |
case (Cons x xs) |
|
233 |
show ?case (is "?l = ?r") |
|
234 |
proof cases |
|
235 |
assume "x \<in> set xs" |
|
60541 | 236 |
have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH) |
60758 | 237 |
also have "set xs = insert x (set xs - {x})" using \<open>x \<in> set xs\<close>by blast |
60541 | 238 |
also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). count_list xs x * f x) = ?r" |
59728 | 239 |
by (simp add: setsum.insert_remove eq_commute) |
240 |
finally show ?thesis . |
|
241 |
next |
|
242 |
assume "x \<notin> set xs" |
|
243 |
hence "\<And>xa. xa \<in> set xs \<Longrightarrow> x \<noteq> xa" by blast |
|
60758 | 244 |
thus ?thesis by (simp add: Cons.IH \<open>x \<notin> set xs\<close>) |
59728 | 245 |
qed |
246 |
qed simp |
|
247 |
||
248 |
lemma listsum_map_eq_setsum_count2: |
|
249 |
assumes "set xs \<subseteq> X" "finite X" |
|
60541 | 250 |
shows "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X" |
59728 | 251 |
proof- |
60541 | 252 |
let ?F = "\<lambda>x. count_list xs x * f x" |
59728 | 253 |
have "setsum ?F X = setsum ?F (set xs \<union> (X - set xs))" |
254 |
using Un_absorb1[OF assms(1)] by(simp) |
|
255 |
also have "\<dots> = setsum ?F (set xs)" |
|
256 |
using assms(2) |
|
257 |
by(simp add: setsum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel) |
|
258 |
finally show ?thesis by(simp add:listsum_map_eq_setsum_count) |
|
259 |
qed |
|
260 |
||
58101 | 261 |
|
60758 | 262 |
subsection \<open>Further facts about @{const List.n_lists}\<close> |
58101 | 263 |
|
264 |
lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n" |
|
265 |
by (induct n) (auto simp add: comp_def length_concat listsum_triv) |
|
266 |
||
267 |
lemma distinct_n_lists: |
|
268 |
assumes "distinct xs" |
|
269 |
shows "distinct (List.n_lists n xs)" |
|
270 |
proof (rule card_distinct) |
|
271 |
from assms have card_length: "card (set xs) = length xs" by (rule distinct_card) |
|
272 |
have "card (set (List.n_lists n xs)) = card (set xs) ^ n" |
|
273 |
proof (induct n) |
|
274 |
case 0 then show ?case by simp |
|
275 |
next |
|
276 |
case (Suc n) |
|
277 |
moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs) |
|
278 |
= (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))" |
|
279 |
by (rule card_UN_disjoint) auto |
|
280 |
moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)" |
|
281 |
by (rule card_image) (simp add: inj_on_def) |
|
282 |
ultimately show ?case by auto |
|
283 |
qed |
|
284 |
also have "\<dots> = length xs ^ n" by (simp add: card_length) |
|
285 |
finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)" |
|
286 |
by (simp add: length_n_lists) |
|
287 |
qed |
|
288 |
||
289 |
||
60758 | 290 |
subsection \<open>Tools setup\<close> |
58101 | 291 |
|
58320 | 292 |
lemmas setsum_code = setsum.set_conv_list |
293 |
||
58101 | 294 |
lemma setsum_set_upto_conv_listsum_int [code_unfold]: |
295 |
"setsum f (set [i..j::int]) = listsum (map f [i..j])" |
|
296 |
by (simp add: interv_listsum_conv_setsum_set_int) |
|
297 |
||
298 |
lemma setsum_set_upt_conv_listsum_nat [code_unfold]: |
|
299 |
"setsum f (set [m..<n]) = listsum (map f [m..<n])" |
|
300 |
by (simp add: interv_listsum_conv_setsum_set_nat) |
|
301 |
||
302 |
context |
|
303 |
begin |
|
304 |
||
305 |
interpretation lifting_syntax . |
|
306 |
||
307 |
lemma listsum_transfer[transfer_rule]: |
|
308 |
assumes [transfer_rule]: "A 0 0" |
|
309 |
assumes [transfer_rule]: "(A ===> A ===> A) op + op +" |
|
310 |
shows "(list_all2 A ===> A) listsum listsum" |
|
58320 | 311 |
unfolding listsum.eq_foldr [abs_def] |
58101 | 312 |
by transfer_prover |
313 |
||
314 |
end |
|
315 |
||
58368 | 316 |
|
60758 | 317 |
subsection \<open>List product\<close> |
58368 | 318 |
|
319 |
context monoid_mult |
|
320 |
begin |
|
321 |
||
61605 | 322 |
sublocale listprod: monoid_list times 1 |
61776 | 323 |
defines |
324 |
listprod = listprod.F .. |
|
58368 | 325 |
|
58320 | 326 |
end |
58368 | 327 |
|
328 |
context comm_monoid_mult |
|
329 |
begin |
|
330 |
||
61605 | 331 |
sublocale listprod: comm_monoid_list times 1 |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset
|
332 |
rewrites |
58368 | 333 |
"monoid_list.F times 1 = listprod" |
334 |
proof - |
|
335 |
show "comm_monoid_list times 1" .. |
|
61605 | 336 |
then interpret listprod: comm_monoid_list times 1 . |
61776 | 337 |
from listprod_def show "monoid_list.F times 1 = listprod" by simp |
58368 | 338 |
qed |
339 |
||
61605 | 340 |
sublocale setprod: comm_monoid_list_set times 1 |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset
|
341 |
rewrites |
58368 | 342 |
"monoid_list.F times 1 = listprod" |
343 |
and "comm_monoid_set.F times 1 = setprod" |
|
344 |
proof - |
|
345 |
show "comm_monoid_list_set times 1" .. |
|
61605 | 346 |
then interpret setprod: comm_monoid_list_set times 1 . |
61776 | 347 |
from listprod_def show "monoid_list.F times 1 = listprod" by simp |
348 |
from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym) |
|
58368 | 349 |
qed |
350 |
||
351 |
end |
|
352 |
||
60758 | 353 |
text \<open>Some syntactic sugar:\<close> |
58368 | 354 |
|
355 |
syntax |
|
356 |
"_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10) |
|
357 |
syntax (xsymbols) |
|
358 |
"_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10) |
|
359 |
||
61799 | 360 |
translations \<comment> \<open>Beware of argument permutation!\<close> |
58368 | 361 |
"PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)" |
362 |
"\<Prod>x\<leftarrow>xs. b" == "CONST listprod (CONST map (%x. b) xs)" |
|
363 |
||
364 |
end |