summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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"