# HG changeset patch
# User haftmann
# Date 1244122139 -7200
# Node ID 2754a0dadccc42089948f58eadd4c97c764c1872
# Parent  2c0959ab073f65982909d057095359fdbb7d3d74
lemma about List.foldl and Finite_Set.fold

diff -r 2c0959ab073f -r 2754a0dadccc src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 04 15:28:58 2009 +0200
+++ b/src/HOL/List.thy	Thu Jun 04 15:28:59 2009 +0200
@@ -2144,7 +2144,7 @@
   "\<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)
 
-text{* @{const foldl} and @{text concat} *}
+text {* @{const foldl} and @{const concat} *}
 
 lemma foldl_conv_concat:
   "foldl (op @) xs xss = xs @ concat xss"
@@ -2158,6 +2158,13 @@
 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 fun_left_comm_idem) fold_set:
+  "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
+  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
+
+
 
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}