# HG changeset patch
# User wenzelm
# Date 1333822213 -7200
# Node ID 8a5a1d26337fbca0a21ae78d1fc030c89d1fb580
# Parent  b72fa7bf9a10ce2acf17244497ba88e55d51df8d# Parent  c1d297ef79697a7cb8c5cf514a3809585e325b1d
merged

diff -r c1d297ef7969 -r 8a5a1d26337f NEWS
--- a/NEWS	Sat Apr 07 19:59:09 2012 +0200
+++ b/NEWS	Sat Apr 07 20:10:13 2012 +0200
@@ -208,10 +208,11 @@
   SUPR_set_fold ~> SUP_set_fold
   INF_code ~> INF_set_foldr
   SUP_code ~> SUP_set_foldr
-  foldr.simps ~> foldr_Nil foldr_Cons (in point-free formulation)
-  foldl.simps ~> foldl_Nil foldl_Cons
-  foldr_fold_rev ~> foldr_def
-  foldl_fold ~> foldl_def
+  foldr.simps ~> foldr.simps (in point-free formulation)
+  foldr_fold_rev ~> foldr_conv_fold
+  foldl_fold ~> foldl_conv_fold
+  foldr_foldr ~> foldr_conv_foldl
+  foldl_foldr ~> foldl_conv_foldr
 
 INCOMPATIBILITY.
 
@@ -220,11 +221,19 @@
 rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,
 concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
 foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,
-listsum_conv_fold, listsum_foldl, sort_foldl_insort.  INCOMPATIBILITY.
-Prefer "List.fold" with canonical argument order, or boil down
-"List.foldr" and "List.foldl" to "List.fold" by unfolding "foldr_def"
-and "foldl_def".  For the common phrases "%xs. List.foldr plus xs 0"
-and "List.foldl plus 0", prefer "List.listsum".
+listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,
+foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.
+INCOMPATIBILITY.  For the common phrases "%xs. List.foldr plus xs 0"
+and "List.foldl plus 0", prefer "List.listsum".  Otherwise it can
+be useful to boil down "List.foldr" and "List.foldl" to "List.fold"
+by unfolding "foldr_conv_fold" and "foldl_conv_fold".
+
+* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,
+inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,
+Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,
+INF_set_foldr, SUP_set_foldr.  INCOMPATIBILITY.  Prefer corresponding
+lemmas over fold rather than foldr, or make use of lemmas
+fold_conv_foldr and fold_rev.
 
 * Congruence rules Option.map_cong and Option.bind_cong for recursion
 through option types.
diff -r c1d297ef7969 -r 8a5a1d26337f src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Sat Apr 07 19:59:09 2012 +0200
+++ b/src/HOL/Library/AList.thy	Sat Apr 07 20:10:13 2012 +0200
@@ -97,7 +97,7 @@
   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_def split_def)
+  then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_conv_fold split_def)
 qed
 
 lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
@@ -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_def zip_rev zip_map_fst_snd)
+  by (simp add: merge_def updates_def foldr_conv_fold 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)
@@ -448,7 +448,7 @@
     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_def fun_eq_iff)
+    by (simp add: merge_def map_add_map_of_foldr foldr_conv_fold fun_eq_iff)
 qed
 
 corollary merge_conv:
diff -r c1d297ef7969 -r 8a5a1d26337f src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Sat Apr 07 19:59:09 2012 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Sat Apr 07 20:10:13 2012 +0200
@@ -1076,7 +1076,7 @@
   from this Empty_is_rbt have
     "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_def)
+  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_conv_fold)
 qed
 
 hide_const (open) R B Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
diff -r c1d297ef7969 -r 8a5a1d26337f src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Apr 07 19:59:09 2012 +0200
+++ b/src/HOL/List.thy	Sat Apr 07 20:10:13 2012 +0200
@@ -85,18 +85,20 @@
 syntax (HTML output)
   "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
 
-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 f s xs = fold (\<lambda>x s. f s x)  xs s"
+primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
+where
+  fold_Nil:  "fold f [] = id"
+| fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x" -- {* natural argument order *}
+
+primrec foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
+where
+  foldr_Nil:  "foldr f [] = id"
+| foldr_Cons: "foldr f (x # xs) = f x \<circ> foldr f xs" -- {* natural argument order *}
+
+primrec 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
   concat:: "'a list list \<Rightarrow> 'a list" where
@@ -250,8 +252,8 @@
 @{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 "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 "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
+@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
 @{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}\\
@@ -277,7 +279,7 @@
 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add: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 foldr_def)}
+@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}
 \end{tabular}}
 \caption{Characteristic examples}
 \label{fig:Characteristic}
@@ -2387,7 +2389,7 @@
 by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
 
 
-subsubsection {* @{const fold} with canonical argument order *}
+subsubsection {* @{const fold} with natural 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"
@@ -2477,7 +2479,7 @@
   qed
 qed
 
-lemma union_set_fold:
+lemma union_set_fold [code]:
   "set xs \<union> A = fold Set.insert xs A"
 proof -
   interpret comp_fun_idem Set.insert
@@ -2485,7 +2487,11 @@
   show ?thesis by (simp add: union_fold_insert fold_set_fold)
 qed
 
-lemma minus_set_fold:
+lemma union_coset_filter [code]:
+  "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
+  by auto
+
+lemma minus_set_fold [code]:
   "A - set xs = fold Set.remove xs A"
 proof -
   interpret comp_fun_idem Set.remove
@@ -2494,6 +2500,18 @@
     by (simp add: minus_fold_remove [of _ A] fold_set_fold)
 qed
 
+lemma minus_coset_filter [code]:
+  "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
+  by auto
+
+lemma inter_set_filter [code]:
+  "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
+  by auto
+
+lemma inter_coset_fold [code]:
+  "A \<inter> List.coset xs = fold Set.remove xs A"
+  by (simp add: Diff_eq [symmetric] minus_set_fold)
+
 lemma (in lattice) Inf_fin_set_fold:
   "Inf_fin (set (x # xs)) = fold inf xs x"
 proof -
@@ -2503,6 +2521,8 @@
     by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
 qed
 
+declare Inf_fin_set_fold [code]
+
 lemma (in lattice) Sup_fin_set_fold:
   "Sup_fin (set (x # xs)) = fold sup xs x"
 proof -
@@ -2512,6 +2532,8 @@
     by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
 qed
 
+declare Sup_fin_set_fold [code]
+
 lemma (in linorder) Min_fin_set_fold:
   "Min (set (x # xs)) = fold min xs x"
 proof -
@@ -2521,6 +2543,8 @@
     by (simp add: Min_def fold1_set_fold del: set.simps)
 qed
 
+declare Min_fin_set_fold [code]
+
 lemma (in linorder) Max_fin_set_fold:
   "Max (set (x # xs)) = fold max xs x"
 proof -
@@ -2530,6 +2554,8 @@
     by (simp add: Max_def fold1_set_fold del: set.simps)
 qed
 
+declare Max_fin_set_fold [code]
+
 lemma (in complete_lattice) Inf_set_fold:
   "Inf (set xs) = fold inf xs top"
 proof -
@@ -2538,6 +2564,8 @@
   show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute)
 qed
 
+declare Inf_set_fold [where 'a = "'a set", code]
+
 lemma (in complete_lattice) Sup_set_fold:
   "Sup (set xs) = fold sup xs bot"
 proof -
@@ -2546,137 +2574,72 @@
   show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute)
 qed
 
+declare Sup_set_fold [where 'a = "'a set", code]
+
 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 ..
 
+declare INF_set_fold [code]
+
 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 ..
 
+declare SUP_set_fold [code]
 
 subsubsection {* Fold variants: @{const foldr} and @{const foldl} *}
 
 text {* Correspondence *}
 
-lemma foldr_foldl: -- {* The ``Third Duality Theorem'' in Bird \& Wadler: *}
+lemma foldr_conv_fold [code_abbrev]:
+  "foldr f xs = fold f (rev xs)"
+  by (induct xs) simp_all
+
+lemma foldl_conv_fold:
+  "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
+  by (induct xs arbitrary: s) simp_all
+
+lemma foldr_conv_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:
+  by (simp add: foldr_conv_fold foldl_conv_fold)
+
+lemma foldl_conv_foldr:
   "foldl f a xs = foldr (\<lambda>x y. f y x) (rev xs) a"
-  by (simp add: foldr_def foldl_def)
+  by (simp add: foldr_conv_fold foldl_conv_fold)
 
 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)
+  using assms unfolding foldr_conv_fold by (rule fold_rev)
 
 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)
+  by (auto simp add: foldr_conv_fold 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)
+  by (auto simp add: foldl_conv_fold intro!: fold_cong)
 
 lemma foldr_append [simp]:
   "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
-  by (simp add: foldr_def)
+  by (simp add: foldr_conv_fold)
 
 lemma foldl_append [simp]:
   "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
-  by (simp add: foldl_def)
+  by (simp add: foldl_conv_fold)
 
 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)
+  by (simp add: foldr_conv_fold 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! *}
+  by (simp add: foldl_conv_fold fold_map comp_def)
 
 lemma concat_conv_foldr [code]:
   "concat xss = foldr append xss []"
-  by (simp add: fold_append_concat_rev foldr_def)
-
-lemma minus_set_foldr [code]:
-  "A - set xs = foldr Set.remove xs A"
-proof -
-  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
-    by (auto simp add: remove_def)
-  then show ?thesis by (simp add: minus_set_fold foldr_fold)
-qed
-
-lemma subtract_coset_filter [code]:
-  "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
-  by auto
-
-lemma union_set_foldr [code]:
-  "set xs \<union> A = foldr Set.insert xs A"
-proof -
-  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
-    by auto
-  then show ?thesis by (simp add: union_set_fold foldr_fold)
-qed
-
-lemma union_coset_foldr [code]:
-  "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
-  by auto
-
-lemma inter_set_filer [code]:
-  "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
-  by auto
-
-lemma inter_coset_foldr [code]:
-  "A \<inter> List.coset xs = foldr Set.remove xs A"
-  by (simp add: Diff_eq [symmetric] minus_set_foldr)
-
-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)
-
-declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code]
-
-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])
+  by (simp add: fold_append_concat_rev foldr_conv_fold)
 
 
 subsubsection {* @{text upt} *}
@@ -3108,7 +3071,7 @@
 
 lemma (in comm_monoid_add) listsum_rev [simp]:
   "listsum (rev xs) = listsum xs"
-  by (simp add: listsum_def foldr_def fold_rev fun_eq_iff add_ac)
+  by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff add_ac)
 
 lemma (in monoid_add) fold_plus_listsum_rev:
   "fold plus xs = plus (listsum (rev xs))"
@@ -3116,40 +3079,12 @@
   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> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_conv_fold)
   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
@@ -3186,17 +3121,18 @@
 
 lemma listsum_eq_0_nat_iff_nat [simp]:
   "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
-  by (simp add: listsum_def foldr_conv_foldl)
+  by (induct ns) simp_all
+
+lemma member_le_listsum_nat:
+  "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns"
+  by (induct ns) auto
 
 lemma elem_le_listsum_nat:
   "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
-apply(induct ns arbitrary: k)
- apply simp
-apply(fastforce simp add:nth_Cons split: nat.split)
-done
+  by (rule member_le_listsum_nat) simp
 
 lemma listsum_update_nat:
-  "k<size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
+  "k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
 apply(induct ns arbitrary:k)
  apply (auto split:nat.split)
 apply(drule elem_le_listsum_nat)
@@ -4053,7 +3989,7 @@
     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)
+  then show ?thesis by (simp add: sort_key_def foldr_conv_fold)
 qed
 
 lemma (in linorder) sort_conv_fold:
@@ -4601,7 +4537,7 @@
 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
 proof (rule mono_inf [where f=listsp, THEN order_antisym])
   show "mono listsp" by (simp add: mono_def listsp_mono)
-  show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
+  show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI)
 qed
 
 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def]
@@ -5631,8 +5567,6 @@
 
 subsubsection {* Implementation of sets by lists *}
 
-text {* Basic operations *}
-
 lemma is_empty_set [code]:
   "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
   by (simp add: Set.is_empty_def null_def)
@@ -5676,6 +5610,17 @@
   "image f (set xs) = set (map f xs)"
   by simp
 
+lemma subset_code [code]:
+  "set xs \<le> B \<longleftrightarrow> (\<forall>x\<in>set xs. x \<in> B)"
+  "A \<le> List.coset ys \<longleftrightarrow> (\<forall>y\<in>set ys. y \<notin> A)"
+  "List.coset [] \<le> set [] \<longleftrightarrow> False"
+  by auto
+
+text {* A frequent case – avoid intermediate sets *}
+lemma [code_unfold]:
+  "set xs \<subseteq> set ys \<longleftrightarrow> list_all (\<lambda>x. x \<in> set ys) xs"
+  by (auto simp: list_all_iff)
+
 lemma Ball_set [code]:
   "Ball (set xs) P \<longleftrightarrow> list_all P xs"
   by (simp add: list_all_iff)
@@ -5701,20 +5646,6 @@
   "Pow (set (x # xs)) = (let A = Pow (set xs) in A \<union> insert x ` A)"
   by (simp_all add: Pow_insert Let_def)
 
-text {* Further operations on sets *}
-
-(* Minimal refinement of equality on sets *)
-declare subset_eq[code del]
-lemma subset_code [code]:
-  "set xs <= B \<longleftrightarrow> (ALL x : set xs. x : B)"
-  "List.coset xs <= List.coset ys \<longleftrightarrow> set ys <= set xs"
-  "List.coset [] <= set [] \<longleftrightarrow> False"
-by auto
-
-text{* Optimising a frequent case: *}
-lemma [code_unfold]: "set xs \<subseteq> set ys \<longleftrightarrow> list_all (\<lambda>x. x \<in> set ys) xs"
-by (auto simp: list_all_iff)
-
 lemma setsum_code [code]:
   "setsum f (set xs) = listsum (map f (remdups xs))"
 by (simp add: listsum_distinct_conv_setsum_set)
