separated listsum material
authorhaftmann
Sun Aug 31 09:10:42 2014 +0200 (2014-08-31)
changeset 58101e7ebe5554281
parent 58100 f54a8a4134d3
child 58102 73f46283c247
separated listsum material
src/Doc/Main/Main_Doc.thy
src/HOL/Enum.thy
src/HOL/Groups_List.thy
src/HOL/List.thy
src/HOL/Random.thy
     1.1 --- a/src/Doc/Main/Main_Doc.thy	Sun Aug 31 09:10:41 2014 +0200
     1.2 +++ b/src/Doc/Main/Main_Doc.thy	Sun Aug 31 09:10:42 2014 +0200
     1.3 @@ -517,7 +517,7 @@
     1.4  @{const List.listrel1} & @{term_type_only List.listrel1 "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
     1.5  @{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\
     1.6  @{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\
     1.7 -@{const List.listsum} & @{typeof List.listsum}\\
     1.8 +@{const Groups_List.listsum} & @{typeof Groups_List.listsum}\\
     1.9  @{const List.list_all2} & @{typeof List.list_all2}\\
    1.10  @{const List.list_update} & @{typeof List.list_update}\\
    1.11  @{const List.map} & @{typeof List.map}\\
     2.1 --- a/src/HOL/Enum.thy	Sun Aug 31 09:10:41 2014 +0200
     2.2 +++ b/src/HOL/Enum.thy	Sun Aug 31 09:10:42 2014 +0200
     2.3 @@ -3,7 +3,7 @@
     2.4  header {* Finite types as explicit enumerations *}
     2.5  
     2.6  theory Enum
     2.7 -imports Map
     2.8 +imports Map Groups_List
     2.9  begin
    2.10  
    2.11  subsection {* Class @{text enum} *}
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Groups_List.thy	Sun Aug 31 09:10:42 2014 +0200
     3.3 @@ -0,0 +1,212 @@
     3.4 +
     3.5 +(* Author: Tobias Nipkow, TU Muenchen *)
     3.6 +
     3.7 +header {* Summation over lists *}
     3.8 +
     3.9 +theory Groups_List
    3.10 +imports List
    3.11 +begin
    3.12 +
    3.13 +definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where
    3.14 +"listsum xs = foldr plus xs 0"
    3.15 +
    3.16 +subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
    3.17 +
    3.18 +lemma (in monoid_add) listsum_simps [simp]:
    3.19 +  "listsum [] = 0"
    3.20 +  "listsum (x # xs) = x + listsum xs"
    3.21 +  by (simp_all add: listsum_def)
    3.22 +
    3.23 +lemma (in monoid_add) listsum_append [simp]:
    3.24 +  "listsum (xs @ ys) = listsum xs + listsum ys"
    3.25 +  by (induct xs) (simp_all add: add.assoc)
    3.26 +
    3.27 +lemma (in comm_monoid_add) listsum_rev [simp]:
    3.28 +  "listsum (rev xs) = listsum xs"
    3.29 +  by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff add_ac)
    3.30 +
    3.31 +lemma (in monoid_add) fold_plus_listsum_rev:
    3.32 +  "fold plus xs = plus (listsum (rev xs))"
    3.33 +proof
    3.34 +  fix x
    3.35 +  have "fold plus xs x = fold plus xs (x + 0)" by simp
    3.36 +  also have "\<dots> = fold plus (x # xs) 0" by simp
    3.37 +  also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_conv_fold)
    3.38 +  also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def)
    3.39 +  also have "\<dots> = listsum (rev xs) + listsum [x]" by simp
    3.40 +  finally show "fold plus xs x = listsum (rev xs) + x" by simp
    3.41 +qed
    3.42 +
    3.43 +text{* Some syntactic sugar for summing a function over a list: *}
    3.44 +
    3.45 +syntax
    3.46 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
    3.47 +syntax (xsymbols)
    3.48 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    3.49 +syntax (HTML output)
    3.50 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    3.51 +
    3.52 +translations -- {* Beware of argument permutation! *}
    3.53 +  "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
    3.54 +  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
    3.55 +
    3.56 +lemma (in comm_monoid_add) listsum_map_remove1:
    3.57 +  "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
    3.58 +  by (induct xs) (auto simp add: ac_simps)
    3.59 +
    3.60 +lemma (in monoid_add) size_list_conv_listsum:
    3.61 +  "size_list f xs = listsum (map f xs) + size xs"
    3.62 +  by (induct xs) auto
    3.63 +
    3.64 +lemma (in monoid_add) length_concat:
    3.65 +  "length (concat xss) = listsum (map length xss)"
    3.66 +  by (induct xss) simp_all
    3.67 +
    3.68 +lemma (in monoid_add) length_product_lists:
    3.69 +  "length (product_lists xss) = foldr op * (map length xss) 1"
    3.70 +proof (induct xss)
    3.71 +  case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
    3.72 +qed simp
    3.73 +
    3.74 +lemma (in monoid_add) listsum_map_filter:
    3.75 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
    3.76 +  shows "listsum (map f (filter P xs)) = listsum (map f xs)"
    3.77 +  using assms by (induct xs) auto
    3.78 +
    3.79 +lemma (in comm_monoid_add) distinct_listsum_conv_Setsum:
    3.80 +  "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
    3.81 +  by (induct xs) simp_all
    3.82 +
    3.83 +lemma listsum_eq_0_nat_iff_nat [simp]:
    3.84 +  "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
    3.85 +  by (induct ns) simp_all
    3.86 +
    3.87 +lemma member_le_listsum_nat:
    3.88 +  "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns"
    3.89 +  by (induct ns) auto
    3.90 +
    3.91 +lemma elem_le_listsum_nat:
    3.92 +  "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
    3.93 +  by (rule member_le_listsum_nat) simp
    3.94 +
    3.95 +lemma listsum_update_nat:
    3.96 +  "k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
    3.97 +apply(induct ns arbitrary:k)
    3.98 + apply (auto split:nat.split)
    3.99 +apply(drule elem_le_listsum_nat)
   3.100 +apply arith
   3.101 +done
   3.102 +
   3.103 +lemma (in monoid_add) listsum_triv:
   3.104 +  "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
   3.105 +  by (induct xs) (simp_all add: distrib_right)
   3.106 +
   3.107 +lemma (in monoid_add) listsum_0 [simp]:
   3.108 +  "(\<Sum>x\<leftarrow>xs. 0) = 0"
   3.109 +  by (induct xs) (simp_all add: distrib_right)
   3.110 +
   3.111 +text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
   3.112 +lemma (in ab_group_add) uminus_listsum_map:
   3.113 +  "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
   3.114 +  by (induct xs) simp_all
   3.115 +
   3.116 +lemma (in comm_monoid_add) listsum_addf:
   3.117 +  "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
   3.118 +  by (induct xs) (simp_all add: algebra_simps)
   3.119 +
   3.120 +lemma (in ab_group_add) listsum_subtractf:
   3.121 +  "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
   3.122 +  by (induct xs) (simp_all add: algebra_simps)
   3.123 +
   3.124 +lemma (in semiring_0) listsum_const_mult:
   3.125 +  "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
   3.126 +  by (induct xs) (simp_all add: algebra_simps)
   3.127 +
   3.128 +lemma (in semiring_0) listsum_mult_const:
   3.129 +  "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
   3.130 +  by (induct xs) (simp_all add: algebra_simps)
   3.131 +
   3.132 +lemma (in ordered_ab_group_add_abs) listsum_abs:
   3.133 +  "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
   3.134 +  by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])
   3.135 +
   3.136 +lemma listsum_mono:
   3.137 +  fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}"
   3.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)"
   3.139 +  by (induct xs) (simp, simp add: add_mono)
   3.140 +
   3.141 +lemma (in monoid_add) listsum_distinct_conv_setsum_set:
   3.142 +  "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
   3.143 +  by (induct xs) simp_all
   3.144 +
   3.145 +lemma (in monoid_add) interv_listsum_conv_setsum_set_nat:
   3.146 +  "listsum (map f [m..<n]) = setsum f (set [m..<n])"
   3.147 +  by (simp add: listsum_distinct_conv_setsum_set)
   3.148 +
   3.149 +lemma (in monoid_add) interv_listsum_conv_setsum_set_int:
   3.150 +  "listsum (map f [k..l]) = setsum f (set [k..l])"
   3.151 +  by (simp add: listsum_distinct_conv_setsum_set)
   3.152 +
   3.153 +text {* General equivalence between @{const listsum} and @{const setsum} *}
   3.154 +lemma (in monoid_add) listsum_setsum_nth:
   3.155 +  "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
   3.156 +  using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
   3.157 +
   3.158 +
   3.159 +subsection {* Further facts about @{const List.n_lists} *}
   3.160 +
   3.161 +lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
   3.162 +  by (induct n) (auto simp add: comp_def length_concat listsum_triv)
   3.163 +
   3.164 +lemma distinct_n_lists:
   3.165 +  assumes "distinct xs"
   3.166 +  shows "distinct (List.n_lists n xs)"
   3.167 +proof (rule card_distinct)
   3.168 +  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
   3.169 +  have "card (set (List.n_lists n xs)) = card (set xs) ^ n"
   3.170 +  proof (induct n)
   3.171 +    case 0 then show ?case by simp
   3.172 +  next
   3.173 +    case (Suc n)
   3.174 +    moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs)
   3.175 +      = (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
   3.176 +      by (rule card_UN_disjoint) auto
   3.177 +    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
   3.178 +      by (rule card_image) (simp add: inj_on_def)
   3.179 +    ultimately show ?case by auto
   3.180 +  qed
   3.181 +  also have "\<dots> = length xs ^ n" by (simp add: card_length)
   3.182 +  finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)"
   3.183 +    by (simp add: length_n_lists)
   3.184 +qed
   3.185 +
   3.186 +
   3.187 +subsection {* Tools setup *}
   3.188 +
   3.189 +lemma setsum_set_upto_conv_listsum_int [code_unfold]:
   3.190 +  "setsum f (set [i..j::int]) = listsum (map f [i..j])"
   3.191 +  by (simp add: interv_listsum_conv_setsum_set_int)
   3.192 +
   3.193 +lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
   3.194 +  "setsum f (set [m..<n]) = listsum (map f [m..<n])"
   3.195 +  by (simp add: interv_listsum_conv_setsum_set_nat)
   3.196 +
   3.197 +lemma setsum_code [code]:
   3.198 +  "setsum f (set xs) = listsum (map f (remdups xs))"
   3.199 +  by (simp add: listsum_distinct_conv_setsum_set)
   3.200 +
   3.201 +context
   3.202 +begin
   3.203 +
   3.204 +interpretation lifting_syntax .
   3.205 +
   3.206 +lemma listsum_transfer[transfer_rule]:
   3.207 +  assumes [transfer_rule]: "A 0 0"
   3.208 +  assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
   3.209 +  shows "(list_all2 A ===> A) listsum listsum"
   3.210 +  unfolding listsum_def[abs_def]
   3.211 +  by transfer_prover
   3.212 +
   3.213 +end
   3.214 +
   3.215 +end
   3.216 \ No newline at end of file
     4.1 --- a/src/HOL/List.thy	Sun Aug 31 09:10:41 2014 +0200
     4.2 +++ b/src/HOL/List.thy	Sun Aug 31 09:10:42 2014 +0200
     4.3 @@ -105,9 +105,6 @@
     4.4  "concat [] = []" |
     4.5  "concat (x # xs) = x @ concat xs"
     4.6  
     4.7 -definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where
     4.8 -"listsum xs = foldr plus xs 0"
     4.9 -
    4.10  primrec drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    4.11  drop_Nil: "drop n [] = []" |
    4.12  drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"
    4.13 @@ -313,8 +310,7 @@
    4.14  @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
    4.15  @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
    4.16  @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
    4.17 -@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
    4.18 -@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}
    4.19 +@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}
    4.20  \end{tabular}}
    4.21  \caption{Characteristic examples}
    4.22  \label{fig:Characteristic}
    4.23 @@ -3490,149 +3486,6 @@
    4.24        auto simp add: injD[OF assms])
    4.25  
    4.26  
    4.27 -subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
    4.28 -
    4.29 -lemma (in monoid_add) listsum_simps [simp]:
    4.30 -  "listsum [] = 0"
    4.31 -  "listsum (x # xs) = x + listsum xs"
    4.32 -  by (simp_all add: listsum_def)
    4.33 -
    4.34 -lemma (in monoid_add) listsum_append [simp]:
    4.35 -  "listsum (xs @ ys) = listsum xs + listsum ys"
    4.36 -  by (induct xs) (simp_all add: add.assoc)
    4.37 -
    4.38 -lemma (in comm_monoid_add) listsum_rev [simp]:
    4.39 -  "listsum (rev xs) = listsum xs"
    4.40 -  by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff ac_simps)
    4.41 -
    4.42 -lemma (in monoid_add) fold_plus_listsum_rev:
    4.43 -  "fold plus xs = plus (listsum (rev xs))"
    4.44 -proof
    4.45 -  fix x
    4.46 -  have "fold plus xs x = fold plus xs (x + 0)" by simp
    4.47 -  also have "\<dots> = fold plus (x # xs) 0" by simp
    4.48 -  also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_conv_fold)
    4.49 -  also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def)
    4.50 -  also have "\<dots> = listsum (rev xs) + listsum [x]" by simp
    4.51 -  finally show "fold plus xs x = listsum (rev xs) + x" by simp
    4.52 -qed
    4.53 -
    4.54 -text{* Some syntactic sugar for summing a function over a list: *}
    4.55 -
    4.56 -syntax
    4.57 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
    4.58 -syntax (xsymbols)
    4.59 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    4.60 -syntax (HTML output)
    4.61 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    4.62 -
    4.63 -translations -- {* Beware of argument permutation! *}
    4.64 -  "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
    4.65 -  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
    4.66 -
    4.67 -lemma (in comm_monoid_add) listsum_map_remove1:
    4.68 -  "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
    4.69 -  by (induct xs) (auto simp add: ac_simps)
    4.70 -
    4.71 -lemma (in monoid_add) size_list_conv_listsum:
    4.72 -  "size_list f xs = listsum (map f xs) + size xs"
    4.73 -  by (induct xs) auto
    4.74 -
    4.75 -lemma (in monoid_add) length_concat:
    4.76 -  "length (concat xss) = listsum (map length xss)"
    4.77 -  by (induct xss) simp_all
    4.78 -
    4.79 -lemma (in monoid_add) length_product_lists:
    4.80 -  "length (product_lists xss) = foldr op * (map length xss) 1"
    4.81 -proof (induct xss)
    4.82 -  case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
    4.83 -qed simp
    4.84 -
    4.85 -lemma (in monoid_add) listsum_map_filter:
    4.86 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
    4.87 -  shows "listsum (map f (filter P xs)) = listsum (map f xs)"
    4.88 -  using assms by (induct xs) auto
    4.89 -
    4.90 -lemma (in comm_monoid_add) distinct_listsum_conv_Setsum:
    4.91 -  "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
    4.92 -  by (induct xs) simp_all
    4.93 -
    4.94 -lemma listsum_eq_0_nat_iff_nat [simp]:
    4.95 -  "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
    4.96 -  by (induct ns) simp_all
    4.97 -
    4.98 -lemma member_le_listsum_nat:
    4.99 -  "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns"
   4.100 -  by (induct ns) auto
   4.101 -
   4.102 -lemma elem_le_listsum_nat:
   4.103 -  "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
   4.104 -  by (rule member_le_listsum_nat) simp
   4.105 -
   4.106 -lemma listsum_update_nat:
   4.107 -  "k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
   4.108 -apply(induct ns arbitrary:k)
   4.109 - apply (auto split:nat.split)
   4.110 -apply(drule elem_le_listsum_nat)
   4.111 -apply arith
   4.112 -done
   4.113 -
   4.114 -lemma (in monoid_add) listsum_triv:
   4.115 -  "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
   4.116 -  by (induct xs) (simp_all add: distrib_right)
   4.117 -
   4.118 -lemma (in monoid_add) listsum_0 [simp]:
   4.119 -  "(\<Sum>x\<leftarrow>xs. 0) = 0"
   4.120 -  by (induct xs) (simp_all add: distrib_right)
   4.121 -
   4.122 -text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
   4.123 -lemma (in ab_group_add) uminus_listsum_map:
   4.124 -  "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
   4.125 -  by (induct xs) simp_all
   4.126 -
   4.127 -lemma (in comm_monoid_add) listsum_addf:
   4.128 -  "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
   4.129 -  by (induct xs) (simp_all add: algebra_simps)
   4.130 -
   4.131 -lemma (in ab_group_add) listsum_subtractf:
   4.132 -  "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
   4.133 -  by (induct xs) (simp_all add: algebra_simps)
   4.134 -
   4.135 -lemma (in semiring_0) listsum_const_mult:
   4.136 -  "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
   4.137 -  by (induct xs) (simp_all add: algebra_simps)
   4.138 -
   4.139 -lemma (in semiring_0) listsum_mult_const:
   4.140 -  "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
   4.141 -  by (induct xs) (simp_all add: algebra_simps)
   4.142 -
   4.143 -lemma (in ordered_ab_group_add_abs) listsum_abs:
   4.144 -  "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
   4.145 -  by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])
   4.146 -
   4.147 -lemma listsum_mono:
   4.148 -  fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}"
   4.149 -  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)"
   4.150 -  by (induct xs) (simp, simp add: add_mono)
   4.151 -
   4.152 -lemma (in monoid_add) listsum_distinct_conv_setsum_set:
   4.153 -  "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
   4.154 -  by (induct xs) simp_all
   4.155 -
   4.156 -lemma (in monoid_add) interv_listsum_conv_setsum_set_nat:
   4.157 -  "listsum (map f [m..<n]) = setsum f (set [m..<n])"
   4.158 -  by (simp add: listsum_distinct_conv_setsum_set)
   4.159 -
   4.160 -lemma (in monoid_add) interv_listsum_conv_setsum_set_int:
   4.161 -  "listsum (map f [k..l]) = setsum f (set [k..l])"
   4.162 -  by (simp add: listsum_distinct_conv_setsum_set)
   4.163 -
   4.164 -text {* General equivalence between @{const listsum} and @{const setsum} *}
   4.165 -lemma (in monoid_add) listsum_setsum_nth:
   4.166 -  "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
   4.167 -  using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
   4.168 -
   4.169 -
   4.170  subsubsection {* @{const insert} *}
   4.171  
   4.172  lemma in_set_insert [simp]:
   4.173 @@ -4314,9 +4167,6 @@
   4.174  lemma n_lists_Nil [simp]: "List.n_lists n [] = (if n = 0 then [[]] else [])"
   4.175    by (induct n) simp_all
   4.176  
   4.177 -lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
   4.178 -  by (induct n) (auto simp add: length_concat o_def listsum_triv)
   4.179 -
   4.180  lemma length_n_lists_elem: "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
   4.181    by (induct n arbitrary: ys) auto
   4.182  
   4.183 @@ -4335,28 +4185,6 @@
   4.184    qed
   4.185  qed
   4.186  
   4.187 -lemma distinct_n_lists:
   4.188 -  assumes "distinct xs"
   4.189 -  shows "distinct (List.n_lists n xs)"
   4.190 -proof (rule card_distinct)
   4.191 -  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
   4.192 -  have "card (set (List.n_lists n xs)) = card (set xs) ^ n"
   4.193 -  proof (induct n)
   4.194 -    case 0 then show ?case by simp
   4.195 -  next
   4.196 -    case (Suc n)
   4.197 -    moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs)
   4.198 -      = (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
   4.199 -      by (rule card_UN_disjoint) auto
   4.200 -    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
   4.201 -      by (rule card_image) (simp add: inj_on_def)
   4.202 -    ultimately show ?case by auto
   4.203 -  qed
   4.204 -  also have "\<dots> = length xs ^ n" by (simp add: card_length)
   4.205 -  finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)"
   4.206 -    by (simp add: length_n_lists)
   4.207 -qed
   4.208 -
   4.209  
   4.210  subsubsection {* @{const splice} *}
   4.211  
   4.212 @@ -6264,10 +6092,6 @@
   4.213    "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
   4.214    by auto
   4.215  
   4.216 -lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
   4.217 -  "setsum f (set [m..<n]) = listsum (map f [m..<n])"
   4.218 -  by (simp add: interv_listsum_conv_setsum_set_nat)
   4.219 -
   4.220  text{* Bounded @{text LEAST} operator: *}
   4.221  
   4.222  definition "Bleast S P = (LEAST x. x \<in> S \<and> P x)"
   4.223 @@ -6315,10 +6139,6 @@
   4.224  
   4.225  lemmas atLeastAtMost_upto [code_unfold] = set_upto [symmetric]
   4.226  
   4.227 -lemma setsum_set_upto_conv_listsum_int [code_unfold]:
   4.228 -  "setsum f (set [i..j::int]) = listsum (map f [i..j])"
   4.229 -  by (simp add: interv_listsum_conv_setsum_set_int)
   4.230 -
   4.231  
   4.232  subsubsection {* Optimizing by rewriting *}
   4.233  
   4.234 @@ -6629,10 +6449,6 @@
   4.235    "Pow (set (x # xs)) = (let A = Pow (set xs) in A \<union> insert x ` A)"
   4.236    by (simp_all add: Pow_insert Let_def)
   4.237  
   4.238 -lemma setsum_code [code]:
   4.239 -  "setsum f (set xs) = listsum (map f (remdups xs))"
   4.240 -by (simp add: listsum_distinct_conv_setsum_set)
   4.241 -
   4.242  definition map_project :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a set \<Rightarrow> 'b set" where
   4.243    "map_project f A = {b. \<exists> a \<in> A. f a = Some b}"
   4.244  
   4.245 @@ -6883,13 +6699,6 @@
   4.246    apply (erule_tac xs=x in list_all2_induct, simp, simp add: rel_fun_def)
   4.247    done
   4.248  
   4.249 -lemma listsum_transfer[transfer_rule]:
   4.250 -  assumes [transfer_rule]: "A 0 0"
   4.251 -  assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
   4.252 -  shows "(list_all2 A ===> A) listsum listsum"
   4.253 -  unfolding listsum_def[abs_def]
   4.254 -  by transfer_prover
   4.255 -
   4.256  lemma rtrancl_parametric [transfer_rule]:
   4.257    assumes [transfer_rule]: "bi_unique A" "bi_total A"
   4.258    shows "(rel_set (rel_prod A A) ===> rel_set (rel_prod A A)) rtrancl rtrancl"
     5.1 --- a/src/HOL/Random.thy	Sun Aug 31 09:10:41 2014 +0200
     5.2 +++ b/src/HOL/Random.thy	Sun Aug 31 09:10:42 2014 +0200
     5.3 @@ -4,7 +4,7 @@
     5.4  header {* A HOL random engine *}
     5.5  
     5.6  theory Random
     5.7 -imports List
     5.8 +imports List Groups_List
     5.9  begin
    5.10  
    5.11  notation fcomp (infixl "\<circ>>" 60)