src/HOL/Library/More_List.thy
 changeset 39921 45f95e4de831 parent 39791 a91430778479 child 40949 1d46d893d682
1.1 --- a/src/HOL/Library/More_List.thy	Mon Oct 04 14:46:49 2010 +0200
1.2 +++ b/src/HOL/Library/More_List.thy	Tue Oct 05 11:37:42 2010 +0200
1.3 @@ -45,11 +45,19 @@
1.4    shows "fold f xs = id"
1.5    using assms by (induct xs) simp_all
1.7 -lemma fold_apply:
1.8 +lemma fold_commute:
1.9    assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
1.10    shows "h \<circ> fold g xs = fold f xs \<circ> h"
1.11    using assms by (induct xs) (simp_all add: fun_eq_iff)
1.13 +lemma fold_commute_apply:
1.14 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
1.15 +  shows "h (fold g xs s) = fold f xs (h s)"
1.16 +proof -
1.17 +  from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
1.18 +  then show ?thesis by (simp add: fun_eq_iff)
1.19 +qed
1.20 +
1.21  lemma fold_invariant:
1.22    assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
1.23      and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
1.24 @@ -73,7 +81,7 @@
1.25  lemma fold_rev:
1.26    assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
1.27    shows "fold f (rev xs) = fold f xs"
1.28 -  using assms by (induct xs) (simp_all del: o_apply add: fold_apply)
1.29 +  using assms by (induct xs) (simp_all del: o_apply add: fold_commute)
1.31  lemma foldr_fold:
1.32    assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"