# HG changeset patch # User haftmann # Date 1276866200 -7200 # Node ID 4a76497f2eaaf75518265e4ae6ce68a321d1c697 # Parent 7201c7e0db8719594dd6cf014444cc9b1a5fd360 prefer fold over foldl diff -r 7201c7e0db87 -r 4a76497f2eaa src/HOL/Library/AssocList.thy --- a/src/HOL/Library/AssocList.thy Fri Jun 18 09:21:41 2010 +0200 +++ b/src/HOL/Library/AssocList.thy Fri Jun 18 15:03:20 2010 +0200 @@ -5,7 +5,7 @@ header {* Map operations implemented on association lists*} theory AssocList -imports Main Mapping +imports Main More_List Mapping begin text {* @@ -79,7 +79,7 @@ by (simp add: update_conv' image_map_upd) definition updates :: "'key list \ 'val list \ ('key \ 'val) list \ ('key \ 'val) list" where - "updates ks vs al = foldl (\al (k, v). update k v al) al (zip ks vs)" + "updates ks vs = More_List.fold (prod_case update) (zip ks vs)" lemma updates_simps [simp]: "updates [] vs ps = ps" @@ -94,11 +94,10 @@ lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\]vs)" proof - - have "foldl (\f (k, v). f(k \ v)) (map_of al) (zip ks vs) = - map_of (foldl (\al (k, v). update k v al) al (zip ks vs))" - by (rule foldl_apply) (auto simp add: expand_fun_eq update_conv') - then show ?thesis - by (simp add: updates_def map_upds_fold_map_upd) + 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: expand_fun_eq update_conv') + then show ?thesis by (auto simp add: updates_def expand_fun_eq map_upds_fold_map_upd foldl_fold split_def) qed lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\]vs)) k" @@ -108,15 +107,14 @@ assumes "distinct (map fst al)" shows "distinct (map fst (updates ks vs al))" proof - - from assms have "distinct (foldl - (\al (k, v). if k \ set al then al else al @ [k]) - (map fst al) (zip ks vs))" - by (rule foldl_invariant) auto - moreover have "foldl (\al (k, v). if k \ set al then al else al @ [k]) - (map fst al) (zip ks vs) - = map fst (foldl (\al (k, v). update k v al) al (zip ks vs))" - by (rule foldl_apply) (simp add: update_keys split_def comp_def) - ultimately show ?thesis by (simp add: updates_def) + have "distinct (More_List.fold + (\(k, v) al. if k \ set al then al else al @ [k]) + (zip ks vs) (map fst al))" + 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) + ultimately show ?thesis by (simp add: updates_def expand_fun_eq) qed lemma updates_append1[simp]: "size ks < size vs \ @@ -341,10 +339,10 @@ lemma clearjunk_updates: "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)" proof - - have "foldl (\al (k, v). update k v al) (clearjunk al) (zip ks vs) = - clearjunk (foldl (\al (k, v). update k v al) al (zip ks vs))" - by (rule foldl_apply) (simp add: clearjunk_update expand_fun_eq split_def) - then show ?thesis by (simp add: updates_def) + 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) + then show ?thesis by (simp add: updates_def expand_fun_eq) qed lemma clearjunk_delete: @@ -429,8 +427,8 @@ lemma merge_updates: "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs" - by (simp add: merge_def updates_def split_def - foldr_foldl zip_rev zip_map_fst_snd) + by (simp add: merge_def updates_def split_prod_case + foldr_fold_rev zip_rev zip_map_fst_snd) lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \ fst ` set ys" by (induct ys arbitrary: xs) (auto simp add: dom_update) @@ -447,11 +445,11 @@ lemma merge_conv': "map_of (merge xs ys) = map_of xs ++ map_of ys" proof - - have "foldl (\m (k, v). m(k \ v)) (map_of xs) (rev ys) = - map_of (foldl (\xs (k, v). update k v xs) xs (rev ys)) " - by (rule foldl_apply) (simp add: expand_fun_eq split_def update_conv') + 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 expand_fun_eq) then show ?thesis - by (simp add: merge_def map_add_map_of_foldr foldr_foldl split_def) + by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev split_prod_case expand_fun_eq) qed corollary merge_conv: diff -r 7201c7e0db87 -r 4a76497f2eaa src/HOL/Library/RBT_Impl.thy --- a/src/HOL/Library/RBT_Impl.thy Fri Jun 18 09:21:41 2010 +0200 +++ b/src/HOL/Library/RBT_Impl.thy Fri Jun 18 15:03:20 2010 +0200 @@ -6,7 +6,7 @@ header {* Implementation of Red-Black Trees *} theory RBT_Impl -imports Main +imports Main More_List begin text {* @@ -1049,7 +1049,7 @@ subsection {* Folding over entries *} definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a, 'b) rbt \ 'c \ 'c" where - "fold f t s = foldl (\s (k, v). f k v s) s (entries t)" + "fold f t = More_List.fold (prod_case f) (entries t)" lemma fold_simps [simp, code]: "fold f Empty = id" @@ -1071,12 +1071,12 @@ proof - obtain ys where "ys = rev xs" by simp have "\t. is_rbt t \ - lookup (foldl (\t (k, v). insert k v t) t ys) = lookup t ++ map_of (rev ys)" - by (induct ys) (simp_all add: bulkload_def split_def lookup_insert) + lookup (More_List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)" + by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta) from this Empty_is_rbt have - "lookup (foldl (\t (k, v). insert k v t) Empty (rev xs)) = lookup Empty ++ map_of xs" + "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs" by (simp add: `ys = rev xs`) - then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def) + then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev prod_case_split) qed hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted