separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
--- a/src/HOL/Complex_Main.thy Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/Complex_Main.thy Tue Mar 26 12:20:52 2013 +0100
@@ -4,7 +4,6 @@
imports
Main
Real
- SupInf
Complex
Log
Ln
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Conditional_Complete_Lattices.thy Tue Mar 26 12:20:52 2013 +0100
@@ -0,0 +1,295 @@
+(* Title: HOL/Conditional_Complete_Lattices.thy
+ Author: Amine Chaieb and L C Paulson, University of Cambridge
+ Author: Johanens Hölzl, TU München
+*)
+
+header {* Conditional Complete Lattices *}
+
+theory Conditional_Complete_Lattices
+imports Main Lubs
+begin
+
+lemma Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
+ by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
+
+lemma Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
+ by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
+
+text {*
+
+To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
+@{const Inf} in theorem names with c.
+
+*}
+
+class conditional_complete_lattice = lattice + Sup + Inf +
+ assumes cInf_lower: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> z \<le> a) \<Longrightarrow> Inf X \<le> x"
+ and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X"
+ assumes cSup_upper: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> a \<le> z) \<Longrightarrow> x \<le> Sup X"
+ and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
+begin
+
+lemma cSup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
+ "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
+ by (blast intro: antisym cSup_upper cSup_least)
+
+lemma cInf_eq_minimum: (*REAL_INF_MIN in HOL4*)
+ "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
+ by (intro antisym cInf_lower[of z X z] cInf_greatest[of X z]) auto
+
+lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> a \<le> z) \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)"
+ by (metis order_trans cSup_upper cSup_least)
+
+lemma le_cInf_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> z \<le> a) \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
+ by (metis order_trans cInf_lower cInf_greatest)
+
+lemma cSup_singleton [simp]: "Sup {x} = x"
+ by (intro cSup_eq_maximum) auto
+
+lemma cInf_singleton [simp]: "Inf {x} = x"
+ by (intro cInf_eq_minimum) auto
+
+lemma cSup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
+ "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
+ by (metis cSup_upper order_trans)
+
+lemma cInf_lower2:
+ "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
+ by (metis cInf_lower order_trans)
+
+lemma cSup_upper_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
+ by (blast intro: cSup_upper)
+
+lemma cInf_lower_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
+ by (blast intro: cInf_lower)
+
+lemma cSup_eq_non_empty:
+ assumes 1: "X \<noteq> {}"
+ assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
+ assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
+ shows "Sup X = a"
+ by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper)
+
+lemma cInf_eq_non_empty:
+ assumes 1: "X \<noteq> {}"
+ assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
+ assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
+ shows "Inf X = a"
+ by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
+
+lemma cInf_cSup: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf S = Sup {x. \<forall>s\<in>S. x \<le> s}"
+ by (rule cInf_eq_non_empty) (auto intro: cSup_upper cSup_least)
+
+lemma cSup_cInf: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup S = Inf {x. \<forall>s\<in>S. s \<le> x}"
+ by (rule cSup_eq_non_empty) (auto intro: cInf_lower cInf_greatest)
+
+lemma cSup_insert:
+ assumes x: "X \<noteq> {}"
+ and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
+ shows "Sup (insert a X) = sup a (Sup X)"
+proof (intro cSup_eq_non_empty)
+ fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> x \<le> y" with x show "sup a (Sup X) \<le> y" by (auto intro: cSup_least)
+qed (auto intro: le_supI2 z cSup_upper)
+
+lemma cInf_insert:
+ assumes x: "X \<noteq> {}"
+ and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
+ shows "Inf (insert a X) = inf a (Inf X)"
+proof (intro cInf_eq_non_empty)
+ fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> y \<le> x" with x show "y \<le> inf a (Inf X)" by (auto intro: cInf_greatest)
+qed (auto intro: le_infI2 z cInf_lower)
+
+lemma cSup_insert_If:
+ "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
+ using cSup_insert[of X z] by simp
+
+lemma cInf_insert_if:
+ "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
+ using cInf_insert[of X z] by simp
+
+lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X"
+proof (induct X arbitrary: x rule: finite_induct)
+ case (insert x X y) then show ?case
+ apply (cases "X = {}")
+ apply simp
+ apply (subst cSup_insert[of _ "Sup X"])
+ apply (auto intro: le_supI2)
+ done
+qed simp
+
+lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x"
+proof (induct X arbitrary: x rule: finite_induct)
+ case (insert x X y) then show ?case
+ apply (cases "X = {}")
+ apply simp
+ apply (subst cInf_insert[of _ "Inf X"])
+ apply (auto intro: le_infI2)
+ done
+qed simp
+
+lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X"
+proof (induct X rule: finite_ne_induct)
+ case (insert x X) then show ?case
+ using cSup_insert[of X "Sup_fin X" x] le_cSup_finite[of X] by simp
+qed simp
+
+lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X"
+proof (induct X rule: finite_ne_induct)
+ case (insert x X) then show ?case
+ using cInf_insert[of X "Inf_fin X" x] cInf_le_finite[of X] by simp
+qed simp
+
+lemma cSup_atMost[simp]: "Sup {..x} = x"
+ by (auto intro!: cSup_eq_maximum)
+
+lemma cSup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = x"
+ by (auto intro!: cSup_eq_maximum)
+
+lemma cSup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = x"
+ by (auto intro!: cSup_eq_maximum)
+
+lemma cInf_atLeast[simp]: "Inf {x..} = x"
+ by (auto intro!: cInf_eq_minimum)
+
+lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y"
+ by (auto intro!: cInf_eq_minimum)
+
+lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
+ by (auto intro!: cInf_eq_minimum)
+
+end
+
+instance complete_lattice \<subseteq> conditional_complete_lattice
+ by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
+
+lemma isLub_cSup:
+ "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
+ by (auto simp add: isLub_def setle_def leastP_def isUb_def
+ intro!: setgeI intro: cSup_upper cSup_least)
+
+lemma cSup_eq:
+ fixes a :: "'a :: {conditional_complete_lattice, no_bot}"
+ assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
+ assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
+ shows "Sup X = a"
+proof cases
+ assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
+qed (intro cSup_eq_non_empty assms)
+
+lemma cInf_eq:
+ fixes a :: "'a :: {conditional_complete_lattice, no_top}"
+ assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
+ assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
+ shows "Inf X = a"
+proof cases
+ assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
+qed (intro cInf_eq_non_empty assms)
+
+lemma cSup_le: "(S::'a::conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
+ by (metis cSup_least setle_def)
+
+lemma cInf_ge: "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
+ by (metis cInf_greatest setge_def)
+
+class conditional_complete_linorder = conditional_complete_lattice + linorder
+begin
+
+lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
+ "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
+ by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
+
+lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)"
+ by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
+
+lemma less_cSupE:
+ assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
+ by (metis cSup_least assms not_le that)
+
+lemma less_cSupD:
+ "X \<noteq> {} \<Longrightarrow> z < Sup X \<Longrightarrow> \<exists>x\<in>X. z < x"
+ by (metis less_cSup_iff not_leE)
+
+lemma cInf_lessD:
+ "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
+ by (metis cInf_less_iff not_leE)
+
+lemma complete_interval:
+ assumes "a < b" and "P a" and "\<not> P b"
+ shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and>
+ (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
+proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
+ show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+ by (rule cSup_upper [where z=b], auto)
+ (metis `a < b` `\<not> P b` linear less_le)
+next
+ show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
+ apply (rule cSup_least)
+ apply auto
+ apply (metis less_le_not_le)
+ apply (metis `a<b` `~ P b` linear less_le)
+ done
+next
+ fix x
+ assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+ show "P x"
+ apply (rule less_cSupE [OF lt], auto)
+ apply (metis less_le_not_le)
+ apply (metis x)
+ done
+next
+ fix d
+ assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
+ thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+ by (rule_tac z="b" in cSup_upper, auto)
+ (metis `a<b` `~ P b` linear less_le)
+qed
+
+end
+
+lemma cSup_bounds:
+ fixes S :: "'a :: conditional_complete_lattice set"
+ assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
+ shows "a \<le> Sup S \<and> Sup S \<le> b"
+proof-
+ from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
+ hence b: "Sup S \<le> b" using u
+ by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
+ from Se obtain y where y: "y \<in> S" by blast
+ from lub l have "a \<le> Sup S"
+ by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
+ (metis le_iff_sup le_sup_iff y)
+ with b show ?thesis by blast
+qed
+
+
+lemma cSup_unique: "(S::'a :: {conditional_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
+ by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
+
+lemma cInf_unique: "b <=* (S::'a :: {conditional_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
+ by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
+
+lemma cSup_eq_Max: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
+ using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
+
+lemma cInf_eq_Min: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
+ using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
+
+lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
+ by (auto intro!: cSup_eq_non_empty intro: dense_le)
+
+lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
+ by (auto intro!: cSup_eq intro: dense_le_bounded)
+
+lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
+ by (auto intro!: cSup_eq intro: dense_le_bounded)
+
+lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditional_complete_linorder, dense_linorder} <..} = x"
+ by (auto intro!: cInf_eq intro: dense_ge)
+
+lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditional_complete_linorder, dense_linorder}} = y"
+ by (auto intro!: cInf_eq intro: dense_ge_bounded)
+
+lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = y"
+ by (auto intro!: cInf_eq intro: dense_ge_bounded)
+
+end
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Mar 26 12:20:52 2013 +0100
@@ -8,17 +8,56 @@
"~~/src/HOL/Library/Indicator_Function"
begin
-lemma cSup_finite_ge_iff:
+lemma cSup_abs_le: (* TODO: is this really needed? *)
+ fixes S :: "real set"
+ shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
+by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2)
+
+lemma cInf_abs_ge: (* TODO: is this really needed? *)
+ fixes S :: "real set"
+ shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
+by (simp add: Inf_real_def) (rule cSup_abs_le, auto)
+
+lemma cSup_asclose: (* TODO: is this really needed? *)
fixes S :: "real set"
- assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
-by (metis Max_ge Se cSup_eq_Max Max_in fS linorder_not_le less_le_trans)
+ assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
+proof-
+ have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
+ thus ?thesis using S b cSup_bounds[of S "l - e" "l+e"] unfolding th
+ by (auto simp add: setge_def setle_def)
+qed
+
+lemma cInf_asclose: (* TODO: is this really needed? *)
+ fixes S :: "real set"
+ assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
+proof -
+ have "\<bar>- Sup (uminus ` S) - l\<bar> = \<bar>Sup (uminus ` S) - (-l)\<bar>"
+ by auto
+ also have "... \<le> e"
+ apply (rule cSup_asclose)
+ apply (auto simp add: S)
+ apply (metis abs_minus_add_cancel b add_commute diff_minus)
+ done
+ finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
+ thus ?thesis
+ by (simp add: Inf_real_def)
+qed
+
+lemma cSup_finite_ge_iff:
+ fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Sup S \<longleftrightarrow> (\<exists>x\<in>S. a \<le> x)"
+ by (metis cSup_eq_Max Max_ge_iff)
lemma cSup_finite_le_iff:
- fixes S :: "real set"
- assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
-by (metis Max_ge Se cSup_eq_Max Max_in fS order_trans)
+ fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Sup S \<longleftrightarrow> (\<forall>x\<in>S. a \<ge> x)"
+ by (metis cSup_eq_Max Max_le_iff)
+
+lemma cInf_finite_ge_iff:
+ fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
+ by (metis cInf_eq_Min Min_ge_iff)
+
+lemma cInf_finite_le_iff:
+ fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
+ by (metis cInf_eq_Min Min_le_iff)
lemma Inf: (* rename *)
fixes S :: "real set"
@@ -6282,7 +6321,8 @@
unfolding real_norm_def abs_le_iff
apply auto
done
- show "((\<lambda>k. Inf {f j x |j. k \<le> j}) ---> g x) sequentially"
+
+ show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
proof (rule LIMSEQ_I)
case goal1
hence "0<r/2" by auto
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Mar 26 12:20:52 2013 +0100
@@ -1374,34 +1374,33 @@
by (simp add: sequentially_imp_eventually_within)
lemma Lim_right_bound:
- fixes f :: "real \<Rightarrow> real"
+ fixes f :: "'a :: {linorder_topology, conditional_complete_linorder, no_top} \<Rightarrow>
+ 'b::{linorder_topology, conditional_complete_linorder}"
assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
assumes bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
proof cases
assume "{x<..} \<inter> I = {}" then show ?thesis by (simp add: Lim_within_empty)
next
- assume [simp]: "{x<..} \<inter> I \<noteq> {}"
+ assume e: "{x<..} \<inter> I \<noteq> {}"
show ?thesis
- proof (rule Lim_within_LIMSEQ, safe)
- fix S assume S: "\<forall>n. S n \<noteq> x \<and> S n \<in> {x <..} \<inter> I" "S ----> x"
-
- show "(\<lambda>n. f (S n)) ----> Inf (f ` ({x<..} \<inter> I))"
- proof (rule LIMSEQ_I, rule ccontr)
- fix r :: real assume "0 < r"
- with cInf_close[of "f ` ({x<..} \<inter> I)" r]
- obtain y where y: "x < y" "y \<in> I" "f y < Inf (f ` ({x <..} \<inter> I)) + r" by auto
- from `x < y` have "0 < y - x" by auto
- from S(2)[THEN LIMSEQ_D, OF this]
- obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>S n - x\<bar> < y - x" by auto
-
- assume "\<not> (\<exists>N. \<forall>n\<ge>N. norm (f (S n) - Inf (f ` ({x<..} \<inter> I))) < r)"
- moreover have "\<And>n. Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
- using S bnd by (intro cInf_lower[where z=K]) auto
- ultimately obtain n where n: "N \<le> n" "r + Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
- by (auto simp: not_less field_simps)
- with N[OF n(1)] mono[OF _ `y \<in> I`, of "S n"] S(1)[THEN spec, of n] y
- show False by auto
+ proof (rule order_tendstoI)
+ fix a assume a: "a < Inf (f ` ({x<..} \<inter> I))"
+ { fix y assume "y \<in> {x<..} \<inter> I"
+ with e bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
+ by (auto intro: cInf_lower)
+ with a have "a < f y" by (blast intro: less_le_trans) }
+ then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
+ by (auto simp: Topological_Spaces.eventually_within intro: exI[of _ 1] zero_less_one)
+ next
+ fix a assume "Inf (f ` ({x<..} \<inter> I)) < a"
+ from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto
+ show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
+ unfolding within_within_eq[symmetric]
+ Topological_Spaces.eventually_within[of _ _ I] eventually_at_right
+ proof (safe intro!: exI[of _ y] y)
+ fix z assume "x < z" "z \<in> I" "z < y"
+ with mono[OF `z\<in>I` `y\<in>I`] `f y < a` show "f z < a" by (auto simp: less_imp_le)
qed
qed
qed
@@ -1718,12 +1717,11 @@
using cInf_lower_EX[of _ S] assms by metis
fix e :: real assume "0 < e"
- then obtain x where x: "x \<in> S" "x < Inf S + e"
- using cInf_close `S \<noteq> {}` by auto
- moreover then have "x > Inf S - e" using * by auto
- ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
- then show "\<exists>x\<in>S. dist x (Inf S) < e"
- using x by (auto simp: dist_norm)
+ then have "Inf S < Inf S + e" by simp
+ with assms obtain x where "x \<in> S" "x < Inf S + e"
+ by (subst (asm) cInf_less_iff[of _ B]) auto
+ with * show "\<exists>x\<in>S. dist x (Inf S) < e"
+ by (intro bexI[of _ x]) (auto simp add: dist_real_def)
qed
lemma closed_contains_Inf:
--- a/src/HOL/RComplete.thy Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/RComplete.thy Tue Mar 26 12:20:52 2013 +0100
@@ -8,7 +8,7 @@
header {* Completeness of the Reals; Floor and Ceiling Functions *}
theory RComplete
-imports Lubs RealDef
+imports Conditional_Complete_Lattices RealDef
begin
lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
--- a/src/HOL/RealDef.thy Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/RealDef.thy Tue Mar 26 12:20:52 2013 +0100
@@ -8,7 +8,7 @@
header {* Development of the Reals using Cauchy Sequences *}
theory RealDef
-imports Rat
+imports Rat Conditional_Complete_Lattices
begin
text {*
@@ -922,6 +922,56 @@
using 1 2 3 by (rule_tac x="Real B" in exI, simp)
qed
+
+instantiation real :: conditional_complete_linorder
+begin
+
+subsection{*Supremum of a set of reals*}
+
+definition
+ Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
+
+definition
+ Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
+
+instance
+proof
+ { fix z x :: real and X :: "real set"
+ assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
+ then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
+ using complete_real[of X] by blast
+ then show "x \<le> Sup X"
+ unfolding Sup_real_def by (rule LeastI2_order) (auto simp: x) }
+ note Sup_upper = this
+
+ { fix z :: real and X :: "real set"
+ assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
+ then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
+ using complete_real[of X] by blast
+ then have "Sup X = s"
+ unfolding Sup_real_def by (best intro: Least_equality)
+ also with s z have "... \<le> z"
+ by blast
+ finally show "Sup X \<le> z" . }
+ note Sup_least = this
+
+ { fix x z :: real and X :: "real set"
+ assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
+ have "-x \<le> Sup (uminus ` X)"
+ by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
+ then show "Inf X \<le> x"
+ by (auto simp add: Inf_real_def) }
+
+ { fix z :: real and X :: "real set"
+ assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
+ have "Sup (uminus ` X) \<le> -z"
+ using x z by (force intro: Sup_least)
+ then show "z \<le> Inf X"
+ by (auto simp add: Inf_real_def) }
+qed
+end
+
+
subsection {* Hiding implementation details *}
hide_const (open) vanishes cauchy positive Real
@@ -1525,7 +1575,6 @@
lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
by simp
-
subsection {* Implementation of rational real numbers *}
text {* Formal constructor *}
--- a/src/HOL/RealVector.thy Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/RealVector.thy Tue Mar 26 12:20:52 2013 +0100
@@ -5,7 +5,7 @@
header {* Vector Spaces and Algebras over the Reals *}
theory RealVector
-imports RComplete Metric_Spaces SupInf
+imports Metric_Spaces
begin
subsection {* Locale for additive functions *}
@@ -685,6 +685,8 @@
end
+instance real :: linear_continuum_topology ..
+
subsection {* Extra type constraints *}
text {* Only allow @{term "open"} in class @{text topological_space}. *}
@@ -917,180 +919,4 @@
by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp)
qed
-section {* Connectedness *}
-
-class linear_continuum_topology = linorder_topology + conditional_complete_linorder + inner_dense_linorder
-begin
-
-lemma Inf_notin_open:
- assumes A: "open A" and bnd: "\<forall>a\<in>A. x < a"
- shows "Inf A \<notin> A"
-proof
- assume "Inf A \<in> A"
- then obtain b where "b < Inf A" "{b <.. Inf A} \<subseteq> A"
- using open_left[of A "Inf A" x] assms by auto
- with dense[of b "Inf A"] obtain c where "c < Inf A" "c \<in> A"
- by (auto simp: subset_eq)
- then show False
- using cInf_lower[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
-qed
-
-lemma Sup_notin_open:
- assumes A: "open A" and bnd: "\<forall>a\<in>A. a < x"
- shows "Sup A \<notin> A"
-proof
- assume "Sup A \<in> A"
- then obtain b where "Sup A < b" "{Sup A ..< b} \<subseteq> A"
- using open_right[of A "Sup A" x] assms by auto
- with dense[of "Sup A" b] obtain c where "Sup A < c" "c \<in> A"
- by (auto simp: subset_eq)
- then show False
- using cSup_upper[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
-qed
-
end
-
-instance real :: linear_continuum_topology ..
-
-lemma connectedI_interval:
- 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)
- { fix A B assume "open A" "open B" "A \<inter> B \<inter> U = {}" "U \<subseteq> A \<union> B"
- fix x y assume "x < y" "x \<in> A" "y \<in> B" "x \<in> U" "y \<in> U"
-
- let ?z = "Inf (B \<inter> {x <..})"
-
- have "x \<le> ?z" "?z \<le> y"
- using `y \<in> B` `x < y` by (auto intro: cInf_lower[where z=x] cInf_greatest)
- with `x \<in> U` `y \<in> U` have "?z \<in> U"
- by (rule *)
- moreover have "?z \<notin> B \<inter> {x <..}"
- using `open B` by (intro Inf_notin_open) auto
- ultimately have "?z \<in> A"
- using `x \<le> ?z` `A \<inter> B \<inter> U = {}` `x \<in> A` `U \<subseteq> A \<union> B` by auto
-
- { assume "?z < y"
- obtain a where "?z < a" "{?z ..< a} \<subseteq> A"
- using open_right[OF `open A` `?z \<in> A` `?z < y`] by auto
- moreover obtain b where "b \<in> B" "x < b" "b < min a y"
- using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
- by (auto intro: less_imp_le)
- moreover then have "?z \<le> b"
- by (intro cInf_lower[where z=x]) auto
- moreover have "b \<in> U"
- using `x \<le> ?z` `?z \<le> b` `b < min a y`
- by (intro *[OF `x \<in> U` `y \<in> U`]) (auto simp: less_imp_le)
- ultimately have "\<exists>b\<in>B. b \<in> A \<and> b \<in> U"
- by (intro bexI[of _ b]) auto }
- then have False
- using `?z \<le> y` `?z \<in> A` `y \<in> B` `y \<in> U` `A \<inter> B \<inter> U = {}` unfolding le_less by blast }
- note not_disjoint = this
-
- fix A B assume AB: "open A" "open B" "U \<subseteq> A \<union> B" "A \<inter> B \<inter> U = {}"
- moreover assume "A \<inter> U \<noteq> {}" then obtain x where x: "x \<in> U" "x \<in> A" by auto
- moreover assume "B \<inter> U \<noteq> {}" then obtain y where y: "y \<in> U" "y \<in> B" by auto
- moreover note not_disjoint[of B A y x] not_disjoint[of A B x y]
- ultimately show False by (cases x y rule: linorder_cases) auto
-qed
-
-lemma connected_iff_interval:
- 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::linear_continuum_topology set)"
- unfolding connected_iff_interval by auto
-
-lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
- unfolding connected_iff_interval by auto
-
-lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
- unfolding connected_iff_interval by auto
-
-lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
- unfolding connected_iff_interval by auto
-
-lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
- unfolding connected_iff_interval by auto
-
-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::linear_continuum_topology}"
- unfolding connected_iff_interval by auto
-
-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::linear_continuum_topology}"
- unfolding connected_iff_interval by auto
-
-lemma connected_contains_Ioo:
- fixes A :: "'a :: linorder_topology set"
- assumes A: "connected A" "a \<in> A" "b \<in> A" shows "{a <..< b} \<subseteq> A"
- using connectedD_interval[OF A] by (simp add: subset_eq Ball_def less_imp_le)
-
-subsection {* Intermediate Value Theorem *}
-
-lemma IVT':
- 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"
-proof -
- have "connected {a..b}"
- unfolding connected_iff_interval by auto
- from connected_continuous_image[OF * this, THEN connectedD_interval, of "f a" "f b" y] y
- show ?thesis
- by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
-qed
-
-lemma IVT2':
- 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"
-proof -
- have "connected {a..b}"
- unfolding connected_iff_interval by auto
- from connected_continuous_image[OF * this, THEN connectedD_interval, of "f b" "f a" y] y
- show ?thesis
- by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
-qed
-
-lemma IVT:
- 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 :: 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::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}"
- shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
-proof -
- note I = inj_on_iff[OF inj]
- { assume "f x < f a" "f x < f b"
- then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f x < f s"
- using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
- by (auto simp: continuous_on_subset[OF cont] less_imp_le)
- with x I have False by auto }
- moreover
- { assume "f a < f x" "f b < f x"
- then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f s < f x"
- using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
- by (auto simp: continuous_on_subset[OF cont] less_imp_le)
- with x I have False by auto }
- ultimately show ?thesis
- using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff)
-qed
-
-end
--- a/src/HOL/SupInf.thy Mon Mar 25 20:00:27 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,433 +0,0 @@
-(* Author: Amine Chaieb and L C Paulson, University of Cambridge *)
-
-header {*Sup and Inf Operators on Sets of Reals.*}
-
-theory SupInf
-imports RComplete
-begin
-
-lemma Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
- by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
-
-lemma Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
- by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
-
-text {*
-
-To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
-@{const Inf} in theorem names with c.
-
-*}
-
-class conditional_complete_lattice = lattice + Sup + Inf +
- assumes cInf_lower: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> z \<le> a) \<Longrightarrow> Inf X \<le> x"
- and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X"
- assumes cSup_upper: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> a \<le> z) \<Longrightarrow> x \<le> Sup X"
- and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
-begin
-
-lemma cSup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
- "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
- by (blast intro: antisym cSup_upper cSup_least)
-
-lemma cInf_eq_minimum: (*REAL_INF_MIN in HOL4*)
- "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
- by (intro antisym cInf_lower[of z X z] cInf_greatest[of X z]) auto
-
-lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> a \<le> z) \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)"
- by (metis order_trans cSup_upper cSup_least)
-
-lemma le_cInf_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> z \<le> a) \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
- by (metis order_trans cInf_lower cInf_greatest)
-
-lemma cSup_singleton [simp]: "Sup {x} = x"
- by (intro cSup_eq_maximum) auto
-
-lemma cInf_singleton [simp]: "Inf {x} = x"
- by (intro cInf_eq_minimum) auto
-
-lemma cSup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
- "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
- by (metis cSup_upper order_trans)
-
-lemma cInf_lower2:
- "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
- by (metis cInf_lower order_trans)
-
-lemma cSup_upper_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
- by (blast intro: cSup_upper)
-
-lemma cInf_lower_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
- by (blast intro: cInf_lower)
-
-lemma cSup_eq_non_empty:
- assumes 1: "X \<noteq> {}"
- assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
- assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
- shows "Sup X = a"
- by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper)
-
-lemma cInf_eq_non_empty:
- assumes 1: "X \<noteq> {}"
- assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
- assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
- shows "Inf X = a"
- by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
-
-lemma cSup_insert:
- assumes x: "X \<noteq> {}"
- and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
- shows "Sup (insert a X) = sup a (Sup X)"
-proof (intro cSup_eq_non_empty)
- fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> x \<le> y" with x show "sup a (Sup X) \<le> y" by (auto intro: cSup_least)
-qed (auto intro: le_supI2 z cSup_upper)
-
-lemma cInf_insert:
- assumes x: "X \<noteq> {}"
- and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
- shows "Inf (insert a X) = inf a (Inf X)"
-proof (intro cInf_eq_non_empty)
- fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> y \<le> x" with x show "y \<le> inf a (Inf X)" by (auto intro: cInf_greatest)
-qed (auto intro: le_infI2 z cInf_lower)
-
-lemma cSup_insert_If:
- "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
- using cSup_insert[of X z] by simp
-
-lemma cInf_insert_if:
- "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
- using cInf_insert[of X z] by simp
-
-lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X"
-proof (induct X arbitrary: x rule: finite_induct)
- case (insert x X y) then show ?case
- apply (cases "X = {}")
- apply simp
- apply (subst cSup_insert[of _ "Sup X"])
- apply (auto intro: le_supI2)
- done
-qed simp
-
-lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x"
-proof (induct X arbitrary: x rule: finite_induct)
- case (insert x X y) then show ?case
- apply (cases "X = {}")
- apply simp
- apply (subst cInf_insert[of _ "Inf X"])
- apply (auto intro: le_infI2)
- done
-qed simp
-
-lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X"
-proof (induct X rule: finite_ne_induct)
- case (insert x X) then show ?case
- using cSup_insert[of X "Sup_fin X" x] le_cSup_finite[of X] by simp
-qed simp
-
-lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X"
-proof (induct X rule: finite_ne_induct)
- case (insert x X) then show ?case
- using cInf_insert[of X "Inf_fin X" x] cInf_le_finite[of X] by simp
-qed simp
-
-lemma cSup_atMost[simp]: "Sup {..x} = x"
- by (auto intro!: cSup_eq_maximum)
-
-lemma cSup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = x"
- by (auto intro!: cSup_eq_maximum)
-
-lemma cSup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = x"
- by (auto intro!: cSup_eq_maximum)
-
-lemma cInf_atLeast[simp]: "Inf {x..} = x"
- by (auto intro!: cInf_eq_minimum)
-
-lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y"
- by (auto intro!: cInf_eq_minimum)
-
-lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
- by (auto intro!: cInf_eq_minimum)
-
-end
-
-instance complete_lattice \<subseteq> conditional_complete_lattice
- by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
-
-lemma isLub_cSup:
- "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
- by (auto simp add: isLub_def setle_def leastP_def isUb_def
- intro!: setgeI intro: cSup_upper cSup_least)
-
-lemma cSup_eq:
- fixes a :: "'a :: {conditional_complete_lattice, no_bot}"
- assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
- assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
- shows "Sup X = a"
-proof cases
- assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
-qed (intro cSup_eq_non_empty assms)
-
-lemma cInf_eq:
- fixes a :: "'a :: {conditional_complete_lattice, no_top}"
- assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
- assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
- shows "Inf X = a"
-proof cases
- assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
-qed (intro cInf_eq_non_empty assms)
-
-lemma cSup_le: "(S::'a::conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
- by (metis cSup_least setle_def)
-
-lemma cInf_ge: "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
- by (metis cInf_greatest setge_def)
-
-class conditional_complete_linorder = conditional_complete_lattice + linorder
-begin
-
-lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
- "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
- by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
-
-lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)"
- by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
-
-lemma less_cSupE:
- assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
- by (metis cSup_least assms not_le that)
-
-lemma complete_interval:
- assumes "a < b" and "P a" and "\<not> P b"
- shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and>
- (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
-proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
- show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
- by (rule cSup_upper [where z=b], auto)
- (metis `a < b` `\<not> P b` linear less_le)
-next
- show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
- apply (rule cSup_least)
- apply auto
- apply (metis less_le_not_le)
- apply (metis `a<b` `~ P b` linear less_le)
- done
-next
- fix x
- assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
- show "P x"
- apply (rule less_cSupE [OF lt], auto)
- apply (metis less_le_not_le)
- apply (metis x)
- done
-next
- fix d
- assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
- thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
- by (rule_tac z="b" in cSup_upper, auto)
- (metis `a<b` `~ P b` linear less_le)
-qed
-
-end
-
-lemma cSup_unique: "(S::'a :: {conditional_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
- by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
-
-lemma cInf_unique: "b <=* (S::'a :: {conditional_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
- by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
-
-lemma cSup_eq_Max: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
- using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
-
-lemma cInf_eq_Min: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
- using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
-
-lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
- by (auto intro!: cSup_eq_non_empty intro: dense_le)
-
-lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
- by (auto intro!: cSup_eq intro: dense_le_bounded)
-
-lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
- by (auto intro!: cSup_eq intro: dense_le_bounded)
-
-lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditional_complete_linorder, dense_linorder} <..} = x"
- by (auto intro!: cInf_eq intro: dense_ge)
-
-lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditional_complete_linorder, dense_linorder}} = y"
- by (auto intro!: cInf_eq intro: dense_ge_bounded)
-
-lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = y"
- by (auto intro!: cInf_eq intro: dense_ge_bounded)
-
-instantiation real :: conditional_complete_linorder
-begin
-
-subsection{*Supremum of a set of reals*}
-
-definition
- Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
-
-definition
- Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
-
-instance
-proof
- { fix z x :: real and X :: "real set"
- assume x: "x \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
- show "x \<le> Sup X"
- proof (auto simp add: Sup_real_def)
- from complete_real[of X]
- obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
- by (blast intro: x z)
- hence "x \<le> s"
- by (blast intro: x z)
- also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
- by (fast intro: Least_equality [symmetric])
- finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
- qed }
- note Sup_upper = this
-
- { fix z :: real and X :: "real set"
- assume x: "X \<noteq> {}"
- and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
- show "Sup X \<le> z"
- proof (auto simp add: Sup_real_def)
- from complete_real x
- obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
- by (blast intro: z)
- hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
- by (best intro: Least_equality)
- also with s z have "... \<le> z"
- by blast
- finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
- qed }
- note Sup_least = this
-
- { fix x z :: real and X :: "real set"
- assume x: "x \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
- show "Inf X \<le> x"
- proof -
- have "-x \<le> Sup (uminus ` X)"
- by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
- thus ?thesis
- by (auto simp add: Inf_real_def)
- qed }
-
- { fix z :: real and X :: "real set"
- assume x: "X \<noteq> {}"
- and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
- show "z \<le> Inf X"
- proof -
- have "Sup (uminus ` X) \<le> -z"
- using x z by (force intro: Sup_least)
- hence "z \<le> - Sup (uminus ` X)"
- by simp
- thus ?thesis
- by (auto simp add: Inf_real_def)
- qed }
-qed
-end
-
-subsection{*Supremum of a set of reals*}
-
-lemma cSup_abs_le:
- fixes S :: "real set"
- shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
-by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2)
-
-lemma cSup_bounds:
- fixes S :: "real set"
- assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
- shows "a \<le> Sup S \<and> Sup S \<le> b"
-proof-
- from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
- hence b: "Sup S \<le> b" using u
- by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
- from Se obtain y where y: "y \<in> S" by blast
- from lub l have "a \<le> Sup S"
- by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
- (metis le_iff_sup le_sup_iff y)
- with b show ?thesis by blast
-qed
-
-lemma cSup_asclose:
- fixes S :: "real set"
- assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
-proof-
- have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
- thus ?thesis using S b cSup_bounds[of S "l - e" "l+e"] unfolding th
- by (auto simp add: setge_def setle_def)
-qed
-
-subsection{*Infimum of a set of reals*}
-
-lemma cInf_greater:
- fixes z :: real
- shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
- by (metis cInf_less_iff not_leE)
-
-lemma cInf_close:
- fixes e :: real
- shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
- by (metis add_strict_increasing add_commute cInf_greater linorder_not_le pos_add_strict)
-
-lemma cInf_finite_in:
- fixes S :: "real set"
- assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "Inf S \<in> S"
- using cInf_eq_Min[OF fS Se] Min_in[OF fS Se] by metis
-
-lemma cInf_finite_ge_iff:
- fixes S :: "real set"
- shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
-by (metis cInf_eq_Min cInf_finite_in Min_le order_trans)
-
-lemma cInf_finite_le_iff:
- fixes S :: "real set"
- shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
-by (metis cInf_eq_Min cInf_finite_ge_iff cInf_finite_in Min_le order_antisym linear)
-
-lemma cInf_finite_gt_iff:
- fixes S :: "real set"
- shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
-by (metis cInf_finite_le_iff linorder_not_less)
-
-lemma cInf_finite_lt_iff:
- fixes S :: "real set"
- shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
-by (metis cInf_finite_ge_iff linorder_not_less)
-
-lemma cInf_abs_ge:
- fixes S :: "real set"
- shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
-by (simp add: Inf_real_def) (rule cSup_abs_le, auto)
-
-lemma cInf_asclose:
- fixes S :: "real set"
- assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
-proof -
- have "\<bar>- Sup (uminus ` S) - l\<bar> = \<bar>Sup (uminus ` S) - (-l)\<bar>"
- by auto
- also have "... \<le> e"
- apply (rule cSup_asclose)
- apply (auto simp add: S)
- apply (metis abs_minus_add_cancel b add_commute diff_minus)
- done
- finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
- thus ?thesis
- by (simp add: Inf_real_def)
-qed
-
-subsection{*Relate max and min to Sup and Inf.*}
-
-lemma real_max_cSup:
- fixes x :: real
- shows "max x y = Sup {x,y}"
- by (subst cSup_insert[of _ y]) (simp_all add: sup_max)
-
-lemma real_min_cInf:
- fixes x :: real
- shows "min x y = Inf {x,y}"
- by (subst cInf_insert[of _ y]) (simp_all add: inf_min)
-
-end
--- a/src/HOL/Topological_Spaces.thy Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/Topological_Spaces.thy Tue Mar 26 12:20:52 2013 +0100
@@ -6,7 +6,7 @@
header {* Topological Spaces *}
theory Topological_Spaces
-imports Main
+imports Main Conditional_Complete_Lattices
begin
subsection {* Topological space *}
@@ -2062,5 +2062,180 @@
unfolding connected_def by blast
qed
+
+section {* Connectedness *}
+
+class linear_continuum_topology = linorder_topology + conditional_complete_linorder + inner_dense_linorder
+begin
+
+lemma Inf_notin_open:
+ assumes A: "open A" and bnd: "\<forall>a\<in>A. x < a"
+ shows "Inf A \<notin> A"
+proof
+ assume "Inf A \<in> A"
+ then obtain b where "b < Inf A" "{b <.. Inf A} \<subseteq> A"
+ using open_left[of A "Inf A" x] assms by auto
+ with dense[of b "Inf A"] obtain c where "c < Inf A" "c \<in> A"
+ by (auto simp: subset_eq)
+ then show False
+ using cInf_lower[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
+qed
+
+lemma Sup_notin_open:
+ assumes A: "open A" and bnd: "\<forall>a\<in>A. a < x"
+ shows "Sup A \<notin> A"
+proof
+ assume "Sup A \<in> A"
+ then obtain b where "Sup A < b" "{Sup A ..< b} \<subseteq> A"
+ using open_right[of A "Sup A" x] assms by auto
+ with dense[of "Sup A" b] obtain c where "Sup A < c" "c \<in> A"
+ by (auto simp: subset_eq)
+ then show False
+ using cSup_upper[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
+qed
+
end
+lemma connectedI_interval:
+ 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)
+ { fix A B assume "open A" "open B" "A \<inter> B \<inter> U = {}" "U \<subseteq> A \<union> B"
+ fix x y assume "x < y" "x \<in> A" "y \<in> B" "x \<in> U" "y \<in> U"
+
+ let ?z = "Inf (B \<inter> {x <..})"
+
+ have "x \<le> ?z" "?z \<le> y"
+ using `y \<in> B` `x < y` by (auto intro: cInf_lower[where z=x] cInf_greatest)
+ with `x \<in> U` `y \<in> U` have "?z \<in> U"
+ by (rule *)
+ moreover have "?z \<notin> B \<inter> {x <..}"
+ using `open B` by (intro Inf_notin_open) auto
+ ultimately have "?z \<in> A"
+ using `x \<le> ?z` `A \<inter> B \<inter> U = {}` `x \<in> A` `U \<subseteq> A \<union> B` by auto
+
+ { assume "?z < y"
+ obtain a where "?z < a" "{?z ..< a} \<subseteq> A"
+ using open_right[OF `open A` `?z \<in> A` `?z < y`] by auto
+ moreover obtain b where "b \<in> B" "x < b" "b < min a y"
+ using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
+ by (auto intro: less_imp_le)
+ moreover then have "?z \<le> b"
+ by (intro cInf_lower[where z=x]) auto
+ moreover have "b \<in> U"
+ using `x \<le> ?z` `?z \<le> b` `b < min a y`
+ by (intro *[OF `x \<in> U` `y \<in> U`]) (auto simp: less_imp_le)
+ ultimately have "\<exists>b\<in>B. b \<in> A \<and> b \<in> U"
+ by (intro bexI[of _ b]) auto }
+ then have False
+ using `?z \<le> y` `?z \<in> A` `y \<in> B` `y \<in> U` `A \<inter> B \<inter> U = {}` unfolding le_less by blast }
+ note not_disjoint = this
+
+ fix A B assume AB: "open A" "open B" "U \<subseteq> A \<union> B" "A \<inter> B \<inter> U = {}"
+ moreover assume "A \<inter> U \<noteq> {}" then obtain x where x: "x \<in> U" "x \<in> A" by auto
+ moreover assume "B \<inter> U \<noteq> {}" then obtain y where y: "y \<in> U" "y \<in> B" by auto
+ moreover note not_disjoint[of B A y x] not_disjoint[of A B x y]
+ ultimately show False by (cases x y rule: linorder_cases) auto
+qed
+
+lemma connected_iff_interval:
+ 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::linear_continuum_topology set)"
+ unfolding connected_iff_interval by auto
+
+lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
+ unfolding connected_iff_interval by auto
+
+lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
+ unfolding connected_iff_interval by auto
+
+lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
+ unfolding connected_iff_interval by auto
+
+lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
+ unfolding connected_iff_interval by auto
+
+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::linear_continuum_topology}"
+ unfolding connected_iff_interval by auto
+
+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::linear_continuum_topology}"
+ unfolding connected_iff_interval by auto
+
+lemma connected_contains_Ioo:
+ fixes A :: "'a :: linorder_topology set"
+ assumes A: "connected A" "a \<in> A" "b \<in> A" shows "{a <..< b} \<subseteq> A"
+ using connectedD_interval[OF A] by (simp add: subset_eq Ball_def less_imp_le)
+
+subsection {* Intermediate Value Theorem *}
+
+lemma IVT':
+ 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"
+proof -
+ have "connected {a..b}"
+ unfolding connected_iff_interval by auto
+ from connected_continuous_image[OF * this, THEN connectedD_interval, of "f a" "f b" y] y
+ show ?thesis
+ by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
+qed
+
+lemma IVT2':
+ 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"
+proof -
+ have "connected {a..b}"
+ unfolding connected_iff_interval by auto
+ from connected_continuous_image[OF * this, THEN connectedD_interval, of "f b" "f a" y] y
+ show ?thesis
+ by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
+qed
+
+lemma IVT:
+ 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 :: 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::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}"
+ shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
+proof -
+ note I = inj_on_iff[OF inj]
+ { assume "f x < f a" "f x < f b"
+ then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f x < f s"
+ using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
+ by (auto simp: continuous_on_subset[OF cont] less_imp_le)
+ with x I have False by auto }
+ moreover
+ { assume "f a < f x" "f b < f x"
+ then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f s < f x"
+ using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
+ by (auto simp: continuous_on_subset[OF cont] less_imp_le)
+ with x I have False by auto }
+ ultimately show ?thesis
+ using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff)
+qed
+
+end
+