--- a/src/HOL/Library/Topology_Euclidean_Space.thy Tue Jun 02 17:03:22 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Tue Jun 02 17:20:20 2009 -0700
@@ -991,65 +991,18 @@
using frontier_complement frontier_subset_eq[of "UNIV - S"]
unfolding open_closed by auto
-subsection{* A variant of nets (Slightly non-standard but good for our purposes). *}
-
-typedef (open) 'a net =
- "{net :: 'a set set. (\<exists>A. A \<in> net)
- \<and> (\<forall>A\<in>net. \<forall>B\<in>net. \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B)}"
-proof
- show "UNIV \<in> ?net" by auto
-qed
-
-lemma Rep_net_nonempty: "\<exists>A. A \<in> Rep_net net"
-using Rep_net [of net] by simp
-
-lemma Rep_net_directed:
- "A \<in> Rep_net net \<Longrightarrow> B \<in> Rep_net net \<Longrightarrow> \<exists>C\<in>Rep_net net. C \<subseteq> A \<and> C \<subseteq> B"
-using Rep_net [of net] by simp
-
-
subsection{* Common nets and The "within" modifier for nets. *}
definition
- at :: "'a::metric_space \<Rightarrow> 'a net" where
- "at a = Abs_net ((\<lambda>r. {x. 0 < dist x a \<and> dist x a < r}) ` {r. 0 < r})"
-
-definition
at_infinity :: "'a::real_normed_vector net" where
"at_infinity = Abs_net (range (\<lambda>r. {x. r \<le> norm x}))"
definition
- sequentially :: "nat net" where
- "sequentially = Abs_net (range (\<lambda>n. {n..}))"
-
-definition
- within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
- "net within S = Abs_net ((\<lambda>A. A \<inter> S) ` Rep_net net)"
-
-definition
indirection :: "real ^'n::finite \<Rightarrow> real ^'n \<Rightarrow> (real ^'n) net" (infixr "indirection" 70) where
"a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = c*s v}"
text{* Prove That They are all nets. *}
-lemma Abs_net_inverse':
- assumes "\<exists>A. A \<in> net"
- assumes "\<And>A B. A \<in> net \<Longrightarrow> B \<in> net \<Longrightarrow> \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B"
- shows "Rep_net (Abs_net net) = net"
-using assms by (simp add: Abs_net_inverse)
-
-lemma image_nonempty: "\<exists>x. x \<in> A \<Longrightarrow> \<exists>x. x \<in> f ` A"
-by auto
-
-lemma Rep_net_at:
- "Rep_net (at a) = ((\<lambda>r. {x. 0 < dist x a \<and> dist x a < r}) ` {r. 0 < r})"
-unfolding at_def
-apply (rule Abs_net_inverse')
-apply (rule image_nonempty, rule_tac x=1 in exI, simp)
-apply (clarsimp, rename_tac r s)
-apply (rule_tac x="min r s" in exI, auto)
-done
-
lemma Rep_net_at_infinity:
"Rep_net at_infinity = range (\<lambda>r. {x. r \<le> norm x})"
unfolding at_infinity_def
@@ -1059,25 +1012,6 @@
apply (rule_tac x="max r s" in exI, auto)
done
-lemma Rep_net_sequentially:
- "Rep_net sequentially = range (\<lambda>n. {n..})"
-unfolding sequentially_def
-apply (rule Abs_net_inverse')
-apply (rule image_nonempty, simp)
-apply (clarsimp, rename_tac m n)
-apply (rule_tac x="max m n" in exI, auto)
-done
-
-lemma Rep_net_within:
- "Rep_net (net within S) = (\<lambda>A. A \<inter> S) ` Rep_net net"
-unfolding within_def
-apply (rule Abs_net_inverse')
-apply (rule image_nonempty, rule Rep_net_nonempty)
-apply (clarsimp, rename_tac A B)
-apply (drule (1) Rep_net_directed)
-apply (clarify, rule_tac x=C in bexI, auto)
-done
-
lemma within_UNIV: "net within UNIV = net"
by (simp add: Rep_net_inject [symmetric] Rep_net_within)
@@ -1135,29 +1069,17 @@
subsection{* Some property holds "sufficiently close" to the limit point. *}
-definition
- eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
- "eventually P net \<longleftrightarrow> (\<exists>A\<in>Rep_net net. \<forall>x\<in>A. P x)"
-
lemma eventually_at:
"eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding eventually_def Rep_net_at by auto
+unfolding eventually_def Rep_net_at dist_nz by auto
lemma eventually_at_infinity:
"eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
unfolding eventually_def Rep_net_at_infinity by auto
-lemma eventually_sequentially:
- "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
-unfolding eventually_def Rep_net_sequentially by auto
-
-lemma eventually_within_eq:
- "eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net"
-unfolding eventually_def Rep_net_within by auto
-
lemma eventually_within: "eventually P (at a within S) \<longleftrightarrow>
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding eventually_within_eq eventually_at by auto
+unfolding eventually_within eventually_at dist_nz by auto
lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow>
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs")
@@ -1175,9 +1097,6 @@
unfolding eventually_def trivial_limit_def
using Rep_net_nonempty [of net] by auto
-lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
- by (simp add: always_eventually)
-
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
unfolding trivial_limit_def eventually_def by auto
@@ -1194,14 +1113,7 @@
lemma eventually_conjI:
"\<lbrakk>eventually (\<lambda>x. P x) net; eventually (\<lambda>x. Q x) net\<rbrakk>
\<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) net"
-unfolding eventually_def
-apply (clarify, rename_tac A B)
-apply (drule (1) Rep_net_directed, clarify)
-apply (rule_tac x=C in bexI, auto)
-done
-
-lemma eventually_mono: "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net"
- by (metis eventually_def)
+by (rule eventually_conj)
lemma eventually_rev_mono:
"eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"
@@ -1210,30 +1122,15 @@
lemma eventually_and: " eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net"
by (auto intro!: eventually_conjI elim: eventually_rev_mono)
-lemma eventually_mp: "eventually (\<lambda>x. P x \<longrightarrow> Q x) net \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net"
- apply (atomize(full))
- unfolding imp_conjL[symmetric] eventually_and[symmetric]
- by (auto simp add: eventually_def)
-
lemma eventually_false: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
by (auto simp add: eventually_False)
lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)"
by (simp add: eventually_False)
-lemma eventually_rev_mp:
- assumes 1: "eventually (\<lambda>x. P x) net"
- assumes 2: "eventually (\<lambda>x. P x \<longrightarrow> Q x) net"
- shows "eventually (\<lambda>x. Q x) net"
-using 2 1 by (rule eventually_mp)
-
subsection{* Limits, defined as vacuously true when the limit is trivial. *}
-definition tendsto:: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "--->" 55) where
- tendsto_def: "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
-
-lemma tendstoD: "(f ---> l) net \<Longrightarrow> e>0 \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
- unfolding tendsto_def by auto
+notation tendsto (infixr "--->" 55)
text{* Notation Lim to avoid collition with lim defined in analysis *}
definition "Lim net f = (THE l. (f ---> l) net)"