# HG changeset patch
# User hoelzl
# Date 1366883961 -7200
# Node ID 408d937c9486553361ef46b884931a55ee1b4d77
# Parent  916271d524668c2eed3ab83441b4629c0d444c7c
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space

diff -r 916271d52466 -r 408d937c9486 NEWS
--- a/NEWS	Thu Apr 25 10:35:56 2013 +0200
+++ b/NEWS	Thu Apr 25 11:59:21 2013 +0200
@@ -106,6 +106,9 @@
   conditionally_complete_lattice for real. Renamed lemmas about
   conditionally-complete lattice from Sup_... to cSup_... and from Inf_...
   to cInf_... to avoid hidding of similar complete lattice lemmas.
+
+  Introduce type class linear_continuum as combination of conditionally-complete
+  lattices and inner dense linorders which have more than one element.
 INCOMPATIBILITY.
 
 * Introduce type classes "no_top" and "no_bot" for orderings without top
@@ -116,8 +119,9 @@
 * Complex_Main: Unify and move various concepts from
   HOL-Multivariate_Analysis to HOL-Complex_Main.
 
- - Introduce type class (lin)order_topology. Allows to generalize theorems
-   about limits and order. Instances are reals and extended reals.
+ - Introduce type class (lin)order_topology and linear_continuum_topology.
+   Allows to generalize theorems about limits and order.
+   Instances are reals and extended reals.
 
  - continuous and continuos_on from Multivariate_Analysis:
    "continuous" is the continuity of a function at a filter.
@@ -132,9 +136,8 @@
    function is continuous, when the function is continuous on a compact set.
 
  - connected from Multivariate_Analysis. Use it to prove the
-   intermediate value theorem. Show connectedness of intervals on order
-   topologies which are a inner dense, conditionally-complete linorder
-   (named connected_linorder_topology).
+   intermediate value theorem. Show connectedness of intervals on
+   linear_continuum_topology).
 
  - first_countable_topology from Multivariate_Analysis. Is used to
    show equivalence of properties on the neighbourhood filter of x and on
diff -r 916271d52466 -r 408d937c9486 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Thu Apr 25 10:35:56 2013 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Thu Apr 25 11:59:21 2013 +0200
@@ -246,6 +246,15 @@
 
 end
 
+class linear_continuum = conditionally_complete_linorder + inner_dense_linorder +
+  assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"
+begin
+
+lemma ex_gt_or_lt: "\<exists>b. a < b \<or> b < a"
+  by (metis UNIV_not_singleton neq_iff)
+
+end
+
 lemma cSup_bounds:
   fixes S :: "'a :: conditionally_complete_lattice set"
   assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
diff -r 916271d52466 -r 408d937c9486 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Apr 25 10:35:56 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Apr 25 11:59:21 2013 +0200
@@ -1151,6 +1151,12 @@
 
 instance ereal :: complete_linorder ..
 
+instance ereal :: linear_continuum
+proof
+  show "\<exists>a b::ereal. a \<noteq> b"
+    using ereal_zero_one by blast
+qed
+
 lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
   by (auto intro!: Sup_eqI
            simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
@@ -1572,7 +1578,7 @@
 
 subsubsection "Topological space"
 
-instantiation ereal :: connected_linorder_topology
+instantiation ereal :: linear_continuum_topology
 begin
 
 definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
@@ -1697,31 +1703,6 @@
   show thesis by auto
 qed
 
-instance ereal :: perfect_space
-proof (default, rule)
-  fix a :: ereal assume a: "open {a}"
-  show False
-  proof (cases a)
-    case MInf
-    then obtain y where "{..<ereal y} \<le> {a}" using a open_MInfty2[of "{a}"] by auto
-    then have "ereal (y - 1) \<in> {a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
-    then show False using `a = -\<infinity>` by auto
-  next
-    case PInf
-    then obtain y where "{ereal y<..} \<le> {a}" using a open_PInfty2[of "{a}"] by auto
-    then have "ereal (y + 1) \<in> {a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
-    then show False using `a = \<infinity>` by auto
-  next
-    case (real r)
-    then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
-    from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
-    then obtain b where b_def: "a<b \<and> b<a+e"
-      using fin ereal_between dense[of a "a+e"] by auto
-    then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
-    then show False using b_def e by auto
-  qed
-qed
-
 subsubsection {* Convergent sequences *}
 
 lemma lim_ereal[simp]:
diff -r 916271d52466 -r 408d937c9486 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Thu Apr 25 10:35:56 2013 +0200
+++ b/src/HOL/Real.thy	Thu Apr 25 11:59:21 2013 +0200
@@ -925,7 +925,7 @@
 qed
 
 
-instantiation real :: conditionally_complete_linorder
+instantiation real :: linear_continuum
 begin
 
 subsection{*Supremum of a set of reals*}
@@ -970,6 +970,9 @@
       using x z by (force intro: Sup_least)
     then show "z \<le> Inf X" 
         by (auto simp add: Inf_real_def) }
