src/HOL/Library/AssocList.thy
changeset 37458 4a76497f2eaa
parent 37051 d3ad914e3e02
child 37591 d3daea901123
child 37595 9591362629e3
     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: