src/HOL/Library/AssocList.thy
changeset 39198 f967a16dfcdd
parent 38857 97775f3e8722
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Library/AssocList.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Library/AssocList.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
     1.5  
     1.6  lemma update_conv': "map_of (update k v al)  = (map_of al)(k\<mapsto>v)"
     1.7 -  by (induct al) (auto simp add: expand_fun_eq)
     1.8 +  by (induct al) (auto simp add: ext_iff)
     1.9  
    1.10  corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
    1.11    by (simp add: update_conv')
    1.12 @@ -67,7 +67,7 @@
    1.13          @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*}
    1.14  lemma update_swap: "k\<noteq>k' 
    1.15    \<Longrightarrow> map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
    1.16 -  by (simp add: update_conv' expand_fun_eq)
    1.17 +  by (simp add: update_conv' ext_iff)
    1.18  
    1.19  lemma update_Some_unfold: 
    1.20    "map_of (update k v al) x = Some y \<longleftrightarrow>
    1.21 @@ -96,8 +96,8 @@
    1.22  proof -
    1.23    have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
    1.24      More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
    1.25 -    by (rule fold_apply) (auto simp add: expand_fun_eq update_conv')
    1.26 -  then show ?thesis by (auto simp add: updates_def expand_fun_eq map_upds_fold_map_upd foldl_fold split_def)
    1.27 +    by (rule fold_apply) (auto simp add: ext_iff update_conv')
    1.28 +  then show ?thesis by (auto simp add: updates_def ext_iff map_upds_fold_map_upd foldl_fold split_def)
    1.29  qed
    1.30  
    1.31  lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
    1.32 @@ -114,7 +114,7 @@
    1.33    moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
    1.34      More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
    1.35      by (rule fold_apply) (simp add: update_keys split_def prod_case_beta comp_def)
    1.36 -  ultimately show ?thesis by (simp add: updates_def expand_fun_eq)
    1.37 +  ultimately show ?thesis by (simp add: updates_def ext_iff)
    1.38  qed
    1.39  
    1.40  lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
    1.41 @@ -161,7 +161,7 @@
    1.42    by (auto simp add: delete_eq)
    1.43  
    1.44  lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
    1.45 -  by (induct al) (auto simp add: expand_fun_eq)
    1.46 +  by (induct al) (auto simp add: ext_iff)
    1.47  
    1.48  corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
    1.49    by (simp add: delete_conv')
    1.50 @@ -301,7 +301,7 @@
    1.51  lemma map_of_clearjunk:
    1.52    "map_of (clearjunk al) = map_of al"
    1.53    by (induct al rule: clearjunk.induct)
    1.54 -    (simp_all add: expand_fun_eq)
    1.55 +    (simp_all add: ext_iff)
    1.56  
    1.57  lemma clearjunk_keys_set:
    1.58    "set (map fst (clearjunk al)) = set (map fst al)"
    1.59 @@ -342,7 +342,7 @@
    1.60    have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
    1.61      More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
    1.62      by (rule fold_apply) (simp add: clearjunk_update prod_case_beta o_def)
    1.63 -  then show ?thesis by (simp add: updates_def expand_fun_eq)
    1.64 +  then show ?thesis by (simp add: updates_def ext_iff)
    1.65  qed
    1.66  
    1.67  lemma clearjunk_delete:
    1.68 @@ -446,9 +446,9 @@
    1.69  proof -
    1.70    have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
    1.71      More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
    1.72 -    by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq)
    1.73 +    by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def ext_iff)
    1.74    then show ?thesis
    1.75 -    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev expand_fun_eq)
    1.76 +    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev ext_iff)
    1.77  qed
    1.78  
    1.79  corollary merge_conv:
    1.80 @@ -699,7 +699,7 @@
    1.81  
    1.82  lemma bulkload_Mapping [code]:
    1.83    "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
    1.84 -  by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
    1.85 +  by (rule mapping_eqI) (simp add: map_of_map_restrict ext_iff)
    1.86  
    1.87  lemma map_of_eqI: (*FIXME move to Map.thy*)
    1.88    assumes set_eq: "set (map fst xs) = set (map fst ys)"