summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Tue, 28 Sep 2010 15:34:47 +0200 | |

changeset 39775 | e4c85d8c2aba |

parent 39772 | 5d5fd2baf99d (current diff) |

parent 39774 | 30cf9d80939e (diff) |

child 39776 | cde508d2eac8 |

merged

--- a/src/HOL/Library/More_List.thy Tue Sep 28 15:34:30 2010 +0200 +++ b/src/HOL/Library/More_List.thy Tue Sep 28 15:34:47 2010 +0200 @@ -16,7 +16,6 @@ declare (in linorder) Max_fin_set_fold [code_unfold del] declare (in complete_lattice) Inf_set_fold [code_unfold del] declare (in complete_lattice) Sup_set_fold [code_unfold del] -declare rev_foldl_cons [code del] text {* Fold combinator with canonical argument order *} @@ -101,11 +100,11 @@ "fold plus xs = plus (listsum (rev xs))" by (induct xs) (simp_all add: add.assoc) -lemma listsum_conv_foldr [code]: - "listsum xs = foldr plus xs 0" - by (fact listsum_foldr) +lemma (in monoid_add) listsum_conv_fold [code]: + "listsum xs = fold (\<lambda>x y. y + x) xs 0" + by (auto simp add: listsum_foldl foldl_fold fun_eq_iff) -lemma sort_key_conv_fold: +lemma (in linorder) sort_key_conv_fold: assumes "inj_on f (set xs)" shows "sort_key f xs = fold (insort_key f) xs []" proof - @@ -115,13 +114,14 @@ fix x y assume "x \<in> set xs" "y \<in> set xs" with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD) + have **: "x = y \<longleftrightarrow> y = x" by auto show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs" - by (induct zs) (auto dest: *) + by (induct zs) (auto intro: * simp add: **) qed then show ?thesis by (simp add: sort_key_def foldr_fold_rev) qed -lemma sort_conv_fold: +lemma (in linorder) sort_conv_fold: "sort xs = fold insort xs []" by (rule sort_key_conv_fold) simp

