author | wenzelm |
Wed, 22 Apr 2020 19:22:43 +0200 | |
changeset 71787 | acfe72ff00c2 |
parent 70928 | 273fc913427b |
child 72024 | 9b4135e8bade |
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 |
locale monoid_list = monoid |
10 |
begin |
|
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
11 |
|
58320 | 12 |
definition F :: "'a list \<Rightarrow> 'a" |
13 |
where |
|
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63101
diff
changeset
|
14 |
eq_foldr [code]: "F xs = foldr f xs \<^bold>1" |
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
15 |
|
58320 | 16 |
lemma Nil [simp]: |
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63101
diff
changeset
|
17 |
"F [] = \<^bold>1" |
58320 | 18 |
by (simp add: eq_foldr) |
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
19 |
|
58320 | 20 |
lemma Cons [simp]: |
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63101
diff
changeset
|
21 |
"F (x # xs) = x \<^bold>* F xs" |
58320 | 22 |
by (simp add: eq_foldr) |
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
23 |
|
58320 | 24 |
lemma append [simp]: |
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63101
diff
changeset
|
25 |
"F (xs @ ys) = F xs \<^bold>* F ys" |
58320 | 26 |
by (induct xs) (simp_all add: assoc) |
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
27 |
|
58320 | 28 |
end |
58101 | 29 |
|
58320 | 30 |
locale comm_monoid_list = comm_monoid + monoid_list |
31 |
begin |
|
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
32 |
|
58320 | 33 |
lemma rev [simp]: |
34 |
"F (rev xs) = F xs" |
|
35 |
by (simp add: eq_foldr foldr_fold fold_rev fun_eq_iff assoc left_commute) |
|
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
36 |
|
58320 | 37 |
end |
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
38 |
|
58320 | 39 |
locale comm_monoid_list_set = list: comm_monoid_list + set: comm_monoid_set |
40 |
begin |
|
58101 | 41 |
|
58320 | 42 |
lemma distinct_set_conv_list: |
43 |
"distinct xs \<Longrightarrow> set.F g (set xs) = list.F (map g xs)" |
|
44 |
by (induct xs) simp_all |
|
58101 | 45 |
|
58320 | 46 |
lemma set_conv_list [code]: |
47 |
"set.F g (set xs) = list.F (map g (remdups xs))" |
|
48 |
by (simp add: distinct_set_conv_list [symmetric]) |
|
49 |
||
50 |
end |
|
51 |
||
52 |
||
60758 | 53 |
subsection \<open>List summation\<close> |
58320 | 54 |
|
55 |
context monoid_add |
|
56 |
begin |
|
57 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
58 |
sublocale sum_list: monoid_list plus 0 |
61776 | 59 |
defines |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
60 |
sum_list = sum_list.F .. |
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
61 |
|
58320 | 62 |
end |
63 |
||
64 |
context comm_monoid_add |
|
65 |
begin |
|
66 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
67 |
sublocale sum_list: comm_monoid_list plus 0 |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset
|
68 |
rewrites |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
69 |
"monoid_list.F plus 0 = sum_list" |
58320 | 70 |
proof - |
71 |
show "comm_monoid_list plus 0" .. |
|
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
72 |
then interpret sum_list: comm_monoid_list plus 0 . |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
73 |
from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp |
58101 | 74 |
qed |
75 |
||
64267 | 76 |
sublocale sum: comm_monoid_list_set plus 0 |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset
|
77 |
rewrites |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
78 |
"monoid_list.F plus 0 = sum_list" |
64267 | 79 |
and "comm_monoid_set.F plus 0 = sum" |
58320 | 80 |
proof - |
81 |
show "comm_monoid_list_set plus 0" .. |
|
64267 | 82 |
then interpret sum: comm_monoid_list_set plus 0 . |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
83 |
from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp |
64267 | 84 |
from sum_def show "comm_monoid_set.F plus 0 = sum" by (auto intro: sym) |
58320 | 85 |
qed |
86 |
||
87 |
end |
|
88 |
||
60758 | 89 |
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
|
90 |
syntax (ASCII) |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
91 |
"_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) |
58101 | 92 |
syntax |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
93 |
"_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) |
61799 | 94 |
translations \<comment> \<open>Beware of argument permutation!\<close> |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
95 |
"\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)" |
58101 | 96 |
|
70928 | 97 |
context |
98 |
includes lifting_syntax |
|
99 |
begin |
|
100 |
||
101 |
lemma sum_list_transfer [transfer_rule]: |
|
102 |
"(list_all2 A ===> A) sum_list sum_list" |
|
103 |
if [transfer_rule]: "A 0 0" "(A ===> A ===> A) (+) (+)" |
|
104 |
unfolding sum_list.eq_foldr [abs_def] |
|
105 |
by transfer_prover |
|
106 |
||
107 |
end |
|
108 |
||
60758 | 109 |
text \<open>TODO duplicates\<close> |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
110 |
lemmas sum_list_simps = sum_list.Nil sum_list.Cons |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
111 |
lemmas sum_list_append = sum_list.append |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
112 |
lemmas sum_list_rev = sum_list.rev |
58320 | 113 |
|
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
114 |
lemma (in monoid_add) fold_plus_sum_list_rev: |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
115 |
"fold plus xs = plus (sum_list (rev xs))" |
58320 | 116 |
proof |
117 |
fix x |
|
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
118 |
have "fold plus xs x = sum_list (rev xs @ [x])" |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
119 |
by (simp add: foldr_conv_fold sum_list.eq_foldr) |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
120 |
also have "\<dots> = sum_list (rev xs) + x" |
58320 | 121 |
by simp |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
122 |
finally show "fold plus xs x = sum_list (rev xs) + x" |
58320 | 123 |
. |
124 |
qed |
|
125 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
126 |
lemma (in comm_monoid_add) sum_list_map_remove1: |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
127 |
"x \<in> set xs \<Longrightarrow> sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))" |
58101 | 128 |
by (induct xs) (auto simp add: ac_simps) |
129 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
130 |
lemma (in monoid_add) size_list_conv_sum_list: |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
131 |
"size_list f xs = sum_list (map f xs) + size xs" |
58101 | 132 |
by (induct xs) auto |
133 |
||
134 |
lemma (in monoid_add) length_concat: |
|
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
135 |
"length (concat xss) = sum_list (map length xss)" |
58101 | 136 |
by (induct xss) simp_all |
137 |
||
138 |
lemma (in monoid_add) length_product_lists: |
|
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
67489
diff
changeset
|
139 |
"length (product_lists xss) = foldr (*) (map length xss) 1" |
58101 | 140 |
proof (induct xss) |
141 |
case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def) |
|
142 |
qed simp |
|
143 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
144 |
lemma (in monoid_add) sum_list_map_filter: |
58101 | 145 |
assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0" |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
146 |
shows "sum_list (map f (filter P xs)) = sum_list (map f xs)" |
58101 | 147 |
using assms by (induct xs) auto |
148 |
||
69231 | 149 |
lemma sum_list_filter_le_nat: |
150 |
fixes f :: "'a \<Rightarrow> nat" |
|
151 |
shows "sum_list (map f (filter P xs)) \<le> sum_list (map f xs)" |
|
152 |
by(induction xs; simp) |
|
153 |
||
64267 | 154 |
lemma (in comm_monoid_add) distinct_sum_list_conv_Sum: |
155 |
"distinct xs \<Longrightarrow> sum_list xs = Sum (set xs)" |
|
58101 | 156 |
by (induct xs) simp_all |
157 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
158 |
lemma sum_list_upt[simp]: |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
159 |
"m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}" |
64267 | 160 |
by(simp add: distinct_sum_list_conv_Sum) |
58995 | 161 |
|
66311 | 162 |
context ordered_comm_monoid_add |
163 |
begin |
|
164 |
||
165 |
lemma sum_list_nonneg: "(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> 0 \<le> sum_list xs" |
|
166 |
by (induction xs) auto |
|
167 |
||
168 |
lemma sum_list_nonpos: "(\<And>x. x \<in> set xs \<Longrightarrow> x \<le> 0) \<Longrightarrow> sum_list xs \<le> 0" |
|
169 |
by (induction xs) (auto simp: add_nonpos_nonpos) |
|
58101 | 170 |
|
66311 | 171 |
lemma sum_list_nonneg_eq_0_iff: |
172 |
"(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> sum_list xs = 0 \<longleftrightarrow> (\<forall>x\<in> set xs. x = 0)" |
|
173 |
by (induction xs) (simp_all add: add_nonneg_eq_0_iff sum_list_nonneg) |
|
174 |
||
175 |
end |
|
176 |
||
177 |
context canonically_ordered_monoid_add |
|
178 |
begin |
|
58101 | 179 |
|
66311 | 180 |
lemma sum_list_eq_0_iff [simp]: |
181 |
"sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)" |
|
182 |
by (simp add: sum_list_nonneg_eq_0_iff) |
|
183 |
||
184 |
lemma member_le_sum_list: |
|
185 |
"x \<in> set xs \<Longrightarrow> x \<le> sum_list xs" |
|
186 |
by (induction xs) (auto simp: add_increasing add_increasing2) |
|
58101 | 187 |
|
66311 | 188 |
lemma elem_le_sum_list: |
189 |
"k < size ns \<Longrightarrow> ns ! k \<le> sum_list (ns)" |
|
190 |
by (rule member_le_sum_list) simp |
|
191 |
||
192 |
end |
|
193 |
||
194 |
lemma (in ordered_cancel_comm_monoid_diff) sum_list_update: |
|
195 |
"k < size xs \<Longrightarrow> sum_list (xs[k := x]) = sum_list xs + x - xs ! k" |
|
196 |
apply(induction xs arbitrary:k) |
|
197 |
apply (auto simp: add_ac split: nat.split) |
|
198 |
apply(drule elem_le_sum_list) |
|
199 |
by (simp add: local.add_diff_assoc local.add_increasing) |
|
58101 | 200 |
|
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
201 |
lemma (in monoid_add) sum_list_triv: |
58101 | 202 |
"(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" |
203 |
by (induct xs) (simp_all add: distrib_right) |
|
204 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
205 |
lemma (in monoid_add) sum_list_0 [simp]: |
58101 | 206 |
"(\<Sum>x\<leftarrow>xs. 0) = 0" |
207 |
by (induct xs) (simp_all add: distrib_right) |
|
208 |
||
61799 | 209 |
text\<open>For non-Abelian groups \<open>xs\<close> needs to be reversed on one side:\<close> |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
210 |
lemma (in ab_group_add) uminus_sum_list_map: |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
211 |
"- sum_list (map f xs) = sum_list (map (uminus \<circ> f) xs)" |
58101 | 212 |
by (induct xs) simp_all |
213 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
214 |
lemma (in comm_monoid_add) sum_list_addf: |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
215 |
"(\<Sum>x\<leftarrow>xs. f x + g x) = sum_list (map f xs) + sum_list (map g xs)" |
58101 | 216 |
by (induct xs) (simp_all add: algebra_simps) |
217 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
218 |
lemma (in ab_group_add) sum_list_subtractf: |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
219 |
"(\<Sum>x\<leftarrow>xs. f x - g x) = sum_list (map f xs) - sum_list (map g xs)" |
58101 | 220 |
by (induct xs) (simp_all add: algebra_simps) |
221 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
222 |
lemma (in semiring_0) sum_list_const_mult: |
58101 | 223 |
"(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)" |
224 |
by (induct xs) (simp_all add: algebra_simps) |
|
225 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
226 |
lemma (in semiring_0) sum_list_mult_const: |
58101 | 227 |
"(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c" |
228 |
by (induct xs) (simp_all add: algebra_simps) |
|
229 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
230 |
lemma (in ordered_ab_group_add_abs) sum_list_abs: |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
231 |
"\<bar>sum_list xs\<bar> \<le> sum_list (map abs xs)" |
58101 | 232 |
by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq]) |
233 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
234 |
lemma sum_list_mono: |
58101 | 235 |
fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}" |
236 |
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)" |
|
69231 | 237 |
by (induct xs) (simp, simp add: add_mono) |
238 |
||
239 |
lemma sum_list_strict_mono: |
|
240 |
fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, strict_ordered_ab_semigroup_add}" |
|
241 |
shows "\<lbrakk> xs \<noteq> []; \<And>x. x \<in> set xs \<Longrightarrow> f x < g x \<rbrakk> |
|
242 |
\<Longrightarrow> sum_list (map f xs) < sum_list (map g xs)" |
|
243 |
proof (induction xs) |
|
244 |
case Nil thus ?case by simp |
|
245 |
next |
|
246 |
case C: (Cons _ xs) |
|
247 |
show ?case |
|
248 |
proof (cases xs) |
|
249 |
case Nil thus ?thesis using C.prems by simp |
|
250 |
next |
|
251 |
case Cons thus ?thesis using C by(simp add: add_strict_mono) |
|
252 |
qed |
|
253 |
qed |
|
58101 | 254 |
|
64267 | 255 |
lemma (in monoid_add) sum_list_distinct_conv_sum_set: |
256 |
"distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)" |
|
58101 | 257 |
by (induct xs) simp_all |
258 |
||
64267 | 259 |
lemma (in monoid_add) interv_sum_list_conv_sum_set_nat: |
260 |
"sum_list (map f [m..<n]) = sum f (set [m..<n])" |
|
261 |
by (simp add: sum_list_distinct_conv_sum_set) |
|
58101 | 262 |
|
64267 | 263 |
lemma (in monoid_add) interv_sum_list_conv_sum_set_int: |
264 |
"sum_list (map f [k..l]) = sum f (set [k..l])" |
|
265 |
by (simp add: sum_list_distinct_conv_sum_set) |
|
58101 | 266 |
|
69593 | 267 |
text \<open>General equivalence between \<^const>\<open>sum_list\<close> and \<^const>\<open>sum\<close>\<close> |
64267 | 268 |
lemma (in monoid_add) sum_list_sum_nth: |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
269 |
"sum_list xs = (\<Sum> i = 0 ..< length xs. xs ! i)" |
67399 | 270 |
using interv_sum_list_conv_sum_set_nat [of "(!) xs" 0 "length xs"] by (simp add: map_nth) |
58101 | 271 |
|
64267 | 272 |
lemma sum_list_map_eq_sum_count: |
273 |
"sum_list (map f xs) = sum (\<lambda>x. count_list xs x * f x) (set xs)" |
|
59728 | 274 |
proof(induction xs) |
275 |
case (Cons x xs) |
|
276 |
show ?case (is "?l = ?r") |
|
277 |
proof cases |
|
278 |
assume "x \<in> set xs" |
|
60541 | 279 |
have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH) |
60758 | 280 |
also have "set xs = insert x (set xs - {x})" using \<open>x \<in> set xs\<close>by blast |
60541 | 281 |
also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). count_list xs x * f x) = ?r" |
64267 | 282 |
by (simp add: sum.insert_remove eq_commute) |
59728 | 283 |
finally show ?thesis . |
284 |
next |
|
285 |
assume "x \<notin> set xs" |
|
286 |
hence "\<And>xa. xa \<in> set xs \<Longrightarrow> x \<noteq> xa" by blast |
|
60758 | 287 |
thus ?thesis by (simp add: Cons.IH \<open>x \<notin> set xs\<close>) |
59728 | 288 |
qed |
289 |
qed simp |
|
290 |
||
64267 | 291 |
lemma sum_list_map_eq_sum_count2: |
59728 | 292 |
assumes "set xs \<subseteq> X" "finite X" |
64267 | 293 |
shows "sum_list (map f xs) = sum (\<lambda>x. count_list xs x * f x) X" |
59728 | 294 |
proof- |
60541 | 295 |
let ?F = "\<lambda>x. count_list xs x * f x" |
64267 | 296 |
have "sum ?F X = sum ?F (set xs \<union> (X - set xs))" |
59728 | 297 |
using Un_absorb1[OF assms(1)] by(simp) |
64267 | 298 |
also have "\<dots> = sum ?F (set xs)" |
59728 | 299 |
using assms(2) |
64267 | 300 |
by(simp add: sum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel) |
301 |
finally show ?thesis by(simp add:sum_list_map_eq_sum_count) |
|
59728 | 302 |
qed |
303 |
||
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
304 |
lemma sum_list_nonneg: |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
305 |
"(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0" |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset
|
306 |
by (induction xs) simp_all |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset
|
307 |
|
69231 | 308 |
lemma sum_list_Suc: |
309 |
"sum_list (map (\<lambda>x. Suc(f x)) xs) = sum_list (map f xs) + length xs" |
|
310 |
by(induction xs; simp) |
|
311 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
312 |
lemma (in monoid_add) sum_list_map_filter': |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
313 |
"sum_list (map f (filter P xs)) = sum_list (map (\<lambda>x. if P x then f x else 0) xs)" |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset
|
314 |
by (induction xs) simp_all |
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
61955
diff
changeset
|
315 |
|
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
316 |
text \<open>Summation of a strictly ascending sequence with length \<open>n\<close> |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
317 |
can be upper-bounded by summation over \<open>{0..<n}\<close>.\<close> |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
318 |
|
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
319 |
lemma sorted_wrt_less_sum_mono_lowerbound: |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
320 |
fixes f :: "nat \<Rightarrow> ('b::ordered_comm_monoid_add)" |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
321 |
assumes mono: "\<And>x y. x\<le>y \<Longrightarrow> f x \<le> f y" |
67399 | 322 |
shows "sorted_wrt (<) ns \<Longrightarrow> |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
323 |
(\<Sum>i\<in>{0..<length ns}. f i) \<le> (\<Sum>i\<leftarrow>ns. f i)" |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
324 |
proof (induction ns rule: rev_induct) |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
325 |
case Nil |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
326 |
then show ?case by simp |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
327 |
next |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
328 |
case (snoc n ns) |
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
329 |
have "sum f {0..<length (ns @ [n])} |
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
330 |
= sum f {0..<length ns} + f (length ns)" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
331 |
by simp |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
332 |
also have "sum f {0..<length ns} \<le> sum_list (map f ns)" |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
333 |
using snoc by (auto simp: sorted_wrt_append) |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
334 |
also have "length ns \<le> n" |
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
335 |
using sorted_wrt_less_idx[OF snoc.prems(1), of "length ns"] by auto |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
336 |
finally have "sum f {0..<length (ns @ [n])} \<le> sum_list (map f ns) + f n" |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
337 |
using mono add_mono by blast |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
338 |
thus ?case by simp |
67489
f1ba59ddd9a6
drop redundant cong rules
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
339 |
qed |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66311
diff
changeset
|
340 |
|
58101 | 341 |
|
69593 | 342 |
subsection \<open>Further facts about \<^const>\<open>List.n_lists\<close>\<close> |
58101 | 343 |
|
344 |
lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n" |
|
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
345 |
by (induct n) (auto simp add: comp_def length_concat sum_list_triv) |
58101 | 346 |
|
347 |
lemma distinct_n_lists: |
|
348 |
assumes "distinct xs" |
|
349 |
shows "distinct (List.n_lists n xs)" |
|
350 |
proof (rule card_distinct) |
|
351 |
from assms have card_length: "card (set xs) = length xs" by (rule distinct_card) |
|
352 |
have "card (set (List.n_lists n xs)) = card (set xs) ^ n" |
|
353 |
proof (induct n) |
|
354 |
case 0 then show ?case by simp |
|
355 |
next |
|
356 |
case (Suc n) |
|
357 |
moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs) |
|
358 |
= (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))" |
|
359 |
by (rule card_UN_disjoint) auto |
|
360 |
moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)" |
|
361 |
by (rule card_image) (simp add: inj_on_def) |
|
362 |
ultimately show ?case by auto |
|
363 |
qed |
|
364 |
also have "\<dots> = length xs ^ n" by (simp add: card_length) |
|
365 |
finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)" |
|
366 |
by (simp add: length_n_lists) |
|
367 |
qed |
|
368 |
||
369 |
||
60758 | 370 |
subsection \<open>Tools setup\<close> |
58101 | 371 |
|
64267 | 372 |
lemmas sum_code = sum.set_conv_list |
58320 | 373 |
|
64267 | 374 |
lemma sum_set_upto_conv_sum_list_int [code_unfold]: |
375 |
"sum f (set [i..j::int]) = sum_list (map f [i..j])" |
|
376 |
by (simp add: interv_sum_list_conv_sum_set_int) |
|
58101 | 377 |
|
64267 | 378 |
lemma sum_set_upt_conv_sum_list_nat [code_unfold]: |
379 |
"sum f (set [m..<n]) = sum_list (map f [m..<n])" |
|
380 |
by (simp add: interv_sum_list_conv_sum_set_nat) |
|
58101 | 381 |
|
58368 | 382 |
|
60758 | 383 |
subsection \<open>List product\<close> |
58368 | 384 |
|
385 |
context monoid_mult |
|
386 |
begin |
|
387 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
388 |
sublocale prod_list: monoid_list times 1 |
61776 | 389 |
defines |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
390 |
prod_list = prod_list.F .. |
58368 | 391 |
|
58320 | 392 |
end |
58368 | 393 |
|
394 |
context comm_monoid_mult |
|
395 |
begin |
|
396 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
397 |
sublocale prod_list: comm_monoid_list times 1 |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset
|
398 |
rewrites |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
399 |
"monoid_list.F times 1 = prod_list" |
58368 | 400 |
proof - |
401 |
show "comm_monoid_list times 1" .. |
|
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
402 |
then interpret prod_list: comm_monoid_list times 1 . |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
403 |
from prod_list_def show "monoid_list.F times 1 = prod_list" by simp |
58368 | 404 |
qed |
405 |
||
64272 | 406 |
sublocale prod: comm_monoid_list_set times 1 |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset
|
407 |
rewrites |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
408 |
"monoid_list.F times 1 = prod_list" |
64272 | 409 |
and "comm_monoid_set.F times 1 = prod" |
58368 | 410 |
proof - |
411 |
show "comm_monoid_list_set times 1" .. |
|
64272 | 412 |
then interpret prod: comm_monoid_list_set times 1 . |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
413 |
from prod_list_def show "monoid_list.F times 1 = prod_list" by simp |
64272 | 414 |
from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym) |
58368 | 415 |
qed |
416 |
||
417 |
end |
|
418 |
||
60758 | 419 |
text \<open>Some syntactic sugar:\<close> |
58368 | 420 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
421 |
syntax (ASCII) |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
422 |
"_prod_list" :: "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
|
423 |
syntax |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
424 |
"_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10) |
61799 | 425 |
translations \<comment> \<open>Beware of argument permutation!\<close> |
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63343
diff
changeset
|
426 |
"\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)" |
58368 | 427 |
|
70928 | 428 |
context |
429 |
includes lifting_syntax |
|
430 |
begin |
|
431 |
||
432 |
lemma prod_list_transfer [transfer_rule]: |
|
433 |
"(list_all2 A ===> A) prod_list prod_list" |
|
434 |
if [transfer_rule]: "A 1 1" "(A ===> A ===> A) (*) (*)" |
|
435 |
unfolding prod_list.eq_foldr [abs_def] |
|
436 |
by transfer_prover |
|
437 |
||
58368 | 438 |
end |
70928 | 439 |
|
440 |
lemma prod_list_zero_iff: |
|
441 |
"prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs" |
|
442 |
by (induction xs) simp_all |
|
443 |
||
444 |
end |