# HG changeset patch
# User haftmann
# Date 1286271462 -7200
# Node ID 45f95e4de83171eac347cda5681447305ddcd777
# Parent  9f6503aaa77d6a2d3c56aead4f6b9f48629eabaf
lemmas fold_commute and fold_commute_apply

diff -r 9f6503aaa77d -r 45f95e4de831 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Mon Oct 04 14:46:49 2010 +0200
+++ b/src/HOL/Library/AssocList.thy	Tue Oct 05 11:37:42 2010 +0200
@@ -96,7 +96,7 @@
 proof -
   have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
     More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
-    by (rule fold_apply) (auto simp add: fun_eq_iff update_conv')
+    by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
   then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_fold split_def)
 qed
 
@@ -113,7 +113,7 @@
     by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
   moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
     More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
-    by (rule fold_apply) (simp add: update_keys split_def prod_case_beta comp_def)
+    by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
   ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
 qed
 
@@ -341,7 +341,7 @@
 proof -
   have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
     More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
-    by (rule fold_apply) (simp add: clearjunk_update prod_case_beta o_def)
+    by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
   then show ?thesis by (simp add: updates_def fun_eq_iff)
 qed
 
@@ -446,7 +446,7 @@
 proof -
   have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
     More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
-    by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
+    by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
   then show ?thesis
     by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev fun_eq_iff)
 qed
diff -r 9f6503aaa77d -r 45f95e4de831 src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Mon Oct 04 14:46:49 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Tue Oct 05 11:37:42 2010 +0200
@@ -257,7 +257,7 @@
     by (simp add: fun_eq_iff)
   have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
     fold More_Set.remove xs \<circ> member"
-    by (rule fold_apply) (simp add: fun_eq_iff)
+    by (rule fold_commute) (simp add: fun_eq_iff)
   then have "fold More_Set.remove xs (member A) = 
     member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
     by (simp add: fun_eq_iff)
@@ -282,7 +282,7 @@
     by (simp add: fun_eq_iff)
   have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
     fold Set.insert xs \<circ> member"
-    by (rule fold_apply) (simp add: fun_eq_iff)
+    by (rule fold_commute) (simp add: fun_eq_iff)
   then have "fold Set.insert xs (member A) =
     member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
     by (simp add: fun_eq_iff)
diff -r 9f6503aaa77d -r 45f95e4de831 src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Mon Oct 04 14:46:49 2010 +0200
+++ b/src/HOL/Library/More_List.thy	Tue Oct 05 11:37:42 2010 +0200
@@ -45,11 +45,19 @@
   shows "fold f xs = id"
   using assms by (induct xs) simp_all
 
-lemma fold_apply:
+lemma fold_commute:
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   shows "h \<circ> fold g xs = fold f xs \<circ> h"
   using assms by (induct xs) (simp_all add: fun_eq_iff)
 
+lemma fold_commute_apply:
+  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
+  shows "h (fold g xs s) = fold f xs (h s)"
+proof -
+  from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
+  then show ?thesis by (simp add: fun_eq_iff)
+qed
+
 lemma fold_invariant: 
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
     and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
@@ -73,7 +81,7 @@
 lemma fold_rev:
   assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   shows "fold f (rev xs) = fold f xs"
-  using assms by (induct xs) (simp_all del: o_apply add: fold_apply)
+  using assms by (induct xs) (simp_all del: o_apply add: fold_commute)
 
 lemma foldr_fold:
   assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"