summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Fri, 03 Jul 2009 08:44:13 +0200 | |

changeset 31930 | 3107b9af1fb3 |

parent 31922 | d6f8f3bfe329 |

child 31931 | 0b1d807b1c2d |

lemma foldl_apply_inv

src/HOL/Library/Fset.thy | file | annotate | diff | comparison | revisions | |

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- 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]

--- 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"