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)