# HG changeset patch # User haftmann # Date 1246603453 -7200 # Node ID 3107b9af1fb3ba190042a8297909d21f995a29a5 # Parent d6f8f3bfe3292aadf2c19a856fefaef22b53857c lemma foldl_apply_inv diff -r d6f8f3bfe329 -r 3107b9af1fb3 src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Fri Jul 03 00:15:59 2009 +0200 +++ b/src/HOL/Library/Fset.thy Fri Jul 03 08:44:13 2009 +0200 @@ -7,11 +7,6 @@ imports List_Set begin -lemma foldl_apply_inv: - assumes "\x. g (h x) = x" - shows "foldl f (g s) xs = g (foldl (\s x. h (f (g s) x)) s xs)" - by (rule sym, induct xs arbitrary: s) (simp_all add: assms) - declare mem_def [simp] diff -r d6f8f3bfe329 -r 3107b9af1fb3 src/HOL/List.thy --- a/src/HOL/List.thy Fri Jul 03 00:15:59 2009 +0200 +++ b/src/HOL/List.thy Fri Jul 03 08:44:13 2009 +0200 @@ -2080,6 +2080,11 @@ "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_inv: + assumes "\x. g (h x) = x" + shows "foldl f (g s) xs = g (foldl (\s x. h (f (g s) x)) s xs)" + by (rule sym, induct xs arbitrary: s) (simp_all add: assms) + lemma foldl_cong [fundef_cong, recdef_cong]: "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] ==> foldl f a l = foldl g b k"