# HG changeset patch # User haftmann # Date 1286271916 -7200 # Node ID 5a8aeeb2e63f782c06a9db5a635995d8d15baca4 # Parent 7479334d2c90ee6533b9ec4645836613afd48252# Parent 45f95e4de83171eac347cda5681447305ddcd777 merged diff -r 7479334d2c90 -r 5a8aeeb2e63f src/HOL/Library/AssocList.thy --- 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 \ More_List.fold (prod_case update) (zip ks vs) = More_List.fold (\(k, v) f. f(k \ v)) (zip ks vs) \ 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" "\_. True"]) (auto intro: assms) moreover have "map fst \ More_List.fold (prod_case update) (zip ks vs) = More_List.fold (\(k, v) al. if k \ set al then al else al @ [k]) (zip ks vs) \ 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 \ More_List.fold (prod_case update) (zip ks vs) = More_List.fold (prod_case update) (zip ks vs) \ 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 \ More_List.fold (prod_case update) (rev ys) = More_List.fold (\(k, v) m. m(k \ v)) (rev ys) \ 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 7479334d2c90 -r 5a8aeeb2e63f src/HOL/Library/Fset.thy --- 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 \ fold (\x. Fset \ More_Set.remove x \ member) xs = fold More_Set.remove xs \ 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 (\x. Fset \ More_Set.remove x \ member) xs A)" by (simp add: fun_eq_iff) @@ -282,7 +282,7 @@ by (simp add: fun_eq_iff) have "member \ fold (\x. Fset \ Set.insert x \ member) xs = fold Set.insert xs \ 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 (\x. Fset \ Set.insert x \ member) xs A)" by (simp add: fun_eq_iff) diff -r 7479334d2c90 -r 5a8aeeb2e63f src/HOL/Library/More_List.thy --- 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 "\x. x \ set xs \ h \ g x = f x \ h" shows "h \ fold g xs = fold f xs \ h" using assms by (induct xs) (simp_all add: fun_eq_iff) +lemma fold_commute_apply: + assumes "\x. x \ set xs \ h \ g x = f x \ h" + shows "h (fold g xs s) = fold f xs (h s)" +proof - + from assms have "h \ fold g xs = fold f xs \ h" by (rule fold_commute) + then show ?thesis by (simp add: fun_eq_iff) +qed + lemma fold_invariant: assumes "\x. x \ set xs \ Q x" and "P s" and "\x s. Q x \ P s \ P (f x s)" @@ -73,7 +81,7 @@ lemma fold_rev: assumes "\x y. x \ set xs \ y \ set xs \ f y \ f x = f x \ 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 "\x y. x \ set xs \ y \ set xs \ f y \ f x = f x \ f y"