1(* Author: Tobias Nipkow, TU Muenchen *) 2 3section \<open>Sum and product over lists\<close> 4 5theory Groups_List 6imports List 7begin 8 9locale monoid_list = monoid 10begin 11 12definition F :: "'a list \<Rightarrow> 'a" 13where 14 eq_foldr [code]: "F xs = foldr f xs \<^bold>1" 15 16lemma Nil [simp]: 17 "F [] = \<^bold>1" 18 by (simp add: eq_foldr) 19 20lemma Cons [simp]: 21 "F (x # xs) = x \<^bold>* F xs" 22 by (simp add: eq_foldr) 23 24lemma append [simp]: 25 "F (xs @ ys) = F xs \<^bold>* F ys" 26 by (induct xs) (simp_all add: assoc) 27 28end 29 30locale comm_monoid_list = comm_monoid + monoid_list 31begin 32 33lemma rev [simp]: 34 "F (rev xs) = F xs" 35 by (simp add: eq_foldr foldr_fold fold_rev fun_eq_iff assoc left_commute) 36 37end 38 39locale comm_monoid_list_set = list: comm_monoid_list + set: comm_monoid_set 40begin 41 42lemma distinct_set_conv_list: 43 "distinct xs \<Longrightarrow> set.F g (set xs) = list.F (map g xs)" 44 by (induct xs) simp_all 45 46lemma 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 50end 51 52 53subsection \<open>List summation\<close> 54 55context monoid_add 56begin 57 58sublocale sum_list: monoid_list plus 0 59defines 60 sum_list = sum_list.F .. 61 62end 63 64context comm_monoid_add 65begin 66 67sublocale sum_list: comm_monoid_list plus 0 68rewrites 69 "monoid_list.F plus 0 = sum_list" 70proof - 71 show "comm_monoid_list plus 0" .. 72 then interpret sum_list: comm_monoid_list plus 0 . 73 from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp 74qed 75 76sublocale sum: comm_monoid_list_set plus 0 77rewrites 78 "monoid_list.F plus 0 = sum_list" 79 and "comm_monoid_set.F plus 0 = sum" 80proof - 81 show "comm_monoid_list_set plus 0" .. 82 then interpret sum: comm_monoid_list_set plus 0 . 83 from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp 84 from sum_def show "comm_monoid_set.F plus 0 = sum" by (auto intro: sym) 85qed 86 87end 88 89text \<open>Some syntactic sugar for summing a function over a list:\<close> 90syntax (ASCII) 91 "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) 92syntax 93 "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) 94translations \<comment> \<open>Beware of argument permutation!\<close> 95 "\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)" 96 97context 98 includes lifting_syntax 99begin 100 101lemma 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 107end 108 109text \<open>TODO duplicates\<close> 110lemmas sum_list_simps = sum_list.Nil sum_list.Cons 111lemmas sum_list_append = sum_list.append 112lemmas sum_list_rev = sum_list.rev 113 114lemma (in monoid_add) fold_plus_sum_list_rev: 115 "fold plus xs = plus (sum_list (rev xs))" 116proof 117 fix x 118 have "fold plus xs x = sum_list (rev xs @ [x])" 119 by (simp add: foldr_conv_fold sum_list.eq_foldr) 120 also have "\<dots> = sum_list (rev xs) + x" 121 by simp 122 finally show "fold plus xs x = sum_list (rev xs) + x" 123 . 124qed 125 126lemma (in comm_monoid_add) sum_list_map_remove1: 127 "x \<in> set xs \<Longrightarrow> sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))" 128 by (induct xs) (auto simp add: ac_simps) 129 130lemma (in monoid_add) size_list_conv_sum_list: 131 "size_list f xs = sum_list (map f xs) + size xs" 132 by (induct xs) auto 133 134lemma (in monoid_add) length_concat: 135 "length (concat xss) = sum_list (map length xss)" 136 by (induct xss) simp_all 137 138lemma (in monoid_add) length_product_lists: 139 "length (product_lists xss) = foldr (*) (map length xss) 1" 140proof (induct xss) 141 case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def) 142qed simp 143 144lemma (in monoid_add) sum_list_map_filter: 145 assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0" 146 shows "sum_list (map f (filter P xs)) = sum_list (map f xs)" 147 using assms by (induct xs) auto 148 149lemma 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)" 152by(induction xs; simp) 153 154lemma (in comm_monoid_add) distinct_sum_list_conv_Sum: 155 "distinct xs \<Longrightarrow> sum_list xs = Sum (set xs)" 156 by (induct xs) simp_all 157 158lemma sum_list_upt[simp]: 159 "m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}" 160by(simp add: distinct_sum_list_conv_Sum) 161 162context ordered_comm_monoid_add 163begin 164 165lemma sum_list_nonneg: "(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> 0 \<le> sum_list xs" 166by (induction xs) auto 167 168lemma sum_list_nonpos: "(\<And>x. x \<in> set xs \<Longrightarrow> x \<le> 0) \<Longrightarrow> sum_list xs \<le> 0" 169by (induction xs) (auto simp: add_nonpos_nonpos) 170 171lemma 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)" 173by (induction xs) (simp_all add: add_nonneg_eq_0_iff sum_list_nonneg) 174 175end 176 177context canonically_ordered_monoid_add 178begin 179 180lemma sum_list_eq_0_iff [simp]: 181 "sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)" 182by (simp add: sum_list_nonneg_eq_0_iff) 183 184lemma member_le_sum_list: 185 "x \<in> set xs \<Longrightarrow> x \<le> sum_list xs" 186by (induction xs) (auto simp: add_increasing add_increasing2) 187 188lemma elem_le_sum_list: 189 "k < size ns \<Longrightarrow> ns ! k \<le> sum_list (ns)" 190by (rule member_le_sum_list) simp 191 192end 193 194lemma (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" 196apply(induction xs arbitrary:k) 197 apply (auto simp: add_ac split: nat.split) 198apply(drule elem_le_sum_list) 199by (simp add: local.add_diff_assoc local.add_increasing) 200 201lemma (in monoid_add) sum_list_triv: 202 "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" 203 by (induct xs) (simp_all add: distrib_right) 204 205lemma (in monoid_add) sum_list_0 [simp]: 206 "(\<Sum>x\<leftarrow>xs. 0) = 0" 207 by (induct xs) (simp_all add: distrib_right) 208 209text\<open>For non-Abelian groups \<open>xs\<close> needs to be reversed on one side:\<close> 210lemma (in ab_group_add) uminus_sum_list_map: 211 "- sum_list (map f xs) = sum_list (map (uminus \<circ> f) xs)" 212 by (induct xs) simp_all 213 214lemma (in comm_monoid_add) sum_list_addf: 215 "(\<Sum>x\<leftarrow>xs. f x + g x) = sum_list (map f xs) + sum_list (map g xs)" 216 by (induct xs) (simp_all add: algebra_simps) 217 218lemma (in ab_group_add) sum_list_subtractf: 219 "(\<Sum>x\<leftarrow>xs. f x - g x) = sum_list (map f xs) - sum_list (map g xs)" 220 by (induct xs) (simp_all add: algebra_simps) 221 222lemma (in semiring_0) sum_list_const_mult: 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 226lemma (in semiring_0) sum_list_mult_const: 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 230lemma (in ordered_ab_group_add_abs) sum_list_abs: 231 "\<bar>sum_list xs\<bar> \<le> sum_list (map abs xs)" 232 by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq]) 233 234lemma sum_list_mono: 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)" 237by (induct xs) (simp, simp add: add_mono) 238 239lemma 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)" 243proof (induction xs) 244 case Nil thus ?case by simp 245next 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 253qed 254 255lemma (in monoid_add) sum_list_distinct_conv_sum_set: 256 "distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)" 257 by (induct xs) simp_all 258 259lemma (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) 262 263lemma (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) 266 267text \<open>General equivalence between \<^const>\<open>sum_list\<close> and \<^const>\<open>sum\<close>\<close> 268lemma (in monoid_add) sum_list_sum_nth: 269 "sum_list xs = (\<Sum> i = 0 ..< length xs. xs ! i)" 270 using interv_sum_list_conv_sum_set_nat [of "(!) xs" 0 "length xs"] by (simp add: map_nth) 271 272lemma sum_list_map_eq_sum_count: 273 "sum_list (map f xs) = sum (\<lambda>x. count_list xs x * f x) (set xs)" 274proof(induction xs) 275 case (Cons x xs) 276 show ?case (is "?l = ?r") 277 proof cases 278 assume "x \<in> set xs" 279 have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH) 280 also have "set xs = insert x (set xs - {x})" using \<open>x \<in> set xs\<close>by blast 281 also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). count_list xs x * f x) = ?r" 282 by (simp add: sum.insert_remove eq_commute) 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 287 thus ?thesis by (simp add: Cons.IH \<open>x \<notin> set xs\<close>) 288 qed 289qed simp 290 291lemma sum_list_map_eq_sum_count2: 292assumes "set xs \<subseteq> X" "finite X" 293shows "sum_list (map f xs) = sum (\<lambda>x. count_list xs x * f x) X" 294proof- 295 let ?F = "\<lambda>x. count_list xs x * f x" 296 have "sum ?F X = sum ?F (set xs \<union> (X - set xs))" 297 using Un_absorb1[OF assms(1)] by(simp) 298 also have "\<dots> = sum ?F (set xs)" 299 using assms(2) 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) 302qed 303 304lemma sum_list_nonneg: 305 "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0" 306 by (induction xs) simp_all 307 308lemma sum_list_Suc: 309 "sum_list (map (\<lambda>x. Suc(f x)) xs) = sum_list (map f xs) + length xs" 310by(induction xs; simp) 311 312lemma (in monoid_add) sum_list_map_filter': 313 "sum_list (map f (filter P xs)) = sum_list (map (\<lambda>x. if P x then f x else 0) xs)" 314 by (induction xs) simp_all 315 316text \<open>Summation of a strictly ascending sequence with length \<open>n\<close> 317 can be upper-bounded by summation over \<open>{0..<n}\<close>.\<close> 318 319lemma sorted_wrt_less_sum_mono_lowerbound: 320 fixes f :: "nat \<Rightarrow> ('b::ordered_comm_monoid_add)" 321 assumes mono: "\<And>x y. x\<le>y \<Longrightarrow> f x \<le> f y" 322 shows "sorted_wrt (<) ns \<Longrightarrow> 323 (\<Sum>i\<in>{0..<length ns}. f i) \<le> (\<Sum>i\<leftarrow>ns. f i)" 324proof (induction ns rule: rev_induct) 325 case Nil 326 then show ?case by simp 327next 328 case (snoc n ns) 329 have "sum f {0..<length (ns @ [n])} 330 = sum f {0..<length ns} + f (length ns)" 331 by simp 332 also have "sum f {0..<length ns} \<le> sum_list (map f ns)" 333 using snoc by (auto simp: sorted_wrt_append) 334 also have "length ns \<le> n" 335 using sorted_wrt_less_idx[OF snoc.prems(1), of "length ns"] by auto 336 finally have "sum f {0..<length (ns @ [n])} \<le> sum_list (map f ns) + f n" 337 using mono add_mono by blast 338 thus ?case by simp 339qed 340 341 342subsection \<open>Further facts about \<^const>\<open>List.n_lists\<close>\<close> 343 344lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n" 345 by (induct n) (auto simp add: comp_def length_concat sum_list_triv) 346 347lemma distinct_n_lists: 348 assumes "distinct xs" 349 shows "distinct (List.n_lists n xs)" 350proof (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) 367qed 368 369 370subsection \<open>Tools setup\<close> 371 372lemmas sum_code = sum.set_conv_list 373 374lemma 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) 377 378lemma 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) 381 382 383subsection \<open>List product\<close> 384 385context monoid_mult 386begin 387 388sublocale prod_list: monoid_list times 1 389defines 390 prod_list = prod_list.F .. 391 392end 393 394context comm_monoid_mult 395begin 396 397sublocale prod_list: comm_monoid_list times 1 398rewrites 399 "monoid_list.F times 1 = prod_list" 400proof - 401 show "comm_monoid_list times 1" .. 402 then interpret prod_list: comm_monoid_list times 1 . 403 from prod_list_def show "monoid_list.F times 1 = prod_list" by simp 404qed 405 406sublocale prod: comm_monoid_list_set times 1 407rewrites 408 "monoid_list.F times 1 = prod_list" 409 and "comm_monoid_set.F times 1 = prod" 410proof - 411 show "comm_monoid_list_set times 1" .. 412 then interpret prod: comm_monoid_list_set times 1 . 413 from prod_list_def show "monoid_list.F times 1 = prod_list" by simp 414 from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym) 415qed 416 417end 418 419text \<open>Some syntactic sugar:\<close> 420 421syntax (ASCII) 422 "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10) 423syntax 424 "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10) 425translations \<comment> \<open>Beware of argument permutation!\<close> 426 "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)" 427 428context 429 includes lifting_syntax 430begin 431 432lemma 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 438end 439 440lemma 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 444end 445