+
+  show "\<exists>a b::real. a \<noteq> b"
+    using zero_neq_one by blast
 qed
 end
 
diff -r 916271d52466 -r 408d937c9486 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Apr 25 11:59:21 2013 +0200
@@ -860,7 +860,7 @@
   qed
 qed
 
-instance real :: connected_linorder_topology ..
+instance real :: linear_continuum_topology ..
 
 lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
 lemmas open_real_lessThan = open_lessThan[where 'a=real]
diff -r 916271d52466 -r 408d937c9486 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy	Thu Apr 25 11:59:21 2013 +0200
@@ -2079,7 +2079,7 @@
 
 section {* Connectedness *}
 
-class connected_linorder_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
+class linear_continuum_topology = linorder_topology + linear_continuum
 begin
 
 lemma Inf_notin_open:
@@ -2110,8 +2110,17 @@
 
 end
 
+instance linear_continuum_topology \<subseteq> perfect_space
+proof
+  fix x :: 'a
+  from ex_gt_or_lt [of x] guess y ..
+  with Inf_notin_open[of "{x}" y] Sup_notin_open[of "{x}" y]
+  show "\<not> open {x}"
+    by auto
+qed
+
 lemma connectedI_interval:
-  fixes U :: "'a :: connected_linorder_topology set"
+  fixes U :: "'a :: linear_continuum_topology set"
   assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
   shows "connected U"
 proof (rule connectedI)
@@ -2154,35 +2163,35 @@
 qed
 
 lemma connected_iff_interval:
-  fixes U :: "'a :: connected_linorder_topology set"
+  fixes U :: "'a :: linear_continuum_topology set"
   shows "connected U \<longleftrightarrow> (\<forall>x\<in>U. \<forall>y\<in>U. \<forall>z. x \<le> z \<longrightarrow> z \<le> y \<longrightarrow> z \<in> U)"
   by (auto intro: connectedI_interval dest: connectedD_interval)
 
-lemma connected_UNIV[simp]: "connected (UNIV::'a::connected_linorder_topology set)"
+lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
   unfolding connected_iff_interval by auto
 
-lemma connected_Ioi[simp]: "connected {a::'a::connected_linorder_topology <..}"
+lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Ici[simp]: "connected {a::'a::connected_linorder_topology ..}"
+lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Iio[simp]: "connected {..< a::'a::connected_linorder_topology}"
+lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Iic[simp]: "connected {.. a::'a::connected_linorder_topology}"
+lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Ioo[simp]: "connected {a <..< b::'a::connected_linorder_topology}"
+lemma connected_Ioo[simp]: "connected {a <..< b::'a::linear_continuum_topology}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Ioc[simp]: "connected {a <.. b::'a::connected_linorder_topology}"
+lemma connected_Ioc[simp]: "connected {a <.. b::'a::linear_continuum_topology}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Ico[simp]: "connected {a ..< b::'a::connected_linorder_topology}"
+lemma connected_Ico[simp]: "connected {a ..< b::'a::linear_continuum_topology}"
   unfolding connected_iff_interval by auto
 
-lemma connected_Icc[simp]: "connected {a .. b::'a::connected_linorder_topology}"
+lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
   unfolding connected_iff_interval by auto
 
 lemma connected_contains_Ioo: 
@@ -2193,7 +2202,7 @@
 subsection {* Intermediate Value Theorem *}
 
 lemma IVT':
-  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
+  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   assumes y: "f a \<le> y" "y \<le> f b" "a \<le> b"
   assumes *: "continuous_on {a .. b} f"
   shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
@@ -2206,7 +2215,7 @@
 qed
 
 lemma IVT2':
-  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
+  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   assumes y: "f b \<le> y" "y \<le> f a" "a \<le> b"
   assumes *: "continuous_on {a .. b} f"
   shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
@@ -2219,17 +2228,17 @@
 qed
 
 lemma IVT:
-  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
+  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   shows "f a \<le> y \<Longrightarrow> y \<le> f b \<Longrightarrow> a \<le> b \<Longrightarrow> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x) \<Longrightarrow> \<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   by (rule IVT') (auto intro: continuous_at_imp_continuous_on)
 
 lemma IVT2:
-  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
+  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   shows "f b \<le> y \<Longrightarrow> y \<le> f a \<Longrightarrow> a \<le> b \<Longrightarrow> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x) \<Longrightarrow> \<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
 
 lemma continuous_inj_imp_mono:
-  fixes f :: "'a::connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
+  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   assumes x: "a < x" "x < b"
   assumes cont: "continuous_on {a..b} f"
   assumes inj: "inj_on f {a..b}"