src/HOL/Map.thy
changeset 39198 f967a16dfcdd
parent 35619 b5f6481772f3
child 39302 d7728f65b353
equal deleted inserted replaced
39166:19efc2af3e6c 39198:f967a16dfcdd
   216   ultimately show ?case by simp
   216   ultimately show ?case by simp
   217 qed
   217 qed
   218 
   218 
   219 lemma map_of_zip_map:
   219 lemma map_of_zip_map:
   220   "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
   220   "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
   221   by (induct xs) (simp_all add: expand_fun_eq)
   221   by (induct xs) (simp_all add: ext_iff)
   222 
   222 
   223 lemma finite_range_map_of: "finite (range (map_of xys))"
   223 lemma finite_range_map_of: "finite (range (map_of xys))"
   224 apply (induct xys)
   224 apply (induct xys)
   225  apply (simp_all add: image_constant)
   225  apply (simp_all add: image_constant)
   226 apply (rule finite_subset)
   226 apply (rule finite_subset)
   243   "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
   243   "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
   244 by (induct xs) auto
   244 by (induct xs) auto
   245 
   245 
   246 lemma map_of_map:
   246 lemma map_of_map:
   247   "map_of (map (\<lambda>(k, v). (k, f v)) xs) = Option.map f \<circ> map_of xs"
   247   "map_of (map (\<lambda>(k, v). (k, f v)) xs) = Option.map f \<circ> map_of xs"
   248   by (induct xs) (auto simp add: expand_fun_eq)
   248   by (induct xs) (auto simp add: ext_iff)
   249 
   249 
   250 lemma dom_option_map:
   250 lemma dom_option_map:
   251   "dom (\<lambda>k. Option.map (f k) (m k)) = dom m"
   251   "dom (\<lambda>k. Option.map (f k) (m k)) = dom m"
   252   by (simp add: dom_def)
   252   by (simp add: dom_def)
   253 
   253 
   345     by(induct arbitrary: m rule: list_induct2) simp_all
   345     by(induct arbitrary: m rule: list_induct2) simp_all
   346 qed
   346 qed
   347 
   347 
   348 lemma map_add_map_of_foldr:
   348 lemma map_add_map_of_foldr:
   349   "m ++ map_of ps = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) ps m"
   349   "m ++ map_of ps = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) ps m"
   350   by (induct ps) (auto simp add: expand_fun_eq map_add_def)
   350   by (induct ps) (auto simp add: ext_iff map_add_def)
   351 
   351 
   352 
   352 
   353 subsection {* @{term [source] restrict_map} *}
   353 subsection {* @{term [source] restrict_map} *}
   354 
   354 
   355 lemma restrict_map_to_empty [simp]: "m|`{} = empty"
   355 lemma restrict_map_to_empty [simp]: "m|`{} = empty"
   379 lemma restrict_restrict [simp]: "m|`A|`B = m|`(A\<inter>B)"
   379 lemma restrict_restrict [simp]: "m|`A|`B = m|`(A\<inter>B)"
   380 by (rule ext) (auto simp: restrict_map_def)
   380 by (rule ext) (auto simp: restrict_map_def)
   381 
   381 
   382 lemma restrict_fun_upd [simp]:
   382 lemma restrict_fun_upd [simp]:
   383   "m(x := y)|`D = (if x \<in> D then (m|`(D-{x}))(x := y) else m|`D)"
   383   "m(x := y)|`D = (if x \<in> D then (m|`(D-{x}))(x := y) else m|`D)"
   384 by (simp add: restrict_map_def expand_fun_eq)
   384 by (simp add: restrict_map_def ext_iff)
   385 
   385 
   386 lemma fun_upd_None_restrict [simp]:
   386 lemma fun_upd_None_restrict [simp]:
   387   "(m|`D)(x := None) = (if x:D then m|`(D - {x}) else m|`D)"
   387   "(m|`D)(x := None) = (if x:D then m|`(D - {x}) else m|`D)"
   388 by (simp add: restrict_map_def expand_fun_eq)
   388 by (simp add: restrict_map_def ext_iff)
   389 
   389 
   390 lemma fun_upd_restrict: "(m|`D)(x := y) = (m|`(D-{x}))(x := y)"
   390 lemma fun_upd_restrict: "(m|`D)(x := y) = (m|`(D-{x}))(x := y)"
   391 by (simp add: restrict_map_def expand_fun_eq)
   391 by (simp add: restrict_map_def ext_iff)
   392 
   392 
   393 lemma fun_upd_restrict_conv [simp]:
   393 lemma fun_upd_restrict_conv [simp]:
   394   "x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
   394   "x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
   395 by (simp add: restrict_map_def expand_fun_eq)
   395 by (simp add: restrict_map_def ext_iff)
   396 
   396 
   397 lemma map_of_map_restrict:
   397 lemma map_of_map_restrict:
   398   "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
   398   "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
   399   by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert)
   399   by (induct ks) (simp_all add: ext_iff restrict_map_insert)
   400 
   400 
   401 lemma restrict_complement_singleton_eq:
   401 lemma restrict_complement_singleton_eq:
   402   "f |` (- {x}) = f(x := None)"
   402   "f |` (- {x}) = f(x := None)"
   403   by (simp add: restrict_map_def expand_fun_eq)
   403   by (simp add: restrict_map_def ext_iff)
   404 
   404 
   405 
   405 
   406 subsection {* @{term [source] map_upds} *}
   406 subsection {* @{term [source] map_upds} *}
   407 
   407 
   408 lemma map_upds_Nil1 [simp]: "m([] [|->] bs) = m"
   408 lemma map_upds_Nil1 [simp]: "m([] [|->] bs) = m"
   639 
   639 
   640 lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
   640 lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
   641 by (fastsimp simp add: map_le_def)
   641 by (fastsimp simp add: map_le_def)
   642 
   642 
   643 lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
   643 lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
   644 by(fastsimp simp: map_add_def map_le_def expand_fun_eq split: option.splits)
   644 by(fastsimp simp: map_add_def map_le_def ext_iff split: option.splits)
   645 
   645 
   646 lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
   646 lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
   647 by (fastsimp simp add: map_le_def map_add_def dom_def)
   647 by (fastsimp simp add: map_le_def map_add_def dom_def)
   648 
   648 
   649 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"
   649 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"