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.25 +  by (induct xs) (simp_all add: add.assoc)
    1.26 +
    1.27 +lemma (in comm_monoid_add) listsum_rev [simp]:
    1.28 +  "listsum (rev xs) = listsum xs"
    1.29 +  by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff add_ac)
    1.30 +
    1.31 +lemma (in monoid_add) fold_plus_listsum_rev:
    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.56 +lemma (in comm_monoid_add) listsum_map_remove1:
    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.60 +lemma (in monoid_add) size_list_conv_listsum:
    1.61 +  "size_list f xs = listsum (map f xs) + size xs"
    1.62 +  by (induct xs) auto
    1.63 +
    1.64 +lemma (in monoid_add) length_concat:
    1.65 +  "length (concat xss) = listsum (map length xss)"
    1.66 +  by (induct xss) simp_all
    1.67 +
    1.68 +lemma (in monoid_add) length_product_lists:
    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.74 +lemma (in monoid_add) listsum_map_filter:
    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.79 +lemma (in comm_monoid_add) distinct_listsum_conv_Setsum:
    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.103 +lemma (in monoid_add) listsum_triv:
   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.112 +lemma (in ab_group_add) uminus_listsum_map:
   1.113 +  "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
   1.114 +  by (induct xs) simp_all
   1.115 +
   1.116 +lemma (in comm_monoid_add) listsum_addf:
   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.120 +lemma (in ab_group_add) listsum_subtractf:
   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.132 +lemma (in ordered_ab_group_add_abs) listsum_abs:
   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.137 +  fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}"
   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.139 +  by (induct xs) (simp, simp add: add_mono)
   1.140 +
   1.141 +lemma (in monoid_add) listsum_distinct_conv_setsum_set:
   1.142 +  "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
   1.143 +  by (induct xs) simp_all
   1.144 +
   1.145 +lemma (in monoid_add) interv_listsum_conv_setsum_set_nat:
   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.149 +lemma (in monoid_add) interv_listsum_conv_setsum_set_int:
   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.154 +lemma (in monoid_add) listsum_setsum_nth:
   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