# HG changeset patch
# User huffman
# Date 1244401203 25200
# Node ID c350f3ad6b0d929740361cbd07557f265978905d
# Parent  10080e31b294b2858426dc5536ce060f3c1254c8
move definitions of open, closed to RealVector.thy

diff -r 10080e31b294 -r c350f3ad6b0d src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Jun 06 10:28:34 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Jun 07 12:00:03 2009 -0700
@@ -196,29 +196,9 @@
 subsection{* The universal Euclidean versions are what we use most of the time *}
 
 definition
-  "open" :: "'a::topological_space set \<Rightarrow> bool" where
-  "open S \<longleftrightarrow> S \<in> topo"
-
-definition
-  closed :: "'a::topological_space set \<Rightarrow> bool" where
-  "closed S \<longleftrightarrow> open(UNIV - S)"
-
-definition
   euclidean :: "'a::topological_space topology" where
   "euclidean = topology open"
 
-lemma open_UNIV[intro,simp]:  "open UNIV"
-  unfolding open_def by (rule topo_UNIV)
-
-lemma open_inter[intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
-  unfolding open_def by (rule topo_Int)
-
-lemma open_Union[intro]: "(\<forall>S\<in>K. open S) \<Longrightarrow> open (\<Union> K)"
-  unfolding open_def subset_eq [symmetric] by (rule topo_Union)
-
-lemma open_empty[intro,simp]: "open {}"
-  using open_Union [of "{}"] by simp
-
 lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
   unfolding euclidean_def
   apply (rule cong[where x=S and y=S])
@@ -235,53 +215,11 @@
   by (simp add: topspace_euclidean topspace_subtopology)
 
 lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
-  by (simp add: closed_def closedin_def topspace_euclidean open_openin)
-
-lemma open_Un[intro]:
-  fixes S T :: "'a::topological_space set"
-  shows "open S \<Longrightarrow> open T \<Longrightarrow> open (S\<union>T)"
-  by (auto simp add: open_openin)
+  by (simp add: closed_def closedin_def topspace_euclidean open_openin Compl_eq_Diff_UNIV)
 
 lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
   by (simp add: open_openin openin_subopen[symmetric])
 
-lemma closed_empty[intro, simp]: "closed {}" by (simp add: closed_closedin)
-
-lemma closed_UNIV[simp,intro]: "closed UNIV"
-  by (simp add: closed_closedin topspace_euclidean[symmetric])
-
-lemma closed_Un[intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S\<union>T)"
-  by (auto simp add: closed_closedin)
-
-lemma closed_Int[intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S\<inter>T)"
-  by (auto simp add: closed_closedin)
-
-lemma closed_Inter[intro]: assumes H: "\<forall>S \<in>K. closed S" shows "closed (\<Inter>K)"
-  using H
-  unfolding closed_closedin
-  apply (cases "K = {}")
-  apply (simp add: closed_closedin[symmetric])
-  apply (rule closedin_Inter, auto)
-  done
-
-lemma open_closed: "open S \<longleftrightarrow> closed (UNIV - S)"
-  by (simp add: open_openin closed_closedin topspace_euclidean openin_closedin_eq)
-
-lemma closed_open: "closed S \<longleftrightarrow> open(UNIV - S)"
-  by (simp add: open_openin closed_closedin topspace_euclidean closedin_def)
-
-lemma open_diff[intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
-  by (auto simp add: open_openin closed_closedin)
-
-lemma closed_diff[intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed(S-T)"
-  by (auto simp add: open_openin closed_closedin)
-
-lemma open_Inter[intro]: assumes fS: "finite S" and h: "\<forall>T\<in>S. open T" shows "open (\<Inter>S)"
-  using h by (induct rule: finite_induct[OF fS], auto)
-
-lemma closed_Union[intro]: assumes fS: "finite S" and h: "\<forall>T\<in>S. closed T" shows "closed (\<Union>S)"
-  using h by (induct rule: finite_induct[OF fS], auto)
-
 subsection{* Open and closed balls. *}
 
 definition
@@ -466,7 +404,7 @@
     unfolding connected_def openin_open closedin_closed
     apply (subst exists_diff) by blast
   hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (UNIV - e2) \<and> e1 \<inter> (UNIV - e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (UNIV - e2) \<inter> S \<noteq> {})"
-    (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis
+    (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def Compl_eq_Diff_UNIV) by metis
 
   have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))"
     (is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)")
@@ -622,7 +560,7 @@
 lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
   unfolding closed_def
   apply (subst open_subopen)
-  apply (simp add: islimpt_def subset_eq)
+  apply (simp add: islimpt_def subset_eq Compl_eq_Diff_UNIV)
   by (metis DiffE DiffI UNIV_I insertCI insert_absorb mem_def)
 
 lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
@@ -679,7 +617,7 @@
   unfolding islimpt_def
   apply (rule ccontr, clarsimp, rename_tac A B)
   apply (drule_tac x="A \<inter> B" in spec)
-  apply (auto simp add: open_inter)
+  apply (auto simp add: open_Int)
   done
 
 lemma discrete_imp_closed:
@@ -731,7 +669,7 @@
 lemma interior_inter[simp]: "interior(S \<inter> T) = interior S \<inter> interior T"
   apply (rule equalityI, simp)
   apply (metis Int_lower1 Int_lower2 subset_interior)
-  by (metis Int_mono interior_subset open_inter open_interior open_subset_interior)
+  by (metis Int_mono interior_subset open_Int open_interior open_subset_interior)
 
 lemma interior_limit_point [intro]:
   fixes x :: "'a::perfect_space"
@@ -770,7 +708,7 @@
       assume "x \<notin> interior S"
       with `x \<in> R` `open R` obtain y where "y \<in> R - S"
         unfolding interior_def expand_set_eq by fast
-      from `open R` `closed S` have "open (R - S)" by (rule open_diff)
+      from `open R` `closed S` have "open (R - S)" by (rule open_Diff)
       from `R \<subseteq> S \<union> T` have "R - S \<subseteq> T" by fast
       from `y \<in> R - S` `open (R - S)` `R - S \<subseteq> T` `interior T = {}`
       show "False" unfolding interior_def by fast
@@ -924,7 +862,7 @@
       fix A
       assume "x \<in> A" "open A"
       with as have "x \<in> A \<inter> S" "open (A \<inter> S)"
-        by (simp_all add: open_inter)
+        by (simp_all add: open_Int)
       with * obtain y where "y \<in> T" "y \<in> A \<inter> S" "y \<noteq> x"
         by (rule islimptE)
       hence "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x"
@@ -955,7 +893,7 @@
 definition "frontier S = closure S - interior S"
 
 lemma frontier_closed: "closed(frontier S)"
-  by (simp add: frontier_def closed_diff closed_closure)
+  by (simp add: frontier_def closed_Diff)
 
 lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(UNIV - S))"
   by (auto simp add: frontier_def interior_closure)
@@ -1027,7 +965,7 @@
 
 lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
   using frontier_complement frontier_subset_eq[of "UNIV - S"]
-  unfolding open_closed by auto
+  unfolding open_closed Compl_eq_Diff_UNIV by auto
 
 subsection{* Common nets and The "within" modifier for nets. *}
 
@@ -1432,7 +1370,7 @@
   shows "l \<in> S"
 proof (rule ccontr)
   assume "l \<notin> S"
-  obtain e where e:"e>0" "ball l e \<subseteq> UNIV - S" using assms(1) `l \<notin> S` unfolding closed_def open_contains_ball by auto
+  obtain e where e:"e>0" "ball l e \<subseteq> UNIV - S" using assms(1) `l \<notin> S` unfolding closed_def open_contains_ball Compl_eq_Diff_UNIV by auto
   hence *:"\<forall>x. dist l x < e \<longrightarrow> x \<notin> S" by auto
   have "eventually (\<lambda>x. dist (f x) l < e) net"
     using assms(4) `e>0` by (rule tendstoD)
@@ -2926,7 +2864,7 @@
 lemma open_delete:
   fixes s :: "'a::metric_space set"
   shows "open s ==> open(s - {x})"
-  using open_diff[of s "{x}"] closed_sing
+  using open_Diff[of s "{x}"] closed_sing
   by blast
 
 text{* Finite intersection property. I could make it an equivalence in fact. *}
@@ -2939,7 +2877,7 @@
 proof
   assume as:"s \<inter> (\<Inter> f) = {}"
   hence "s \<subseteq> \<Union>op - UNIV ` f" by auto
-  moreover have "Ball (op - UNIV ` f) open" using open_diff closed_diff using assms(2) by auto
+  moreover have "Ball (op - UNIV ` f) open" using open_Diff closed_Diff using assms(2) by auto
   ultimately obtain f' where f':"f' \<subseteq> op - UNIV ` f"  "finite f'"  "s \<subseteq> \<Union>f'" using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="(\<lambda>t. UNIV - t) ` f"]] by auto
   hence "finite (op - UNIV ` f') \<and> op - UNIV ` f' \<subseteq> f" by(auto simp add: Diff_Diff_Int)
   hence "s \<inter> \<Inter>op - UNIV ` f' \<noteq> {}" using assms(3)[THEN spec[where x="op - UNIV ` f'"]] by auto
