summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/List.thy

changeset 46133 | d9fe85d3d2cd |

parent 46125 | 00cd193a48dc |

child 46138 | 85f8d8a8c711 |

--- a/src/HOL/List.thy Fri Jan 06 10:19:49 2012 +0100 +++ b/src/HOL/List.thy Fri Jan 06 10:19:49 2012 +0100 @@ -49,6 +49,10 @@ "set [] = {}" | "set (x # xs) = insert x (set xs)" +definition + coset :: "'a list \<Rightarrow> 'a set" where + [simp]: "coset xs = - set xs" + primrec map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where "map f [] = []" @@ -81,15 +85,18 @@ syntax (HTML output) "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") -primrec +primrec -- {* canonical argument order *} + fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where + "fold f [] = id" + | "fold f (x # xs) = fold f xs \<circ> f x" + +definition + foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where + [code_abbrev]: "foldr f xs = fold f (rev xs)" + +definition foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where - foldl_Nil: "foldl f a [] = a" - | foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs" - -primrec - foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where - "foldr f [] a = a" - | "foldr f (x # xs) a = f x (foldr f xs a)" + "foldl f s xs = fold (\<lambda>x s. f s x) xs s" primrec concat:: "'a list list \<Rightarrow> 'a list" where @@ -236,8 +243,9 @@ @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\ @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\ @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\ -@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\ -@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\ +@{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\ +@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by (simp add: foldr_def)}\\ +@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by (simp add: foldl_def)}\\ @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\ @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\ @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ @@ -261,7 +269,7 @@ @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def eval_nat_numeral)}\\ @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\ @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\ -@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)} +@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)} \end{tabular}} \caption{Characteristic examples} \label{fig:Characteristic} @@ -298,11 +306,11 @@ by simp_all primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where -"insort_key f x [] = [x]" | -"insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))" + "insort_key f x [] = [x]" | + "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))" definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where -"sort_key f xs = foldr (insort_key f) xs []" + "sort_key f xs = foldr (insort_key f) xs []" definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where "insort_insert_key f x xs = (if f x \<in> f ` set xs then xs else insort_key f x xs)" @@ -470,6 +478,9 @@ simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *} +code_datatype set coset + +hide_const (open) coset subsubsection {* @{const Nil} and @{const Cons} *} @@ -2368,159 +2379,81 @@ by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong) -subsubsection {* @{text foldl} and @{text foldr} *} - -lemma foldl_append [simp]: - "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys" -by (induct xs arbitrary: a) auto - -lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)" -by (induct xs) auto - -lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a" -by(induct xs) simp_all - -text{* For efficient code generation: avoid intermediate list. *} -lemma foldl_map[code_unfold]: - "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs" -by(induct xs arbitrary:a) simp_all - -lemma foldl_apply: - assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x" - shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)" - by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_iff) - -lemma foldl_cong [fundef_cong]: - "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] - ==> foldl f a l = foldl g b k" -by (induct k arbitrary: a b l) simp_all - -lemma foldr_cong [fundef_cong]: - "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] - ==> foldr f l a = foldr g k b" -by (induct k arbitrary: a b l) simp_all - -lemma foldl_fun_comm: - assumes "\<And>x y s. f (f s x) y = f (f s y) x" - shows "f (foldl f s xs) x = foldl f (f s x) xs" - by (induct xs arbitrary: s) - (simp_all add: assms) - -lemma (in semigroup_add) foldl_assoc: -shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)" -by (induct zs arbitrary: y) (simp_all add:add_assoc) - -lemma (in monoid_add) foldl_absorb0: -shows "x + (foldl op+ 0 zs) = foldl op+ x zs" -by (induct zs) (simp_all add:foldl_assoc) - -lemma foldl_rev: - assumes "\<And>x y s. f (f s x) y = f (f s y) x" - shows "foldl f s (rev xs) = foldl f s xs" -proof (induct xs arbitrary: s) - case Nil then show ?case by simp -next - case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm) -qed - -lemma rev_foldl_cons [code]: - "rev xs = foldl (\<lambda>xs x. x # xs) [] xs" -proof (induct xs) - case Nil then show ?case by simp -next - case Cons - { - fix x xs ys - have "foldl (\<lambda>xs x. x # xs) ys xs @ [x] - = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs" - by (induct xs arbitrary: ys) auto - } - note aux = this - show ?case by (induct xs) (auto simp add: Cons aux) +subsubsection {* @{const fold} with canonical argument order *} + +lemma fold_remove1_split: + assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" + and x: "x \<in> set xs" + shows "fold f xs = fold f (remove1 x xs) \<circ> f x" + using assms by (induct xs) (auto simp add: o_assoc [symmetric]) + +lemma fold_cong [fundef_cong]: + "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x) + \<Longrightarrow> fold f xs a = fold g ys b" + by (induct ys arbitrary: a b xs) simp_all + +lemma fold_id: + assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id" + shows "fold f xs = id" + using assms by (induct xs) simp_all + +lemma fold_commute: + assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h" + shows "h \<circ> fold g xs = fold f xs \<circ> h" + using assms by (induct xs) (simp_all add: fun_eq_iff) + +lemma fold_commute_apply: + assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h" + shows "h (fold g xs s) = fold f xs (h s)" +proof - + from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute) + then show ?thesis by (simp add: fun_eq_iff) 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 (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 -difficult to use because it requires an additional transitivity step. -*} - -lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns" -by (induct ns arbitrary: n) auto - -lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns" -by (force intro: start_le_sum simp add: in_set_conv_decomp) - -lemma sum_eq_0_conv [iff]: - "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))" -by (induct ns arbitrary: m) auto - -lemma foldr_invariant: - "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f x y) \<rbrakk> \<Longrightarrow> Q (foldr f xs x)" - by (induct xs, simp_all) - -lemma foldl_invariant: - "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f y x) \<rbrakk> \<Longrightarrow> Q (foldl f x xs)" - by (induct xs arbitrary: x, simp_all) - -lemma foldl_weak_invariant: - assumes "P s" - and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)" - shows "P (foldl f s xs)" +lemma fold_invariant: + assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s" + and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)" + shows "P (fold f xs s)" using assms by (induct xs arbitrary: s) simp_all -text {* @{const foldl} and @{const concat} *} - -lemma foldl_conv_concat: - "foldl (op @) xs xss = xs @ concat xss" -proof (induct xss arbitrary: xs) - case Nil show ?case by simp -next - interpret monoid_add "op @" "[]" proof qed simp_all - case Cons then show ?case by (simp add: foldl_absorb0) -qed - -lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss" - by (simp add: foldl_conv_concat) - -text {* @{const Finite_Set.fold} and @{const foldl} *} - -lemma (in comp_fun_commute) fold_set_remdups: - "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)" +lemma fold_append [simp]: + "fold f (xs @ ys) = fold f ys \<circ> fold f xs" + by (induct xs) simp_all + +lemma fold_map [code_unfold]: + "fold g (map f xs) = fold (g o f) xs" + by (induct xs) simp_all + +lemma fold_rev: + assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" + shows "fold f (rev xs) = fold f xs" +using assms by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff) + +lemma fold_Cons_rev: + "fold Cons xs = append (rev xs)" + by (induct xs) simp_all + +lemma rev_conv_fold [code]: + "rev xs = fold Cons xs []" + by (simp add: fold_Cons_rev) + +lemma fold_append_concat_rev: + "fold append xss = append (concat (rev xss))" + by (induct xss) simp_all + +text {* @{const Finite_Set.fold} and @{const fold} *} + +lemma (in comp_fun_commute) fold_set_fold_remdups: + "Finite_Set.fold f y (set xs) = fold f (remdups xs) y" by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) -lemma (in comp_fun_idem) fold_set: - "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs" +lemma (in comp_fun_idem) fold_set_fold: + "Finite_Set.fold f y (set xs) = fold f xs y" by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) -lemma (in ab_semigroup_idem_mult) fold1_set: +lemma (in ab_semigroup_idem_mult) fold1_set_fold: assumes "xs \<noteq> []" - shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)" + shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)" proof - interpret comp_fun_idem times by (fact comp_fun_idem) from assms obtain y ys where xs: "xs = y # ys" @@ -2532,10 +2465,160 @@ case False then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)" by (simp only: finite_set fold1_eq_fold_idem) - with xs show ?thesis by (simp add: fold_set mult_commute) + with xs show ?thesis by (simp add: fold_set_fold mult_commute) qed qed +lemma (in lattice) Inf_fin_set_fold: + "Inf_fin (set (x # xs)) = fold inf xs x" +proof - + interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact ab_semigroup_idem_mult_inf) + show ?thesis + by (simp add: Inf_fin_def fold1_set_fold del: set.simps) +qed + +lemma (in lattice) Sup_fin_set_fold: + "Sup_fin (set (x # xs)) = fold sup xs x" +proof - + interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact ab_semigroup_idem_mult_sup) + show ?thesis + by (simp add: Sup_fin_def fold1_set_fold del: set.simps) +qed + +lemma (in linorder) Min_fin_set_fold: + "Min (set (x # xs)) = fold min xs x" +proof - + interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact ab_semigroup_idem_mult_min) + show ?thesis + by (simp add: Min_def fold1_set_fold del: set.simps) +qed + +lemma (in linorder) Max_fin_set_fold: + "Max (set (x # xs)) = fold max xs x" +proof - + interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact ab_semigroup_idem_mult_max) + show ?thesis + by (simp add: Max_def fold1_set_fold del: set.simps) +qed + +lemma (in complete_lattice) Inf_set_fold: + "Inf (set xs) = fold inf xs top" +proof - + interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact comp_fun_idem_inf) + show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute) +qed + +lemma (in complete_lattice) Sup_set_fold: + "Sup (set xs) = fold sup xs bot" +proof - + interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" + by (fact comp_fun_idem_sup) + show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute) +qed + +lemma (in complete_lattice) INF_set_fold: + "INFI (set xs) f = fold (inf \<circ> f) xs top" + unfolding INF_def set_map [symmetric] Inf_set_fold fold_map .. + +lemma (in complete_lattice) SUP_set_fold: + "SUPR (set xs) f = fold (sup \<circ> f) xs bot" + unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map .. + + +subsubsection {* Fold variants: @{const foldr} and @{const foldl} *} + +text {* Correspondence *} + +lemma foldr_foldl: -- {* The ``Third Duality Theorem'' in Bird \& Wadler: *} + "foldr f xs a = foldl (\<lambda>x y. f y x) a (rev xs)" + by (simp add: foldr_def foldl_def) + +lemma foldl_foldr: + "foldl f a xs = foldr (\<lambda>x y. f y x) (rev xs) a" + by (simp add: foldr_def foldl_def) + +lemma foldr_fold: + assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" + shows "foldr f xs = fold f xs" + using assms unfolding foldr_def by (rule fold_rev) + +lemma + foldr_Nil [code, simp]: "foldr f [] = id" + and foldr_Cons [code, simp]: "foldr f (x # xs) = f x \<circ> foldr f xs" + by (simp_all add: foldr_def) + +lemma + foldl_Nil [simp]: "foldl f a [] = a" + and foldl_Cons [simp]: "foldl f a (x # xs) = foldl f (f a x) xs" + by (simp_all add: foldl_def) + +lemma foldr_cong [fundef_cong]: + "a = b \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f x a = g x a) \<Longrightarrow> foldr f l a = foldr g k b" + by (auto simp add: foldr_def intro!: fold_cong) + +lemma foldl_cong [fundef_cong]: + "a = b \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f a x = g a x) \<Longrightarrow> foldl f a l = foldl g b k" + by (auto simp add: foldl_def intro!: fold_cong) + +lemma foldr_append [simp]: + "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)" + by (simp add: foldr_def) + +lemma foldl_append [simp]: + "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys" + by (simp add: foldl_def) + +lemma foldr_map [code_unfold]: + "foldr g (map f xs) a = foldr (g o f) xs a" + by (simp add: foldr_def fold_map rev_map) + +lemma foldl_map [code_unfold]: + "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs" + by (simp add: foldl_def fold_map comp_def) + +text {* Executing operations in terms of @{const foldr} -- tail-recursive! *} + +lemma concat_conv_foldr [code]: + "concat xss = foldr append xss []" + by (simp add: fold_append_concat_rev foldr_def) + +lemma (in lattice) Inf_fin_set_foldr [code]: + "Inf_fin (set (x # xs)) = foldr inf xs x" + by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) + +lemma (in lattice) Sup_fin_set_foldr [code]: + "Sup_fin (set (x # xs)) = foldr sup xs x" + by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) + +lemma (in linorder) Min_fin_set_foldr [code]: + "Min (set (x # xs)) = foldr min xs x" + by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) + +lemma (in linorder) Max_fin_set_foldr [code]: + "Max (set (x # xs)) = foldr max xs x" + by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) + +lemma (in complete_lattice) Inf_set_foldr: + "Inf (set xs) = foldr inf xs top" + by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff) + +lemma (in complete_lattice) Sup_set_foldr: + "Sup (set xs) = foldr sup xs bot" + by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) + +lemma (in complete_lattice) INF_set_foldr [code]: + "INFI (set xs) f = foldr (inf \<circ> f) xs top" + by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric]) + +lemma (in complete_lattice) SUP_set_foldr [code]: + "SUPR (set xs) f = foldr (sup \<circ> f) xs bot" + by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric]) + subsubsection {* @{text upt} *} @@ -2940,16 +3023,11 @@ "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))" by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons) - subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*} -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" + "listsum (x # xs) = x + listsum xs" by (simp_all add: listsum_def) lemma (in monoid_add) listsum_append [simp]: @@ -2958,7 +3036,60 @@ 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) + by (simp add: listsum_def foldr_def fold_rev fun_eq_iff add_ac) + +lemma (in monoid_add) fold_plus_listsum_rev: + "fold plus xs = plus (listsum (rev xs))" +proof + fix x + have "fold plus xs x = fold plus xs (x + 0)" by simp + also have "\<dots> = fold plus (x # xs) 0" by simp + also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_def) + also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def) + also have "\<dots> = listsum (rev xs) + listsum [x]" by simp + finally show "fold plus xs x = listsum (rev xs) + x" by simp +qed + +lemma (in semigroup_add) foldl_assoc: + "foldl plus (x + y) zs = x + foldl plus y zs" + by (simp add: foldl_def fold_commute_apply [symmetric] fun_eq_iff add_assoc) + +lemma (in ab_semigroup_add) foldr_conv_foldl: + "foldr plus xs a = foldl plus a xs" + by (simp add: foldl_def foldr_fold fun_eq_iff add_ac) + +text {* + Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more + difficult to use because it requires an additional transitivity step. +*} + +lemma start_le_sum: + fixes m n :: nat + shows "m \<le> n \<Longrightarrow> m \<le> foldl plus n ns" + by (simp add: foldl_def add_commute fold_plus_listsum_rev) + +lemma elem_le_sum: + fixes m n :: nat + shows "n \<in> set ns \<Longrightarrow> n \<le> foldl plus 0 ns" + by (force intro: start_le_sum simp add: in_set_conv_decomp) + +lemma sum_eq_0_conv [iff]: + fixes m :: nat + shows "foldl plus m ns = 0 \<longleftrightarrow> m = 0 \<and> (\<forall>n \<in> set ns. n = 0)" + by (induct ns arbitrary: m) auto + +text{* Some syntactic sugar for summing a function over a list: *} + +syntax + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) +syntax (xsymbols) + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) +syntax (HTML output) + "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) + +translations -- {* Beware of argument permutation! *} + "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)" + "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)" 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))" @@ -2983,7 +3114,7 @@ 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) + by (simp add: listsum_def foldr_conv_foldl) lemma elem_le_listsum_nat: "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)" @@ -3000,19 +3131,6 @@ apply arith done -text{* Some syntactic sugar for summing a function over a list: *} - -syntax - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) -syntax (xsymbols) - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) -syntax (HTML output) - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) - -translations -- {* Beware of argument permutation! *} - "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)" - "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)" - lemma (in monoid_add) listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" by (induct xs) (simp_all add: left_distrib) @@ -3819,9 +3937,26 @@ "sort_key f (x#xs) = insort_key f x (sort_key f xs)" by (simp_all add: sort_key_def) -lemma sort_foldl_insort: - "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs" - by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm) +lemma (in linorder) sort_key_conv_fold: + assumes "inj_on f (set xs)" + shows "sort_key f xs = fold (insort_key f) xs []" +proof - + have "fold (insort_key f) (rev xs) = fold (insort_key f) xs" + proof (rule fold_rev, rule ext) + fix zs + 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 intro: * simp add: **) + qed + then show ?thesis by (simp add: sort_key_def foldr_def) +qed + +lemma (in linorder) sort_conv_fold: + "sort xs = fold insort xs []" + by (rule sort_key_conv_fold) simp lemma length_sort[simp]: "length (sort_key f xs) = length xs" by (induct xs, auto) @@ -4312,7 +4447,7 @@ "sorted_list_of_set (set xs) = sort (remdups xs)" proof - interpret comp_fun_commute insort by (fact comp_fun_commute_insort) - show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups) + show ?thesis by (simp add: sorted_list_of_set_def sort_conv_fold fold_set_fold_remdups) qed lemma sorted_list_of_set_remove: