# HG changeset patch
# User huffman
# Date 1314590209 25200
# Node ID bd91b77c4cd69f5ee7ece54b7239cc233f76e2a0
# Parent  b93d1b3ee30088a70938d3eab1eca1ecb63ea638
move class perfect_space into RealVector.thy;
use not_open_singleton as perfect_space class axiom;
generalize some lemmas to class perfect_space;

diff -r b93d1b3ee300 -r bd91b77c4cd6 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Sun Aug 28 16:28:07 2011 -0700
+++ b/src/HOL/Lim.thy	Sun Aug 28 20:56:49 2011 -0700
@@ -114,32 +114,25 @@
   by (rule metric_LIM_imp_LIM [OF f],
     simp add: dist_norm le)
 
-lemma trivial_limit_at:
-  fixes a :: "'a::real_normed_algebra_1"
-  shows "\<not> trivial_limit (at a)"  -- {* TODO: find a more appropriate class *}
-unfolding trivial_limit_def
-unfolding eventually_at dist_norm
-by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)
-
 lemma LIM_const_not_eq:
-  fixes a :: "'a::real_normed_algebra_1"
+  fixes a :: "'a::perfect_space"
   fixes k L :: "'b::t2_space"
   shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
-by (simp add: tendsto_const_iff trivial_limit_at)
+  by (simp add: tendsto_const_iff)
 
 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
 
 lemma LIM_const_eq:
-  fixes a :: "'a::real_normed_algebra_1"
+  fixes a :: "'a::perfect_space"
   fixes k L :: "'b::t2_space"
   shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
-  by (simp add: tendsto_const_iff trivial_limit_at)
+  by (simp add: tendsto_const_iff)
 
 lemma LIM_unique:
-  fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
+  fixes a :: "'a::perfect_space"
   fixes L M :: "'b::t2_space"
   shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
-  using trivial_limit_at by (rule tendsto_unique)
+  using at_neq_bot by (rule tendsto_unique)
 
 text{*Limits are equal for functions equal except at limit point*}
 lemma LIM_equal:
diff -r b93d1b3ee300 -r bd91b77c4cd6 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sun Aug 28 16:28:07 2011 -0700
+++ b/src/HOL/Limits.thy	Sun Aug 28 20:56:49 2011 -0700
@@ -331,6 +331,9 @@
 apply (erule le_less_trans [OF dist_triangle])
 done
 
+lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
+  unfolding trivial_limit_def eventually_nhds by simp
+
 lemma eventually_at_topological:
   "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
 unfolding at_def eventually_within eventually_nhds by simp
@@ -340,6 +343,13 @@
   shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
 unfolding at_def eventually_within eventually_nhds_metric by auto
 
+lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
+  unfolding trivial_limit_def eventually_at_topological
+  by (safe, case_tac "S = {a}", simp, fast, fast)
+
+lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
+  by (simp add: at_eq_bot_iff not_open_singleton)
+
 
 subsection {* Boundedness *}
 
diff -r b93d1b3ee300 -r bd91b77c4cd6 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 28 16:28:07 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 28 20:56:49 2011 -0700
@@ -1075,24 +1075,6 @@
   unfolding nth_conv_component
   using component_le_infnorm[of x] .
 
-instance vec :: (perfect_space, finite) perfect_space
-proof
-  fix x :: "'a ^ 'b"
-  show "x islimpt UNIV"
-    apply (rule islimptI)
-    apply (unfold open_vec_def)
-    apply (drule (1) bspec)
-    apply clarsimp
-    apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>y. y \<in> A i \<and> y \<noteq> x $ i")
-     apply (drule finite_choice [OF finite_UNIV], erule exE)
-     apply (rule_tac x="vec_lambda f" in exI)
-     apply (simp add: vec_eq_iff)
-    apply (rule ballI, drule_tac x=i in spec, clarify)
-    apply (cut_tac x="x $ i" in islimpt_UNIV)
-    apply (simp add: islimpt_def)
-    done
-qed
-
 lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
 unfolding continuous_at by (intro tendsto_intros)
 
diff -r b93d1b3ee300 -r bd91b77c4cd6 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Aug 28 16:28:07 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Aug 28 20:56:49 2011 -0700
@@ -220,6 +220,25 @@
   unfolding euclidean_component_def
   by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
 
+subsection {* Subclass relationships *}
+
+instance euclidean_space \<subseteq> perfect_space
+proof
+  fix x :: 'a show "\<not> open {x}"
+  proof
+    assume "open {x}"
+    then obtain e where "0 < e" and e: "\<forall>y. dist y x < e \<longrightarrow> y = x"
+      unfolding open_dist by fast
+    def y \<equiv> "x + scaleR (e/2) (sgn (basis 0))"
+    from `0 < e` have "y \<noteq> x"
+      unfolding y_def by (simp add: sgn_zero_iff DIM_positive)
+    from `0 < e` have "dist y x < e"
+      unfolding y_def by (simp add: dist_norm norm_sgn)
+    from `y \<noteq> x` and `dist y x < e` show "False"
+      using e by simp
+  qed
+qed
+
 subsection {* Class instances *}
 
 subsubsection {* Type @{typ real} *}
diff -r b93d1b3ee300 -r bd91b77c4cd6 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Aug 28 16:28:07 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Aug 28 20:56:49 2011 -0700
@@ -62,10 +62,9 @@
 using assms unfolding closed_def
 using ereal_open_uminus[of "- S"] ereal_uminus_complement by auto
 
