more correspondence lemmas between related operations
authorhaftmann
Sun Jan 31 14:51:32 2010 +0100 (2010-01-31)
changeset 349798cb6e7a42e9c
parent 34978 874150ddd50a
child 34980 6676fd863e02
more correspondence lemmas between related operations
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Sun Jan 31 14:51:32 2010 +0100
     1.2 +++ b/src/HOL/Map.thy	Sun Jan 31 14:51:32 2010 +0100
     1.3 @@ -331,6 +331,19 @@
     1.4    "inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
     1.5  by (fastsimp simp: map_add_def dom_def inj_on_def split: option.splits)
     1.6  
     1.7 +lemma map_upds_fold_map_upd:
     1.8 +  "f(ks[\<mapsto>]vs) = foldl (\<lambda>f (k, v). f(k\<mapsto>v)) f (zip ks vs)"
     1.9 +unfolding map_upds_def proof (rule sym, rule zip_obtain_same_length)
    1.10 +  fix ks :: "'a list" and vs :: "'b list"
    1.11 +  assume "length ks = length vs"
    1.12 +  then show "foldl (\<lambda>f (k, v). f(k\<mapsto>v)) f (zip ks vs) = f ++ map_of (rev (zip ks vs))"
    1.13 +    by (induct arbitrary: f rule: list_induct2) simp_all
    1.14 +qed
    1.15 +
    1.16 +lemma map_add_map_of_foldr:
    1.17 +  "m ++ map_of ps = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) ps m"
    1.18 +  by (induct ps) (auto simp add: expand_fun_eq map_add_def)
    1.19 +
    1.20  
    1.21  subsection {* @{term [source] restrict_map} *}
    1.22  
    1.23 @@ -480,12 +493,13 @@
    1.24    "dom(f(x := y)) = (if y=None then dom f - {x} else insert x (dom f))"
    1.25  by(auto simp add:dom_def)
    1.26  
    1.27 -lemma dom_map_of: "dom(map_of xys) = {x. \<exists>y. (x,y) : set xys}"
    1.28 -by (induct xys) (auto simp del: fun_upd_apply)
    1.29 +lemma dom_if:
    1.30 +  "dom (\<lambda>x. if P x then f x else g x) = dom f \<inter> {x. P x} \<union> dom g \<inter> {x. \<not> P x}"
    1.31 +  by (auto split: if_splits)
    1.32  
    1.33  lemma dom_map_of_conv_image_fst:
    1.34 -  "dom(map_of xys) = fst ` (set xys)"
    1.35 -by(force simp: dom_map_of)
    1.36 +  "dom (map_of xys) = fst ` set xys"
    1.37 +  by (induct xys) (auto simp add: dom_if)
    1.38  
    1.39  lemma dom_map_of_zip [simp]: "[| length xs = length ys; distinct xs |] ==>
    1.40    dom(map_of(zip xs ys)) = set xs"
    1.41 @@ -523,11 +537,6 @@
    1.42    "dom (\<lambda>x. Some y) = UNIV"
    1.43    by auto
    1.44  
    1.45 -lemma dom_if:
    1.46 -  "dom (\<lambda>x. if P x then f x else g x) = dom f \<inter> {x. P x} \<union> dom g \<inter> {x. \<not> P x}"
    1.47 -  by (auto split: if_splits)
    1.48 -
    1.49 -
    1.50  (* Due to John Matthews - could be rephrased with dom *)
    1.51  lemma finite_map_freshness:
    1.52    "finite (dom (f :: 'a \<rightharpoonup> 'b)) \<Longrightarrow> \<not> finite (UNIV :: 'a set) \<Longrightarrow>
    1.53 @@ -559,6 +568,19 @@
    1.54   apply auto
    1.55  done
    1.56  
    1.57 +lemma ran_distinct: 
    1.58 +  assumes dist: "distinct (map fst al)" 
    1.59 +  shows "ran (map_of al) = snd ` set al"
    1.60 +using assms proof (induct al)
    1.61 +  case Nil then show ?case by simp
    1.62 +next
    1.63 +  case (Cons kv al)
    1.64 +  then have "ran (map_of al) = snd ` set al" by simp
    1.65 +  moreover from Cons.prems have "map_of al (fst kv) = None"
    1.66 +    by (simp add: map_of_eq_None_iff)
    1.67 +  ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp
    1.68 +qed
    1.69 +
    1.70  
    1.71  subsection {* @{text "map_le"} *}
    1.72  
    1.73 @@ -610,7 +632,6 @@
    1.74  lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h; f \<subseteq>\<^sub>m f++g \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
    1.75  by (clarsimp simp add: map_le_def map_add_def dom_def split: option.splits)
    1.76  
    1.77 -
    1.78  lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
    1.79  proof(rule iffI)
    1.80    assume "\<exists>v. f = [x \<mapsto> v]"
    1.81 @@ -626,3 +647,4 @@
    1.82  qed
    1.83  
    1.84  end
    1.85 +