author  wenzelm 
Mon, 07 Dec 2015 10:38:04 +0100  
changeset 61799  4cf66f21b764 
parent 61776  57bb7da5c867 
child 61955  e96292f32c3c 
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 

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 nonAbelian 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 