src/HOL/Limits.thy
changeset 46887 cb891d9a23c1
parent 46886 4cd29473c65d
child 47432 e1576d13e933
     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