-lemma not_open_ereal_singleton:
-  "\<not> (open {a :: ereal})"
-proof(rule ccontr)
-  assume "\<not> \<not> open {a}" hence a: "open {a}" by auto
+instance ereal :: perfect_space
+proof (default, rule)
+  fix a :: ereal assume a: "open {a}"
   show False
   proof (cases a)
     case MInf
@@ -138,7 +137,7 @@
   { assume "Inf S=(-\<infinity>)" hence False using * assms(3) by auto }
   moreover
   { assume "Inf S=\<infinity>" hence "S={\<infinity>}" by (metis Inf_eq_PInfty `S ~= {}`)
-    hence False by (metis assms(1) not_open_ereal_singleton) }
+    hence False by (metis assms(1) not_open_singleton) }
   moreover
   { assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
     from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this
diff -r b93d1b3ee300 -r bd91b77c4cd6 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Aug 28 16:28:07 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Aug 28 20:56:49 2011 -0700
@@ -238,8 +238,34 @@
   shows "((\<lambda>x. \<chi> i. f x i) ---> (\<chi> i. a i)) net"
   using assms by (simp add: vec_tendstoI)
 
+lemma open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)"
+proof (rule openI)
+  fix a assume "a \<in> (\<lambda>x. x $ i) ` S"
+  then obtain z where "a = z $ i" and "z \<in> S" ..
+  then obtain A where A: "\<forall>i. open (A i) \<and> z $ i \<in> A i"
+    and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
+    using `open S` unfolding open_vec_def by auto
+  hence "A i \<subseteq> (\<lambda>x. x $ i) ` S"
+    by (clarsimp, rule_tac x="\<chi> j. if j = i then x else z $ j" in image_eqI,
+      simp_all)
+  hence "open (A i) \<and> a \<in> A i \<and> A i \<subseteq> (\<lambda>x. x $ i) ` S"
+    using A `a = z $ i` by simp
+  then show "\<exists>T. open T \<and> a \<in> T \<and> T \<subseteq> (\<lambda>x. x $ i) ` S" by - (rule exI)
+qed
 
-subsection {* Metric *}
+instance vec :: (perfect_space, finite) perfect_space
+proof
+  fix x :: "'a ^ 'b" show "\<not> open {x}"
+  proof
+    assume "open {x}"
+    hence "\<forall>i. open ((\<lambda>x. x $ i) ` {x})" by (fast intro: open_image_vec_nth)   
+    hence "\<forall>i. open {x $ i}" by simp
+    thus "False" by (simp add: not_open_singleton)
+  qed
+qed
+
+
+subsection {* Metric space *}
 
 (* TODO: move somewhere else *)
 lemma finite_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"
diff -r b93d1b3ee300 -r bd91b77c4cd6 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 28 16:28:07 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 28 20:56:49 2011 -0700
@@ -465,10 +465,13 @@
   using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
   by metis 
 
+lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}"
+  unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)
+
 text {* A perfect space has no isolated points. *}
 
-class perfect_space = topological_space +
-  assumes islimpt_UNIV [simp, intro]: "x islimpt UNIV"
+lemma islimpt_UNIV [simp, intro]: "(x::'a::perfect_space) islimpt UNIV"
+  unfolding islimpt_UNIV_iff by (rule not_open_singleton)
 
 lemma perfect_choose_dist:
   fixes x :: "'a::{perfect_space, metric_space}"
@@ -476,21 +479,6 @@
 using islimpt_UNIV [of x]
 by (simp add: islimpt_approachable)
 
-instance euclidean_space \<subseteq> perfect_space
-proof
-  fix x :: 'a
-  { fix e :: real assume "0 < e"
-    def y \<equiv> "x + scaleR (e/2) (sgn (basis 0))"
-    from `0 < e` have "y \<noteq> x"
-      unfolding y_def by (simp add: sgn_zero_iff DIM_positive)
-    from `0 < e` have "dist y x < e"
-      unfolding y_def by (simp add: dist_norm norm_sgn)
-    from `y \<noteq> x` and `dist y x < e`
-    have "\<exists>y\<in>UNIV. y \<noteq> x \<and> dist y x < e" by auto
-  }
-  then show "x islimpt UNIV" unfolding islimpt_approachable by blast
-qed
-
 lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
   unfolding closed_def
   apply (subst open_subopen)
@@ -914,7 +902,7 @@
 lemma trivial_limit_at:
   fixes a :: "'a::perfect_space"
   shows "\<not> trivial_limit (at a)"
-  by (simp add: trivial_limit_at_iff)
+  by (rule at_neq_bot)
 
 lemma trivial_limit_at_infinity:
   "\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,perfect_space}) filter)"
diff -r b93d1b3ee300 -r bd91b77c4cd6 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Sun Aug 28 16:28:07 2011 -0700
+++ b/src/HOL/RealVector.thy	Sun Aug 28 20:56:49 2011 -0700
@@ -1191,4 +1191,17 @@
   shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))"
   using t0_space[of x y] by blast
 
+text {* A perfect space is a topological space with no isolated points. *}
+
+class perfect_space = topological_space +
+  assumes not_open_singleton: "\<not> open {x}"
+
+instance real_normed_algebra_1 \<subseteq> perfect_space
+proof
+  fix x::'a
+  show "\<not> open {x}"
+    unfolding open_dist dist_norm
+    by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp)
+qed
+
 end