1.1 --- a/src/HOL/Library/AssocList.thy	Fri Jun 18 09:21:41 2010 +0200
     1.2 +++ b/src/HOL/Library/AssocList.thy	Fri Jun 18 15:03:20 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Map operations implemented on association lists*}
     1.5  
     1.6  theory AssocList 
     1.7 -imports Main Mapping
     1.8 +imports Main More_List Mapping
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -79,7 +79,7 @@
    1.13    by (simp add: update_conv' image_map_upd)
    1.14  
    1.15  definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
    1.16 -  "updates ks vs al = foldl (\<lambda>al (k, v). update k v al) al (zip ks vs)"
    1.17 +  "updates ks vs = More_List.fold (prod_case update) (zip ks vs)"
    1.18  
    1.19  lemma updates_simps [simp]:
    1.20    "updates [] vs ps = ps"
    1.21 @@ -94,11 +94,10 @@
    1.22  
    1.23  lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
    1.24  proof -
    1.25 -  have "foldl (\<lambda>f (k, v). f(k \<mapsto> v)) (map_of al) (zip ks vs) =
    1.26 -     map_of (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))"
    1.27 -    by (rule foldl_apply) (auto simp add: expand_fun_eq update_conv')
    1.28 -  then show ?thesis
    1.29 -    by (simp add: updates_def map_upds_fold_map_upd)
    1.30 +  have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
    1.31 +    More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
    1.32 +    by (rule fold_apply) (auto simp add: expand_fun_eq update_conv')
    1.33 +  then show ?thesis by (auto simp add: updates_def expand_fun_eq map_upds_fold_map_upd foldl_fold split_def)
    1.34  qed
    1.35  
    1.36  lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
    1.37 @@ -108,15 +107,14 @@
    1.38    assumes "distinct (map fst al)"
    1.39    shows "distinct (map fst (updates ks vs al))"
    1.40  proof -
    1.41 -  from assms have "distinct (foldl
    1.42 -       (\<lambda>al (k, v). if k \<in> set al then al else al @ [k])
    1.43 -       (map fst al) (zip ks vs))"
    1.44 -    by (rule foldl_invariant) auto
    1.45 -  moreover have "foldl (\<lambda>al (k, v). if k \<in> set al then al else al @ [k])
    1.46 -       (map fst al) (zip ks vs)
    1.47 -       = map fst (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))"
    1.48 -    by (rule foldl_apply) (simp add: update_keys split_def comp_def)
    1.49 -  ultimately show ?thesis by (simp add: updates_def)
    1.50 +  have "distinct (More_List.fold
    1.51 +       (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
    1.52 +       (zip ks vs) (map fst al))"
    1.53 +    by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
    1.54 +  moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
    1.55 +    More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
    1.56 +    by (rule fold_apply) (simp add: update_keys split_def prod_case_beta comp_def)
    1.57 +  ultimately show ?thesis by (simp add: updates_def expand_fun_eq)
    1.58  qed
    1.59  
    1.60  lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
    1.61 @@ -341,10 +339,10 @@
    1.62  lemma clearjunk_updates:
    1.63    "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
    1.64  proof -
    1.65 -  have "foldl (\<lambda>al (k, v). update k v al) (clearjunk al) (zip ks vs) =
    1.66 -    clearjunk (foldl (\<lambda>al (k, v). update k v al) al (zip ks vs))"
    1.67 -    by (rule foldl_apply) (simp add: clearjunk_update expand_fun_eq split_def)
    1.68 -  then show ?thesis by (simp add: updates_def)
    1.69 +  have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
    1.70 +    More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
    1.71 +    by (rule fold_apply) (simp add: clearjunk_update prod_case_beta o_def)
    1.72 +  then show ?thesis by (simp add: updates_def expand_fun_eq)
    1.73  qed
    1.74  
    1.75  lemma clearjunk_delete:
    1.76 @@ -429,8 +427,8 @@
    1.77  
    1.78  lemma merge_updates:
    1.79    "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
    1.80 -  by (simp add: merge_def updates_def split_def
    1.81 -    foldr_foldl zip_rev zip_map_fst_snd)
    1.82 +  by (simp add: merge_def updates_def split_prod_case
    1.83 +    foldr_fold_rev zip_rev zip_map_fst_snd)
    1.84  
    1.85  lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
    1.86    by (induct ys arbitrary: xs) (auto simp add: dom_update)
    1.87 @@ -447,11 +445,11 @@
    1.88  lemma merge_conv':
    1.89    "map_of (merge xs ys) = map_of xs ++ map_of ys"
    1.90  proof -
    1.91 -  have "foldl (\<lambda>m (k, v). m(k \<mapsto> v)) (map_of xs) (rev ys) =
    1.92 -    map_of (foldl (\<lambda>xs (k, v). update k v xs) xs (rev ys)) "
    1.93 -    by (rule foldl_apply) (simp add: expand_fun_eq split_def update_conv')
    1.94 +  have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
    1.95 +    More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
    1.96 +    by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq)
    1.97    then show ?thesis
    1.98 -    by (simp add: merge_def map_add_map_of_foldr foldr_foldl split_def)
    1.99 +    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev split_prod_case expand_fun_eq)
   1.100  qed
   1.101  
   1.102  corollary merge_conv:

     2.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Jun 18 09:21:41 2010 +0200
     2.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Jun 18 15:03:20 2010 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* Implementation of Red-Black Trees *}
     2.5  
     2.6  theory RBT_Impl
     2.7 -imports Main
     2.8 +imports Main More_List
     2.9  begin
    2.10  
    2.11  text {*
    2.12 @@ -1049,7 +1049,7 @@
    2.13  subsection {* Folding over entries *}
    2.14  
    2.15  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
    2.16 -  "fold f t s = foldl (\<lambda>s (k, v). f k v s) s (entries t)"
    2.17 +  "fold f t = More_List.fold (prod_case f) (entries t)"
    2.18  
    2.19  lemma fold_simps [simp, code]:
    2.20    "fold f Empty = id"
    2.21 @@ -1071,12 +1071,12 @@
    2.22  proof -
    2.23    obtain ys where "ys = rev xs" by simp
    2.24    have "\<And>t. is_rbt t \<Longrightarrow>
    2.25 -    lookup (foldl (\<lambda>t (k, v). insert k v t) t ys) = lookup t ++ map_of (rev ys)"
    2.26 -      by (induct ys) (simp_all add: bulkload_def split_def lookup_insert)
    2.27 +    lookup (More_List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
    2.28 +      by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta)
    2.29    from this Empty_is_rbt have
    2.30 -    "lookup (foldl (\<lambda>t (k, v). insert k v t) Empty (rev xs)) = lookup Empty ++ map_of xs"
    2.31 +    "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
    2.32       by (simp add: `ys = rev xs`)
    2.33 -  then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
    2.34 +  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev prod_case_split)
    2.35  qed
    2.36  
    2.37  hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted