summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Tue, 05 Oct 2010 11:45:16 +0200 | |

changeset 39922 | 5a8aeeb2e63f |

parent 39920 | 7479334d2c90 (current diff) |

parent 39921 | 45f95e4de831 (diff) |

child 39923 | 0e1bd289c8ea |

merged

--- a/src/HOL/Library/AssocList.thy Fri May 07 15:36:03 2010 +0200 +++ b/src/HOL/Library/AssocList.thy Tue Oct 05 11:45:16 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

--- a/src/HOL/Library/Fset.thy Fri May 07 15:36:03 2010 +0200 +++ b/src/HOL/Library/Fset.thy Tue Oct 05 11:45:16 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)

--- a/src/HOL/Library/More_List.thy Fri May 07 15:36:03 2010 +0200 +++ b/src/HOL/Library/More_List.thy Tue Oct 05 11:45:16 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"