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.6  
     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.12  
    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.30  
    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"