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