# HG changeset patch
# User haftmann
# Date 1325841589 -3600
# Node ID d9fe85d3d2cd7e494e25017ff353a977d7d7d9f5
# Parent  5a29dbf4c1552ffca6f2f447acd1305066972265
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)

diff -r 5a29dbf4c155 -r d9fe85d3d2cd doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Fri Jan 06 10:19:49 2012 +0100
+++ b/doc-src/Main/Docs/Main_Doc.thy	Fri Jan 06 10:19:49 2012 +0100
@@ -495,8 +495,9 @@
 @{const List.drop} & @{typeof List.drop}\\
 @{const List.dropWhile} & @{typeof List.dropWhile}\\
 @{const List.filter} & @{typeof List.filter}\\
+@{const List.fold} & @{typeof List.fold}\\
+@{const List.foldr} & @{typeof List.foldr}\\
 @{const List.foldl} & @{typeof List.foldl}\\
-@{const List.foldr} & @{typeof List.foldr}\\
 @{const List.hd} & @{typeof List.hd}\\
 @{const List.last} & @{typeof List.last}\\
 @{const List.length} & @{typeof List.length}\\
diff -r 5a29dbf4c155 -r d9fe85d3d2cd src/HOL/Import/HOL/rich_list.imp
--- a/src/HOL/Import/HOL/rich_list.imp	Fri Jan 06 10:19:49 2012 +0100
+++ b/src/HOL/Import/HOL/rich_list.imp	Fri Jan 06 10:19:49 2012 +0100
@@ -100,7 +100,6 @@
   "REVERSE_SNOC" > "HOL4Base.rich_list.REVERSE_SNOC"
   "REVERSE_REVERSE" > "List.rev_rev_ident"
   "REVERSE_FOLDR" > "HOL4Base.rich_list.REVERSE_FOLDR"
-  "REVERSE_FOLDL" > "List.rev_foldl_cons"
   "REVERSE_FLAT" > "HOL4Base.rich_list.REVERSE_FLAT"
   "REVERSE_EQ_NIL" > "List.rev_is_Nil_conv"
   "REVERSE_APPEND" > "List.rev_append"
@@ -238,7 +237,6 @@
   "FLAT_SNOC" > "HOL4Base.rich_list.FLAT_SNOC"
   "FLAT_REVERSE" > "HOL4Base.rich_list.FLAT_REVERSE"
   "FLAT_FOLDR" > "HOL4Base.rich_list.FLAT_FOLDR"
-  "FLAT_FOLDL" > "List.concat_conv_foldl"
   "FLAT_FLAT" > "HOL4Base.rich_list.FLAT_FLAT"
   "FLAT_APPEND" > "List.concat_append"
   "FLAT" > "HOL4Compat.FLAT"
diff -r 5a29dbf4c155 -r d9fe85d3d2cd src/HOL/Library/AList_Impl.thy
--- a/src/HOL/Library/AList_Impl.thy	Fri Jan 06 10:19:49 2012 +0100
+++ b/src/HOL/Library/AList_Impl.thy	Fri Jan 06 10:19:49 2012 +0100
@@ -76,10 +76,10 @@
 
 lemma image_update [simp]:
   "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
-  by (simp add: update_conv' image_map_upd)
+  by (simp add: update_conv')
 
 definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
-  "updates ks vs = More_List.fold (prod_case update) (zip ks vs)"
+  "updates ks vs = fold (prod_case update) (zip ks vs)"
 
 lemma updates_simps [simp]:
   "updates [] vs ps = ps"
@@ -94,10 +94,10 @@
 
 lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
 proof -
-  have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
-    More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
+  have "map_of \<circ> fold (prod_case update) (zip ks vs) =
+    fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
     by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
-  then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_fold split_def)
+  then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_def split_def)
 qed
 
 lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
@@ -107,12 +107,12 @@
   assumes "distinct (map fst al)"
   shows "distinct (map fst (updates ks vs al))"
 proof -
-  have "distinct (More_List.fold
+  have "distinct (fold
        (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
        (zip ks vs) (map fst al))"
     by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
-  moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
-    More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
+  moreover have "map fst \<circ> fold (prod_case update) (zip ks vs) =
+    fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
     by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
   ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
 qed
