src/HOL/Groups_List.thy
 changeset 58101 e7ebe5554281 child 58152 6fe60a9a5bad
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Groups_List.thy	Sun Aug 31 09:10:42 2014 +0200
1.3 @@ -0,0 +1,212 @@
1.4 +
1.5 +(* Author: Tobias Nipkow, TU Muenchen *)
1.6 +
1.7 +header {* Summation over lists *}
1.8 +
1.9 +theory Groups_List
1.10 +imports List
1.11 +begin
1.12 +
1.13 +definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where
1.14 +"listsum xs = foldr plus xs 0"
1.15 +
1.16 +subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
1.17 +
1.18 +lemma (in monoid_add) listsum_simps [simp]:
1.19 +  "listsum [] = 0"
1.20 +  "listsum (x # xs) = x + listsum xs"
1.21 +  by (simp_all add: listsum_def)
1.22 +
1.23 +lemma (in monoid_add) listsum_append [simp]:
1.24 +  "listsum (xs @ ys) = listsum xs + listsum ys"
1.26 +
1.27 +lemma (in comm_monoid_add) listsum_rev [simp]:
1.28 +  "listsum (rev xs) = listsum xs"
1.30 +
1.32 +  "fold plus xs = plus (listsum (rev xs))"
1.33 +proof
1.34 +  fix x
1.35 +  have "fold plus xs x = fold plus xs (x + 0)" by simp
1.36 +  also have "\<dots> = fold plus (x # xs) 0" by simp
1.37 +  also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_conv_fold)
1.38 +  also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def)
1.39 +  also have "\<dots> = listsum (rev xs) + listsum [x]" by simp
1.40 +  finally show "fold plus xs x = listsum (rev xs) + x" by simp
1.41 +qed
1.42 +
1.43 +text{* Some syntactic sugar for summing a function over a list: *}
1.44 +
1.45 +syntax
1.46 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
1.47 +syntax (xsymbols)
1.48 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
1.49 +syntax (HTML output)
1.50 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
1.51 +
1.52 +translations -- {* Beware of argument permutation! *}
1.53 +  "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
1.54 +  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
1.55 +
1.57 +  "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
1.58 +  by (induct xs) (auto simp add: ac_simps)
1.59 +
1.61 +  "size_list f xs = listsum (map f xs) + size xs"
1.62 +  by (induct xs) auto
1.63 +
1.65 +  "length (concat xss) = listsum (map length xss)"
1.66 +  by (induct xss) simp_all
1.67 +
1.69 +  "length (product_lists xss) = foldr op * (map length xss) 1"
1.70 +proof (induct xss)
1.71 +  case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
1.72 +qed simp
1.73 +
1.75 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
1.76 +  shows "listsum (map f (filter P xs)) = listsum (map f xs)"
1.77 +  using assms by (induct xs) auto
1.78 +
1.80 +  "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
1.81 +  by (induct xs) simp_all
1.82 +
1.83 +lemma listsum_eq_0_nat_iff_nat [simp]:
1.84 +  "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
1.85 +  by (induct ns) simp_all
1.86 +
1.87 +lemma member_le_listsum_nat:
1.88 +  "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns"
1.89 +  by (induct ns) auto
1.90 +
1.91 +lemma elem_le_listsum_nat:
1.92 +  "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
1.93 +  by (rule member_le_listsum_nat) simp
1.94 +
1.95 +lemma listsum_update_nat:
1.96 +  "k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
1.97 +apply(induct ns arbitrary:k)
1.98 + apply (auto split:nat.split)
1.99 +apply(drule elem_le_listsum_nat)
1.100 +apply arith
1.101 +done
1.102 +
1.104 +  "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
1.105 +  by (induct xs) (simp_all add: distrib_right)
1.106 +
1.107 +lemma (in monoid_add) listsum_0 [simp]:
1.108 +  "(\<Sum>x\<leftarrow>xs. 0) = 0"
1.109 +  by (induct xs) (simp_all add: distrib_right)
1.110 +
1.111 +text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
1.113 +  "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
1.114 +  by (induct xs) simp_all
1.115 +
1.117 +  "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
1.118 +  by (induct xs) (simp_all add: algebra_simps)
1.119 +
1.121 +  "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
1.122 +  by (induct xs) (simp_all add: algebra_simps)
1.123 +
1.124 +lemma (in semiring_0) listsum_const_mult:
1.125 +  "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
1.126 +  by (induct xs) (simp_all add: algebra_simps)
1.127 +
1.128 +lemma (in semiring_0) listsum_mult_const:
1.129 +  "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
1.130 +  by (induct xs) (simp_all add: algebra_simps)
1.131 +
1.133 +  "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
1.134 +  by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])
1.135 +
1.136 +lemma listsum_mono:
1.138 +  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)"
1.140 +
1.142 +  "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
1.143 +  by (induct xs) simp_all
1.144 +
1.146 +  "listsum (map f [m..<n]) = setsum f (set [m..<n])"
1.147 +  by (simp add: listsum_distinct_conv_setsum_set)
1.148 +
1.150 +  "listsum (map f [k..l]) = setsum f (set [k..l])"
1.151 +  by (simp add: listsum_distinct_conv_setsum_set)
1.152 +
1.153 +text {* General equivalence between @{const listsum} and @{const setsum} *}
1.155 +  "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
1.156 +  using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
1.157 +
1.158 +
1.159 +subsection {* Further facts about @{const List.n_lists} *}
1.160 +
1.161 +lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
1.162 +  by (induct n) (auto simp add: comp_def length_concat listsum_triv)
1.163 +
1.164 +lemma distinct_n_lists:
1.165 +  assumes "distinct xs"
1.166 +  shows "distinct (List.n_lists n xs)"
1.167 +proof (rule card_distinct)
1.168 +  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
1.169 +  have "card (set (List.n_lists n xs)) = card (set xs) ^ n"
1.170 +  proof (induct n)
1.171 +    case 0 then show ?case by simp
1.172 +  next
1.173 +    case (Suc n)
1.174 +    moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs)
1.175 +      = (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
1.176 +      by (rule card_UN_disjoint) auto
1.177 +    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
1.178 +      by (rule card_image) (simp add: inj_on_def)
1.179 +    ultimately show ?case by auto
1.180 +  qed
1.181 +  also have "\<dots> = length xs ^ n" by (simp add: card_length)
1.182 +  finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)"
1.183 +    by (simp add: length_n_lists)
1.184 +qed
1.185 +
1.186 +
1.187 +subsection {* Tools setup *}
1.188 +
1.189 +lemma setsum_set_upto_conv_listsum_int [code_unfold]:
1.190 +  "setsum f (set [i..j::int]) = listsum (map f [i..j])"
1.191 +  by (simp add: interv_listsum_conv_setsum_set_int)
1.192 +
1.193 +lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
1.194 +  "setsum f (set [m..<n]) = listsum (map f [m..<n])"
1.195 +  by (simp add: interv_listsum_conv_setsum_set_nat)
1.196 +
1.197 +lemma setsum_code [code]:
1.198 +  "setsum f (set xs) = listsum (map f (remdups xs))"
1.199 +  by (simp add: listsum_distinct_conv_setsum_set)
1.200 +
1.201 +context
1.202 +begin
1.203 +
1.204 +interpretation lifting_syntax .
1.205 +
1.206 +lemma listsum_transfer[transfer_rule]:
1.207 +  assumes [transfer_rule]: "A 0 0"
1.208 +  assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
1.209 +  shows "(list_all2 A ===> A) listsum listsum"
1.210 +  unfolding listsum_def[abs_def]
1.211 +  by transfer_prover
1.212 +
1.213 +end
1.214 +
1.215 +end
1.216 \ No newline at end of file
```