incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
authorhaftmann
Fri Jan 06 10:19:49 2012 +0100 (2012-01-06)
changeset 46133d9fe85d3d2cd
parent 46132 5a29dbf4c155
child 46134 4b9d4659228a
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
doc-src/Main/Docs/Main_Doc.thy
src/HOL/Import/HOL/rich_list.imp
src/HOL/Library/AList_Impl.thy
src/HOL/Library/Cset.thy
src/HOL/Library/Dlist.thy
src/HOL/Library/RBT.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/List.thy
src/HOL/More_List.thy
src/HOL/More_Set.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Quotient_Examples/Lift_RBT.thy
     1.1 --- a/doc-src/Main/Docs/Main_Doc.thy	Fri Jan 06 10:19:49 2012 +0100
     1.2 +++ b/doc-src/Main/Docs/Main_Doc.thy	Fri Jan 06 10:19:49 2012 +0100
     1.3 @@ -495,8 +495,9 @@
     1.4  @{const List.drop} & @{typeof List.drop}\\
     1.5  @{const List.dropWhile} & @{typeof List.dropWhile}\\
     1.6  @{const List.filter} & @{typeof List.filter}\\
     1.7 +@{const List.fold} & @{typeof List.fold}\\
     1.8 +@{const List.foldr} & @{typeof List.foldr}\\
     1.9  @{const List.foldl} & @{typeof List.foldl}\\
    1.10 -@{const List.foldr} & @{typeof List.foldr}\\
    1.11  @{const List.hd} & @{typeof List.hd}\\
    1.12  @{const List.last} & @{typeof List.last}\\
    1.13  @{const List.length} & @{typeof List.length}\\
     2.1 --- a/src/HOL/Import/HOL/rich_list.imp	Fri Jan 06 10:19:49 2012 +0100
     2.2 +++ b/src/HOL/Import/HOL/rich_list.imp	Fri Jan 06 10:19:49 2012 +0100
     2.3 @@ -100,7 +100,6 @@
     2.4    "REVERSE_SNOC" > "HOL4Base.rich_list.REVERSE_SNOC"
     2.5    "REVERSE_REVERSE" > "List.rev_rev_ident"
     2.6    "REVERSE_FOLDR" > "HOL4Base.rich_list.REVERSE_FOLDR"
     2.7 -  "REVERSE_FOLDL" > "List.rev_foldl_cons"
     2.8    "REVERSE_FLAT" > "HOL4Base.rich_list.REVERSE_FLAT"
     2.9    "REVERSE_EQ_NIL" > "List.rev_is_Nil_conv"
    2.10    "REVERSE_APPEND" > "List.rev_append"
    2.11 @@ -238,7 +237,6 @@
    2.12    "FLAT_SNOC" > "HOL4Base.rich_list.FLAT_SNOC"
    2.13    "FLAT_REVERSE" > "HOL4Base.rich_list.FLAT_REVERSE"
    2.14    "FLAT_FOLDR" > "HOL4Base.rich_list.FLAT_FOLDR"
    2.15 -  "FLAT_FOLDL" > "List.concat_conv_foldl"
    2.16    "FLAT_FLAT" > "HOL4Base.rich_list.FLAT_FLAT"
    2.17    "FLAT_APPEND" > "List.concat_append"
    2.18    "FLAT" > "HOL4Compat.FLAT"
     3.1 --- a/src/HOL/Library/AList_Impl.thy	Fri Jan 06 10:19:49 2012 +0100
     3.2 +++ b/src/HOL/Library/AList_Impl.thy	Fri Jan 06 10:19:49 2012 +0100
     3.3 @@ -76,10 +76,10 @@
     3.4  
     3.5  lemma image_update [simp]:
     3.6    "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
     3.7 -  by (simp add: update_conv' image_map_upd)
     3.8 +  by (simp add: update_conv')
     3.9  
    3.10  definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
    3.11 -  "updates ks vs = More_List.fold (prod_case update) (zip ks vs)"
    3.12 +  "updates ks vs = fold (prod_case update) (zip ks vs)"
    3.13  
    3.14  lemma updates_simps [simp]:
    3.15    "updates [] vs ps = ps"
    3.16 @@ -94,10 +94,10 @@
    3.17  
    3.18  lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
    3.19  proof -
    3.20 -  have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
    3.21 -    More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
    3.22 +  have "map_of \<circ> fold (prod_case update) (zip ks vs) =
    3.23 +    fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
    3.24      by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
    3.25 -  then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_fold split_def)
    3.26 +  then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_def split_def)
    3.27  qed
    3.28  
    3.29  lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
    3.30 @@ -107,12 +107,12 @@
    3.31    assumes "distinct (map fst al)"
    3.32    shows "distinct (map fst (updates ks vs al))"
    3.33  proof -
    3.34 -  have "distinct (More_List.fold
    3.35 +  have "distinct (fold
    3.36         (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
    3.37         (zip ks vs) (map fst al))"
    3.38      by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
    3.39 -  moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
    3.40 -    More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
    3.41 +  moreover have "map fst \<circ> fold (prod_case update) (zip ks vs) =
    3.42 +    fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
    3.43      by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
    3.44    ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
    3.45  qed
    3.46 @@ -339,8 +339,8 @@
    3.47  lemma clearjunk_updates:
    3.48    "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
    3.49  proof -
    3.50 -  have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
    3.51 -    More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
    3.52 +  have "clearjunk \<circ> fold (prod_case update) (zip ks vs) =
    3.53 +    fold (prod_case update) (zip ks vs) \<circ> clearjunk"
    3.54      by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
    3.55    then show ?thesis by (simp add: updates_def fun_eq_iff)
    3.56  qed
    3.57 @@ -427,7 +427,7 @@
    3.58  
    3.59  lemma merge_updates:
    3.60    "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
    3.61 -  by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
    3.62 +  by (simp add: merge_def updates_def foldr_def zip_rev zip_map_fst_snd)
    3.63  
    3.64  lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
    3.65    by (induct ys arbitrary: xs) (auto simp add: dom_update)
    3.66 @@ -444,11 +444,11 @@
    3.67  lemma merge_conv':
    3.68    "map_of (merge xs ys) = map_of xs ++ map_of ys"
    3.69  proof -
    3.70 -  have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
    3.71 -    More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
    3.72 +  have "map_of \<circ> fold (prod_case update) (rev ys) =
    3.73 +    fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
    3.74      by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
    3.75    then show ?thesis
    3.76 -    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev fun_eq_iff)
    3.77 +    by (simp add: merge_def map_add_map_of_foldr foldr_def fun_eq_iff)
    3.78  qed
    3.79  
    3.80  corollary merge_conv:
     4.1 --- a/src/HOL/Library/Cset.thy	Fri Jan 06 10:19:49 2012 +0100
     4.2 +++ b/src/HOL/Library/Cset.thy	Fri Jan 06 10:19:49 2012 +0100
     4.3 @@ -370,7 +370,7 @@
     4.4  
     4.5  lemma bind_set:
     4.6    "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
     4.7 -  by (simp add: Cset.bind_def SUPR_set_fold)
     4.8 +  by (simp add: Cset.bind_def SUP_set_fold)
     4.9  hide_fact (open) bind_set
    4.10  
    4.11  lemma pred_of_cset_set:
     5.1 --- a/src/HOL/Library/Dlist.thy	Fri Jan 06 10:19:49 2012 +0100
     5.2 +++ b/src/HOL/Library/Dlist.thy	Fri Jan 06 10:19:49 2012 +0100
     5.3 @@ -74,7 +74,7 @@
     5.4    "length dxs = List.length (list_of_dlist dxs)"
     5.5  
     5.6  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
     5.7 -  "fold f dxs = More_List.fold f (list_of_dlist dxs)"
     5.8 +  "fold f dxs = List.fold f (list_of_dlist dxs)"
     5.9  
    5.10  definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
    5.11    "foldr f dxs = List.foldr f (list_of_dlist dxs)"
     6.1 --- a/src/HOL/Library/RBT.thy	Fri Jan 06 10:19:49 2012 +0100
     6.2 +++ b/src/HOL/Library/RBT.thy	Fri Jan 06 10:19:49 2012 +0100
     6.3 @@ -146,7 +146,7 @@
     6.4    by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
     6.5  
     6.6  lemma fold_fold:
     6.7 -  "fold f t = More_List.fold (prod_case f) (entries t)"
     6.8 +  "fold f t = List.fold (prod_case f) (entries t)"
     6.9    by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
    6.10  
    6.11  lemma is_empty_empty [simp]:
     7.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Jan 06 10:19:49 2012 +0100
     7.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Jan 06 10:19:49 2012 +0100
     7.3 @@ -1049,7 +1049,7 @@
     7.4  subsection {* Folding over entries *}
     7.5  
     7.6  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
     7.7 -  "fold f t = More_List.fold (prod_case f) (entries t)"
     7.8 +  "fold f t = List.fold (prod_case f) (entries t)"
     7.9  
    7.10  lemma fold_simps [simp, code]:
    7.11    "fold f Empty = id"
    7.12 @@ -1071,12 +1071,12 @@
    7.13  proof -
    7.14    obtain ys where "ys = rev xs" by simp
    7.15    have "\<And>t. is_rbt t \<Longrightarrow>
    7.16 -    lookup (More_List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
    7.17 +    lookup (List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
    7.18        by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta)
    7.19    from this Empty_is_rbt have
    7.20 -    "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
    7.21 +    "lookup (List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
    7.22       by (simp add: `ys = rev xs`)
    7.23 -  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev)
    7.24 +  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_def)
    7.25  qed
    7.26  
    7.27  hide_const (open) R B Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
     8.1 --- a/src/HOL/List.thy	Fri Jan 06 10:19:49 2012 +0100
     8.2 +++ b/src/HOL/List.thy	Fri Jan 06 10:19:49 2012 +0100
     8.3 @@ -49,6 +49,10 @@
     8.4      "set [] = {}"
     8.5    | "set (x # xs) = insert x (set xs)"
     8.6  
     8.7 +definition
     8.8 +  coset :: "'a list \<Rightarrow> 'a set" where
     8.9 +  [simp]: "coset xs = - set xs"
    8.10 +
    8.11  primrec
    8.12    map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    8.13      "map f [] = []"
    8.14 @@ -81,15 +85,18 @@
    8.15  syntax (HTML output)
    8.16    "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
    8.17  
    8.18 -primrec
    8.19 +primrec -- {* canonical argument order *}
    8.20 +  fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    8.21 +    "fold f [] = id"
    8.22 +  | "fold f (x # xs) = fold f xs \<circ> f x"
    8.23 +
    8.24 +definition 
    8.25 +  foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    8.26 +  [code_abbrev]: "foldr f xs = fold f (rev xs)"
    8.27 +
    8.28 +definition
    8.29    foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
    8.30 -    foldl_Nil: "foldl f a [] = a"
    8.31 -  | foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
    8.32 -
    8.33 -primrec
    8.34 -  foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    8.35 -    "foldr f [] a = a"
    8.36 -  | "foldr f (x # xs) a = f x (foldr f xs a)"
    8.37 +  "foldl f s xs = fold (\<lambda>x s. f s x)  xs s"
    8.38  
    8.39  primrec
    8.40    concat:: "'a list list \<Rightarrow> 'a list" where
    8.41 @@ -236,8 +243,9 @@
    8.42  @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
    8.43  @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
    8.44  @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
    8.45 -@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
    8.46 -@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
    8.47 +@{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\
    8.48 +@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by (simp add: foldr_def)}\\
    8.49 +@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by (simp add: foldl_def)}\\
    8.50  @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
    8.51  @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
    8.52  @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
    8.53 @@ -261,7 +269,7 @@
    8.54  @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def eval_nat_numeral)}\\
    8.55  @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
    8.56  @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
    8.57 -@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}
    8.58 +@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)}
    8.59  \end{tabular}}
    8.60  \caption{Characteristic examples}
    8.61  \label{fig:Characteristic}
    8.62 @@ -298,11 +306,11 @@
    8.63    by simp_all
    8.64  
    8.65  primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
    8.66 -"insort_key f x [] = [x]" |
    8.67 -"insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
    8.68 +  "insort_key f x [] = [x]" |
    8.69 +  "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
    8.70  
    8.71  definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
    8.72 -"sort_key f xs = foldr (insort_key f) xs []"
    8.73 +  "sort_key f xs = foldr (insort_key f) xs []"
    8.74  
    8.75  definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
    8.76    "insort_insert_key f x xs = (if f x \<in> f ` set xs then xs else insort_key f x xs)"
    8.77 @@ -470,6 +478,9 @@
    8.78  
    8.79  simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
    8.80  
    8.81 +code_datatype set coset
    8.82 +
    8.83 +hide_const (open) coset
    8.84  
    8.85  subsubsection {* @{const Nil} and @{const Cons} *}
    8.86  
    8.87 @@ -2368,159 +2379,81 @@
    8.88  by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
    8.89  
    8.90  
    8.91 -subsubsection {* @{text foldl} and @{text foldr} *}
    8.92 -
    8.93 -lemma foldl_append [simp]:
    8.94 -  "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
    8.95 -by (induct xs arbitrary: a) auto
    8.96 -
    8.97 -lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
    8.98 -by (induct xs) auto
    8.99 -
   8.100 -lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
   8.101 -by(induct xs) simp_all
   8.102 -
   8.103 -text{* For efficient code generation: avoid intermediate list. *}
   8.104 -lemma foldl_map[code_unfold]:
   8.105 -  "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
   8.106 -by(induct xs arbitrary:a) simp_all
   8.107 -
   8.108 -lemma foldl_apply:
   8.109 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x"
   8.110 -  shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
   8.111 -  by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_iff)
   8.112 -
   8.113 -lemma foldl_cong [fundef_cong]:
   8.114 -  "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
   8.115 -  ==> foldl f a l = foldl g b k"
   8.116 -by (induct k arbitrary: a b l) simp_all
   8.117 -
   8.118 -lemma foldr_cong [fundef_cong]:
   8.119 -  "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
   8.120 -  ==> foldr f l a = foldr g k b"
   8.121 -by (induct k arbitrary: a b l) simp_all
   8.122 -
   8.123 -lemma foldl_fun_comm:
   8.124 -  assumes "\<And>x y s. f (f s x) y = f (f s y) x"
   8.125 -  shows "f (foldl f s xs) x = foldl f (f s x) xs"
   8.126 -  by (induct xs arbitrary: s)
   8.127 -    (simp_all add: assms)
   8.128 -
   8.129 -lemma (in semigroup_add) foldl_assoc:
   8.130 -shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
   8.131 -by (induct zs arbitrary: y) (simp_all add:add_assoc)
   8.132 -
   8.133 -lemma (in monoid_add) foldl_absorb0:
   8.134 -shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
   8.135 -by (induct zs) (simp_all add:foldl_assoc)
   8.136 -
   8.137 -lemma foldl_rev:
   8.138 -  assumes "\<And>x y s. f (f s x) y = f (f s y) x"
   8.139 -  shows "foldl f s (rev xs) = foldl f s xs"
   8.140 -proof (induct xs arbitrary: s)
   8.141 -  case Nil then show ?case by simp
   8.142 -next
   8.143 -  case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)
   8.144 -qed
   8.145 -
   8.146 -lemma rev_foldl_cons [code]:
   8.147 -  "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
   8.148 -proof (induct xs)
   8.149 -  case Nil then show ?case by simp
   8.150 -next
   8.151 -  case Cons
   8.152 -  {
   8.153 -    fix x xs ys
   8.154 -    have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
   8.155 -      = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
   8.156 -    by (induct xs arbitrary: ys) auto
   8.157 -  }
   8.158 -  note aux = this
   8.159 -  show ?case by (induct xs) (auto simp add: Cons aux)
   8.160 +subsubsection {* @{const fold} with canonical argument order *}
   8.161 +
   8.162 +lemma fold_remove1_split:
   8.163 +  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"
   8.164 +    and x: "x \<in> set xs"
   8.165 +  shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
   8.166 +  using assms by (induct xs) (auto simp add: o_assoc [symmetric])
   8.167 +
   8.168 +lemma fold_cong [fundef_cong]:
   8.169 +  "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
   8.170 +    \<Longrightarrow> fold f xs a = fold g ys b"
   8.171 +  by (induct ys arbitrary: a b xs) simp_all
   8.172 +
   8.173 +lemma fold_id:
   8.174 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
   8.175 +  shows "fold f xs = id"
   8.176 +  using assms by (induct xs) simp_all
   8.177 +
   8.178 +lemma fold_commute:
   8.179 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   8.180 +  shows "h \<circ> fold g xs = fold f xs \<circ> h"
   8.181 +  using assms by (induct xs) (simp_all add: fun_eq_iff)
   8.182 +
   8.183 +lemma fold_commute_apply:
   8.184 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   8.185 +  shows "h (fold g xs s) = fold f xs (h s)"
   8.186 +proof -
   8.187 +  from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
   8.188 +  then show ?thesis by (simp add: fun_eq_iff)
   8.189  qed
   8.190  
   8.191 -
   8.192 -text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
   8.193 -
   8.194 -lemma foldr_foldl:
   8.195 -  "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
   8.196 -  by (induct xs) auto
   8.197 -
   8.198 -lemma foldl_foldr:
   8.199 -  "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
   8.200 -  by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
   8.201 -
   8.202 -
   8.203 -text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
   8.204 -
   8.205 -lemma (in monoid_add) foldl_foldr1_lemma:
   8.206 -  "foldl op + a xs = a + foldr op + xs 0"
   8.207 -  by (induct xs arbitrary: a) (auto simp: add_assoc)
   8.208 -
   8.209 -corollary (in monoid_add) foldl_foldr1:
   8.210 -  "foldl op + 0 xs = foldr op + xs 0"
   8.211 -  by (simp add: foldl_foldr1_lemma)
   8.212 -
   8.213 -lemma (in ab_semigroup_add) foldr_conv_foldl:
   8.214 -  "foldr op + xs a = foldl op + a xs"
   8.215 -  by (induct xs) (simp_all add: foldl_assoc add.commute)
   8.216 -
   8.217 -text {*
   8.218 -Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
   8.219 -difficult to use because it requires an additional transitivity step.
   8.220 -*}
   8.221 -
   8.222 -lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
   8.223 -by (induct ns arbitrary: n) auto
   8.224 -
   8.225 -lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
   8.226 -by (force intro: start_le_sum simp add: in_set_conv_decomp)
   8.227 -
   8.228 -lemma sum_eq_0_conv [iff]:
   8.229 -  "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
   8.230 -by (induct ns arbitrary: m) auto
   8.231 -
   8.232 -lemma foldr_invariant: 
   8.233 -  "\<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)"
   8.234 -  by (induct xs, simp_all)
   8.235 -
   8.236 -lemma foldl_invariant: 
   8.237 -  "\<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)"
   8.238 -  by (induct xs arbitrary: x, simp_all)
   8.239 -
   8.240 -lemma foldl_weak_invariant:
   8.241 -  assumes "P s"
   8.242 -    and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)"
   8.243 -  shows "P (foldl f s xs)"
   8.244 +lemma fold_invariant: 
   8.245 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
   8.246 +    and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
   8.247 +  shows "P (fold f xs s)"
   8.248    using assms by (induct xs arbitrary: s) simp_all
   8.249  
   8.250 -text {* @{const foldl} and @{const concat} *}
   8.251 -
   8.252 -lemma foldl_conv_concat:
   8.253 -  "foldl (op @) xs xss = xs @ concat xss"
   8.254 -proof (induct xss arbitrary: xs)
   8.255 -  case Nil show ?case by simp
   8.256 -next
   8.257 -  interpret monoid_add "op @" "[]" proof qed simp_all
   8.258 -  case Cons then show ?case by (simp add: foldl_absorb0)
   8.259 -qed
   8.260 -
   8.261 -lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
   8.262 -  by (simp add: foldl_conv_concat)
   8.263 -
   8.264 -text {* @{const Finite_Set.fold} and @{const foldl} *}
   8.265 -
   8.266 -lemma (in comp_fun_commute) fold_set_remdups:
   8.267 -  "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
   8.268 +lemma fold_append [simp]:
   8.269 +  "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
   8.270 +  by (induct xs) simp_all
   8.271 +
   8.272 +lemma fold_map [code_unfold]:
   8.273 +  "fold g (map f xs) = fold (g o f) xs"
   8.274 +  by (induct xs) simp_all
   8.275 +
   8.276 +lemma fold_rev:
   8.277 +  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   8.278 +  shows "fold f (rev xs) = fold f xs"
   8.279 +using assms by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
   8.280 +
   8.281 +lemma fold_Cons_rev:
   8.282 +  "fold Cons xs = append (rev xs)"
   8.283 +  by (induct xs) simp_all
   8.284 +
   8.285 +lemma rev_conv_fold [code]:
   8.286 +  "rev xs = fold Cons xs []"
   8.287 +  by (simp add: fold_Cons_rev)
   8.288 +
   8.289 +lemma fold_append_concat_rev:
   8.290 +  "fold append xss = append (concat (rev xss))"
   8.291 +  by (induct xss) simp_all
   8.292 +
   8.293 +text {* @{const Finite_Set.fold} and @{const fold} *}
   8.294 +
   8.295 +lemma (in comp_fun_commute) fold_set_fold_remdups:
   8.296 +  "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
   8.297    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
   8.298  
   8.299 -lemma (in comp_fun_idem) fold_set:
   8.300 -  "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
   8.301 +lemma (in comp_fun_idem) fold_set_fold:
   8.302 +  "Finite_Set.fold f y (set xs) = fold f xs y"
   8.303    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
   8.304  
   8.305 -lemma (in ab_semigroup_idem_mult) fold1_set:
   8.306 +lemma (in ab_semigroup_idem_mult) fold1_set_fold:
   8.307    assumes "xs \<noteq> []"
   8.308 -  shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"
   8.309 +  shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
   8.310  proof -
   8.311    interpret comp_fun_idem times by (fact comp_fun_idem)
   8.312    from assms obtain y ys where xs: "xs = y # ys"
   8.313 @@ -2532,10 +2465,160 @@
   8.314      case False
   8.315      then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
   8.316        by (simp only: finite_set fold1_eq_fold_idem)
   8.317 -    with xs show ?thesis by (simp add: fold_set mult_commute)
   8.318 +    with xs show ?thesis by (simp add: fold_set_fold mult_commute)
   8.319    qed
   8.320  qed
   8.321  
   8.322 +lemma (in lattice) Inf_fin_set_fold:
   8.323 +  "Inf_fin (set (x # xs)) = fold inf xs x"
   8.324 +proof -
   8.325 +  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   8.326 +    by (fact ab_semigroup_idem_mult_inf)
   8.327 +  show ?thesis
   8.328 +    by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
   8.329 +qed
   8.330 +
   8.331 +lemma (in lattice) Sup_fin_set_fold:
   8.332 +  "Sup_fin (set (x # xs)) = fold sup xs x"
   8.333 +proof -
   8.334 +  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   8.335 +    by (fact ab_semigroup_idem_mult_sup)
   8.336 +  show ?thesis
   8.337 +    by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
   8.338 +qed
   8.339 +
   8.340 +lemma (in linorder) Min_fin_set_fold:
   8.341 +  "Min (set (x # xs)) = fold min xs x"
   8.342 +proof -
   8.343 +  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   8.344 +    by (fact ab_semigroup_idem_mult_min)
   8.345 +  show ?thesis
   8.346 +    by (simp add: Min_def fold1_set_fold del: set.simps)
   8.347 +qed
   8.348 +
   8.349 +lemma (in linorder) Max_fin_set_fold:
   8.350 +  "Max (set (x # xs)) = fold max xs x"
   8.351 +proof -
   8.352 +  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   8.353 +    by (fact ab_semigroup_idem_mult_max)
   8.354 +  show ?thesis
   8.355 +    by (simp add: Max_def fold1_set_fold del: set.simps)
   8.356 +qed
   8.357 +
   8.358 +lemma (in complete_lattice) Inf_set_fold:
   8.359 +  "Inf (set xs) = fold inf xs top"
   8.360 +proof -
   8.361 +  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   8.362 +    by (fact comp_fun_idem_inf)
   8.363 +  show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute)
   8.364 +qed
   8.365 +
   8.366 +lemma (in complete_lattice) Sup_set_fold:
   8.367 +  "Sup (set xs) = fold sup xs bot"
   8.368 +proof -
   8.369 +  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   8.370 +    by (fact comp_fun_idem_sup)
   8.371 +  show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute)
   8.372 +qed
   8.373 +
   8.374 +lemma (in complete_lattice) INF_set_fold:
   8.375 +  "INFI (set xs) f = fold (inf \<circ> f) xs top"
   8.376 +  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
   8.377 +
   8.378 +lemma (in complete_lattice) SUP_set_fold:
   8.379 +  "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
   8.380 +  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
   8.381 +
   8.382 +
   8.383 +subsubsection {* Fold variants: @{const foldr} and @{const foldl} *}
   8.384 +
   8.385 +text {* Correspondence *}
   8.386 +
   8.387 +lemma foldr_foldl: -- {* The ``Third Duality Theorem'' in Bird \& Wadler: *}
   8.388 +  "foldr f xs a = foldl (\<lambda>x y. f y x) a (rev xs)"
   8.389 +  by (simp add: foldr_def foldl_def)
   8.390 +
   8.391 +lemma foldl_foldr:
   8.392 +  "foldl f a xs = foldr (\<lambda>x y. f y x) (rev xs) a"
   8.393 +  by (simp add: foldr_def foldl_def)
   8.394 +
   8.395 +lemma foldr_fold:
   8.396 +  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   8.397 +  shows "foldr f xs = fold f xs"
   8.398 +  using assms unfolding foldr_def by (rule fold_rev)
   8.399 +
   8.400 +lemma
   8.401 +  foldr_Nil [code, simp]: "foldr f [] = id"
   8.402 +  and foldr_Cons [code, simp]: "foldr f (x # xs) = f x \<circ> foldr f xs"
   8.403 +  by (simp_all add: foldr_def)
   8.404 +
   8.405 +lemma
   8.406 +  foldl_Nil [simp]: "foldl f a [] = a"
   8.407 +  and foldl_Cons [simp]: "foldl f a (x # xs) = foldl f (f a x) xs"
   8.408 +  by (simp_all add: foldl_def)
   8.409 +
   8.410 +lemma foldr_cong [fundef_cong]:
   8.411 +  "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"
   8.412 +  by (auto simp add: foldr_def intro!: fold_cong)
   8.413 +
   8.414 +lemma foldl_cong [fundef_cong]:
   8.415 +  "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"
   8.416 +  by (auto simp add: foldl_def intro!: fold_cong)
   8.417 +
   8.418 +lemma foldr_append [simp]:
   8.419 +  "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
   8.420 +  by (simp add: foldr_def)
   8.421 +
   8.422 +lemma foldl_append [simp]:
   8.423 +  "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
   8.424 +  by (simp add: foldl_def)
   8.425 +
   8.426 +lemma foldr_map [code_unfold]:
   8.427 +  "foldr g (map f xs) a = foldr (g o f) xs a"
   8.428 +  by (simp add: foldr_def fold_map rev_map)
   8.429 +
   8.430 +lemma foldl_map [code_unfold]:
   8.431 +  "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs"
   8.432 +  by (simp add: foldl_def fold_map comp_def)
   8.433 +
   8.434 +text {* Executing operations in terms of @{const foldr} -- tail-recursive! *}
   8.435 +
   8.436 +lemma concat_conv_foldr [code]:
   8.437 +  "concat xss = foldr append xss []"
   8.438 +  by (simp add: fold_append_concat_rev foldr_def)
   8.439 +
   8.440 +lemma (in lattice) Inf_fin_set_foldr [code]:
   8.441 +  "Inf_fin (set (x # xs)) = foldr inf xs x"
   8.442 +  by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   8.443 +
   8.444 +lemma (in lattice) Sup_fin_set_foldr [code]:
   8.445 +  "Sup_fin (set (x # xs)) = foldr sup xs x"
   8.446 +  by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   8.447 +
   8.448 +lemma (in linorder) Min_fin_set_foldr [code]:
   8.449 +  "Min (set (x # xs)) = foldr min xs x"
   8.450 +  by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   8.451 +
   8.452 +lemma (in linorder) Max_fin_set_foldr [code]:
   8.453 +  "Max (set (x # xs)) = foldr max xs x"
   8.454 +  by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   8.455 +
   8.456 +lemma (in complete_lattice) Inf_set_foldr:
   8.457 +  "Inf (set xs) = foldr inf xs top"
   8.458 +  by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
   8.459 +
   8.460 +lemma (in complete_lattice) Sup_set_foldr:
   8.461 +  "Sup (set xs) = foldr sup xs bot"
   8.462 +  by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
   8.463 +
   8.464 +lemma (in complete_lattice) INF_set_foldr [code]:
   8.465 +  "INFI (set xs) f = foldr (inf \<circ> f) xs top"
   8.466 +  by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric])
   8.467 +
   8.468 +lemma (in complete_lattice) SUP_set_foldr [code]:
   8.469 +  "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
   8.470 +  by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
   8.471 +
   8.472  
   8.473  subsubsection {* @{text upt} *}
   8.474  
   8.475 @@ -2940,16 +3023,11 @@
   8.476  "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
   8.477  by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
   8.478  
   8.479 -
   8.480  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
   8.481  
   8.482 -lemma (in monoid_add) listsum_foldl [code]:
   8.483 -  "listsum = foldl (op +) 0"
   8.484 -  by (simp add: listsum_def foldl_foldr1 fun_eq_iff)
   8.485 -
   8.486  lemma (in monoid_add) listsum_simps [simp]:
   8.487    "listsum [] = 0"
   8.488 -  "listsum (x#xs) = x + listsum xs"
   8.489 +  "listsum (x # xs) = x + listsum xs"
   8.490    by (simp_all add: listsum_def)
   8.491  
   8.492  lemma (in monoid_add) listsum_append [simp]:
   8.493 @@ -2958,7 +3036,60 @@
   8.494  
   8.495  lemma (in comm_monoid_add) listsum_rev [simp]:
   8.496    "listsum (rev xs) = listsum xs"
   8.497 -  by (simp add: listsum_def [of "rev xs"]) (simp add: listsum_foldl foldr_foldl add.commute)
   8.498 +  by (simp add: listsum_def foldr_def fold_rev fun_eq_iff add_ac)
   8.499 +
   8.500 +lemma (in monoid_add) fold_plus_listsum_rev:
   8.501 +  "fold plus xs = plus (listsum (rev xs))"
   8.502 +proof
   8.503 +  fix x
   8.504 +  have "fold plus xs x = fold plus xs (x + 0)" by simp
   8.505 +  also have "\<dots> = fold plus (x # xs) 0" by simp
   8.506 +  also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_def)
   8.507 +  also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def)
   8.508 +  also have "\<dots> = listsum (rev xs) + listsum [x]" by simp
   8.509 +  finally show "fold plus xs x = listsum (rev xs) + x" by simp
   8.510 +qed
   8.511 +
   8.512 +lemma (in semigroup_add) foldl_assoc:
   8.513 +  "foldl plus (x + y) zs = x + foldl plus y zs"
   8.514 +  by (simp add: foldl_def fold_commute_apply [symmetric] fun_eq_iff add_assoc)
   8.515 +
   8.516 +lemma (in ab_semigroup_add) foldr_conv_foldl:
   8.517 +  "foldr plus xs a = foldl plus a xs"
   8.518 +  by (simp add: foldl_def foldr_fold fun_eq_iff add_ac)
   8.519 +
   8.520 +text {*
   8.521 +  Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
   8.522 +  difficult to use because it requires an additional transitivity step.
   8.523 +*}
   8.524 +
   8.525 +lemma start_le_sum:
   8.526 +  fixes m n :: nat
   8.527 +  shows "m \<le> n \<Longrightarrow> m \<le> foldl plus n ns"
   8.528 +  by (simp add: foldl_def add_commute fold_plus_listsum_rev)
   8.529 +
   8.530 +lemma elem_le_sum:
   8.531 +  fixes m n :: nat 
   8.532 +  shows "n \<in> set ns \<Longrightarrow> n \<le> foldl plus 0 ns"
   8.533 +  by (force intro: start_le_sum simp add: in_set_conv_decomp)
   8.534 +
   8.535 +lemma sum_eq_0_conv [iff]:
   8.536 +  fixes m :: nat
   8.537 +  shows "foldl plus m ns = 0 \<longleftrightarrow> m = 0 \<and> (\<forall>n \<in> set ns. n = 0)"
   8.538 +  by (induct ns arbitrary: m) auto
   8.539 +
   8.540 +text{* Some syntactic sugar for summing a function over a list: *}
   8.541 +
   8.542 +syntax
   8.543 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
   8.544 +syntax (xsymbols)
   8.545 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
   8.546 +syntax (HTML output)
   8.547 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
   8.548 +
   8.549 +translations -- {* Beware of argument permutation! *}
   8.550 +  "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
   8.551 +  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
   8.552  
   8.553  lemma (in comm_monoid_add) listsum_map_remove1:
   8.554    "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
   8.555 @@ -2983,7 +3114,7 @@
   8.556  
   8.557  lemma listsum_eq_0_nat_iff_nat [simp]:
   8.558    "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
   8.559 -  by (simp add: listsum_foldl)
   8.560 +  by (simp add: listsum_def foldr_conv_foldl)
   8.561  
   8.562  lemma elem_le_listsum_nat:
   8.563    "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
   8.564 @@ -3000,19 +3131,6 @@
   8.565  apply arith
   8.566  done
   8.567  
   8.568 -text{* Some syntactic sugar for summing a function over a list: *}
   8.569 -
   8.570 -syntax
   8.571 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
   8.572 -syntax (xsymbols)
   8.573 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
   8.574 -syntax (HTML output)
   8.575 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
   8.576 -
   8.577 -translations -- {* Beware of argument permutation! *}
   8.578 -  "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
   8.579 -  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
   8.580 -
   8.581  lemma (in monoid_add) listsum_triv:
   8.582    "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
   8.583    by (induct xs) (simp_all add: left_distrib)
   8.584 @@ -3819,9 +3937,26 @@
   8.585    "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
   8.586    by (simp_all add: sort_key_def)
   8.587  
   8.588 -lemma sort_foldl_insort:
   8.589 -  "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs"
   8.590 -  by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm)
   8.591 +lemma (in linorder) sort_key_conv_fold:
   8.592 +  assumes "inj_on f (set xs)"
   8.593 +  shows "sort_key f xs = fold (insort_key f) xs []"
   8.594 +proof -
   8.595 +  have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
   8.596 +  proof (rule fold_rev, rule ext)
   8.597 +    fix zs
   8.598 +    fix x y
   8.599 +    assume "x \<in> set xs" "y \<in> set xs"
   8.600 +    with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
   8.601 +    have **: "x = y \<longleftrightarrow> y = x" by auto
   8.602 +    show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
   8.603 +      by (induct zs) (auto intro: * simp add: **)
   8.604 +  qed
   8.605 +  then show ?thesis by (simp add: sort_key_def foldr_def)
   8.606 +qed
   8.607 +
   8.608 +lemma (in linorder) sort_conv_fold:
   8.609 +  "sort xs = fold insort xs []"
   8.610 +  by (rule sort_key_conv_fold) simp
   8.611  
   8.612  lemma length_sort[simp]: "length (sort_key f xs) = length xs"
   8.613  by (induct xs, auto)
   8.614 @@ -4312,7 +4447,7 @@
   8.615    "sorted_list_of_set (set xs) = sort (remdups xs)"
   8.616  proof -
   8.617    interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
   8.618 -  show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
   8.619 +  show ?thesis by (simp add: sorted_list_of_set_def sort_conv_fold fold_set_fold_remdups)
   8.620  qed
   8.621  
   8.622  lemma sorted_list_of_set_remove:
     9.1 --- a/src/HOL/More_List.thy	Fri Jan 06 10:19:49 2012 +0100
     9.2 +++ b/src/HOL/More_List.thy	Fri Jan 06 10:19:49 2012 +0100
     9.3 @@ -6,242 +6,6 @@
     9.4  imports List
     9.5  begin
     9.6  
     9.7 -text {* Fold combinator with canonical argument order *}
     9.8 -
     9.9 -primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    9.10 -    "fold f [] = id"
    9.11 -  | "fold f (x # xs) = fold f xs \<circ> f x"
    9.12 -
    9.13 -lemma foldl_fold:
    9.14 -  "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
    9.15 -  by (induct xs arbitrary: s) simp_all
    9.16 -
    9.17 -lemma foldr_fold_rev:
    9.18 -  "foldr f xs = fold f (rev xs)"
    9.19 -  by (simp add: foldr_foldl foldl_fold fun_eq_iff)
    9.20 -
    9.21 -lemma fold_rev_conv [code_unfold]:
    9.22 -  "fold f (rev xs) = foldr f xs"
    9.23 -  by (simp add: foldr_fold_rev)
    9.24 -  
    9.25 -lemma fold_cong [fundef_cong]:
    9.26 -  "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
    9.27 -    \<Longrightarrow> fold f xs a = fold g ys b"
    9.28 -  by (induct ys arbitrary: a b xs) simp_all
    9.29 -
    9.30 -lemma fold_id:
    9.31 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
    9.32 -  shows "fold f xs = id"
    9.33 -  using assms by (induct xs) simp_all
    9.34 -
    9.35 -lemma fold_commute:
    9.36 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
    9.37 -  shows "h \<circ> fold g xs = fold f xs \<circ> h"
    9.38 -  using assms by (induct xs) (simp_all add: fun_eq_iff)
    9.39 -
    9.40 -lemma fold_commute_apply:
    9.41 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
    9.42 -  shows "h (fold g xs s) = fold f xs (h s)"
    9.43 -proof -
    9.44 -  from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
    9.45 -  then show ?thesis by (simp add: fun_eq_iff)
    9.46 -qed
    9.47 -
    9.48 -lemma fold_invariant: 
    9.49 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
    9.50 -    and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
    9.51 -  shows "P (fold f xs s)"
    9.52 -  using assms by (induct xs arbitrary: s) simp_all
    9.53 -
    9.54 -lemma fold_weak_invariant:
    9.55 -  assumes "P s"
    9.56 -    and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
    9.57 -  shows "P (fold f xs s)"
    9.58 -  using assms by (induct xs arbitrary: s) simp_all
    9.59 -
    9.60 -lemma fold_append [simp]:
    9.61 -  "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
    9.62 -  by (induct xs) simp_all
    9.63 -
    9.64 -lemma fold_map [code_unfold]:
    9.65 -  "fold g (map f xs) = fold (g o f) xs"
    9.66 -  by (induct xs) simp_all
    9.67 -
    9.68 -lemma fold_remove1_split:
    9.69 -  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"
    9.70 -    and x: "x \<in> set xs"
    9.71 -  shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
    9.72 -  using assms by (induct xs) (auto simp add: o_assoc [symmetric])
    9.73 -
    9.74 -lemma fold_rev:
    9.75 -  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
    9.76 -  shows "fold f (rev xs) = fold f xs"
    9.77 -using assms by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
    9.78 -
    9.79 -lemma foldr_fold:
    9.80 -  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
    9.81 -  shows "foldr f xs = fold f xs"
    9.82 -  using assms unfolding foldr_fold_rev by (rule fold_rev)
    9.83 -
    9.84 -lemma fold_Cons_rev:
    9.85 -  "fold Cons xs = append (rev xs)"
    9.86 -  by (induct xs) simp_all
    9.87 -
    9.88 -lemma rev_conv_fold [code]:
    9.89 -  "rev xs = fold Cons xs []"
    9.90 -  by (simp add: fold_Cons_rev)
    9.91 -
    9.92 -lemma fold_append_concat_rev:
    9.93 -  "fold append xss = append (concat (rev xss))"
    9.94 -  by (induct xss) simp_all
    9.95 -
    9.96 -lemma concat_conv_foldr [code]:
    9.97 -  "concat xss = foldr append xss []"
    9.98 -  by (simp add: fold_append_concat_rev foldr_fold_rev)
    9.99 -
   9.100 -lemma fold_plus_listsum_rev:
   9.101 -  "fold plus xs = plus (listsum (rev xs))"
   9.102 -  by (induct xs) (simp_all add: add.assoc)
   9.103 -
   9.104 -lemma (in monoid_add) listsum_conv_fold [code]:
   9.105 -  "listsum xs = fold (\<lambda>x y. y + x) xs 0"
   9.106 -  by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
   9.107 -
   9.108 -lemma (in linorder) sort_key_conv_fold:
   9.109 -  assumes "inj_on f (set xs)"
   9.110 -  shows "sort_key f xs = fold (insort_key f) xs []"
   9.111 -proof -
   9.112 -  have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
   9.113 -  proof (rule fold_rev, rule ext)
   9.114 -    fix zs
   9.115 -    fix x y
   9.116 -    assume "x \<in> set xs" "y \<in> set xs"
   9.117 -    with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
   9.118 -    have **: "x = y \<longleftrightarrow> y = x" by auto
   9.119 -    show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
   9.120 -      by (induct zs) (auto intro: * simp add: **)
   9.121 -  qed
   9.122 -  then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
   9.123 -qed
   9.124 -
   9.125 -lemma (in linorder) sort_conv_fold:
   9.126 -  "sort xs = fold insort xs []"
   9.127 -  by (rule sort_key_conv_fold) simp
   9.128 -
   9.129 -
   9.130 -text {* @{const Finite_Set.fold} and @{const fold} *}
   9.131 -
   9.132 -lemma (in comp_fun_commute) fold_set_fold_remdups:
   9.133 -  "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
   9.134 -  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
   9.135 -
   9.136 -lemma (in comp_fun_idem) fold_set_fold:
   9.137 -  "Finite_Set.fold f y (set xs) = fold f xs y"
   9.138 -  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
   9.139 -
   9.140 -lemma (in ab_semigroup_idem_mult) fold1_set_fold:
   9.141 -  assumes "xs \<noteq> []"
   9.142 -  shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
   9.143 -proof -
   9.144 -  interpret comp_fun_idem times by (fact comp_fun_idem)
   9.145 -  from assms obtain y ys where xs: "xs = y # ys"
   9.146 -    by (cases xs) auto
   9.147 -  show ?thesis
   9.148 -  proof (cases "set ys = {}")
   9.149 -    case True with xs show ?thesis by simp
   9.150 -  next
   9.151 -    case False
   9.152 -    then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
   9.153 -      by (simp only: finite_set fold1_eq_fold_idem)
   9.154 -    with xs show ?thesis by (simp add: fold_set_fold mult_commute)
   9.155 -  qed
   9.156 -qed
   9.157 -
   9.158 -lemma (in lattice) Inf_fin_set_fold:
   9.159 -  "Inf_fin (set (x # xs)) = fold inf xs x"
   9.160 -proof -
   9.161 -  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.162 -    by (fact ab_semigroup_idem_mult_inf)
   9.163 -  show ?thesis
   9.164 -    by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
   9.165 -qed
   9.166 -
   9.167 -lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
   9.168 -  "Inf_fin (set (x # xs)) = foldr inf xs x"
   9.169 -  by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   9.170 -
   9.171 -lemma (in lattice) Sup_fin_set_fold:
   9.172 -  "Sup_fin (set (x # xs)) = fold sup xs x"
   9.173 -proof -
   9.174 -  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.175 -    by (fact ab_semigroup_idem_mult_sup)
   9.176 -  show ?thesis
   9.177 -    by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
   9.178 -qed
   9.179 -
   9.180 -lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
   9.181 -  "Sup_fin (set (x # xs)) = foldr sup xs x"
   9.182 -  by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   9.183 -
   9.184 -lemma (in linorder) Min_fin_set_fold:
   9.185 -  "Min (set (x # xs)) = fold min xs x"
   9.186 -proof -
   9.187 -  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.188 -    by (fact ab_semigroup_idem_mult_min)
   9.189 -  show ?thesis
   9.190 -    by (simp add: Min_def fold1_set_fold del: set.simps)
   9.191 -qed
   9.192 -
   9.193 -lemma (in linorder) Min_fin_set_foldr [code_unfold]:
   9.194 -  "Min (set (x # xs)) = foldr min xs x"
   9.195 -  by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   9.196 -
   9.197 -lemma (in linorder) Max_fin_set_fold:
   9.198 -  "Max (set (x # xs)) = fold max xs x"
   9.199 -proof -
   9.200 -  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.201 -    by (fact ab_semigroup_idem_mult_max)
   9.202 -  show ?thesis
   9.203 -    by (simp add: Max_def fold1_set_fold del: set.simps)
   9.204 -qed
   9.205 -
   9.206 -lemma (in linorder) Max_fin_set_foldr [code_unfold]:
   9.207 -  "Max (set (x # xs)) = foldr max xs x"
   9.208 -  by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   9.209 -
   9.210 -lemma (in complete_lattice) Inf_set_fold:
   9.211 -  "Inf (set xs) = fold inf xs top"
   9.212 -proof -
   9.213 -  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.214 -    by (fact comp_fun_idem_inf)
   9.215 -  show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute)
   9.216 -qed
   9.217 -
   9.218 -lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
   9.219 -  "Inf (set xs) = foldr inf xs top"
   9.220 -  by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
   9.221 -
   9.222 -lemma (in complete_lattice) Sup_set_fold:
   9.223 -  "Sup (set xs) = fold sup xs bot"
   9.224 -proof -
   9.225 -  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   9.226 -    by (fact comp_fun_idem_sup)
   9.227 -  show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute)
   9.228 -qed
   9.229 -
   9.230 -lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
   9.231 -  "Sup (set xs) = foldr sup xs bot"
   9.232 -  by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
   9.233 -
   9.234 -lemma (in complete_lattice) INFI_set_fold:
   9.235 -  "INFI (set xs) f = fold (inf \<circ> f) xs top"
   9.236 -  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
   9.237 -
   9.238 -lemma (in complete_lattice) SUPR_set_fold:
   9.239 -  "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
   9.240 -  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
   9.241 -
   9.242 -
   9.243  text {* @{text nth_map} *}
   9.244  
   9.245  definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    10.1 --- a/src/HOL/More_Set.thy	Fri Jan 06 10:19:49 2012 +0100
    10.2 +++ b/src/HOL/More_Set.thy	Fri Jan 06 10:19:49 2012 +0100
    10.3 @@ -192,14 +192,6 @@
    10.4    "More_Set.Sup (coset []) = top"
    10.5    by (simp_all add: Sup_set_foldr)
    10.6  
    10.7 -lemma INF_code [code]:
    10.8 -  "INFI (set xs) f = foldr (inf \<circ> f) xs top"
    10.9 -  by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map)
   10.10 -
   10.11 -lemma SUP_sup [code]:
   10.12 -  "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
   10.13 -  by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map)
   10.14 -
   10.15  (* FIXME: better implement conversion by bisection *)
   10.16  
   10.17  lemma pred_of_set_fold_sup:
   10.18 @@ -223,8 +215,6 @@
   10.19    "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
   10.20    by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
   10.21  
   10.22 -hide_const (open) coset
   10.23 -
   10.24  
   10.25  subsection {* Operations on relations *}
   10.26  
    11.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Fri Jan 06 10:19:49 2012 +0100
    11.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Jan 06 10:19:49 2012 +0100
    11.3 @@ -247,7 +247,7 @@
    11.4      and "x \<in> set xs"
    11.5    shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
    11.6  proof -
    11.7 -  from assms have "More_List.fold f (remdups xs) = More_List.fold f (remove1 x (remdups xs)) \<circ> f x"
    11.8 +  from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \<circ> f x"
    11.9      by (auto intro!: fold_remove1_split elim: rsp_foldE)
   11.10    then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll)
   11.11  qed
    12.1 --- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Jan 06 10:19:49 2012 +0100
    12.2 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Jan 06 10:19:49 2012 +0100
    12.3 @@ -186,7 +186,7 @@
    12.4    by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
    12.5  
    12.6  lemma fold_fold:
    12.7 -  "fold f t = More_List.fold (prod_case f) (entries t)"
    12.8 +  "fold f t = List.fold (prod_case f) (entries t)"
    12.9    by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
   12.10  
   12.11  lemma is_empty_empty [simp]: