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.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
```