1.1 --- a/src/HOL/Library/More_List.thy Tue Sep 28 15:34:30 2010 +0200
1.2 +++ b/src/HOL/Library/More_List.thy Tue Sep 28 15:34:47 2010 +0200
1.3 @@ -16,7 +16,6 @@
1.4 declare (in linorder) Max_fin_set_fold [code_unfold del]
1.5 declare (in complete_lattice) Inf_set_fold [code_unfold del]
1.6 declare (in complete_lattice) Sup_set_fold [code_unfold del]
1.7 -declare rev_foldl_cons [code del]
1.8
1.9 text {* Fold combinator with canonical argument order *}
1.10
1.11 @@ -101,11 +100,11 @@
1.12 "fold plus xs = plus (listsum (rev xs))"
1.13 by (induct xs) (simp_all add: add.assoc)
1.14
1.15 -lemma listsum_conv_foldr [code]:
1.16 - "listsum xs = foldr plus xs 0"
1.17 - by (fact listsum_foldr)
1.18 +lemma (in monoid_add) listsum_conv_fold [code]:
1.19 + "listsum xs = fold (\<lambda>x y. y + x) xs 0"
1.20 + by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
1.21
1.22 -lemma sort_key_conv_fold:
1.23 +lemma (in linorder) sort_key_conv_fold:
1.24 assumes "inj_on f (set xs)"
1.25 shows "sort_key f xs = fold (insort_key f) xs []"
1.26 proof -
1.27 @@ -115,13 +114,14 @@
1.28 fix x y
1.29 assume "x \<in> set xs" "y \<in> set xs"
1.30 with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
1.31 + have **: "x = y \<longleftrightarrow> y = x" by auto
1.32 show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
1.33 - by (induct zs) (auto dest: *)
1.34 + by (induct zs) (auto intro: * simp add: **)
1.35 qed
1.36 then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
1.37 qed
1.38
1.39 -lemma sort_conv_fold:
1.40 +lemma (in linorder) sort_conv_fold:
1.41 "sort xs = fold insort xs []"
1.42 by (rule sort_key_conv_fold) simp
1.43
2.1 --- a/src/HOL/List.thy Tue Sep 28 15:34:30 2010 +0200
2.2 +++ b/src/HOL/List.thy Tue Sep 28 15:34:47 2010 +0200
2.3 @@ -94,10 +94,9 @@
2.4 "concat [] = []"
2.5 | "concat (x # xs) = x @ concat xs"
2.6
2.7 -primrec (in monoid_add)
2.8 +definition (in monoid_add)
2.9 listsum :: "'a list \<Rightarrow> 'a" where
2.10 - "listsum [] = 0"
2.11 - | "listsum (x # xs) = x + listsum xs"
2.12 + "listsum xs = foldr plus xs 0"
2.13
2.14 primrec
2.15 drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
2.16 @@ -261,7 +260,7 @@
2.17 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number')}\\
2.18 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\
2.19 @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\
2.20 -@{lemma "listsum [1,2,3::nat] = 6" by simp}
2.21 +@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}
2.22 \end{tabular}}
2.23 \caption{Characteristic examples}
2.24 \label{fig:Characteristic}
2.25 @@ -2369,27 +2368,30 @@
2.26 qed
2.27
2.28
2.29 +text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
2.30 +
2.31 +lemma foldr_foldl:
2.32 + "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
2.33 + by (induct xs) auto
2.34 +
2.35 +lemma foldl_foldr:
2.36 + "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
2.37 + by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
2.38 +
2.39 +
2.40 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
2.41
2.42 -lemma foldl_foldr1_lemma:
2.43 - "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
2.44 -by (induct xs arbitrary: a) (auto simp:add_assoc)
2.45 -
2.46 -corollary foldl_foldr1:
2.47 - "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
2.48 -by (simp add:foldl_foldr1_lemma)
2.49 -
2.50 -
2.51 -text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
2.52 -
2.53 -lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
2.54 -by (induct xs) auto
2.55 -
2.56 -lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
2.57 -by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
2.58 -
2.59 -lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
2.60 - by (induct xs, auto simp add: foldl_assoc add_commute)
2.61 +lemma (in monoid_add) foldl_foldr1_lemma:
2.62 + "foldl op + a xs = a + foldr op + xs 0"
2.63 + by (induct xs arbitrary: a) (auto simp: add_assoc)
2.64 +
2.65 +corollary (in monoid_add) foldl_foldr1:
2.66 + "foldl op + 0 xs = foldr op + xs 0"
2.67 + by (simp add: foldl_foldr1_lemma)
2.68 +
2.69 +lemma (in ab_semigroup_add) foldr_conv_foldl:
2.70 + "foldr op + xs a = foldl op + a xs"
2.71 + by (induct xs) (simp_all add: foldl_assoc add.commute)
2.72
2.73 text {*
2.74 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
2.75 @@ -2869,56 +2871,57 @@
2.76
2.77 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
2.78
2.79 -lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
2.80 -by (induct xs) (simp_all add:add_assoc)
2.81 -
2.82 -lemma listsum_rev [simp]:
2.83 - fixes xs :: "'a\<Colon>comm_monoid_add list"
2.84 - shows "listsum (rev xs) = listsum xs"
2.85 -by (induct xs) (simp_all add:add_ac)
2.86 -
2.87 -lemma listsum_map_remove1:
2.88 -fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
2.89 -shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
2.90 -by (induct xs)(auto simp add:add_ac)
2.91 -
2.92 -lemma list_size_conv_listsum:
2.93 +lemma (in monoid_add) listsum_foldl [code]:
2.94 + "listsum = foldl (op +) 0"
2.95 + by (simp add: listsum_def foldl_foldr1 fun_eq_iff)
2.96 +
2.97 +lemma (in monoid_add) listsum_simps [simp]:
2.98 + "listsum [] = 0"
2.99 + "listsum (x#xs) = x + listsum xs"
2.100 + by (simp_all add: listsum_def)
2.101 +
2.102 +lemma (in monoid_add) listsum_append [simp]:
2.103 + "listsum (xs @ ys) = listsum xs + listsum ys"
2.104 + by (induct xs) (simp_all add: add.assoc)
2.105 +
2.106 +lemma (in comm_monoid_add) listsum_rev [simp]:
2.107 + "listsum (rev xs) = listsum xs"
2.108 + by (simp add: listsum_def [of "rev xs"]) (simp add: listsum_foldl foldr_foldl add.commute)
2.109 +
2.110 +lemma (in comm_monoid_add) listsum_map_remove1:
2.111 + "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
2.112 + by (induct xs) (auto simp add: ac_simps)
2.113 +
2.114 +lemma (in monoid_add) list_size_conv_listsum:
2.115 "list_size f xs = listsum (map f xs) + size xs"
2.116 -by(induct xs) auto
2.117 -
2.118 -lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
2.119 -by (induct xs) auto
2.120 -
2.121 -lemma length_concat: "length (concat xss) = listsum (map length xss)"
2.122 -by (induct xss) simp_all
2.123 -
2.124 -lemma listsum_map_filter:
2.125 - fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"
2.126 - assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"
2.127 + by (induct xs) auto
2.128 +
2.129 +lemma (in monoid_add) length_concat:
2.130 + "length (concat xss) = listsum (map length xss)"
2.131 + by (induct xss) simp_all
2.132 +
2.133 +lemma (in monoid_add) listsum_map_filter:
2.134 + assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
2.135 shows "listsum (map f (filter P xs)) = listsum (map f xs)"
2.136 -using assms by (induct xs) auto
2.137 -
2.138 -text{* For efficient code generation ---
2.139 - @{const listsum} is not tail recursive but @{const foldl} is. *}
2.140 -lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
2.141 -by(simp add:listsum_foldr foldl_foldr1)
2.142 -
2.143 -lemma distinct_listsum_conv_Setsum:
2.144 - "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
2.145 -by (induct xs) simp_all
2.146 -
2.147 -lemma listsum_eq_0_nat_iff_nat[simp]:
2.148 - "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"
2.149 -by(simp add: listsum)
2.150 -
2.151 -lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> ns!k <= listsum(ns::nat list)"
2.152 + using assms by (induct xs) auto
2.153 +
2.154 +lemma (in monoid_add) distinct_listsum_conv_Setsum:
2.155 + "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
2.156 + by (induct xs) simp_all
2.157 +
2.158 +lemma listsum_eq_0_nat_iff_nat [simp]:
2.159 + "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
2.160 + by (simp add: listsum_foldl)
2.161 +
2.162 +lemma elem_le_listsum_nat:
2.163 + "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
2.164 apply(induct ns arbitrary: k)
2.165 apply simp
2.166 apply(fastsimp simp add:nth_Cons split: nat.split)
2.167 done
2.168
2.169 -lemma listsum_update_nat: "k<size ns \<Longrightarrow>
2.170 - listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k"
2.171 +lemma listsum_update_nat:
2.172 + "k<size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
2.173 apply(induct ns arbitrary:k)
2.174 apply (auto split:nat.split)
2.175 apply(drule elem_le_listsum_nat)
2.176 @@ -2938,62 +2941,58 @@
2.177 "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
2.178 "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
2.179
2.180 -lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
2.181 +lemma (in monoid_add) listsum_triv:
2.182 + "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
2.183 by (induct xs) (simp_all add: left_distrib)
2.184
2.185 -lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
2.186 +lemma (in monoid_add) listsum_0 [simp]:
2.187 + "(\<Sum>x\<leftarrow>xs. 0) = 0"
2.188 by (induct xs) (simp_all add: left_distrib)
2.189
2.190 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
2.191 -lemma uminus_listsum_map:
2.192 - fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
2.193 - shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
2.194 -by (induct xs) simp_all
2.195 -
2.196 -lemma listsum_addf:
2.197 - fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
2.198 - shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
2.199 -by (induct xs) (simp_all add: algebra_simps)
2.200 -
2.201 -lemma listsum_subtractf:
2.202 - fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
2.203 - shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
2.204 -by (induct xs) simp_all
2.205 -
2.206 -lemma listsum_const_mult:
2.207 - fixes f :: "'a \<Rightarrow> 'b::semiring_0"
2.208 - shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
2.209 -by (induct xs, simp_all add: algebra_simps)
2.210 -
2.211 -lemma listsum_mult_const:
2.212 - fixes f :: "'a \<Rightarrow> 'b::semiring_0"
2.213 - shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
2.214 -by (induct xs, simp_all add: algebra_simps)
2.215 -
2.216 -lemma listsum_abs:
2.217 - fixes xs :: "'a::ordered_ab_group_add_abs list"
2.218 - shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
2.219 -by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
2.220 +lemma (in ab_group_add) uminus_listsum_map:
2.221 + "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
2.222 + by (induct xs) simp_all
2.223 +
2.224 +lemma (in comm_monoid_add) listsum_addf:
2.225 + "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
2.226 + by (induct xs) (simp_all add: algebra_simps)
2.227 +
2.228 +lemma (in ab_group_add) listsum_subtractf:
2.229 + "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
2.230 + by (induct xs) (simp_all add: algebra_simps)
2.231 +
2.232 +lemma (in semiring_0) listsum_const_mult:
2.233 + "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
2.234 + by (induct xs) (simp_all add: algebra_simps)
2.235 +
2.236 +lemma (in semiring_0) listsum_mult_const:
2.237 + "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
2.238 + by (induct xs) (simp_all add: algebra_simps)
2.239 +
2.240 +lemma (in ordered_ab_group_add_abs) listsum_abs:
2.241 + "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
2.242 + by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])
2.243
2.244 lemma listsum_mono:
2.245 - fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}"
2.246 + fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}"
2.247 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)"
2.248 -by (induct xs, simp, simp add: add_mono)
2.249 -
2.250 -lemma listsum_distinct_conv_setsum_set:
2.251 + by (induct xs) (simp, simp add: add_mono)
2.252 +
2.253 +lemma (in monoid_add) listsum_distinct_conv_setsum_set:
2.254 "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
2.255 by (induct xs) simp_all
2.256
2.257 -lemma interv_listsum_conv_setsum_set_nat:
2.258 +lemma (in monoid_add) interv_listsum_conv_setsum_set_nat:
2.259 "listsum (map f [m..<n]) = setsum f (set [m..<n])"
2.260 by (simp add: listsum_distinct_conv_setsum_set)
2.261
2.262 -lemma interv_listsum_conv_setsum_set_int:
2.263 +lemma (in monoid_add) interv_listsum_conv_setsum_set_int:
2.264 "listsum (map f [k..l]) = setsum f (set [k..l])"
2.265 by (simp add: listsum_distinct_conv_setsum_set)
2.266
2.267 text {* General equivalence between @{const listsum} and @{const setsum} *}
2.268 -lemma listsum_setsum_nth:
2.269 +lemma (in monoid_add) listsum_setsum_nth:
2.270 "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
2.271 using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
2.272