# HG changeset patch
# User huffman
# Date 1259562467 28800
# Node ID 9095ba4d2cd49dc41a3dc79399e72a17d32549cb
# Parent  d397496894c4a3d5469a6cb4ad10d197cd6c0d04
make proof use only abstract properties of eventually

diff -r d397496894c4 -r 9095ba4d2cd4 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Dec 16 15:10:08 2009 -0800
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Nov 29 22:27:47 2009 -0800
@@ -208,13 +208,14 @@
     have *:"\<And>x. x - vec 0 = (x::real^'n)" by auto 
     have **:"\<And>d x. d * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k)) = (d *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net) ))) $k" by(auto simp add:field_simps)
     fix e assume "\<not> trivial_limit net" "0 < (e::real)"
-    then obtain A where A:"A\<in>Rep_net net" "\<forall>x\<in>A. dist ((1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net)))) 0 < e"
-      using assms[unfolded has_derivative_def Lim] unfolding eventually_def by auto
-    show "eventually (\<lambda>x. dist (1 / norm (x - netlimit net) * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k))) 0 < e) net"
-      unfolding eventually_def apply(rule_tac x=A in bexI) apply rule proof-
-      case goal1 thus ?case apply -apply(drule A(2)[rule_format]) unfolding vector_dist_norm vec1_vec apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1[unfolded vec1_vec]
-	using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto
-      qed(insert A, auto) qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed 
+    then have "eventually (\<lambda>x. dist ((1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net)))) 0 < e) net"
+      using assms[unfolded has_derivative_def Lim] by auto
+    thus "eventually (\<lambda>x. dist (1 / norm (x - netlimit net) * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k))) 0 < e) net"
+      proof (rule eventually_elim1)
+      case goal1 thus ?case apply - unfolding vector_dist_norm vec1_vec apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1[unfolded vec1_vec]
+        using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto
+      qed
+      qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed 
 
 lemma has_derivative_vmul_within: fixes c::"real \<Rightarrow> real" and v::"real^'a::finite"
   assumes "(c has_derivative c') (at x within s)"