# HG changeset patch
# User huffman
# Date 1243988420 25200
# Node ID b8570dead501523fd1d1c7f11a0914ef6ec91bb2
# Parent  69570155ddf8aa541bd4fbc7b7ef8d38af6ea04f
reuse definition of nets from Limits.thy

diff -r 69570155ddf8 -r b8570dead501 src/HOL/Library/Topology_Euclidean_Space.thy
--- 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)"