@@ -339,8 +339,8 @@
 lemma clearjunk_updates:
   "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
 proof -
-  have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
-    More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
+  have "clearjunk \<circ> fold (prod_case update) (zip ks vs) =
+    fold (prod_case update) (zip ks vs) \<circ> clearjunk"
     by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
   then show ?thesis by (simp add: updates_def fun_eq_iff)
 qed
@@ -427,7 +427,7 @@
 
 lemma merge_updates:
   "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
-  by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
+  by (simp add: merge_def updates_def foldr_def zip_rev zip_map_fst_snd)
 
 lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
   by (induct ys arbitrary: xs) (auto simp add: dom_update)
@@ -444,11 +444,11 @@
 lemma merge_conv':
   "map_of (merge xs ys) = map_of xs ++ map_of ys"
 proof -
-  have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
-    More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
+  have "map_of \<circ> fold (prod_case update) (rev ys) =
+    fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
     by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
   then show ?thesis
-    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev fun_eq_iff)
+    by (simp add: merge_def map_add_map_of_foldr foldr_def fun_eq_iff)
 qed
 
 corollary merge_conv:
diff -r 5a29dbf4c155 -r d9fe85d3d2cd src/HOL/Library/Cset.thy
--- a/src/HOL/Library/Cset.thy	Fri Jan 06 10:19:49 2012 +0100
+++ b/src/HOL/Library/Cset.thy	Fri Jan 06 10:19:49 2012 +0100
@@ -370,7 +370,7 @@
 
 lemma bind_set:
   "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
-  by (simp add: Cset.bind_def SUPR_set_fold)
+  by (simp add: Cset.bind_def SUP_set_fold)
 hide_fact (open) bind_set
 
 lemma pred_of_cset_set:
diff -r 5a29dbf4c155 -r d9fe85d3d2cd src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Fri Jan 06 10:19:49 2012 +0100
+++ b/src/HOL/Library/Dlist.thy	Fri Jan 06 10:19:49 2012 +0100
@@ -74,7 +74,7 @@
   "length dxs = List.length (list_of_dlist dxs)"
 
 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
-  "fold f dxs = More_List.fold f (list_of_dlist dxs)"
+  "fold f dxs = List.fold f (list_of_dlist dxs)"
 
 definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
   "foldr f dxs = List.foldr f (list_of_dlist dxs)"
diff -r 5a29dbf4c155 -r d9fe85d3d2cd src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Fri Jan 06 10:19:49 2012 +0100
+++ b/src/HOL/Library/RBT.thy	Fri Jan 06 10:19:49 2012 +0100
@@ -146,7 +146,7 @@
   by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
 
 lemma fold_fold:
-  "fold f t = More_List.fold (prod_case f) (entries t)"
+  "fold f t = List.fold (prod_case f) (entries t)"
   by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
 
 lemma is_empty_empty [simp]:
diff -r 5a29dbf4c155 -r d9fe85d3d2cd src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Fri Jan 06 10:19:49 2012 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Fri Jan 06 10:19:49 2012 +0100
@@ -1049,7 +1049,7 @@
 subsection {* Folding over entries *}
 
 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
-  "fold f t = More_List.fold (prod_case f) (entries t)"
+  "fold f t = List.fold (prod_case f) (entries t)"
 
 lemma fold_simps [simp, code]:
   "fold f Empty = id"
@@ -1071,12 +1071,12 @@
 proof -
   obtain ys where "ys = rev xs" by simp
   have "\<And>t. is_rbt t \<Longrightarrow>
-    lookup (More_List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
+    lookup (List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
       by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta)
   from this Empty_is_rbt have
-    "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
+    "lookup (List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
      by (simp add: `ys = rev xs`)
-  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev)
+  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_def)
 qed
 
 hide_const (open) R B Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
diff -r 5a29dbf4c155 -r d9fe85d3d2cd src/HOL/List.thy
--- 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:
diff -r 5a29dbf4c155 -r d9fe85d3d2cd src/HOL/More_List.thy
--- a/src/HOL/More_List.thy	Fri Jan 06 10:19:49 2012 +0100
+++ b/src/HOL/More_List.thy	Fri Jan 06 10:19:49 2012 +0100
@@ -6,242 +6,6 @@
 imports List
 begin
 
