src/HOL/Map.thy
changeset 31080 21ffc770ebc0
parent 30935 db5dcc1f276d
child 31380 f25536c0bb80
     1.1 --- a/src/HOL/Map.thy	Fri May 08 19:20:00 2009 +0200
     1.2 +++ b/src/HOL/Map.thy	Sat May 09 07:25:22 2009 +0200
     1.3 @@ -452,6 +452,9 @@
     1.4  
     1.5  subsection {* @{term [source] dom} *}
     1.6  
     1.7 +lemma dom_eq_empty_conv [simp]: "dom f = {} \<longleftrightarrow> f = empty"
     1.8 +by(auto intro!:ext simp: dom_def)
     1.9 +
    1.10  lemma domI: "m a = Some b ==> a : dom m"
    1.11  by(simp add:dom_def)
    1.12  (* declare domI [intro]? *)
    1.13 @@ -593,4 +596,19 @@
    1.14  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.15  by (clarsimp simp add: map_le_def map_add_def dom_def split: option.splits)
    1.16  
    1.17 +
    1.18 +lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
    1.19 +proof(rule iffI)
    1.20 +  assume "\<exists>v. f = [x \<mapsto> v]"
    1.21 +  thus "dom f = {x}" by(auto split: split_if_asm)
    1.22 +next
    1.23 +  assume "dom f = {x}"
    1.24 +  then obtain v where "f x = Some v" by auto
    1.25 +  hence "[x \<mapsto> v] \<subseteq>\<^sub>m f" by(auto simp add: map_le_def)
    1.26 +  moreover have "f \<subseteq>\<^sub>m [x \<mapsto> v]" using `dom f = {x}` `f x = Some v`
    1.27 +    by(auto simp add: map_le_def)
    1.28 +  ultimately have "f = [x \<mapsto> v]" by-(rule map_le_antisym)
    1.29 +  thus "\<exists>v. f = [x \<mapsto> v]" by blast
    1.30 +qed
    1.31 +
    1.32  end