1.1 --- a/src/HOL/Limits.thy Mon Mar 12 21:28:10 2012 +0100
1.2 +++ b/src/HOL/Limits.thy Mon Mar 12 21:34:43 2012 +0100
1.3 @@ -449,14 +449,12 @@
1.4 then have "eventually (\<lambda>x. norm (f x) < r / K) F"
1.5 using ZfunD [OF f] by fast
1.6 with g show "eventually (\<lambda>x. norm (g x) < r) F"
1.7 - proof (rule eventually_elim2)
1.8 - fix x
1.9 - assume *: "norm (g x) \<le> norm (f x) * K"
1.10 - assume "norm (f x) < r / K"
1.11 + proof eventually_elim
1.12 + case (elim x)
1.13 hence "norm (f x) * K < r"
1.14 by (simp add: pos_less_divide_eq K)
1.15 - thus "norm (g x) < r"
1.16 - by (simp add: order_le_less_trans [OF *])
1.17 + thus ?case
1.18 + by (simp add: order_le_less_trans [OF elim(1)])
1.19 qed
1.20 qed
1.21 next
1.22 @@ -467,12 +465,11 @@
1.23 fix r :: real
1.24 assume "0 < r"
1.25 from g show "eventually (\<lambda>x. norm (g x) < r) F"
1.26 - proof (rule eventually_elim1)
1.27 - fix x
1.28 - assume "norm (g x) \<le> norm (f x) * K"
1.29 - also have "\<dots> \<le> norm (f x) * 0"
1.30 + proof eventually_elim
1.31 + case (elim x)
1.32 + also have "norm (f x) * K \<le> norm (f x) * 0"
1.33 using K norm_ge_zero by (rule mult_left_mono)
1.34 - finally show "norm (g x) < r"
1.35 + finally show ?case
1.36 using `0 < r` by simp
1.37 qed
1.38 qed
1.39 @@ -494,14 +491,13 @@
1.40 using g r by (rule ZfunD)
1.41 ultimately
1.42 show "eventually (\<lambda>x. norm (f x + g x) < r) F"
1.43 - proof (rule eventually_elim2)
1.44 - fix x
1.45 - assume *: "norm (f x) < r/2" "norm (g x) < r/2"
1.46 + proof eventually_elim
1.47 + case (elim x)
1.48 have "norm (f x + g x) \<le> norm (f x) + norm (g x)"
1.49 by (rule norm_triangle_ineq)
1.50 also have "\<dots> < r/2 + r/2"
1.51 - using * by (rule add_strict_mono)
1.52 - finally show "norm (f x + g x) < r"
1.53 + using elim by (rule add_strict_mono)
1.54 + finally show ?case
1.55 by simp
1.56 qed
1.57 qed
1.58 @@ -542,16 +538,15 @@
1.59 using g K' by (rule ZfunD)
1.60 ultimately
1.61 show "eventually (\<lambda>x. norm (f x ** g x) < r) F"
1.62 - proof (rule eventually_elim2)
1.63 - fix x
1.64 - assume *: "norm (f x) < r" "norm (g x) < inverse K"
1.65 + proof eventually_elim
1.66 + case (elim x)
1.67 have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K"
1.68 by (rule norm_le)
1.69 also have "norm (f x) * norm (g x) * K < r * inverse K * K"
1.70 - by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero * K)
1.71 + by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K)
1.72 also from K have "r * inverse K * K = r"
1.73 by simp
1.74 - finally show "norm (f x ** g x) < r" .
1.75 + finally show ?case .
1.76 qed
1.77 qed
1.78
1.79 @@ -655,11 +650,10 @@
1.80 using `(f ---> b) F` `open V` `b \<in> V` by (rule topological_tendstoD)
1.81 ultimately
1.82 have "eventually (\<lambda>x. False) F"
1.83 - proof (rule eventually_elim2)
1.84 - fix x
1.85 - assume "f x \<in> U" "f x \<in> V"
1.86 + proof eventually_elim
1.87 + case (elim x)
1.88 hence "f x \<in> U \<inter> V" by simp
1.89 - with `U \<inter> V = {}` show "False" by simp
1.90 + with `U \<inter> V = {}` show ?case by simp
1.91 qed
1.92 with `\<not> trivial_limit F` show "False"
1.93 by (simp add: trivial_limit_def)
1.94 @@ -732,8 +726,8 @@
1.95 hence e2: "0 < e/2" by simp
1.96 from tendstoD [OF f e2] tendstoD [OF g e2]
1.97 show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) F"
1.98 - proof (rule eventually_elim2)
1.99 - fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2"
1.100 + proof (eventually_elim)
1.101 + case (elim x)
1.102 then show "dist (dist (f x) (g x)) (dist l m) < e"
1.103 unfolding dist_real_def
1.104 using dist_triangle2 [of "f x" "g x" "l"]
1.105 @@ -912,14 +906,13 @@
1.106 and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) F"
1.107 using g by (rule BfunE)
1.108 have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) F"
1.109 - using norm_g proof (rule eventually_elim1)
1.110 - fix x
1.111 - assume *: "norm (g x) \<le> B"
1.112 + using norm_g proof eventually_elim
1.113 + case (elim x)
1.114 have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K"
1.115 by (rule norm_le)
1.116 also have "\<dots> \<le> norm (f x) * B * K"
1.117 by (intro mult_mono' order_refl norm_g norm_ge_zero
1.118 - mult_nonneg_nonneg K *)
1.119 + mult_nonneg_nonneg K elim)
1.120 also have "\<dots> = norm (f x) * (B * K)"
1.121 by (rule mult_assoc)
1.122 finally show "norm (f x ** g x) \<le> norm (f x) * (B * K)" .
1.123 @@ -963,9 +956,8 @@
1.124 have "eventually (\<lambda>x. dist (f x) a < r) F"
1.125 using tendstoD [OF f r1] by fast
1.126 hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) F"
1.127 - proof (rule eventually_elim1)
1.128 - fix x
1.129 - assume "dist (f x) a < r"
1.130 + proof eventually_elim
1.131 + case (elim x)
1.132 hence 1: "norm (f x - a) < r"
1.133 by (simp add: dist_norm)
1.134 hence 2: "f x \<noteq> 0" using r2 by auto
2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 12 21:28:10 2012 +0100
2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 12 21:34:43 2012 +0100
2.3 @@ -3175,8 +3175,8 @@
2.4 have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
2.5 using x(2) `d>0` by simp
2.6 hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
2.7 - proof (rule eventually_elim1)
2.8 - fix n assume "dist (x n) a < d" thus "(f \<circ> x) n \<in> T"
2.9 + proof eventually_elim
2.10 + case (elim n) thus ?case
2.11 using d x(1) `f a \<in> T` unfolding dist_nz[THEN sym] by auto
2.12 qed
2.13 }