1.1 --- a/NEWS	Fri Apr 06 14:40:00 2012 +0200
     1.2 +++ b/NEWS	Fri Apr 06 18:17:16 2012 +0200
     1.3 @@ -208,10 +208,11 @@
     1.4    SUPR_set_fold ~> SUP_set_fold
     1.5    INF_code ~> INF_set_foldr
     1.6    SUP_code ~> SUP_set_foldr
     1.7 -  foldr.simps ~> foldr_Nil foldr_Cons (in point-free formulation)
     1.8 -  foldl.simps ~> foldl_Nil foldl_Cons
     1.9 -  foldr_fold_rev ~> foldr_def
    1.10 -  foldl_fold ~> foldl_def
    1.11 +  foldr.simps ~> foldr.simps (in point-free formulation)
    1.12 +  foldr_fold_rev ~> foldr_conv_fold
    1.13 +  foldl_fold ~> foldl_conv_fold
    1.14 +  foldr_foldr ~> foldr_conv_foldl
    1.15 +  foldl_foldr ~> foldl_conv_foldr
    1.16  
    1.17  INCOMPATIBILITY.
    1.18  
    1.19 @@ -220,11 +221,12 @@
    1.20  rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,
    1.21  concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
    1.22  foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,
    1.23 -listsum_conv_fold, listsum_foldl, sort_foldl_insort.  INCOMPATIBILITY.
    1.24 -Prefer "List.fold" with canonical argument order, or boil down
    1.25 -"List.foldr" and "List.foldl" to "List.fold" by unfolding "foldr_def"
    1.26 -and "foldl_def".  For the common phrases "%xs. List.foldr plus xs 0"
    1.27 -and "List.foldl plus 0", prefer "List.listsum".
    1.28 +listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,
    1.29 +foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.
    1.30 +INCOMPATIBILITY.  For the common phrases "%xs. List.foldr plus xs 0"
    1.31 +and "List.foldl plus 0", prefer "List.listsum".  Otherwise it can
    1.32 +be useful to boil down "List.foldr" and "List.foldl" to "List.fold"
    1.33 +by unfolding "foldr_conv_fold" and "foldl_conv_fold".  
    1.34  
    1.35  * Congruence rules Option.map_cong and Option.bind_cong for recursion
    1.36  through option types.

     2.1 --- a/src/HOL/Library/AList.thy	Fri Apr 06 14:40:00 2012 +0200
     2.2 +++ b/src/HOL/Library/AList.thy	Fri Apr 06 18:17:16 2012 +0200
     2.3 @@ -97,7 +97,7 @@
     2.4    have "map_of \<circ> fold (prod_case update) (zip ks vs) =
     2.5      fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
     2.6      by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
     2.7 -  then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_def split_def)
     2.8 +  then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_conv_fold split_def)
     2.9  qed
    2.10  
    2.11  lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
    2.12 @@ -427,7 +427,7 @@
    2.13  
    2.14  lemma merge_updates:
    2.15    "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
    2.16 -  by (simp add: merge_def updates_def foldr_def zip_rev zip_map_fst_snd)
    2.17 +  by (simp add: merge_def updates_def foldr_conv_fold zip_rev zip_map_fst_snd)
    2.18  
    2.19  lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
    2.20    by (induct ys arbitrary: xs) (auto simp add: dom_update)
    2.21 @@ -448,7 +448,7 @@
    2.22      fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
    2.23      by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
    2.24    then show ?thesis
    2.25 -    by (simp add: merge_def map_add_map_of_foldr foldr_def fun_eq_iff)
    2.26 +    by (simp add: merge_def map_add_map_of_foldr foldr_conv_fold fun_eq_iff)
    2.27  qed
    2.28  
    2.29  corollary merge_conv:

     3.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Apr 06 14:40:00 2012 +0200
     3.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Apr 06 18:17:16 2012 +0200
     3.3 @@ -1076,7 +1076,7 @@
     3.4    from this Empty_is_rbt have
     3.5      "lookup (List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
     3.6       by (simp add: `ys = rev xs`)
     3.7 -  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_def)
     3.8 +  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_conv_fold)
     3.9  qed
    3.10  
    3.11  hide_const (open) R B Empty insert delete entries keys bulkload lookup map_entry map fold union sorted

     4.1 --- a/src/HOL/List.thy	Fri Apr 06 14:40:00 2012 +0200
     4.2 +++ b/src/HOL/List.thy	Fri Apr 06 18:17:16 2012 +0200
     4.3 @@ -85,18 +85,20 @@
     4.4  syntax (HTML output)
     4.5    "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
     4.6  
     4.7 -primrec -- {* canonical argument order *}
     4.8 -  fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
     4.9 -    "fold f [] = id"
    4.10 -  | "fold f (x # xs) = fold f xs \<circ> f x"
    4.11 -
    4.12 -definition 
    4.13 -  foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    4.14 -  [code_abbrev]: "foldr f xs = fold f (rev xs)"
    4.15 -
    4.16 -definition
    4.17 -  foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
    4.18 -  "foldl f s xs = fold (\<lambda>x s. f s x)  xs s"
    4.19 +primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
    4.20 +where
    4.21 +  fold_Nil:  "fold f [] = id"
    4.22 +| fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x" -- {* natural argument order *}
    4.23 +
    4.24 +primrec foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
    4.25 +where
    4.26 +  foldr_Nil:  "foldr f [] = id"
    4.27 +| foldr_Cons: "foldr f (x # xs) = f x \<circ> foldr f xs" -- {* natural argument order *}
    4.28 +
    4.29 +primrec foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
    4.30 +where
    4.31 +  foldl_Nil:  "foldl f a [] = a"
    4.32 +| foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
    4.33  
    4.34  primrec
    4.35    concat:: "'a list list \<Rightarrow> 'a list" where
    4.36 @@ -250,8 +252,8 @@
    4.37  @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
    4.38  @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
    4.39  @{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\
    4.40 -@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by (simp add: foldr_def)}\\
    4.41 -@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by (simp add: foldl_def)}\\
    4.42 +@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
    4.43 +@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
    4.44  @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
    4.45  @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
    4.46  @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
    4.47 @@ -277,7 +279,7 @@
    4.48  @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
    4.49  @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
    4.50  @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
    4.51 -@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)}
    4.52 +@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}
    4.53  \end{tabular}}
    4.54  \caption{Characteristic examples}
    4.55  \label{fig:Characteristic}
    4.56 @@ -2387,7 +2389,7 @@
    4.57  by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
    4.58  
    4.59  
    4.60 -subsubsection {* @{const fold} with canonical argument order *}
    4.61 +subsubsection {* @{const fold} with natural argument order *}
    4.62  
    4.63  lemma fold_remove1_split:
    4.64    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"
    4.65 @@ -2477,7 +2479,7 @@
    4.66    qed
    4.67  qed
    4.68  
    4.69 -lemma union_set_fold:
    4.70 +lemma union_set_fold [code]:
    4.71    "set xs \<union> A = fold Set.insert xs A"
    4.72  proof -
    4.73    interpret comp_fun_idem Set.insert
    4.74 @@ -2485,7 +2487,11 @@
    4.75    show ?thesis by (simp add: union_fold_insert fold_set_fold)
    4.76  qed
    4.77  
    4.78 -lemma minus_set_fold:
    4.79 +lemma union_coset_filter [code]:
    4.80 +  "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
    4.81 +  by auto
    4.82 +
    4.83 +lemma minus_set_fold [code]:
    4.84    "A - set xs = fold Set.remove xs A"
    4.85  proof -
    4.86    interpret comp_fun_idem Set.remove
    4.87 @@ -2494,6 +2500,18 @@
    4.88      by (simp add: minus_fold_remove [of _ A] fold_set_fold)
    4.89  qed
    4.90  
    4.91 +lemma minus_coset_filter [code]:
    4.92 +  "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
    4.93 +  by auto
    4.94 +
    4.95 +lemma inter_set_filter [code]:
    4.96 +  "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
    4.97 +  by auto
    4.98 +
    4.99 +lemma inter_coset_fold [code]:
   4.100 +  "A \<inter> List.coset xs = fold Set.remove xs A"
   4.101 +  by (simp add: Diff_eq [symmetric] minus_set_fold)
   4.102 +
   4.103  lemma (in lattice) Inf_fin_set_fold:
   4.104    "Inf_fin (set (x # xs)) = fold inf xs x"
   4.105  proof -
   4.106 @@ -2503,6 +2521,8 @@
   4.107      by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
   4.108  qed
   4.109  
   4.110 +declare Inf_fin_set_fold [code]
   4.111 +
   4.112  lemma (in lattice) Sup_fin_set_fold:
   4.113    "Sup_fin (set (x # xs)) = fold sup xs x"
   4.114  proof -
   4.115 @@ -2512,6 +2532,8 @@
   4.116      by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
   4.117  qed
   4.118  
   4.119 +declare Sup_fin_set_fold [code]
   4.120 +
   4.121  lemma (in linorder) Min_fin_set_fold:
   4.122    "Min (set (x # xs)) = fold min xs x"
   4.123  proof -
   4.124 @@ -2521,6 +2543,8 @@
   4.125      by (simp add: Min_def fold1_set_fold del: set.simps)
   4.126  qed
   4.127  
   4.128 +declare Min_fin_set_fold [code]
   4.129 +
   4.130  lemma (in linorder) Max_fin_set_fold:
   4.131    "Max (set (x # xs)) = fold max xs x"
   4.132  proof -
   4.133 @@ -2530,6 +2554,8 @@
   4.134      by (simp add: Max_def fold1_set_fold del: set.simps)
   4.135  qed
   4.136  
   4.137 +declare Max_fin_set_fold [code]
   4.138 +
   4.139  lemma (in complete_lattice) Inf_set_fold:
   4.140    "Inf (set xs) = fold inf xs top"
   4.141  proof -
   4.142 @@ -2538,6 +2564,8 @@
   4.143    show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute)
   4.144  qed
   4.145  
   4.146 +declare Inf_set_fold [where 'a = "'a set", code]
   4.147 +
   4.148  lemma (in complete_lattice) Sup_set_fold:
   4.149    "Sup (set xs) = fold sup xs bot"
   4.150  proof -
   4.151 @@ -2546,73 +2574,74 @@
   4.152    show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute)
   4.153  qed
   4.154  
   4.155 +declare Sup_set_fold [where 'a = "'a set", code]
   4.156 +
   4.157  lemma (in complete_lattice) INF_set_fold:
   4.158    "INFI (set xs) f = fold (inf \<circ> f) xs top"
   4.159    unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
   4.160  
   4.161 +declare INF_set_fold [code]
   4.162 +
   4.163  lemma (in complete_lattice) SUP_set_fold:
   4.164    "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
   4.165    unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
   4.166  
   4.167 +declare SUP_set_fold [code]
   4.168  
   4.169  subsubsection {* Fold variants: @{const foldr} and @{const foldl} *}
   4.170  
   4.171  text {* Correspondence *}
   4.172  
   4.173 -lemma foldr_foldl: -- {* The ``Third Duality Theorem'' in Bird \& Wadler: *}
   4.174 +lemma foldr_conv_fold [code_abbrev]:
   4.175 +  "foldr f xs = fold f (rev xs)"
   4.176 +  by (induct xs) simp_all
   4.177 +
   4.178 +lemma foldl_conv_fold:
   4.179 +  "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
   4.180 +  by (induct xs arbitrary: s) simp_all
   4.181 +
   4.182 +lemma foldr_conv_foldl: -- {* The ``Third Duality Theorem'' in Bird \& Wadler: *}
   4.183    "foldr f xs a = foldl (\<lambda>x y. f y x) a (rev xs)"
   4.184 -  by (simp add: foldr_def foldl_def)
   4.185 -
   4.186 -lemma foldl_foldr:
   4.187 +  by (simp add: foldr_conv_fold foldl_conv_fold)
   4.188 +
   4.189 +lemma foldl_conv_foldr:
   4.190    "foldl f a xs = foldr (\<lambda>x y. f y x) (rev xs) a"
   4.191 -  by (simp add: foldr_def foldl_def)
   4.192 +  by (simp add: foldr_conv_fold foldl_conv_fold)
   4.193  
   4.194  lemma foldr_fold:
   4.195    assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   4.196    shows "foldr f xs = fold f xs"
   4.197 -  using assms unfolding foldr_def by (rule fold_rev)
   4.198 -
   4.199 -lemma
   4.200 -  foldr_Nil [code, simp]: "foldr f [] = id"
   4.201 -  and foldr_Cons [code, simp]: "foldr f (x # xs) = f x \<circ> foldr f xs"
   4.202 -  by (simp_all add: foldr_def)
   4.203 -
   4.204 -lemma
   4.205 -  foldl_Nil [simp]: "foldl f a [] = a"
   4.206 -  and foldl_Cons [simp]: "foldl f a (x # xs) = foldl f (f a x) xs"
   4.207 -  by (simp_all add: foldl_def)
   4.208 +  using assms unfolding foldr_conv_fold by (rule fold_rev)
   4.209  
   4.210  lemma foldr_cong [fundef_cong]:
   4.211    "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"
   4.212 -  by (auto simp add: foldr_def intro!: fold_cong)
   4.213 +  by (auto simp add: foldr_conv_fold intro!: fold_cong)
   4.214  
   4.215  lemma foldl_cong [fundef_cong]:
   4.216    "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"
   4.217 -  by (auto simp add: foldl_def intro!: fold_cong)
   4.218 +  by (auto simp add: foldl_conv_fold intro!: fold_cong)
   4.219  
   4.220  lemma foldr_append [simp]:
   4.221    "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
   4.222 -  by (simp add: foldr_def)
   4.223 +  by (simp add: foldr_conv_fold)
   4.224  
   4.225  lemma foldl_append [simp]:
   4.226    "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
   4.227 -  by (simp add: foldl_def)
   4.228 +  by (simp add: foldl_conv_fold)
   4.229  
   4.230  lemma foldr_map [code_unfold]:
   4.231    "foldr g (map f xs) a = foldr (g o f) xs a"
   4.232 -  by (simp add: foldr_def fold_map rev_map)
   4.233 +  by (simp add: foldr_conv_fold fold_map rev_map)
   4.234  
   4.235  lemma foldl_map [code_unfold]:
   4.236    "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs"
   4.237 -  by (simp add: foldl_def fold_map comp_def)
   4.238 -
   4.239 -text {* Executing operations in terms of @{const foldr} -- tail-recursive! *}
   4.240 +  by (simp add: foldl_conv_fold fold_map comp_def)
   4.241  
   4.242  lemma concat_conv_foldr [code]:
   4.243    "concat xss = foldr append xss []"
   4.244 -  by (simp add: fold_append_concat_rev foldr_def)
   4.245 -
   4.246 -lemma minus_set_foldr [code]:
   4.247 +  by (simp add: fold_append_concat_rev foldr_conv_fold)
   4.248 +
   4.249 +lemma minus_set_foldr:
   4.250    "A - set xs = foldr Set.remove xs A"
   4.251  proof -
   4.252    have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
   4.253 @@ -2620,11 +2649,7 @@
   4.254    then show ?thesis by (simp add: minus_set_fold foldr_fold)
   4.255  qed
   4.256  
   4.257 -lemma subtract_coset_filter [code]:
   4.258 -  "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
   4.259 -  by auto
   4.260 -
   4.261 -lemma union_set_foldr [code]:
   4.262 +lemma union_set_foldr:
   4.263    "set xs \<union> A = foldr Set.insert xs A"
   4.264  proof -
   4.265    have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
   4.266 @@ -2632,31 +2657,23 @@
   4.267    then show ?thesis by (simp add: union_set_fold foldr_fold)
   4.268  qed
   4.269  
   4.270 -lemma union_coset_foldr [code]:
   4.271 -  "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
   4.272 -  by auto
   4.273 -
   4.274 -lemma inter_set_filer [code]:
   4.275 -  "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
   4.276 -  by auto
   4.277 -
   4.278 -lemma inter_coset_foldr [code]:
   4.279 +lemma inter_coset_foldr:
   4.280    "A \<inter> List.coset xs = foldr Set.remove xs A"
   4.281    by (simp add: Diff_eq [symmetric] minus_set_foldr)
   4.282  
   4.283 -lemma (in lattice) Inf_fin_set_foldr [code]:
   4.284 +lemma (in lattice) Inf_fin_set_foldr:
   4.285    "Inf_fin (set (x # xs)) = foldr inf xs x"
   4.286    by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   4.287  
   4.288 -lemma (in lattice) Sup_fin_set_foldr [code]:
   4.289 +lemma (in lattice) Sup_fin_set_foldr:
   4.290    "Sup_fin (set (x # xs)) = foldr sup xs x"
   4.291    by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   4.292  
   4.293 -lemma (in linorder) Min_fin_set_foldr [code]:
   4.294 +lemma (in linorder) Min_fin_set_foldr:
   4.295    "Min (set (x # xs)) = foldr min xs x"
   4.296    by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   4.297  
   4.298 -lemma (in linorder) Max_fin_set_foldr [code]:
   4.299 +lemma (in linorder) Max_fin_set_foldr:
   4.300    "Max (set (x # xs)) = foldr max xs x"
   4.301    by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   4.302  
   4.303 @@ -2668,13 +2685,11 @@
   4.304    "Sup (set xs) = foldr sup xs bot"
   4.305    by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
   4.306  
   4.307 -declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code]
   4.308 -
   4.309 -lemma (in complete_lattice) INF_set_foldr [code]:
   4.310 +lemma (in complete_lattice) INF_set_foldr:
   4.311    "INFI (set xs) f = foldr (inf \<circ> f) xs top"
   4.312    by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric])
   4.313  
   4.314 -lemma (in complete_lattice) SUP_set_foldr [code]:
   4.315 +lemma (in complete_lattice) SUP_set_foldr:
   4.316    "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
   4.317    by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
   4.318  
   4.319 @@ -3108,7 +3123,7 @@
   4.320  
   4.321  lemma (in comm_monoid_add) listsum_rev [simp]:
   4.322    "listsum (rev xs) = listsum xs"
   4.323 -  by (simp add: listsum_def foldr_def fold_rev fun_eq_iff add_ac)
   4.324 +  by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff add_ac)
   4.325  
   4.326  lemma (in monoid_add) fold_plus_listsum_rev:
   4.327    "fold plus xs = plus (listsum (rev xs))"
   4.328 @@ -3116,40 +3131,12 @@
   4.329    fix x
   4.330    have "fold plus xs x = fold plus xs (x + 0)" by simp
   4.331    also have "\<dots> = fold plus (x # xs) 0" by simp
   4.332 -  also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_def)
   4.333 +  also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_conv_fold)
   4.334    also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def)
   4.335    also have "\<dots> = listsum (rev xs) + listsum [x]" by simp
   4.336    finally show "fold plus xs x = listsum (rev xs) + x" by simp
   4.337  qed
   4.338  
   4.339 -lemma (in semigroup_add) foldl_assoc:
   4.340 -  "foldl plus (x + y) zs = x + foldl plus y zs"
   4.341 -  by (simp add: foldl_def fold_commute_apply [symmetric] fun_eq_iff add_assoc)
   4.342 -
   4.343 -lemma (in ab_semigroup_add) foldr_conv_foldl:
   4.344 -  "foldr plus xs a = foldl plus a xs"
   4.345 -  by (simp add: foldl_def foldr_fold fun_eq_iff add_ac)
   4.346 -
   4.347 -text {*
   4.348 -  Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
   4.349 -  difficult to use because it requires an additional transitivity step.
   4.350 -*}
   4.351 -
   4.352 -lemma start_le_sum:
   4.353 -  fixes m n :: nat
   4.354 -  shows "m \<le> n \<Longrightarrow> m \<le> foldl plus n ns"
   4.355 -  by (simp add: foldl_def add_commute fold_plus_listsum_rev)
   4.356 -
   4.357 -lemma elem_le_sum:
   4.358 -  fixes m n :: nat 
   4.359 -  shows "n \<in> set ns \<Longrightarrow> n \<le> foldl plus 0 ns"
   4.360 -  by (force intro: start_le_sum simp add: in_set_conv_decomp)
   4.361 -
   4.362 -lemma sum_eq_0_conv [iff]:
   4.363 -  fixes m :: nat
   4.364 -  shows "foldl plus m ns = 0 \<longleftrightarrow> m = 0 \<and> (\<forall>n \<in> set ns. n = 0)"
   4.365 -  by (induct ns arbitrary: m) auto
   4.366 -
   4.367  text{* Some syntactic sugar for summing a function over a list: *}
   4.368  
   4.369  syntax
   4.370 @@ -3186,17 +3173,18 @@
   4.371  
   4.372  lemma listsum_eq_0_nat_iff_nat [simp]:
   4.373    "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
   4.374 -  by (simp add: listsum_def foldr_conv_foldl)
   4.375 +  by (induct ns) simp_all
   4.376 +
   4.377 +lemma member_le_listsum_nat:
   4.378 +  "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns"
   4.379 +  by (induct ns) auto
   4.380  
   4.381  lemma elem_le_listsum_nat:
   4.382    "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
   4.383 -apply(induct ns arbitrary: k)
   4.384 - apply simp
   4.385 -apply(fastforce simp add:nth_Cons split: nat.split)
   4.386 -done
   4.387 +  by (rule member_le_listsum_nat) simp
   4.388  
   4.389  lemma listsum_update_nat:
   4.390 -  "k<size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
   4.391 +  "k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
   4.392  apply(induct ns arbitrary:k)
   4.393   apply (auto split:nat.split)
   4.394  apply(drule elem_le_listsum_nat)
   4.395 @@ -4053,7 +4041,7 @@
   4.396      show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
   4.397        by (induct zs) (auto intro: * simp add: **)
   4.398    qed
   4.399 -  then show ?thesis by (simp add: sort_key_def foldr_def)
   4.400 +  then show ?thesis by (simp add: sort_key_def foldr_conv_fold)
   4.401  qed
   4.402  
   4.403  lemma (in linorder) sort_conv_fold:
   4.404 @@ -4601,7 +4589,7 @@
   4.405  lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
   4.406  proof (rule mono_inf [where f=listsp, THEN order_antisym])
   4.407    show "mono listsp" by (simp add: mono_def listsp_mono)
   4.408 -  show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
   4.409 +  show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI)
   4.410  qed
   4.411  
   4.412  lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def]
   4.413 @@ -5756,3 +5744,4 @@
   4.414    by (simp add: wf_iff_acyclic_if_finite)
   4.415  
   4.416  end
   4.417 +

     5.1 --- a/src/HOL/Nominal/Examples/Standardization.thy	Fri Apr 06 14:40:00 2012 +0200
     5.2 +++ b/src/HOL/Nominal/Examples/Standardization.thy	Fri Apr 06 18:17:16 2012 +0200
     5.3 @@ -213,7 +213,8 @@
     5.4      prefer 2
     5.5      apply (erule allE, erule impE, rule refl, erule spec)
     5.6      apply simp
     5.7 -   apply (clarsimp simp add: foldr_conv_foldl [symmetric] foldr_def fold_plus_listsum_rev listsum_map_remove1)
     5.8 +    apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev)
     5.9 +    apply (fastforce simp add: listsum_map_remove1)
    5.10    apply clarify
    5.11    apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)")
    5.12     prefer 2
    5.13 @@ -232,8 +233,10 @@
    5.14    apply clarify
    5.15    apply (erule allE, erule impE)
    5.16     prefer 2
    5.17 -   apply blast   
    5.18 -  apply (force intro: le_imp_less_Suc trans_le_add1 trans_le_add2 elem_le_sum) 
    5.19 +   apply blast
    5.20 +  apply simp
    5.21 +  apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev)
    5.22 +  apply (fastforce simp add: listsum_map_remove1)
    5.23    done
    5.24  
    5.25  theorem Apps_lam_induct:
    5.26 @@ -855,3 +858,4 @@
    5.27  qed
    5.28  
    5.29  end
    5.30 +

     6.1 --- a/src/HOL/Proofs/Lambda/ListApplication.thy	Fri Apr 06 14:40:00 2012 +0200
     6.2 +++ b/src/HOL/Proofs/Lambda/ListApplication.thy	Fri Apr 06 18:17:16 2012 +0200
     6.3 @@ -110,10 +110,8 @@
     6.4      prefer 2
     6.5      apply (erule allE, erule mp, rule refl)
     6.6     apply simp
     6.7 -   apply (rule lem0)
     6.8 -    apply force
     6.9 -   apply (rule elem_le_sum)
    6.10 -   apply force
    6.11 +   apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev)
    6.12 +   apply (fastforce simp add: listsum_map_remove1)
    6.13    apply clarify
    6.14    apply (rule assms)
    6.15     apply (erule allE, erule impE)
    6.16 @@ -128,8 +126,8 @@
    6.17    apply (rule le_imp_less_Suc)
    6.18    apply (rule trans_le_add1)
    6.19    apply (rule trans_le_add2)
    6.20 -  apply (rule elem_le_sum)
    6.21 -  apply force
    6.22 +  apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev)
    6.23 +  apply (simp add: member_le_listsum_nat)
    6.24    done
    6.25  
    6.26  theorem Apps_dB_induct:
    6.27 @@ -143,3 +141,4 @@
    6.28    done
    6.29  
    6.30  end
    6.31 +