@@ -3657,7 +3595,7 @@
 proof-
   obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> T"
     using continuous_open_in_preimage[OF assms(1,3)] unfolding openin_open by auto
-  thus ?thesis using open_inter[of s T, OF assms(2)] by auto
+  thus ?thesis using open_Int[of s T, OF assms(2)] by auto
 qed
 
 lemma continuous_closed_preimage:
@@ -5149,13 +5087,13 @@
 lemma open_halfspace_lt: "open {x::real^_. a \<bullet> x < b}"
 proof-
   have "UNIV - {x. b \<le> a \<bullet> x} = {x. a \<bullet> x < b}" by auto
-  thus ?thesis using closed_halfspace_ge[unfolded closed_def, of b a] by auto
+  thus ?thesis using closed_halfspace_ge[unfolded closed_def Compl_eq_Diff_UNIV, of b a] by auto
 qed
 
 lemma open_halfspace_gt: "open {x::real^_. a \<bullet> x > b}"
 proof-
   have "UNIV - {x. b \<ge> a \<bullet> x} = {x. a \<bullet> x > b}" by auto
-  thus ?thesis using closed_halfspace_le[unfolded closed_def, of a b] by auto
+  thus ?thesis using closed_halfspace_le[unfolded closed_def Compl_eq_Diff_UNIV, of a b] by auto
 qed
 
 lemma open_halfspace_component_lt:
diff -r 10080e31b294 -r c350f3ad6b0d src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Sat Jun 06 10:28:34 2009 -0700
+++ b/src/HOL/RealVector.thy	Sun Jun 07 12:00:03 2009 -0700
@@ -421,10 +421,94 @@
 class topo =
   fixes topo :: "'a set set"
 
+text {*
+  The syntactic class uses @{term topo} instead of @{text "open"}
+  so that @{text "open"} and @{text closed} will have the same type.
+  Maybe we could use extra type constraints instead, like with
+  @{text dist} and @{text norm}?
+*}
+
 class topological_space = topo +
   assumes topo_UNIV: "UNIV \<in> topo"
   assumes topo_Int: "A \<in> topo \<Longrightarrow> B \<in> topo \<Longrightarrow> A \<inter> B \<in> topo"
   assumes topo_Union: "T \<subseteq> topo \<Longrightarrow> \<Union>T \<in> topo"
+begin
+
+definition
+  "open" :: "'a set \<Rightarrow> bool" where
+  "open S \<longleftrightarrow> S \<in> topo"
+
+definition
+  closed :: "'a set \<Rightarrow> bool" where
+  "closed S \<longleftrightarrow> open (- S)"
+
+lemma open_UNIV [intro, simp]:  "open UNIV"
+  unfolding open_def by (rule topo_UNIV)
+
+lemma open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
+  unfolding open_def by (rule topo_Int)
+
+lemma open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)"
+  unfolding open_def subset_eq [symmetric] by (rule topo_Union)
+
+lemma open_empty [intro, simp]: "open {}"
+  using open_Union [of "{}"] by simp
+
+lemma open_Un [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)"
+  using open_Union [of "{S, T}"] by simp
+
+lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
+  unfolding UN_eq by (rule open_Union) auto
+
+lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
+  by (induct set: finite) auto
+
+lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
+  unfolding Inter_def by (rule open_INT)
+
+lemma closed_empty [intro, simp]:  "closed {}"
+  unfolding closed_def by simp
+
+lemma closed_Un [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
+  unfolding closed_def by auto
+
+lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
+  unfolding closed_def Inter_def by auto
+
+lemma closed_UNIV [intro, simp]: "closed UNIV"
+  unfolding closed_def by simp
+
+lemma closed_Int [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)"
+  unfolding closed_def by auto
+
+lemma closed_INT [intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
+  unfolding closed_def by auto
+
+lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
+  by (induct set: finite) auto
+
+lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
+  unfolding Union_def by (rule closed_UN)
+
+lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
+  unfolding closed_def by simp
+
+lemma closed_open: "closed S \<longleftrightarrow> open (- S)"
+  unfolding closed_def by simp
+
+lemma open_Diff [intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
+  unfolding closed_open Diff_eq by (rule open_Int)
+
+lemma closed_Diff [intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S - T)"
+  unfolding open_closed Diff_eq by (rule closed_Int)
+
+lemma open_Compl [intro]: "closed S \<Longrightarrow> open (- S)"
+  unfolding closed_open .
+
+lemma closed_Compl [intro]: "open S \<Longrightarrow> closed (- S)"
+  unfolding open_closed .
+
+end
 
 
 subsection {* Metric spaces *}