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 97text \<open>TODO duplicates\<close> 98lemmas sum_list_simps = sum_list.Nil sum_list.Cons 99lemmas sum_list_append = sum_list.append 100lemmas sum_list_rev = sum_list.rev 101 102lemma (in monoid_add) fold_plus_sum_list_rev: 103 "fold plus xs = plus (sum_list (rev xs))" 104proof 105 fix x 106 have "fold plus xs x = sum_list (rev xs @ [x])" 107 by (simp add: foldr_conv_fold sum_list.eq_foldr) 108 also have "\<dots> = sum_list (rev xs) + x" 109 by simp 110 finally show "fold plus xs x = sum_list (rev xs) + x" 111 . 112qed 113 114lemma (in comm_monoid_add) sum_list_map_remove1: 115 "x \<in> set xs \<Longrightarrow> sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))" 116 by (induct xs) (auto simp add: ac_simps) 117 118lemma (in monoid_add) size_list_conv_sum_list: 119 "size_list f xs = sum_list (map f xs) + size xs" 120 by (induct xs) auto 121 122lemma (in monoid_add) length_concat: 123 "length (concat xss) = sum_list (map length xss)" 124 by (induct xss) simp_all 125 126lemma (in monoid_add) length_product_lists: 127 "length (product_lists xss) = foldr ( * ) (map length xss) 1" 128proof (induct xss) 129 case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def) 130qed simp 131 132lemma (in monoid_add) sum_list_map_filter: 133 assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0" 134 shows "sum_list (map f (filter P xs)) = sum_list (map f xs)" 135 using assms by (induct xs) auto 136 137lemma (in comm_monoid_add) distinct_sum_list_conv_Sum: 138 "distinct xs \<Longrightarrow> sum_list xs = Sum (set xs)" 139 by (induct xs) simp_all 140 141lemma sum_list_upt[simp]: 142 "m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}" 143by(simp add: distinct_sum_list_conv_Sum) 144 145context ordered_comm_monoid_add 146begin 147 148lemma sum_list_nonneg: "(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> 0 \<le> sum_list xs" 149by (induction xs) auto 150 151lemma sum_list_nonpos: "(\<And>x. x \<in> set xs \<Longrightarrow> x \<le> 0) \<Longrightarrow> sum_list xs \<le> 0" 152by (induction xs) (auto simp: add_nonpos_nonpos) 153 154lemma sum_list_nonneg_eq_0_iff: 155 "(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> sum_list xs = 0 \<longleftrightarrow> (\<forall>x\<in> set xs. x = 0)" 156by (induction xs) (simp_all add: add_nonneg_eq_0_iff sum_list_nonneg) 157 158end 159 160context canonically_ordered_monoid_add 161begin 162 163lemma sum_list_eq_0_iff [simp]: 164 "sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)" 165by (simp add: sum_list_nonneg_eq_0_iff) 166 167lemma member_le_sum_list: 168 "x \<in> set xs \<Longrightarrow> x \<le> sum_list xs" 169by (induction xs) (auto simp: add_increasing add_increasing2) 170 171lemma elem_le_sum_list: 172 "k < size ns \<Longrightarrow> ns ! k \<le> sum_list (ns)" 173by (rule member_le_sum_list) simp 174 175end 176 177lemma (in ordered_cancel_comm_monoid_diff) sum_list_update: 178 "k < size xs \<Longrightarrow> sum_list (xs[k := x]) = sum_list xs + x - xs ! k" 179apply(induction xs arbitrary:k) 180 apply (auto simp: add_ac split: nat.split) 181apply(drule elem_le_sum_list) 182by (simp add: local.add_diff_assoc local.add_increasing) 183 184lemma (in monoid_add) sum_list_triv: 185 "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" 186 by (induct xs) (simp_all add: distrib_right) 187 188lemma (in monoid_add) sum_list_0 [simp]: 189 "(\<Sum>x\<leftarrow>xs. 0) = 0" 190 by (induct xs) (simp_all add: distrib_right) 191 192text\<open>For non-Abelian groups \<open>xs\<close> needs to be reversed on one side:\<close> 193lemma (in ab_group_add) uminus_sum_list_map: 194 "- sum_list (map f xs) = sum_list (map (uminus \<circ> f) xs)" 195 by (induct xs) simp_all 196 197lemma (in comm_monoid_add) sum_list_addf: 198 "(\<Sum>x\<leftarrow>xs. f x + g x) = sum_list (map f xs) + sum_list (map g xs)" 199 by (induct xs) (simp_all add: algebra_simps) 200 201lemma (in ab_group_add) sum_list_subtractf: 202 "(\<Sum>x\<leftarrow>xs. f x - g x) = sum_list (map f xs) - sum_list (map g xs)" 203 by (induct xs) (simp_all add: algebra_simps) 204 205lemma (in semiring_0) sum_list_const_mult: 206 "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)" 207 by (induct xs) (simp_all add: algebra_simps) 208 209lemma (in semiring_0) sum_list_mult_const: 210 "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c" 211 by (induct xs) (simp_all add: algebra_simps) 212 213lemma (in ordered_ab_group_add_abs) sum_list_abs: 214 "\<bar>sum_list xs\<bar> \<le> sum_list (map abs xs)" 215 by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq]) 216 217lemma sum_list_mono: 218 fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}" 219 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)" 220 by (induct xs) (simp, simp add: add_mono) 221 222lemma (in monoid_add) sum_list_distinct_conv_sum_set: 223 "distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)" 224 by (induct xs) simp_all 225 226lemma (in monoid_add) interv_sum_list_conv_sum_set_nat: 227 "sum_list (map f [m..<n]) = sum f (set [m..<n])" 228 by (simp add: sum_list_distinct_conv_sum_set) 229 230lemma (in monoid_add) interv_sum_list_conv_sum_set_int: 231 "sum_list (map f [k..l]) = sum f (set [k..l])" 232 by (simp add: sum_list_distinct_conv_sum_set) 233 234text \<open>General equivalence between @{const sum_list} and @{const sum}\<close> 235lemma (in monoid_add) sum_list_sum_nth: 236 "sum_list xs = (\<Sum> i = 0 ..< length xs. xs ! i)" 237 using interv_sum_list_conv_sum_set_nat [of "(!) xs" 0 "length xs"] by (simp add: map_nth) 238 239lemma sum_list_map_eq_sum_count: 240 "sum_list (map f xs) = sum (\<lambda>x. count_list xs x * f x) (set xs)" 241proof(induction xs) 242 case (Cons x xs) 243 show ?case (is "?l = ?r") 244 proof cases 245 assume "x \<in> set xs" 246 have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH) 247 also have "set xs = insert x (set xs - {x})" using \<open>x \<in> set xs\<close>by blast 248 also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). count_list xs x * f x) = ?r" 249 by (simp add: sum.insert_remove eq_commute) 250 finally show ?thesis . 251 next 252 assume "x \<notin> set xs" 253 hence "\<And>xa. xa \<in> set xs \<Longrightarrow> x \<noteq> xa" by blast 254 thus ?thesis by (simp add: Cons.IH \<open>x \<notin> set xs\<close>) 255 qed 256qed simp 257 258lemma sum_list_map_eq_sum_count2: 259assumes "set xs \<subseteq> X" "finite X" 260shows "sum_list (map f xs) = sum (\<lambda>x. count_list xs x * f x) X" 261proof- 262 let ?F = "\<lambda>x. count_list xs x * f x" 263 have "sum ?F X = sum ?F (set xs \<union> (X - set xs))" 264 using Un_absorb1[OF assms(1)] by(simp) 265 also have "\<dots> = sum ?F (set xs)" 266 using assms(2) 267 by(simp add: sum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel) 268 finally show ?thesis by(simp add:sum_list_map_eq_sum_count) 269qed 270 271lemma sum_list_nonneg: 272 "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0" 273 by (induction xs) simp_all 274 275lemma (in monoid_add) sum_list_map_filter': 276 "sum_list (map f (filter P xs)) = sum_list (map (\<lambda>x. if P x then f x else 0) xs)" 277 by (induction xs) simp_all 278 279text \<open>Summation of a strictly ascending sequence with length \<open>n\<close> 280 can be upper-bounded by summation over \<open>{0..<n}\<close>.\<close> 281 282lemma sorted_wrt_less_sum_mono_lowerbound: 283 fixes f :: "nat \<Rightarrow> ('b::ordered_comm_monoid_add)" 284 assumes mono: "\<And>x y. x\<le>y \<Longrightarrow> f x \<le> f y" 285 shows "sorted_wrt (<) ns \<Longrightarrow> 286 (\<Sum>i\<in>{0..<length ns}. f i) \<le> (\<Sum>i\<leftarrow>ns. f i)" 287proof (induction ns rule: rev_induct) 288 case Nil 289 then show ?case by simp 290next 291 case (snoc n ns) 292 have "sum f {0..<length (ns @ [n])} 293 = sum f {0..<length ns} + f (length ns)" 294 by simp 295 also have "sum f {0..<length ns} \<le> sum_list (map f ns)" 296 using snoc by (auto simp: sorted_wrt_append) 297 also have "length ns \<le> n" 298 using sorted_wrt_less_idx[OF snoc.prems(1), of "length ns"] by auto 299 finally have "sum f {0..<length (ns @ [n])} \<le> sum_list (map f ns) + f n" 300 using mono add_mono by blast 301 thus ?case by simp 302qed 303 304 305subsection \<open>Further facts about @{const List.n_lists}\<close> 306 307lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n" 308 by (induct n) (auto simp add: comp_def length_concat sum_list_triv) 309 310lemma distinct_n_lists: 311 assumes "distinct xs" 312 shows "distinct (List.n_lists n xs)" 313proof (rule card_distinct) 314 from assms have card_length: "card (set xs) = length xs" by (rule distinct_card) 315 have "card (set (List.n_lists n xs)) = card (set xs) ^ n" 316 proof (induct n) 317 case 0 then show ?case by simp 318 next 319 case (Suc n) 320 moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs) 321 = (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))" 322 by (rule card_UN_disjoint) auto 323 moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)" 324 by (rule card_image) (simp add: inj_on_def) 325 ultimately show ?case by auto 326 qed 327 also have "\<dots> = length xs ^ n" by (simp add: card_length) 328 finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)" 329 by (simp add: length_n_lists) 330qed 331 332 333subsection \<open>Tools setup\<close> 334 335lemmas sum_code = sum.set_conv_list 336 337lemma sum_set_upto_conv_sum_list_int [code_unfold]: 338 "sum f (set [i..j::int]) = sum_list (map f [i..j])" 339 by (simp add: interv_sum_list_conv_sum_set_int) 340 341lemma sum_set_upt_conv_sum_list_nat [code_unfold]: 342 "sum f (set [m..<n]) = sum_list (map f [m..<n])" 343 by (simp add: interv_sum_list_conv_sum_set_nat) 344 345lemma sum_list_transfer[transfer_rule]: 346 includes lifting_syntax 347 assumes [transfer_rule]: "A 0 0" 348 assumes [transfer_rule]: "(A ===> A ===> A) (+) (+)" 349 shows "(list_all2 A ===> A) sum_list sum_list" 350 unfolding sum_list.eq_foldr [abs_def] 351 by transfer_prover 352 353 354subsection \<open>List product\<close> 355 356context monoid_mult 357begin 358 359sublocale prod_list: monoid_list times 1 360defines 361 prod_list = prod_list.F .. 362 363end 364 365context comm_monoid_mult 366begin 367 368sublocale prod_list: comm_monoid_list times 1 369rewrites 370 "monoid_list.F times 1 = prod_list" 371proof - 372 show "comm_monoid_list times 1" .. 373 then interpret prod_list: comm_monoid_list times 1 . 374 from prod_list_def show "monoid_list.F times 1 = prod_list" by simp 375qed 376 377sublocale prod: comm_monoid_list_set times 1 378rewrites 379 "monoid_list.F times 1 = prod_list" 380 and "comm_monoid_set.F times 1 = prod" 381proof - 382 show "comm_monoid_list_set times 1" .. 383 then interpret prod: comm_monoid_list_set times 1 . 384 from prod_list_def show "monoid_list.F times 1 = prod_list" by simp 385 from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym) 386qed 387 388end 389 390lemma prod_list_zero_iff: 391 "prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs" 392 by (induction xs) simp_all 393 394text \<open>Some syntactic sugar:\<close> 395 396syntax (ASCII) 397 "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10) 398syntax 399 "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10) 400translations \<comment> \<open>Beware of argument permutation!\<close> 401 "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)" 402 403end 404