revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
authorhoelzl
Thu Apr 25 11:59:21 2013 +0200 (2013-04-25)
changeset 51775408d937c9486
parent 51774 916271d52466
child 51776 8ea64fb16bae
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
NEWS
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/NEWS	Thu Apr 25 10:35:56 2013 +0200
     1.2 +++ b/NEWS	Thu Apr 25 11:59:21 2013 +0200
     1.3 @@ -106,6 +106,9 @@
     1.4    conditionally_complete_lattice for real. Renamed lemmas about
     1.5    conditionally-complete lattice from Sup_... to cSup_... and from Inf_...
     1.6    to cInf_... to avoid hidding of similar complete lattice lemmas.
     1.7 +
     1.8 +  Introduce type class linear_continuum as combination of conditionally-complete
     1.9 +  lattices and inner dense linorders which have more than one element.
    1.10  INCOMPATIBILITY.
    1.11  
    1.12  * Introduce type classes "no_top" and "no_bot" for orderings without top
    1.13 @@ -116,8 +119,9 @@
    1.14  * Complex_Main: Unify and move various concepts from
    1.15    HOL-Multivariate_Analysis to HOL-Complex_Main.
    1.16  
    1.17 - - Introduce type class (lin)order_topology. Allows to generalize theorems
    1.18 -   about limits and order. Instances are reals and extended reals.
    1.19 + - Introduce type class (lin)order_topology and linear_continuum_topology.
    1.20 +   Allows to generalize theorems about limits and order.
    1.21 +   Instances are reals and extended reals.
    1.22  
    1.23   - continuous and continuos_on from Multivariate_Analysis:
    1.24     "continuous" is the continuity of a function at a filter.
    1.25 @@ -132,9 +136,8 @@
    1.26     function is continuous, when the function is continuous on a compact set.
    1.27  
    1.28   - connected from Multivariate_Analysis. Use it to prove the
    1.29 -   intermediate value theorem. Show connectedness of intervals on order
    1.30 -   topologies which are a inner dense, conditionally-complete linorder
    1.31 -   (named connected_linorder_topology).
    1.32 +   intermediate value theorem. Show connectedness of intervals on
    1.33 +   linear_continuum_topology).
    1.34  
    1.35   - first_countable_topology from Multivariate_Analysis. Is used to
    1.36     show equivalence of properties on the neighbourhood filter of x and on
     2.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Thu Apr 25 10:35:56 2013 +0200
     2.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Thu Apr 25 11:59:21 2013 +0200
     2.3 @@ -246,6 +246,15 @@
     2.4  
     2.5  end
     2.6  
     2.7 +class linear_continuum = conditionally_complete_linorder + inner_dense_linorder +
     2.8 +  assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"
     2.9 +begin
    2.10 +
    2.11 +lemma ex_gt_or_lt: "\<exists>b. a < b \<or> b < a"
    2.12 +  by (metis UNIV_not_singleton neq_iff)
    2.13 +
    2.14 +end
    2.15 +
    2.16  lemma cSup_bounds:
    2.17    fixes S :: "'a :: conditionally_complete_lattice set"
    2.18    assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
     3.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Apr 25 10:35:56 2013 +0200
     3.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Apr 25 11:59:21 2013 +0200
     3.3 @@ -1151,6 +1151,12 @@
     3.4  
     3.5  instance ereal :: complete_linorder ..
     3.6  
     3.7 +instance ereal :: linear_continuum
     3.8 +proof
     3.9 +  show "\<exists>a b::ereal. a \<noteq> b"
    3.10 +    using ereal_zero_one by blast
    3.11 +qed
    3.12 +
    3.13  lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
    3.14    by (auto intro!: Sup_eqI
    3.15             simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
    3.16 @@ -1572,7 +1578,7 @@
    3.17  
    3.18  subsubsection "Topological space"
    3.19  
    3.20 -instantiation ereal :: connected_linorder_topology
    3.21 +instantiation ereal :: linear_continuum_topology
    3.22  begin
    3.23  
    3.24  definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
    3.25 @@ -1697,31 +1703,6 @@
    3.26    show thesis by auto
    3.27  qed
    3.28  
    3.29 -instance ereal :: perfect_space
    3.30 -proof (default, rule)
    3.31 -  fix a :: ereal assume a: "open {a}"
    3.32 -  show False
    3.33 -  proof (cases a)
    3.34 -    case MInf
    3.35 -    then obtain y where "{..<ereal y} \<le> {a}" using a open_MInfty2[of "{a}"] by auto
    3.36 -    then have "ereal (y - 1) \<in> {a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
    3.37 -    then show False using `a = -\<infinity>` by auto
    3.38 -  next
    3.39 -    case PInf
    3.40 -    then obtain y where "{ereal y<..} \<le> {a}" using a open_PInfty2[of "{a}"] by auto
    3.41 -    then have "ereal (y + 1) \<in> {a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
    3.42 -    then show False using `a = \<infinity>` by auto
    3.43 -  next
    3.44 -    case (real r)
    3.45 -    then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
    3.46 -    from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
    3.47 -    then obtain b where b_def: "a<b \<and> b<a+e"
    3.48 -      using fin ereal_between dense[of a "a+e"] by auto
    3.49 -    then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
    3.50 -    then show False using b_def e by auto
    3.51 -  qed
    3.52 -qed
    3.53 -
    3.54  subsubsection {* Convergent sequences *}
    3.55  
    3.56  lemma lim_ereal[simp]:
     4.1 --- a/src/HOL/Real.thy	Thu Apr 25 10:35:56 2013 +0200
     4.2 +++ b/src/HOL/Real.thy	Thu Apr 25 11:59:21 2013 +0200
     4.3 @@ -925,7 +925,7 @@
     4.4  qed
     4.5  
     4.6  
     4.7 -instantiation real :: conditionally_complete_linorder
     4.8 +instantiation real :: linear_continuum
     4.9  begin
    4.10  
    4.11  subsection{*Supremum of a set of reals*}
    4.12 @@ -970,6 +970,9 @@
    4.13        using x z by (force intro: Sup_least)
    4.14      then show "z \<le> Inf X" 
    4.15          by (auto simp add: Inf_real_def) }
    4.16 +
    4.17 +  show "\<exists>a b::real. a \<noteq> b"
    4.18 +    using zero_neq_one by blast
    4.19  qed
    4.20  end
    4.21  
     5.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
     5.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Apr 25 11:59:21 2013 +0200
     5.3 @@ -860,7 +860,7 @@
     5.4    qed
     5.5  qed
     5.6  
     5.7 -instance real :: connected_linorder_topology ..
     5.8 +instance real :: linear_continuum_topology ..
     5.9  
    5.10  lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
    5.11  lemmas open_real_lessThan = open_lessThan[where 'a=real]
     6.1 --- a/src/HOL/Topological_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
     6.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Apr 25 11:59:21 2013 +0200
     6.3 @@ -2079,7 +2079,7 @@
     6.4  
     6.5  section {* Connectedness *}
     6.6  
     6.7 -class connected_linorder_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
     6.8 +class linear_continuum_topology = linorder_topology + linear_continuum
     6.9  begin
    6.10  
    6.11  lemma Inf_notin_open:
    6.12 @@ -2110,8 +2110,17 @@
    6.13  
    6.14  end
    6.15  
    6.16 +instance linear_continuum_topology \<subseteq> perfect_space
    6.17 +proof
    6.18 +  fix x :: 'a
    6.19 +  from ex_gt_or_lt [of x] guess y ..
    6.20 +  with Inf_notin_open[of "{x}" y] Sup_notin_open[of "{x}" y]
    6.21 +  show "\<not> open {x}"
    6.22 +    by auto
    6.23 +qed
    6.24 +
    6.25  lemma connectedI_interval:
    6.26 -  fixes U :: "'a :: connected_linorder_topology set"
    6.27 +  fixes U :: "'a :: linear_continuum_topology set"
    6.28    assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
    6.29    shows "connected U"
    6.30  proof (rule connectedI)
    6.31 @@ -2154,35 +2163,35 @@
    6.32  qed
    6.33  
    6.34  lemma connected_iff_interval:
    6.35 -  fixes U :: "'a :: connected_linorder_topology set"
    6.36 +  fixes U :: "'a :: linear_continuum_topology set"
    6.37    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)"
    6.38    by (auto intro: connectedI_interval dest: connectedD_interval)
    6.39  
    6.40 -lemma connected_UNIV[simp]: "connected (UNIV::'a::connected_linorder_topology set)"
    6.41 +lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
    6.42    unfolding connected_iff_interval by auto
    6.43  
    6.44 -lemma connected_Ioi[simp]: "connected {a::'a::connected_linorder_topology <..}"
    6.45 +lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
    6.46    unfolding connected_iff_interval by auto
    6.47  
    6.48 -lemma connected_Ici[simp]: "connected {a::'a::connected_linorder_topology ..}"
    6.49 +lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
    6.50    unfolding connected_iff_interval by auto
    6.51  
    6.52 -lemma connected_Iio[simp]: "connected {..< a::'a::connected_linorder_topology}"
    6.53 +lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
    6.54    unfolding connected_iff_interval by auto
    6.55  
    6.56 -lemma connected_Iic[simp]: "connected {.. a::'a::connected_linorder_topology}"
    6.57 +lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
    6.58    unfolding connected_iff_interval by auto
    6.59  
    6.60 -lemma connected_Ioo[simp]: "connected {a <..< b::'a::connected_linorder_topology}"
    6.61 +lemma connected_Ioo[simp]: "connected {a <..< b::'a::linear_continuum_topology}"
    6.62    unfolding connected_iff_interval by auto
    6.63  
    6.64 -lemma connected_Ioc[simp]: "connected {a <.. b::'a::connected_linorder_topology}"
    6.65 +lemma connected_Ioc[simp]: "connected {a <.. b::'a::linear_continuum_topology}"
    6.66    unfolding connected_iff_interval by auto
    6.67  
    6.68 -lemma connected_Ico[simp]: "connected {a ..< b::'a::connected_linorder_topology}"
    6.69 +lemma connected_Ico[simp]: "connected {a ..< b::'a::linear_continuum_topology}"
    6.70    unfolding connected_iff_interval by auto
    6.71  
    6.72 -lemma connected_Icc[simp]: "connected {a .. b::'a::connected_linorder_topology}"
    6.73 +lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
    6.74    unfolding connected_iff_interval by auto
    6.75  
    6.76  lemma connected_contains_Ioo: 
    6.77 @@ -2193,7 +2202,7 @@
    6.78  subsection {* Intermediate Value Theorem *}
    6.79  
    6.80  lemma IVT':
    6.81 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    6.82 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    6.83    assumes y: "f a \<le> y" "y \<le> f b" "a \<le> b"
    6.84    assumes *: "continuous_on {a .. b} f"
    6.85    shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
    6.86 @@ -2206,7 +2215,7 @@
    6.87  qed
    6.88  
    6.89  lemma IVT2':
    6.90 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    6.91 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    6.92    assumes y: "f b \<le> y" "y \<le> f a" "a \<le> b"
    6.93    assumes *: "continuous_on {a .. b} f"
    6.94    shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
    6.95 @@ -2219,17 +2228,17 @@
    6.96  qed
    6.97  
    6.98  lemma IVT:
    6.99 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   6.100 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   6.101    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"
   6.102    by (rule IVT') (auto intro: continuous_at_imp_continuous_on)
   6.103  
   6.104  lemma IVT2:
   6.105 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   6.106 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   6.107    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"
   6.108    by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
   6.109  
   6.110  lemma continuous_inj_imp_mono:
   6.111 -  fixes f :: "'a::connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   6.112 +  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   6.113    assumes x: "a < x" "x < b"
   6.114    assumes cont: "continuous_on {a..b} f"
   6.115    assumes inj: "inj_on f {a..b}"