src/HOL/Map.thy
changeset 63834 6a757f36997e
parent 63828 ca467e73f912
child 66010 2f7d39285a1a
     1.1 --- a/src/HOL/Map.thy	Sun Sep 11 00:14:37 2016 +0200
     1.2 +++ b/src/HOL/Map.thy	Sun Sep 11 00:14:44 2016 +0200
     1.3 @@ -695,17 +695,23 @@
     1.4  by (metis map_add_subsumed1 map_le_iff_map_add_commute)
     1.5  
     1.6  lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
     1.7 -proof(rule iffI)
     1.8 -  assume "\<exists>v. f = [x \<mapsto> v]"
     1.9 -  thus "dom f = {x}" by(auto split: if_split_asm)
    1.10 +  (is "?lhs \<longleftrightarrow> ?rhs")
    1.11 +proof
    1.12 +  assume ?rhs
    1.13 +  then show ?lhs by (auto split: if_split_asm)
    1.14  next
    1.15 -  assume "dom f = {x}"
    1.16 -  then obtain v where "f x = Some v" by auto
    1.17 -  hence "[x \<mapsto> v] \<subseteq>\<^sub>m f" by(auto simp add: map_le_def)
    1.18 -  moreover have "f \<subseteq>\<^sub>m [x \<mapsto> v]" using \<open>dom f = {x}\<close> \<open>f x = Some v\<close>
    1.19 -    by(auto simp add: map_le_def)
    1.20 -  ultimately have "f = [x \<mapsto> v]" by-(rule map_le_antisym)
    1.21 -  thus "\<exists>v. f = [x \<mapsto> v]" by blast
    1.22 +  assume ?lhs
    1.23 +  then obtain v where v: "f x = Some v" by auto
    1.24 +  show ?rhs
    1.25 +  proof
    1.26 +    show "f = [x \<mapsto> v]"
    1.27 +    proof (rule map_le_antisym)
    1.28 +      show "[x \<mapsto> v] \<subseteq>\<^sub>m f"
    1.29 +        using v by (auto simp add: map_le_def)
    1.30 +      show "f \<subseteq>\<^sub>m [x \<mapsto> v]"
    1.31 +        using \<open>dom f = {x}\<close> \<open>f x = Some v\<close> by (auto simp add: map_le_def)
    1.32 +    qed
    1.33 +  qed
    1.34  qed
    1.35  
    1.36