# 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 "\<And>x. g (h x) = x"
-  shows "foldl f (g s) xs = g (foldl (\<lambda>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 "\<And>x. g (h x) = x"
+  shows "foldl f (g s) xs = g (foldl (\<lambda>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"