--- a/src/HOL/List.thy Tue Sep 28 15:34:30 2010 +0200 +++ b/src/HOL/List.thy Tue Sep 28 15:34:47 2010 +0200 @@ -94,10 +94,9 @@ "concat [] = []" | "concat (x # xs) = x @ concat xs" -primrec (in monoid_add) +definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where - "listsum [] = 0" - | "listsum (x # xs) = x + listsum xs" + "listsum xs = foldr plus xs 0" primrec drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where @@ -261,7 +260,7 @@ @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number')}\\ @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\ @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\ -@{lemma "listsum [1,2,3::nat] = 6" by simp} +@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)} \end{tabular}} \caption{Characteristic examples} \label{fig:Characteristic} @@ -2369,27 +2368,30 @@ qed +text{* The ``Third Duality Theorem'' in Bird \& Wadler: *} + +lemma foldr_foldl: + "foldr f xs a = foldl (%x y. f y x) a (rev xs)" + by (induct xs) auto + +lemma foldl_foldr: + "foldl f a xs = foldr (%x y. f y x) (rev xs) a" + by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"]) + + text{* The ``First Duality Theorem'' in Bird \& Wadler: *} -lemma foldl_foldr1_lemma: - "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)" -by (induct xs arbitrary: a) (auto simp:add_assoc) - -corollary foldl_foldr1: - "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)" -by (simp add:foldl_foldr1_lemma) - - -text{* The ``Third Duality Theorem'' in Bird \& Wadler: *} - -lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)" -by (induct xs) auto - -lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a" -by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"]) - -lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs" - by (induct xs, auto simp add: foldl_assoc add_commute) +lemma (in monoid_add) foldl_foldr1_lemma: + "foldl op + a xs = a + foldr op + xs 0" + by (induct xs arbitrary: a) (auto simp: add_assoc) + +corollary (in monoid_add) foldl_foldr1: + "foldl op + 0 xs = foldr op + xs 0" + by (simp add: foldl_foldr1_lemma) + +lemma (in ab_semigroup_add) foldr_conv_foldl: + "foldr op + xs a = foldl op + a xs" + by (induct xs) (simp_all add: foldl_assoc add.commute) text {* Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more @@ -2869,56 +2871,57 @@ subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*} -lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys" -by (induct xs) (simp_all add:add_assoc) - -lemma listsum_rev [simp]: - fixes xs :: "'a\<Colon>comm_monoid_add list" - shows "listsum (rev xs) = listsum xs" -by (induct xs) (simp_all add:add_ac) - -lemma listsum_map_remove1: -fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)" -shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))" -by (induct xs)(auto simp add:add_ac) - -lemma list_size_conv_listsum: +lemma (in monoid_add) listsum_foldl [code]: + "listsum = foldl (op +) 0" + by (simp add: listsum_def foldl_foldr1 fun_eq_iff) + +lemma (in monoid_add) listsum_simps [simp]: + "listsum [] = 0" + "listsum (x#xs) = x + listsum xs" + by (simp_all add: listsum_def) + +lemma (in monoid_add) listsum_append [simp]: + "listsum (xs @ ys) = listsum xs + listsum ys" + by (induct xs) (simp_all add: add.assoc) + +lemma (in comm_monoid_add) listsum_rev [simp]: + "listsum (rev xs) = listsum xs" + by (simp add: listsum_def [of "rev xs"]) (simp add: listsum_foldl foldr_foldl add.commute) + +lemma (in comm_monoid_add) listsum_map_remove1: + "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))" + by (induct xs) (auto simp add: ac_simps) + +lemma (in monoid_add) list_size_conv_listsum: "list_size f xs = listsum (map f xs) + size xs" -by(induct xs) auto - -lemma listsum_foldr: "listsum xs = foldr (op +) xs 0" -by (induct xs) auto - -lemma length_concat: "length (concat xss) = listsum (map length xss)" -by (induct xss) simp_all - -lemma listsum_map_filter: - fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add" - assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0" + by (induct xs) auto + +lemma (in monoid_add) length_concat: + "length (concat xss) = listsum (map length xss)" + by (induct xss) simp_all + +lemma (in monoid_add) listsum_map_filter: + assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0" shows "listsum (map f (filter P xs)) = listsum (map f xs)" -using assms by (induct xs) auto - -text{* For efficient code generation --- - @{const listsum} is not tail recursive but @{const foldl} is. *} -lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs" -by(simp add:listsum_foldr foldl_foldr1) - -lemma distinct_listsum_conv_Setsum: - "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)" -by (induct xs) simp_all - -lemma listsum_eq_0_nat_iff_nat[simp]: - "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)" -by(simp add: listsum) - -lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> ns!k <= listsum(ns::nat list)" + using assms by (induct xs) auto + +lemma (in monoid_add) distinct_listsum_conv_Setsum: + "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)" + by (induct xs) simp_all + +lemma listsum_eq_0_nat_iff_nat [simp]: + "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)" + by (simp add: listsum_foldl) + +lemma elem_le_listsum_nat: + "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)" apply(induct ns arbitrary: k) apply simp apply(fastsimp simp add:nth_Cons split: nat.split) done -lemma listsum_update_nat: "k<size ns \<Longrightarrow> - listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k" +lemma listsum_update_nat: + "k<size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k" apply(induct ns arbitrary:k) apply (auto split:nat.split) apply(drule elem_le_listsum_nat) @@ -2938,62 +2941,58 @@ "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)" "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)" -lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" +lemma (in monoid_add) listsum_triv: + "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" by (induct xs) (simp_all add: left_distrib) -lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0" +lemma (in monoid_add) listsum_0 [simp]: + "(\<Sum>x\<leftarrow>xs. 0) = 0" by (induct xs) (simp_all add: left_distrib) text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *} -lemma uminus_listsum_map: - fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add" - shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))" -by (induct xs) simp_all - -lemma listsum_addf: - fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add" - shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)" -by (induct xs) (simp_all add: algebra_simps) - -lemma listsum_subtractf: - fixes f g :: "'a \<Rightarrow> 'b::ab_group_add" - shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)" -by (induct xs) simp_all - -lemma listsum_const_mult: - fixes f :: "'a \<Rightarrow> 'b::semiring_0" - shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)" -by (induct xs, simp_all add: algebra_simps) - -lemma listsum_mult_const: - fixes f :: "'a \<Rightarrow> 'b::semiring_0" - shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c" -by (induct xs, simp_all add: algebra_simps) - -lemma listsum_abs: - fixes xs :: "'a::ordered_ab_group_add_abs list" - shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)" -by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq]) +lemma (in ab_group_add) uminus_listsum_map: + "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)" + by (induct xs) simp_all + +lemma (in comm_monoid_add) listsum_addf: + "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)" + by (induct xs) (simp_all add: algebra_simps) + +lemma (in ab_group_add) listsum_subtractf: + "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)" + by (induct xs) (simp_all add: algebra_simps) + +lemma (in semiring_0) listsum_const_mult: + "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)" + by (induct xs) (simp_all add: algebra_simps) + +lemma (in semiring_0) listsum_mult_const: + "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c" + by (induct xs) (simp_all add: algebra_simps) + +lemma (in ordered_ab_group_add_abs) listsum_abs: + "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)" + by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq]) lemma listsum_mono: - fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}" + fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}" 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)" -by (induct xs, simp, simp add: add_mono) - -lemma listsum_distinct_conv_setsum_set: + by (induct xs) (simp, simp add: add_mono) + +lemma (in monoid_add) listsum_distinct_conv_setsum_set: "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)" by (induct xs) simp_all -lemma interv_listsum_conv_setsum_set_nat: +lemma (in monoid_add) interv_listsum_conv_setsum_set_nat: "listsum (map f [m..<n]) = setsum f (set [m..<n])" by (simp add: listsum_distinct_conv_setsum_set) -lemma interv_listsum_conv_setsum_set_int: +lemma (in monoid_add) interv_listsum_conv_setsum_set_int: "listsum (map f [k..l]) = setsum f (set [k..l])" by (simp add: listsum_distinct_conv_setsum_set) text {* General equivalence between @{const listsum} and @{const setsum} *} -lemma listsum_setsum_nth: +lemma (in monoid_add) listsum_setsum_nth: "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)" using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)