src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 44518 219a6fe4cfae parent 44517 68e8eb0ce8aa child 44519 ea85d78a994e
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 15:32:40 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 16:08:21 2011 -0700
1.3 @@ -644,59 +644,25 @@
1.4
1.5  definition "closure S = S \<union> {x | x. x islimpt S}"
1.6
1.7 +lemma interior_closure: "interior S = - (closure (- S))"
1.8 +  unfolding interior_def closure_def islimpt_def by auto
1.9 +
1.10  lemma closure_interior: "closure S = - interior (- S)"
1.11 -proof-
1.12 -  { fix x
1.13 -    have "x\<in>- interior (- S) \<longleftrightarrow> x \<in> closure S"  (is "?lhs = ?rhs")
1.14 -    proof
1.15 -      let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> - S)"
1.16 -      assume "?lhs"
1.17 -      hence *:"\<not> ?exT x"
1.18 -        unfolding interior_def
1.19 -        by simp
1.20 -      { assume "\<not> ?rhs"
1.21 -        hence False using *
1.22 -          unfolding closure_def islimpt_def
1.23 -          by blast
1.24 -      }
1.25 -      thus "?rhs"
1.26 -        by blast
1.27 -    next
1.28 -      assume "?rhs" thus "?lhs"
1.29 -        unfolding closure_def interior_def islimpt_def
1.30 -        by blast
1.31 -    qed
1.32 -  }
1.33 -  thus ?thesis
1.34 -    by blast
1.35 -qed
1.36 -
1.37 -lemma interior_closure: "interior S = - (closure (- S))"
1.38 -proof-
1.39 -  { fix x
1.40 -    have "x \<in> interior S \<longleftrightarrow> x \<in> - (closure (- S))"
1.41 -      unfolding interior_def closure_def islimpt_def
1.42 -      by auto
1.43 -  }
1.44 -  thus ?thesis
1.45 -    by blast
1.46 -qed
1.47 +  unfolding interior_closure by simp
1.48
1.49  lemma closed_closure[simp, intro]: "closed (closure S)"
1.50 -proof-
1.51 -  have "closed (- interior (-S))" by blast
1.52 -  thus ?thesis using closure_interior[of S] by simp
1.53 -qed
1.54 +  unfolding closure_interior by (simp add: closed_Compl)
1.55 +
1.56 +lemma closure_subset: "S \<subseteq> closure S"
1.57 +  unfolding closure_def by simp
1.58
1.59  lemma closure_hull: "closure S = closed hull S"
1.60  proof-
1.61    have "S \<subseteq> closure S"
1.62 -    unfolding closure_def
1.63 -    by blast
1.64 +    by (rule closure_subset)
1.65    moreover
1.66    have "closed (closure S)"
1.67 -    using closed_closure[of S]
1.68 -    by assumption
1.69 +    by (rule closed_closure)
1.70    moreover
1.71    { fix t
1.72      assume *:"S \<subseteq> t" "closed t"
1.73 @@ -712,8 +678,7 @@
1.74        by auto
1.75    }
1.76    ultimately show ?thesis
1.77 -    using hull_unique[of S, of "closure S", of closed]
1.78 -    by simp
1.79 +    by (rule hull_unique [symmetric])
1.80  qed
1.81
1.82  lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
1.83 @@ -726,24 +691,13 @@
1.84    by simp
1.85
1.86  lemma closure_closure[simp]: "closure (closure S) = closure S"
1.87 -  unfolding closure_hull
1.88 -  using hull_hull[of closed S]
1.89 -  by assumption
1.90 -
1.91 -lemma closure_subset: "S \<subseteq> closure S"
1.92 -  unfolding closure_hull
1.93 -  using hull_subset[of S closed]
1.94 -  by assumption
1.95 +  unfolding closure_hull by (rule hull_hull)
1.96
1.97  lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
1.98 -  unfolding closure_hull
1.99 -  using hull_mono[of S T closed]
1.100 -  by assumption
1.101 +  unfolding closure_hull by (rule hull_mono)
1.102
1.103  lemma closure_minimal: "S \<subseteq> T \<Longrightarrow>  closed T \<Longrightarrow> closure S \<subseteq> T"
1.104 -  using hull_minimal[of S T closed]
1.105 -  unfolding closure_hull
1.106 -  by simp
1.107 +  unfolding closure_hull by (rule hull_minimal)
1.108
1.109  lemma closure_unique: "S \<subseteq> T \<and> closed T \<and> (\<forall> T'. S \<subseteq> T' \<and> closed T' \<longrightarrow> T \<subseteq> T') \<Longrightarrow> closure S = T"
1.110    using hull_unique[of S T closed]
1.111 @@ -751,12 +705,13 @@
1.112    by simp
1.113
1.114  lemma closure_empty[simp]: "closure {} = {}"
1.115 -  using closed_empty closure_closed[of "{}"]
1.116 -  by simp
1.117 +  using closed_empty by (rule closure_closed)
1.118
1.119  lemma closure_univ[simp]: "closure UNIV = UNIV"
1.120 -  using closure_closed[of UNIV]
1.121 -  by simp
1.122 +  using closed_UNIV by (rule closure_closed)
1.123 +
1.124 +lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
1.125 +  unfolding closure_interior by simp
1.126
1.127  lemma closure_eq_empty: "closure S = {} \<longleftrightarrow> S = {}"
1.128    using closure_empty closure_subset[of S]
1.129 @@ -798,17 +753,10 @@
1.130  qed
1.131
1.132  lemma closure_complement: "closure(- S) = - interior(S)"
1.133 -proof-
1.134 -  have "S = - (- S)"
1.135 -    by auto
1.136 -  thus ?thesis
1.137 -    unfolding closure_interior
1.138 -    by auto
1.139 -qed
1.140 +  unfolding closure_interior by simp
1.141
1.142  lemma interior_complement: "interior(- S) = - closure(S)"
1.143 -  unfolding closure_interior
1.144 -  by blast
1.145 +  unfolding closure_interior by simp
1.146
1.147  lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
1.148  proof (intro closure_unique conjI)
```