replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
--- a/src/HOL/Library/Extended_Real.thy Wed Feb 06 17:18:01 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy Wed Feb 06 17:57:21 2013 +0100
@@ -11,6 +11,13 @@
imports "~~/src/HOL/Complex_Main" Extended_Nat
begin
+text {*
+
+For more lemmas about the extended real numbers go to
+ @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
+
+*}
+
lemma LIMSEQ_SUP:
fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
assumes "incseq X"
@@ -22,24 +29,37 @@
lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
by (cases P) (simp_all add: eventually_False)
-lemma (in complete_lattice) Inf_le_Sup:
- assumes "A \<noteq> {}" shows "Inf A \<le> Sup A"
-proof -
- from `A \<noteq> {}` obtain x where "x \<in> A" by auto
- then show ?thesis
- by (metis Sup_upper2 Inf_lower)
-qed
-
-lemma (in complete_lattice) INF_le_SUP:
- "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
+lemma (in complete_lattice) Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
+ by (metis Sup_upper2 Inf_lower ex_in_conv)
+
+lemma (in complete_lattice) INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
-text {*
-
-For more lemmas about the extended real numbers go to
- @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
-
-*}
+lemma (in complete_linorder) le_Sup_iff:
+ "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
+proof safe
+ fix y assume "x \<le> Sup A" "y < x"
+ then have "y < Sup A" by auto
+ then show "\<exists>a\<in>A. y < a"
+ unfolding less_Sup_iff .
+qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] Sup_upper)
+
+lemma (in complete_linorder) le_SUP_iff:
+ "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
+ unfolding le_Sup_iff SUP_def by simp
+
+lemma (in complete_linorder) Inf_le_iff:
+ "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
+proof safe
+ fix y assume "x \<ge> Inf A" "y > x"
+ then have "y > Inf A" by auto
+ then show "\<exists>a\<in>A. y > a"
+ unfolding Inf_less_iff .
+qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] Inf_lower)
+
+lemma (in complete_linorder) le_INF_iff:
+ "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
+ unfolding Inf_le_iff INF_def by simp
lemma (in complete_lattice) Sup_eqI:
assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
@@ -1429,8 +1449,7 @@
lemma ereal_le_Sup:
fixes x :: ereal
- shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))"
-(is "?lhs <-> ?rhs")
+ shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))" (is "?lhs = ?rhs")
proof-
{ assume "?rhs"
{ assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
@@ -1994,18 +2013,13 @@
qed
lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
- unfolding tendsto_def
-proof safe
- fix S :: "ereal set" assume "open S" "\<infinity> \<in> S"
- from open_PInfty[OF this] guess B .. note B = this
- moreover
- assume "\<forall>r::real. eventually (\<lambda>z. r < f z) F"
- then have "eventually (\<lambda>z. f z \<in> {B <..}) F" by auto
- ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
-next
- fix x assume "\<forall>S. open S \<longrightarrow> \<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
- from this[rule_format, of "{ereal x <..}"]
- show "eventually (\<lambda>y. ereal x < f y) F" by auto
+proof -
+ { fix l :: ereal assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
+ from this[THEN spec, of "real l"]
+ have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
+ by (cases l) (auto elim: eventually_elim1) }
+ then show ?thesis
+ by (auto simp: order_tendsto_iff)
qed
lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
@@ -2209,7 +2223,6 @@
"[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
by (metis sup_ereal_def sup_least)
-
lemma ereal_LimI_finite:
fixes x :: ereal
assumes "\<bar>x\<bar> \<noteq> \<infinity>"
@@ -2403,25 +2416,142 @@
shows "Limsup F X \<le> C"
using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
+lemma le_Liminf_iff:
+ fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
+ shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
+proof -
+ { fix y P assume "eventually P F" "y < INFI (Collect P) X"
+ then have "eventually (\<lambda>x. y < X x) F"
+ by (auto elim!: eventually_elim1 dest: less_INF_D) }
+ moreover
+ { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
+ have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
+ proof cases
+ assume "\<exists>z. y < z \<and> z < C"
+ then guess z ..
+ moreover then have "z \<le> INFI {x. z < X x} X"
+ by (auto intro!: INF_greatest)
+ ultimately show ?thesis
+ using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
+ next
+ assume "\<not> (\<exists>z. y < z \<and> z < C)"
+ then have "C \<le> INFI {x. y < X x} X"
+ by (intro INF_greatest) auto
+ with `y < C` show ?thesis
+ using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
+ qed }
+ ultimately show ?thesis
+ unfolding Liminf_def le_SUP_iff by auto
+qed
+
+lemma lim_imp_Liminf:
+ fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes lim: "(f ---> f0) F"
+ shows "Liminf F f = f0"
+proof (intro Liminf_eqI)
+ fix P assume P: "eventually P F"
+ then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
+ by eventually_elim (auto intro!: INF_lower)
+ then show "INFI (Collect P) f \<le> f0"
+ by (rule tendsto_le[OF ntriv lim tendsto_const])
+next
+ fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
+ show "f0 \<le> y"
+ proof cases
+ assume "\<exists>z. y < z \<and> z < f0"
+ then guess z ..
+ moreover have "z \<le> INFI {x. z < f x} f"
+ by (rule INF_greatest) simp
+ ultimately show ?thesis
+ using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
+ next
+ assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
+ show ?thesis
+ proof (rule classical)
+ assume "\<not> f0 \<le> y"
+ then have "eventually (\<lambda>x. y < f x) F"
+ using lim[THEN topological_tendstoD, of "{y <..}"] by auto
+ then have "eventually (\<lambda>x. f0 \<le> f x) F"
+ using discrete by (auto elim!: eventually_elim1)
+ then have "INFI {x. f0 \<le> f x} f \<le> y"
+ by (rule upper)
+ moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
+ by (intro INF_greatest) simp
+ ultimately show "f0 \<le> y" by simp
+ qed
+ qed
+qed
+
+lemma lim_imp_Limsup:
+ fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+ assumes ntriv: "\<not> trivial_limit F"
+ assumes lim: "(f ---> f0) F"
+ shows "Limsup F f = f0"
+proof (intro Limsup_eqI)
+ fix P assume P: "eventually P F"
+ then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
+ by eventually_elim (auto intro!: SUP_upper)
+ then show "f0 \<le> SUPR (Collect P) f"
+ by (rule tendsto_le[OF ntriv tendsto_const lim])
+next
+ fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
+ show "y \<le> f0"
+ proof cases
+ assume "\<exists>z. f0 < z \<and> z < y"
+ then guess z ..
+ moreover have "SUPR {x. f x < z} f \<le> z"
+ by (rule SUP_least) simp
+ ultimately show ?thesis
+ using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
+ next
+ assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
+ show ?thesis
+ proof (rule classical)
+ assume "\<not> y \<le> f0"
+ then have "eventually (\<lambda>x. f x < y) F"
+ using lim[THEN topological_tendstoD, of "{..< y}"] by auto
+ then have "eventually (\<lambda>x. f x \<le> f0) F"
+ using discrete by (auto elim!: eventually_elim1 simp: not_less)
+ then have "y \<le> SUPR {x. f x \<le> f0} f"
+ by (rule lower)
+ moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
+ by (intro SUP_least) simp
+ ultimately show "y \<le> f0" by simp
+ qed
+ qed
+qed
+
+lemma Liminf_eq_Limsup:
+ fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+ assumes ntriv: "\<not> trivial_limit F"
+ and lim: "Liminf F f = f0" "Limsup F f = f0"
+ shows "(f ---> f0) F"
+proof (rule order_tendstoI)
+ fix a assume "f0 < a"
+ with assms have "Limsup F f < a" by simp
+ then obtain P where "eventually P F" "SUPR (Collect P) f < a"
+ unfolding Limsup_def INF_less_iff by auto
+ then show "eventually (\<lambda>x. f x < a) F"
+ by (auto elim!: eventually_elim1 dest: SUP_lessD)
+next
+ fix a assume "a < f0"
+ with assms have "a < Liminf F f" by simp
+ then obtain P where "eventually P F" "a < INFI (Collect P) f"
+ unfolding Liminf_def less_SUP_iff by auto
+ then show "eventually (\<lambda>x. a < f x) F"
+ by (auto elim!: eventually_elim1 dest: less_INF_D)
+qed
+
+lemma tendsto_iff_Liminf_eq_Limsup:
+ fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+ shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
+ by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
+
lemma liminf_bounded_iff:
fixes x :: "nat \<Rightarrow> ereal"
shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
-proof safe
- fix B assume "B < C" "C \<le> liminf x"
- then have "B < liminf x" by auto
- then obtain N where "B < (INF m:{N..}. x m)"
- unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
- from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
-next
- assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
- { fix B assume "B<C"
- then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
- hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
- also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
- finally have "B \<le> liminf x" .
- } then show "?lhs"
- by (metis * leD Liminf_bounded[OF sequentially_bot] linorder_le_less_linear eventually_sequentially)
-qed
+ unfolding le_Liminf_iff eventually_sequentially ..
lemma liminf_subseq_mono:
fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
@@ -2449,56 +2579,6 @@
then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
qed
-lemma lim_imp_Liminf:
- fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
- assumes ntriv: "\<not> trivial_limit F"
- assumes lim: "(f ---> f0) F"
- shows "Liminf F f = f0"
-proof (rule Liminf_eqI)
- fix y assume *: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
- show "f0 \<le> y"
- proof (rule ereal_le_ereal)
- fix B
- assume "B < f0"
- have "B \<le> INFI {x. B < f x} f"
- by (rule INF_greatest) simp
- also have "INFI {x. B < f x} f \<le> y"
- using lim[THEN topological_tendstoD, of "{B <..}"] `B < f0` * by auto
- finally show "B \<le> y" .
- qed
-next
- fix P assume P: "eventually P F"
- then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
- by eventually_elim (auto intro!: INF_lower)
- then show "INFI (Collect P) f \<le> f0"
- by (rule tendsto_le[OF ntriv lim tendsto_const])
-qed
-
-lemma lim_imp_Limsup:
- fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
- assumes ntriv: "\<not> trivial_limit F"
- assumes lim: "(f ---> f0) F"
- shows "Limsup F f = f0"
-proof (rule Limsup_eqI)
- fix y assume *: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
- show "y \<le> f0"
- proof (rule ereal_ge_ereal, safe)
- fix B
- assume "f0 < B"
- have "y \<le> SUPR {x. f x < B} f"
- using lim[THEN topological_tendstoD, of "{..< B}"] `f0 < B` * by auto
- also have "SUPR {x. f x < B} f \<le> B"
- by (rule SUP_least) simp
- finally show "y \<le> B" .
- qed
-next
- fix P assume P: "eventually P F"
- then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
- by eventually_elim (auto intro!: SUP_upper)
- then show "f0 \<le> SUPR (Collect P) f"
- by (rule tendsto_le[OF ntriv tendsto_const lim])
-qed
-
definition (in order) mono_set:
"mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
--- a/src/HOL/Limits.thy Wed Feb 06 17:18:01 2013 +0100
+++ b/src/HOL/Limits.thy Wed Feb 06 17:57:21 2013 +0100
@@ -469,12 +469,6 @@
apply (erule le_less_trans [OF dist_triangle])
done
-lemma eventually_nhds_order:
- "eventually P (nhds (a::'a::linorder_topology)) \<longleftrightarrow>
- (\<exists>S. open_interval S \<and> a \<in> S \<and> (\<forall>z\<in>S. P z))"
- (is "_ \<longleftrightarrow> ?rhs")
- unfolding eventually_nhds by (auto dest!: open_orderD dest: open_interval_imp_open)
-
lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
unfolding trivial_limit_def eventually_nhds by simp
@@ -838,6 +832,35 @@
"(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
using tendstoI tendstoD by fast
+lemma order_tendstoI:
+ fixes y :: "_ :: order_topology"
+ assumes "\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
+ assumes "\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
+ shows "(f ---> y) F"
+proof (rule topological_tendstoI)
+ fix S assume "open S" "y \<in> S"
+ then show "eventually (\<lambda>x. f x \<in> S) F"
+ unfolding open_generated_order
+ proof induct
+ case (UN K)
+ then obtain k where "y \<in> k" "k \<in> K" by auto
+ with UN(2)[of k] show ?case
+ by (auto elim: eventually_elim1)
+ qed (insert assms, auto elim: eventually_elim2)
+qed
+
+lemma order_tendstoD:
+ fixes y :: "_ :: order_topology"
+ assumes y: "(f ---> y) F"
+ shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
+ and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
+ using topological_tendstoD[OF y, of "{..< a}"] topological_tendstoD[OF y, of "{a <..}"] by auto
+
+lemma order_tendsto_iff:
+ fixes f :: "_ \<Rightarrow> 'a :: order_topology"
+ shows "(f ---> x) F \<longleftrightarrow>(\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
+ by (metis order_tendstoI order_tendstoD)
+
lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
by (simp only: tendsto_iff Zfun_def dist_norm)
@@ -908,34 +931,18 @@
qed
lemma increasing_tendsto:
- fixes f :: "_ \<Rightarrow> 'a::linorder_topology"
+ fixes f :: "_ \<Rightarrow> 'a::order_topology"
assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
shows "(f ---> l) F"
-proof (rule topological_tendstoI)
- fix S assume "open S" "l \<in> S"
- then show "eventually (\<lambda>x. f x \<in> S) F"
- proof (induct rule: open_order_induct)
- case (greaterThanLessThan a b) with en bdd show ?case
- by (auto elim!: eventually_elim2)
- qed (insert en bdd, auto elim!: eventually_elim1)
-qed
+ using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
lemma decreasing_tendsto:
- fixes f :: "_ \<Rightarrow> 'a::linorder_topology"
+ fixes f :: "_ \<Rightarrow> 'a::order_topology"
assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
shows "(f ---> l) F"
-proof (rule topological_tendstoI)
- fix S assume "open S" "l \<in> S"
- then show "eventually (\<lambda>x. f x \<in> S) F"
- proof (induct rule: open_order_induct)
- case (greaterThanLessThan a b)
- with en have "eventually (\<lambda>n. f n < b) F" by auto
- with bdd show ?case
- by eventually_elim (insert greaterThanLessThan, auto)
- qed (insert en bdd, auto elim!: eventually_elim1)
-qed
+ using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
subsubsection {* Distance and norms *}
@@ -1039,20 +1046,16 @@
qed
lemma tendsto_sandwich:
- fixes f g h :: "'a \<Rightarrow> 'b::linorder_topology"
+ fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
assumes lim: "(f ---> c) net" "(h ---> c) net"
shows "(g ---> c) net"
-proof (rule topological_tendstoI)
- fix S assume "open S" "c \<in> S"
- from open_orderD[OF this] obtain T where "open_interval T" "c \<in> T" "T \<subseteq> S" by auto
- with lim[THEN topological_tendstoD, of T]
- have "eventually (\<lambda>x. f x \<in> T) net" "eventually (\<lambda>x. h x \<in> T) net"
- by (auto dest: open_interval_imp_open)
- with ev have "eventually (\<lambda>x. g x \<in> T) net"
- by eventually_elim (insert `open_interval T`, auto dest: open_intervalD)
- with `T \<subseteq> S` show "eventually (\<lambda>x. g x \<in> S) net"
- by (auto elim: eventually_elim1)
+proof (rule order_tendstoI)
+ fix a show "a < c \<Longrightarrow> eventually (\<lambda>x. a < g x) net"
+ using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2)
+next
+ fix a show "c < a \<Longrightarrow> eventually (\<lambda>x. g x < a) net"
+ using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
qed
lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
@@ -1129,15 +1132,12 @@
shows "y \<le> x"
proof (rule ccontr)
assume "\<not> y \<le> x"
- then have "x < y" by simp
- from less_separate[OF this] obtain a b where xy: "x \<in> {..<a}" "y \<in> {b <..}" "{..<a} \<inter> {b<..} = {}"
- by auto
- then have less: "\<And>x y. x < a \<Longrightarrow> b < y \<Longrightarrow> x < y"
- by auto
- from x[THEN topological_tendstoD, of "{..<a}"] y[THEN topological_tendstoD, of "{b <..}"] xy
- have "eventually (\<lambda>x. f x \<in> {..<a}) F" "eventually (\<lambda>x. g x \<in> {b <..}) F" by auto
+ with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} \<inter> {b<..} = {}"
+ by (auto simp: not_le)
+ then have "eventually (\<lambda>x. f x < a) F" "eventually (\<lambda>x. b < g x) F"
+ using x y by (auto intro: order_tendstoD)
with ev have "eventually (\<lambda>x. False) F"
- by eventually_elim (auto dest!: less)
+ by eventually_elim (insert xy, fastforce)
with F show False
by (simp add: eventually_False)
qed
--- a/src/HOL/RealVector.thy Wed Feb 06 17:18:01 2013 +0100
+++ b/src/HOL/RealVector.thy Wed Feb 06 17:57:21 2013 +0100
@@ -559,60 +559,6 @@
by (simp add: closed_Int)
qed
-inductive open_interval :: "'a::order set \<Rightarrow> bool" where
- empty[intro]: "open_interval {}" |
- UNIV[intro]: "open_interval UNIV" |
- greaterThan[intro]: "open_interval {a <..}" |
- lessThan[intro]: "open_interval {..< b}" |
- greaterThanLessThan[intro]: "open_interval {a <..< b}"
-hide_fact (open) empty UNIV greaterThan lessThan greaterThanLessThan
-
-lemma open_intervalD:
- "open_interval S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> S"
- by (cases rule: open_interval.cases) auto
-
-lemma open_interval_Int[intro]:
- fixes S T :: "'a :: linorder set"
- assumes S: "open_interval S" and T: "open_interval T"
- shows "open_interval (S \<inter> T)"
-proof -
- { fix a b :: 'a have "{..<b} \<inter> {a<..} = { a <..} \<inter> {..< b }" by auto } note this[simp]
- { fix a b :: 'a and A have "{a <..} \<inter> ({b <..} \<inter> A) = {max a b <..} \<inter> A" by auto } note this[simp]
- { fix a b :: 'a and A have "{..<b} \<inter> (A \<inter> {..<a}) = A \<inter> {..<min a b}" by auto } note this[simp]
- { fix a b :: 'a have "open_interval ({ a <..} \<inter> {..< b})"
- unfolding greaterThanLessThan_eq[symmetric] by auto } note this[simp]
- show ?thesis
- by (cases rule: open_interval.cases[OF S, case_product open_interval.cases[OF T]])
- (auto simp: greaterThanLessThan_eq lessThan_Int_lessThan greaterThan_Int_greaterThan Int_assoc)
-qed
-
-lemma open_interval_imp_open: "open_interval S \<Longrightarrow> open (S::'a::order_topology set)"
- by (cases S rule: open_interval.cases) auto
-
-lemma open_orderD:
- "open (S::'a::linorder_topology set) \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>T. open_interval T \<and> T \<subseteq> S \<and> x \<in> T"
- unfolding open_generated_order
-proof (induct rule: generate_topology.induct)
- case (UN K) then obtain k where "k \<in> K" "x \<in> k" by auto
- with UN(2)[of k] show ?case by auto
-qed auto
-
-lemma open_order_induct[consumes 2, case_names subset UNIV lessThan greaterThan greaterThanLessThan]:
- fixes S :: "'a::linorder_topology set"
- assumes S: "open S" "x \<in> S"
- assumes subset: "\<And>S T. P S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> P T"
- assumes univ: "P UNIV"
- assumes lt: "\<And>a. x < a \<Longrightarrow> P {..< a}"
- assumes gt: "\<And>a. a < x \<Longrightarrow> P {a <..}"
- assumes lgt: "\<And>a b. a < x \<Longrightarrow> x < b \<Longrightarrow> P {a <..< b}"
- shows "P S"
-proof -
- from open_orderD[OF S] obtain T where "open_interval T" "T \<subseteq> S" "x \<in> T"
- by auto
- then show "P S"
- by induct (auto intro: univ subset lt gt lgt)
-qed
-
subsection {* Metric spaces *}
class dist =