@@ -5724,8 +5655,7 @@
 
 lemma [code]:
   "map_project f (set xs) = set (List.map_filter f xs)"
-unfolding map_project_def map_filter_def
-by auto (metis (lifting, mono_tags) CollectI image_eqI o_apply the.simps)
+  by (auto simp add: map_project_def map_filter_def image_def)
 
 hide_const (open) map_project
 
@@ -5756,3 +5686,4 @@
   by (simp add: wf_iff_acyclic_if_finite)
 
 end
+
diff -r c1d297ef7969 -r 8a5a1d26337f src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Sat Apr 07 19:59:09 2012 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sat Apr 07 20:10:13 2012 +0200
@@ -408,7 +408,7 @@
 
 lemma [code]:
   "unstables r step ss = 
-   foldr (\<lambda>p A. if \<not>stable r step ss p then insert p A else A) [0..<size ss] {}"
+   fold (\<lambda>p A. if \<not>stable r step ss p then insert p A else A) [0..<size ss] {}"
 proof -
   have "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
     apply (unfold unstables_def)
@@ -425,7 +425,7 @@
     apply simp+
     done
   also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
-  also note Sup_set_foldr also note foldr_map
+  also note Sup_set_fold also note fold_map
   also have "op \<union> \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) = 
             (\<lambda>p A. if \<not>stable r step ss p then insert p A else A)"
     by(auto simp add: fun_eq_iff)
@@ -486,3 +486,4 @@
 *}
 
 end
+
diff -r c1d297ef7969 -r 8a5a1d26337f src/HOL/Nominal/Examples/Standardization.thy
--- a/src/HOL/Nominal/Examples/Standardization.thy	Sat Apr 07 19:59:09 2012 +0200
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Sat Apr 07 20:10:13 2012 +0200
@@ -213,7 +213,8 @@
     prefer 2
     apply (erule allE, erule impE, rule refl, erule spec)
     apply simp
-   apply (clarsimp simp add: foldr_conv_foldl [symmetric] foldr_def fold_plus_listsum_rev listsum_map_remove1)
+    apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev)
+    apply (fastforce simp add: listsum_map_remove1)
   apply clarify
   apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)")
    prefer 2
@@ -232,8 +233,10 @@
   apply clarify
   apply (erule allE, erule impE)
    prefer 2
-   apply blast   
-  apply (force intro: le_imp_less_Suc trans_le_add1 trans_le_add2 elem_le_sum) 
+   apply blast
+  apply simp
+  apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev)
+  apply (fastforce simp add: listsum_map_remove1)
   done
 
 theorem Apps_lam_induct:
@@ -855,3 +858,4 @@
 qed
 
 end
+
diff -r c1d297ef7969 -r 8a5a1d26337f src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sat Apr 07 19:59:09 2012 +0200
+++ b/src/HOL/Predicate.thy	Sat Apr 07 20:10:13 2012 +0200
@@ -702,7 +702,8 @@
 
 text {* Misc *}
 
-declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
+declare Inf_set_fold [where 'a = "'a Predicate.pred", code]
+declare Sup_set_fold [where 'a = "'a Predicate.pred", code]
 
 (* FIXME: better implement conversion by bisection *)
 
diff -r c1d297ef7969 -r 8a5a1d26337f src/HOL/Proofs/Lambda/ListApplication.thy
--- a/src/HOL/Proofs/Lambda/ListApplication.thy	Sat Apr 07 19:59:09 2012 +0200
+++ b/src/HOL/Proofs/Lambda/ListApplication.thy	Sat Apr 07 20:10:13 2012 +0200
@@ -110,10 +110,8 @@
     prefer 2
     apply (erule allE, erule mp, rule refl)
    apply simp
-   apply (rule lem0)
-    apply force
-   apply (rule elem_le_sum)
-   apply force
+   apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev)
+   apply (fastforce simp add: listsum_map_remove1)
   apply clarify
   apply (rule assms)
    apply (erule allE, erule impE)
@@ -128,8 +126,8 @@
   apply (rule le_imp_less_Suc)
   apply (rule trans_le_add1)
   apply (rule trans_le_add2)
-  apply (rule elem_le_sum)
-  apply force
+  apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev)
+  apply (simp add: member_le_listsum_nat)
   done
 
 theorem Apps_dB_induct:
@@ -143,3 +141,4 @@
   done
 
 end
+
diff -r c1d297ef7969 -r 8a5a1d26337f src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Apr 07 19:59:09 2012 +0200
+++ b/src/HOL/Set.thy	Sat Apr 07 20:10:13 2012 +0200
@@ -506,7 +506,7 @@
   -- {* Classical elimination rule. *}
   by (auto simp add: less_eq_set_def le_fun_def)
 
-lemma subset_eq [code, no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
+lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
 
 lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   by blast