author  ballarin 
Wed, 04 Nov 2015 08:13:52 +0100  
changeset 61566  c3d6e570ccef 
parent 61378  3e04c9ca001a 
child 61605  1bf7b186542e 
permissions  rwrr 
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 

64 
definition listsum :: "'a list \<Rightarrow> 'a" 

65 
where 

66 
"listsum = monoid_list.F plus 0" 

58101  67 

58320  68 
sublocale listsum!: monoid_list plus 0 
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset

69 
rewrites 
58320  70 
"monoid_list.F plus 0 = listsum" 
71 
proof  

72 
show "monoid_list plus 0" .. 

73 
then interpret listsum!: monoid_list plus 0 . 

74 
from listsum_def show "monoid_list.F plus 0 = listsum" by rule 

75 
qed 

76 

77 
end 

78 

79 
context comm_monoid_add 

80 
begin 

81 

82 
sublocale listsum!: comm_monoid_list 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 
proof  

86 
show "comm_monoid_list plus 0" .. 

87 
then interpret listsum!: comm_monoid_list plus 0 . 

88 
from listsum_def show "monoid_list.F plus 0 = listsum" by rule 

58101  89 
qed 
90 

58320  91 
sublocale setsum!: comm_monoid_list_set plus 0 
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset

92 
rewrites 
58320  93 
"monoid_list.F plus 0 = listsum" 
94 
and "comm_monoid_set.F plus 0 = setsum" 

95 
proof  

96 
show "comm_monoid_list_set plus 0" .. 

97 
then interpret setsum!: comm_monoid_list_set plus 0 . 

98 
from listsum_def show "monoid_list.F plus 0 = listsum" by rule 

99 
from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule 

100 
qed 

101 

102 
end 

103 

60758  104 
text \<open>Some syntactic sugar for summing a function over a list:\<close> 
58101  105 

106 
syntax 

107 
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<_. _)" [0, 51, 10] 10) 

108 
syntax (xsymbols) 

109 
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) 

110 

60758  111 
translations  \<open>Beware of argument permutation!\<close> 
58101  112 
"SUM x<xs. b" == "CONST listsum (CONST map (%x. b) xs)" 
113 
"\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)" 

114 

60758  115 
text \<open>TODO duplicates\<close> 
58320  116 
lemmas listsum_simps = listsum.Nil listsum.Cons 
117 
lemmas listsum_append = listsum.append 

118 
lemmas listsum_rev = listsum.rev 

119 

120 
lemma (in monoid_add) fold_plus_listsum_rev: 

121 
"fold plus xs = plus (listsum (rev xs))" 

122 
proof 

123 
fix x 

124 
have "fold plus xs x = listsum (rev xs @ [x])" 

125 
by (simp add: foldr_conv_fold listsum.eq_foldr) 

126 
also have "\<dots> = listsum (rev xs) + x" 

127 
by simp 

128 
finally show "fold plus xs x = listsum (rev xs) + x" 

129 
. 

130 
qed 

131 

58101  132 
lemma (in comm_monoid_add) listsum_map_remove1: 
133 
"x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))" 

134 
by (induct xs) (auto simp add: ac_simps) 

135 

136 
lemma (in monoid_add) size_list_conv_listsum: 

137 
"size_list f xs = listsum (map f xs) + size xs" 

138 
by (induct xs) auto 

139 

140 
lemma (in monoid_add) length_concat: 

141 
"length (concat xss) = listsum (map length xss)" 

142 
by (induct xss) simp_all 

143 

144 
lemma (in monoid_add) length_product_lists: 

145 
"length (product_lists xss) = foldr op * (map length xss) 1" 

146 
proof (induct xss) 

147 
case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def) 

148 
qed simp 

149 

150 
lemma (in monoid_add) listsum_map_filter: 

151 
assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0" 

152 
shows "listsum (map f (filter P xs)) = listsum (map f xs)" 

153 
using assms by (induct xs) auto 

154 

155 
lemma (in comm_monoid_add) distinct_listsum_conv_Setsum: 

156 
"distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)" 

157 
by (induct xs) simp_all 

158 

58995  159 
lemma listsum_upt[simp]: 
160 
"m \<le> n \<Longrightarrow> listsum [m..<n] = \<Sum> {m..<n}" 

161 
by(simp add: distinct_listsum_conv_Setsum) 

162 

58101  163 
lemma listsum_eq_0_nat_iff_nat [simp]: 
164 
"listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)" 

165 
by (induct ns) simp_all 

166 

167 
lemma member_le_listsum_nat: 

168 
"(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns" 

169 
by (induct ns) auto 

170 

171 
lemma elem_le_listsum_nat: 

172 
"k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)" 

173 
by (rule member_le_listsum_nat) simp 

174 

175 
lemma listsum_update_nat: 

176 
"k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n  ns ! k" 

177 
apply(induct ns arbitrary:k) 

178 
apply (auto split:nat.split) 

179 
apply(drule elem_le_listsum_nat) 

180 
apply arith 

181 
done 

182 

183 
lemma (in monoid_add) listsum_triv: 

184 
"(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" 

185 
by (induct xs) (simp_all add: distrib_right) 

186 

187 
lemma (in monoid_add) listsum_0 [simp]: 

188 
"(\<Sum>x\<leftarrow>xs. 0) = 0" 

189 
by (induct xs) (simp_all add: distrib_right) 

190 

60758  191 
text\<open>For nonAbelian groups @{text xs} needs to be reversed on one side:\<close> 
58101  192 
lemma (in ab_group_add) uminus_listsum_map: 
193 
" listsum (map f xs) = listsum (map (uminus \<circ> f) xs)" 

194 
by (induct xs) simp_all 

195 

196 
lemma (in comm_monoid_add) listsum_addf: 

197 
"(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)" 

198 
by (induct xs) (simp_all add: algebra_simps) 

199 

200 
lemma (in ab_group_add) listsum_subtractf: 

201 
"(\<Sum>x\<leftarrow>xs. f x  g x) = listsum (map f xs)  listsum (map g xs)" 

202 
by (induct xs) (simp_all add: algebra_simps) 

203 

204 
lemma (in semiring_0) listsum_const_mult: 

205 
"(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)" 

206 
by (induct xs) (simp_all add: algebra_simps) 

207 

208 
lemma (in semiring_0) listsum_mult_const: 

209 
"(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c" 

210 
by (induct xs) (simp_all add: algebra_simps) 

211 

212 
lemma (in ordered_ab_group_add_abs) listsum_abs: 

213 
"\<bar>listsum xs\<bar> \<le> listsum (map abs xs)" 

214 
by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq]) 

215 

216 
lemma listsum_mono: 

217 
fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}" 

218 
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)" 

219 
by (induct xs) (simp, simp add: add_mono) 

220 

221 
lemma (in monoid_add) listsum_distinct_conv_setsum_set: 

222 
"distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)" 

223 
by (induct xs) simp_all 

224 

225 
lemma (in monoid_add) interv_listsum_conv_setsum_set_nat: 

226 
"listsum (map f [m..<n]) = setsum f (set [m..<n])" 

227 
by (simp add: listsum_distinct_conv_setsum_set) 

228 

229 
lemma (in monoid_add) interv_listsum_conv_setsum_set_int: 

230 
"listsum (map f [k..l]) = setsum f (set [k..l])" 

231 
by (simp add: listsum_distinct_conv_setsum_set) 

232 

60758  233 
text \<open>General equivalence between @{const listsum} and @{const setsum}\<close> 
58101  234 
lemma (in monoid_add) listsum_setsum_nth: 
235 
"listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)" 

236 
using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth) 

237 

59728  238 
lemma listsum_map_eq_setsum_count: 
60541  239 
"listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) (set xs)" 
59728  240 
proof(induction xs) 
241 
case (Cons x xs) 

242 
show ?case (is "?l = ?r") 

243 
proof cases 

244 
assume "x \<in> set xs" 

60541  245 
have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH) 
60758  246 
also have "set xs = insert x (set xs  {x})" using \<open>x \<in> set xs\<close>by blast 
60541  247 
also have "f x + (\<Sum>x\<in>insert x (set xs  {x}). count_list xs x * f x) = ?r" 
59728  248 
by (simp add: setsum.insert_remove eq_commute) 
249 
finally show ?thesis . 

250 
next 

251 
assume "x \<notin> set xs" 

252 
hence "\<And>xa. xa \<in> set xs \<Longrightarrow> x \<noteq> xa" by blast 

60758  253 
thus ?thesis by (simp add: Cons.IH \<open>x \<notin> set xs\<close>) 
59728  254 
qed 
255 
qed simp 

256 

257 
lemma listsum_map_eq_setsum_count2: 

258 
assumes "set xs \<subseteq> X" "finite X" 

60541  259 
shows "listsum (map f xs) = setsum (\<lambda>x. count_list xs x * f x) X" 
59728  260 
proof 
60541  261 
let ?F = "\<lambda>x. count_list xs x * f x" 
59728  262 
have "setsum ?F X = setsum ?F (set xs \<union> (X  set xs))" 
263 
using Un_absorb1[OF assms(1)] by(simp) 

264 
also have "\<dots> = setsum ?F (set xs)" 

265 
using assms(2) 

266 
by(simp add: setsum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel) 