-text {* Fold combinator with canonical argument order *}
-
-primrec 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"
-
-lemma foldl_fold:
-  "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
-  by (induct xs arbitrary: s) simp_all
-
-lemma foldr_fold_rev:
-  "foldr f xs = fold f (rev xs)"
-  by (simp add: foldr_foldl foldl_fold fun_eq_iff)
-
-lemma fold_rev_conv [code_unfold]:
-  "fold f (rev xs) = foldr f xs"
-  by (simp add: foldr_fold_rev)
-  
-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
-
-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
-
-lemma fold_weak_invariant:
-  assumes "P s"
-    and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
-  shows "P (fold f xs s)"
-  using assms by (induct xs arbitrary: s) simp_all
-
-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_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_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 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_fold_rev by (rule fold_rev)
-
-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
-
-lemma concat_conv_foldr [code]:
-  "concat xss = foldr append xss []"
-  by (simp add: fold_append_concat_rev foldr_fold_rev)
-
-lemma fold_plus_listsum_rev:
-  "fold plus xs = plus (listsum (rev xs))"
-  by (induct xs) (simp_all add: add.assoc)
-
-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 (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_fold_rev)
-qed
-
-lemma (in linorder) sort_conv_fold:
-  "sort xs = fold insort xs []"
-  by (rule sort_key_conv_fold) simp
-
-
-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_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_fold:
-  assumes "xs \<noteq> []"
-  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"
-    by (cases xs) auto
-  show ?thesis
-  proof (cases "set ys = {}")
-    case True with xs show ?thesis by simp
-  next
-    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_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) Inf_fin_set_foldr [code_unfold]:
-  "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_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 lattice) Sup_fin_set_foldr [code_unfold]:
-  "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_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) Min_fin_set_foldr [code_unfold]:
-  "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_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 linorder) Max_fin_set_foldr [code_unfold]:
-  "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_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) Inf_set_foldr [code_unfold]:
-  "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_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) Sup_set_foldr [code_unfold]:
-  "Sup (set xs) = foldr sup xs bot"
-  by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
-
-lemma (in complete_lattice) INFI_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) SUPR_set_fold:
-  "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
-  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
-
-
 text {* @{text nth_map} *}
 
 definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
diff -r 5a29dbf4c155 -r d9fe85d3d2cd src/HOL/More_Set.thy
--- a/src/HOL/More_Set.thy	Fri Jan 06 10:19:49 2012 +0100
+++ b/src/HOL/More_Set.thy	Fri Jan 06 10:19:49 2012 +0100
@@ -192,14 +192,6 @@
   "More_Set.Sup (coset []) = top"
   by (simp_all add: Sup_set_foldr)
 
-lemma INF_code [code]:
-  "INFI (set xs) f = foldr (inf \<circ> f) xs top"
-  by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map)
-
-lemma SUP_sup [code]:
-  "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
-  by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map)
-
 (* FIXME: better implement conversion by bisection *)
 
 lemma pred_of_set_fold_sup:
@@ -223,8 +215,6 @@
   "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
   by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
 
-hide_const (open) coset
-
 
 subsection {* Operations on relations *}
 
diff -r 5a29dbf4c155 -r d9fe85d3d2cd src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Fri Jan 06 10:19:49 2012 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Jan 06 10:19:49 2012 +0100
@@ -247,7 +247,7 @@
     and "x \<in> set xs"
   shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
 proof -
-  from assms have "More_List.fold f (remdups xs) = More_List.fold f (remove1 x (remdups xs)) \<circ> f x"
+  from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \<circ> f x"
     by (auto intro!: fold_remove1_split elim: rsp_foldE)
   then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll)
 qed
diff -r 5a29dbf4c155 -r d9fe85d3d2cd src/HOL/Quotient_Examples/Lift_RBT.thy
--- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Jan 06 10:19:49 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Jan 06 10:19:49 2012 +0100
@@ -186,7 +186,7 @@
   by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
 
 lemma fold_fold:
-  "fold f t = More_List.fold (prod_case f) (entries t)"
+  "fold f t = List.fold (prod_case f) (entries t)"
   by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
 
 lemma is_empty_empty [simp]: