1.1 --- a/src/HOL/Lim.thy	Sun Aug 28 16:28:07 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Sun Aug 28 20:56:49 2011 -0700
     1.3 @@ -114,32 +114,25 @@
     1.4    by (rule metric_LIM_imp_LIM [OF f],
     1.5      simp add: dist_norm le)
     1.6  
     1.7 -lemma trivial_limit_at:
     1.8 -  fixes a :: "'a::real_normed_algebra_1"
     1.9 -  shows "\<not> trivial_limit (at a)"  -- {* TODO: find a more appropriate class *}
    1.10 -unfolding trivial_limit_def
    1.11 -unfolding eventually_at dist_norm
    1.12 -by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)
    1.13 -
    1.14  lemma LIM_const_not_eq:
    1.15 -  fixes a :: "'a::real_normed_algebra_1"
    1.16 +  fixes a :: "'a::perfect_space"
    1.17    fixes k L :: "'b::t2_space"
    1.18    shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
    1.19 -by (simp add: tendsto_const_iff trivial_limit_at)
    1.20 +  by (simp add: tendsto_const_iff)
    1.21  
    1.22  lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
    1.23  
    1.24  lemma LIM_const_eq:
    1.25 -  fixes a :: "'a::real_normed_algebra_1"
    1.26 +  fixes a :: "'a::perfect_space"
    1.27    fixes k L :: "'b::t2_space"
    1.28    shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
    1.29 -  by (simp add: tendsto_const_iff trivial_limit_at)
    1.30 +  by (simp add: tendsto_const_iff)
    1.31  
    1.32  lemma LIM_unique:
    1.33 -  fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
    1.34 +  fixes a :: "'a::perfect_space"
    1.35    fixes L M :: "'b::t2_space"
    1.36    shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
    1.37 -  using trivial_limit_at by (rule tendsto_unique)
    1.38 +  using at_neq_bot by (rule tendsto_unique)
    1.39  
    1.40  text{*Limits are equal for functions equal except at limit point*}
    1.41  lemma LIM_equal:

     2.1 --- a/src/HOL/Limits.thy	Sun Aug 28 16:28:07 2011 -0700
     2.2 +++ b/src/HOL/Limits.thy	Sun Aug 28 20:56:49 2011 -0700
     2.3 @@ -331,6 +331,9 @@
     2.4  apply (erule le_less_trans [OF dist_triangle])
     2.5  done
     2.6  
     2.7 +lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
     2.8 +  unfolding trivial_limit_def eventually_nhds by simp
     2.9 +
    2.10  lemma eventually_at_topological:
    2.11    "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
    2.12  unfolding at_def eventually_within eventually_nhds by simp
    2.13 @@ -340,6 +343,13 @@
    2.14    shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
    2.15  unfolding at_def eventually_within eventually_nhds_metric by auto
    2.16  
    2.17 +lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
    2.18 +  unfolding trivial_limit_def eventually_at_topological
    2.19 +  by (safe, case_tac "S = {a}", simp, fast, fast)
    2.20 +
    2.21 +lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
    2.22 +  by (simp add: at_eq_bot_iff not_open_singleton)
    2.23 +
    2.24  
    2.25  subsection {* Boundedness *}
    2.26  

     3.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 28 16:28:07 2011 -0700
     3.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Aug 28 20:56:49 2011 -0700
     3.3 @@ -1075,24 +1075,6 @@
     3.4    unfolding nth_conv_component
     3.5    using component_le_infnorm[of x] .
     3.6  
     3.7 -instance vec :: (perfect_space, finite) perfect_space
     3.8 -proof
     3.9 -  fix x :: "'a ^ 'b"
    3.10 -  show "x islimpt UNIV"
    3.11 -    apply (rule islimptI)
    3.12 -    apply (unfold open_vec_def)
    3.13 -    apply (drule (1) bspec)
    3.14 -    apply clarsimp
    3.15 -    apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>y. y \<in> A i \<and> y \<noteq> x $ i")
    3.16 -     apply (drule finite_choice [OF finite_UNIV], erule exE)
    3.17 -     apply (rule_tac x="vec_lambda f" in exI)
    3.18 -     apply (simp add: vec_eq_iff)
    3.19 -    apply (rule ballI, drule_tac x=i in spec, clarify)
    3.20 -    apply (cut_tac x="x $ i" in islimpt_UNIV)
    3.21 -    apply (simp add: islimpt_def)
    3.22 -    done
    3.23 -qed
    3.24 -
    3.25  lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
    3.26  unfolding continuous_at by (intro tendsto_intros)
    3.27  

     4.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Aug 28 16:28:07 2011 -0700
     4.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Aug 28 20:56:49 2011 -0700
     4.3 @@ -220,6 +220,25 @@
     4.4    unfolding euclidean_component_def
     4.5    by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
     4.6  
     4.7 +subsection {* Subclass relationships *}
     4.8 +
     4.9 +instance euclidean_space \<subseteq> perfect_space
    4.10 +proof
    4.11 +  fix x :: 'a show "\<not> open {x}"
    4.12 +  proof
    4.13 +    assume "open {x}"
    4.14 +    then obtain e where "0 < e" and e: "\<forall>y. dist y x < e \<longrightarrow> y = x"
    4.15 +      unfolding open_dist by fast
    4.16 +    def y \<equiv> "x + scaleR (e/2) (sgn (basis 0))"
    4.17 +    from `0 < e` have "y \<noteq> x"
    4.18 +      unfolding y_def by (simp add: sgn_zero_iff DIM_positive)
    4.19 +    from `0 < e` have "dist y x < e"
    4.20 +      unfolding y_def by (simp add: dist_norm norm_sgn)
    4.21 +    from `y \<noteq> x` and `dist y x < e` show "False"
    4.22 +      using e by simp
    4.23 +  qed
    4.24 +qed
    4.25 +
    4.26  subsection {* Class instances *}
    4.27  
    4.28  subsubsection {* Type @{typ real} *}

     5.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Aug 28 16:28:07 2011 -0700
     5.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Aug 28 20:56:49 2011 -0700
     5.3 @@ -62,10 +62,9 @@
     5.4  using assms unfolding closed_def
     5.5  using ereal_open_uminus[of "- S"] ereal_uminus_complement by auto
     5.6  
     5.7 -lemma not_open_ereal_singleton:
     5.8 -  "\<not> (open {a :: ereal})"
     5.9 -proof(rule ccontr)
    5.10 -  assume "\<not> \<not> open {a}" hence a: "open {a}" by auto
    5.11 +instance ereal :: perfect_space
    5.12 +proof (default, rule)
    5.13 +  fix a :: ereal assume a: "open {a}"
    5.14    show False
    5.15    proof (cases a)
    5.16      case MInf
    5.17 @@ -138,7 +137,7 @@
    5.18    { assume "Inf S=(-\<infinity>)" hence False using * assms(3) by auto }
    5.19    moreover
    5.20    { assume "Inf S=\<infinity>" hence "S={\<infinity>}" by (metis Inf_eq_PInfty `S ~= {}`)
    5.21 -    hence False by (metis assms(1) not_open_ereal_singleton) }
    5.22 +    hence False by (metis assms(1) not_open_singleton) }
    5.23    moreover
    5.24    { assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
    5.25      from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this

     6.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Aug 28 16:28:07 2011 -0700
     6.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Aug 28 20:56:49 2011 -0700
     6.3 @@ -238,8 +238,34 @@
     6.4    shows "((\<lambda>x. \<chi> i. f x i) ---> (\<chi> i. a i)) net"
     6.5    using assms by (simp add: vec_tendstoI)
     6.6  
     6.7 +lemma open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)"
     6.8 +proof (rule openI)
     6.9 +  fix a assume "a \<in> (\<lambda>x. x $ i) ` S"
    6.10 +  then obtain z where "a = z $ i" and "z \<in> S" ..
    6.11 +  then obtain A where A: "\<forall>i. open (A i) \<and> z $ i \<in> A i"
    6.12 +    and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
    6.13 +    using `open S` unfolding open_vec_def by auto
    6.14 +  hence "A i \<subseteq> (\<lambda>x. x $ i) ` S"
    6.15 +    by (clarsimp, rule_tac x="\<chi> j. if j = i then x else z $ j" in image_eqI,
    6.16 +      simp_all)
    6.17 +  hence "open (A i) \<and> a \<in> A i \<and> A i \<subseteq> (\<lambda>x. x $ i) ` S"
    6.18 +    using A `a = z $ i` by simp
    6.19 +  then show "\<exists>T. open T \<and> a \<in> T \<and> T \<subseteq> (\<lambda>x. x $ i) ` S" by - (rule exI)
    6.20 +qed
    6.21  
    6.22 -subsection {* Metric *}
    6.23 +instance vec :: (perfect_space, finite) perfect_space
    6.24 +proof
    6.25 +  fix x :: "'a ^ 'b" show "\<not> open {x}"
    6.26 +  proof
    6.27 +    assume "open {x}"
    6.28 +    hence "\<forall>i. open ((\<lambda>x. x $ i) ` {x})" by (fast intro: open_image_vec_nth)   
    6.29 +    hence "\<forall>i. open {x $ i}" by simp
    6.30 +    thus "False" by (simp add: not_open_singleton)
    6.31 +  qed
    6.32 +qed
    6.33 +
    6.34 +
    6.35 +subsection {* Metric space *}
    6.36  
    6.37  (* TODO: move somewhere else *)
    6.38  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)"

     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 28 16:28:07 2011 -0700
     7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 28 20:56:49 2011 -0700
     7.3 @@ -465,10 +465,13 @@
     7.4    using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
     7.5    by metis 
     7.6  
     7.7 +lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}"
     7.8 +  unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)
     7.9 +
    7.10  text {* A perfect space has no isolated points. *}
    7.11  
    7.12 -class perfect_space = topological_space +
    7.13 -  assumes islimpt_UNIV [simp, intro]: "x islimpt UNIV"
    7.14 +lemma islimpt_UNIV [simp, intro]: "(x::'a::perfect_space) islimpt UNIV"
    7.15 +  unfolding islimpt_UNIV_iff by (rule not_open_singleton)
    7.16  
    7.17  lemma perfect_choose_dist:
    7.18    fixes x :: "'a::{perfect_space, metric_space}"
    7.19 @@ -476,21 +479,6 @@
    7.20  using islimpt_UNIV [of x]
    7.21  by (simp add: islimpt_approachable)
    7.22  
    7.23 -instance euclidean_space \<subseteq> perfect_space
    7.24 -proof
    7.25 -  fix x :: 'a
    7.26 -  { fix e :: real assume "0 < e"
    7.27 -    def y \<equiv> "x + scaleR (e/2) (sgn (basis 0))"
    7.28 -    from `0 < e` have "y \<noteq> x"
    7.29 -      unfolding y_def by (simp add: sgn_zero_iff DIM_positive)
    7.30 -    from `0 < e` have "dist y x < e"
    7.31 -      unfolding y_def by (simp add: dist_norm norm_sgn)
    7.32 -    from `y \<noteq> x` and `dist y x < e`
    7.33 -    have "\<exists>y\<in>UNIV. y \<noteq> x \<and> dist y x < e" by auto
    7.34 -  }
    7.35 -  then show "x islimpt UNIV" unfolding islimpt_approachable by blast
    7.36 -qed
    7.37 -
    7.38  lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
    7.39    unfolding closed_def
    7.40    apply (subst open_subopen)
    7.41 @@ -914,7 +902,7 @@
    7.42  lemma trivial_limit_at:
    7.43    fixes a :: "'a::perfect_space"
    7.44    shows "\<not> trivial_limit (at a)"
    7.45 -  by (simp add: trivial_limit_at_iff)
    7.46 +  by (rule at_neq_bot)
    7.47  
    7.48  lemma trivial_limit_at_infinity:
    7.49    "\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,perfect_space}) filter)"

     8.1 --- a/src/HOL/RealVector.thy	Sun Aug 28 16:28:07 2011 -0700
     8.2 +++ b/src/HOL/RealVector.thy	Sun Aug 28 20:56:49 2011 -0700
     8.3 @@ -1191,4 +1191,17 @@
     8.4    shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))"
     8.5    using t0_space[of x y] by blast
     8.6  
     8.7 +text {* A perfect space is a topological space with no isolated points. *}
     8.8 +
     8.9 +class perfect_space = topological_space +
    8.10 +  assumes not_open_singleton: "\<not> open {x}"
    8.11 +
    8.12 +instance real_normed_algebra_1 \<subseteq> perfect_space
    8.13 +proof
    8.14 +  fix x::'a
    8.15 +  show "\<not> open {x}"
    8.16 +    unfolding open_dist dist_norm
    8.17 +    by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp)
    8.18 +qed
    8.19 +
    8.20  end