267 
finally show ?thesis by(simp add:listsum_map_eq_setsum_count) 

268 
qed 

269 

58101  270 

60758  271 
subsection \<open>Further facts about @{const List.n_lists}\<close> 
58101  272 

273 
lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n" 

274 
by (induct n) (auto simp add: comp_def length_concat listsum_triv) 

275 

276 
lemma distinct_n_lists: 

277 
assumes "distinct xs" 

278 
shows "distinct (List.n_lists n xs)" 

279 
proof (rule card_distinct) 

280 
from assms have card_length: "card (set xs) = length xs" by (rule distinct_card) 

281 
have "card (set (List.n_lists n xs)) = card (set xs) ^ n" 

282 
proof (induct n) 

283 
case 0 then show ?case by simp 

284 
next 

285 
case (Suc n) 

286 
moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs) 

287 
= (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))" 

288 
by (rule card_UN_disjoint) auto 

289 
moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)" 

290 
by (rule card_image) (simp add: inj_on_def) 

291 
ultimately show ?case by auto 

292 
qed 

293 
also have "\<dots> = length xs ^ n" by (simp add: card_length) 

294 
finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)" 

295 
by (simp add: length_n_lists) 

296 
qed 

297 

298 

60758  299 
subsection \<open>Tools setup\<close> 
58101  300 

58320  301 
lemmas setsum_code = setsum.set_conv_list 
302 

58101  303 
lemma setsum_set_upto_conv_listsum_int [code_unfold]: 
304 
"setsum f (set [i..j::int]) = listsum (map f [i..j])" 

305 
by (simp add: interv_listsum_conv_setsum_set_int) 

306 

307 
lemma setsum_set_upt_conv_listsum_nat [code_unfold]: 

308 
"setsum f (set [m..<n]) = listsum (map f [m..<n])" 

309 
by (simp add: interv_listsum_conv_setsum_set_nat) 

310 

311 
context 

312 
begin 

313 

314 
interpretation lifting_syntax . 

315 

316 
lemma listsum_transfer[transfer_rule]: 

317 
assumes [transfer_rule]: "A 0 0" 

318 
assumes [transfer_rule]: "(A ===> A ===> A) op + op +" 

319 
shows "(list_all2 A ===> A) listsum listsum" 

58320  320 
unfolding listsum.eq_foldr [abs_def] 
58101  321 
by transfer_prover 
322 

323 
end 

324 

58368  325 

60758  326 
subsection \<open>List product\<close> 
58368  327 

328 
context monoid_mult 

329 
begin 

330 

331 
definition listprod :: "'a list \<Rightarrow> 'a" 

332 
where 

333 
"listprod = monoid_list.F times 1" 

334 

335 
sublocale listprod!: monoid_list times 1 

61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset

336 
rewrites 
58368  337 
"monoid_list.F times 1 = listprod" 
338 
proof  

339 
show "monoid_list times 1" .. 

340 
then interpret listprod!: monoid_list times 1 . 

341 
from listprod_def show "monoid_list.F times 1 = listprod" by rule 

342 
qed 

343 

58320  344 
end 
58368  345 

346 
context comm_monoid_mult 

347 
begin 

348 

349 
sublocale listprod!: comm_monoid_list times 1 

61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset

350 
rewrites 
58368  351 
"monoid_list.F times 1 = listprod" 
352 
proof  

353 
show "comm_monoid_list times 1" .. 

354 
then interpret listprod!: comm_monoid_list times 1 . 

355 
from listprod_def show "monoid_list.F times 1 = listprod" by rule 

356 
qed 

357 

358 
sublocale setprod!: comm_monoid_list_set times 1 

61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61378
diff
changeset

359 
rewrites 
58368  360 
"monoid_list.F times 1 = listprod" 
361 
and "comm_monoid_set.F times 1 = setprod" 

362 
proof  

363 
show "comm_monoid_list_set times 1" .. 

364 
then interpret setprod!: comm_monoid_list_set times 1 . 

365 
from listprod_def show "monoid_list.F times 1 = listprod" by rule 

366 
from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule 

367 
qed 

368 

369 
end 

370 

60758  371 
text \<open>Some syntactic sugar:\<close> 
58368  372 

373 
syntax 

374 
"_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<_. _)" [0, 51, 10] 10) 

375 
syntax (xsymbols) 

376 
"_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10) 

377 

60758  378 
translations  \<open>Beware of argument permutation!\<close> 
58368  379 
"PROD x<xs. b" == "CONST listprod (CONST map (%x. b) xs)" 
380 
"\<Prod>x\<leftarrow>xs. b" == "CONST listprod (CONST map (%x. b) xs)" 

381 

382 
end 