# HG changeset patch
# User huffman
# Date 1243794439 25200
# Node ID 738eb25e1dd80bf285ff44a649fb981ac82246b9
# Parent  357d58c5743a7c6bd6a58ee1b0f9fbea49317dfa
more abstract properties of eventually

diff -r 357d58c5743a -r 738eb25e1dd8 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sun May 31 10:59:46 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sun May 31 11:27:19 2009 -0700
@@ -1196,6 +1196,12 @@
 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 eventually_def by simp
+
+lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
+  unfolding eventually_def trivial_limit_def by auto
+
 text{* Combining theorems for "eventually" *}
 
 lemma eventually_and: " eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net"
@@ -1246,9 +1252,8 @@
 lemma Lim:
  "(f ---> l) net \<longleftrightarrow>
         trivial_limit net \<or>
-        (\<forall>e>0. \<exists>y. (\<exists>x. netord net x y) \<and>
-                           (\<forall>x. netord(net) x y \<longrightarrow> dist (f x) l < e))"
-  by (auto simp add: tendsto_def eventually_def)
+        (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+  unfolding tendsto_def trivial_limit_eq by auto
 
 
 text{* Show that they yield usual definitions in the various cases. *}
@@ -1281,7 +1286,7 @@
   unfolding Lim_sequentially LIMSEQ_def ..
 
 lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
-  by (auto simp add: eventually_def Lim)
+  unfolding tendsto_def by (auto elim: eventually_rev_mono)
 
 text{* The expected monotonicity property. *}
 
@@ -1462,11 +1467,12 @@
 
 lemma Lim_component: "(f ---> l) net
                       ==> ((\<lambda>a. vec1((f a :: real ^'n::finite)$i)) ---> vec1(l$i)) net"
-  apply (simp add: Lim dist_norm vec1_sub[symmetric] norm_vec1  vector_minus_component[symmetric] del: vector_minus_component)
+  unfolding tendsto_def
+  apply (simp add: dist_norm vec1_sub[symmetric] norm_vec1  vector_minus_component[symmetric] del: vector_minus_component)
   apply (auto simp del: vector_minus_component)
   apply (erule_tac x=e in allE)
   apply clarify
-  apply (rule_tac x=y in exI)
+  apply (erule eventually_rev_mono)
   apply (auto simp del: vector_minus_component)
   apply (rule order_le_less_trans)
   apply (rule component_le_norm)
@@ -3052,14 +3058,13 @@
 
 lemma continuous_trivial_limit:
  "trivial_limit net ==> continuous net f"
-  unfolding continuous_def tendsto_def eventually_def by auto
+  unfolding continuous_def tendsto_def trivial_limit_eq by auto
 
 lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f(x)) (at x within s)"
   unfolding continuous_def
   unfolding tendsto_def
   using netlimit_within[of x s]
-  unfolding eventually_def
-  by (cases "trivial_limit (at x within s)") auto
+  by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
 
 lemma continuous_at: "continuous (at x) f \<longleftrightarrow> (f ---> f(x)) (at x)"
   using continuous_within [of x UNIV f] by (simp add: within_UNIV)
@@ -4179,12 +4184,8 @@
   fixes f :: "real ^ _ \<Rightarrow> real"
   assumes "continuous (at a within s) (vec1 o f)" "f a \<noteq> 0"
   shows "continuous (at a within s) (vec1 o inverse o f)"
-proof(cases "trivial_limit (at a within s)")
-  case True thus ?thesis unfolding continuous_def tendsto_def eventually_def by auto
-next
-  case False note cs = this
-  thus ?thesis using netlimit_within[OF cs] assms(2) continuous_inv[OF assms(1)] by auto
-qed
+  using assms unfolding continuous_within o_apply
+  by (rule Lim_inv)
 
 lemma continuous_at_inv:
   fixes f :: "real ^ _ \<Rightarrow> real"