--- a/NEWS Mon Mar 12 21:42:40 2012 +0100
+++ b/NEWS Mon Mar 12 22:11:10 2012 +0100
@@ -355,6 +355,9 @@
* Command 'try0':
- Renamed from 'try_methods'. INCOMPATIBILITY.
+* New "eventually_elim" method as a generalized variant of the
+ eventually_elim* rules. Supports structured proofs.
+
*** FOL ***
--- a/src/HOL/Limits.thy Mon Mar 12 21:42:40 2012 +0100
+++ b/src/HOL/Limits.thy Mon Mar 12 22:11:10 2012 +0100
@@ -111,6 +111,26 @@
then show ?thesis by (auto elim: eventually_elim2)
qed
+ML {*
+ fun ev_elim_tac ctxt thms thm = let
+ val thy = Proof_Context.theory_of ctxt
+ val mp_thms = thms RL [@{thm eventually_rev_mp}]
+ val raw_elim_thm =
+ (@{thm allI} RS @{thm always_eventually})
+ |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
+ |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
+ val cases_prop = prop_of (raw_elim_thm RS thm)
+ val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
+ in
+ CASES cases (rtac raw_elim_thm 1) thm
+ end
+
+ fun eventually_elim_setup name =
+ Method.setup name (Scan.succeed (fn ctxt => METHOD_CASES (ev_elim_tac ctxt)))
+ "elimination of eventually quantifiers"
+*}
+
+setup {* eventually_elim_setup @{binding "eventually_elim"} *}
subsection {* Finer-than relation *}
@@ -429,14 +449,12 @@
then have "eventually (\<lambda>x. norm (f x) < r / K) F"
using ZfunD [OF f] by fast
with g show "eventually (\<lambda>x. norm (g x) < r) F"
- proof (rule eventually_elim2)
- fix x
- assume *: "norm (g x) \<le> norm (f x) * K"
- assume "norm (f x) < r / K"
+ proof eventually_elim
+ case (elim x)
hence "norm (f x) * K < r"
by (simp add: pos_less_divide_eq K)
- thus "norm (g x) < r"
- by (simp add: order_le_less_trans [OF *])
+ thus ?case
+ by (simp add: order_le_less_trans [OF elim(1)])
qed
qed
next
@@ -447,12 +465,11 @@
fix r :: real
assume "0 < r"
from g show "eventually (\<lambda>x. norm (g x) < r) F"
- proof (rule eventually_elim1)
- fix x
- assume "norm (g x) \<le> norm (f x) * K"
- also have "\<dots> \<le> norm (f x) * 0"
+ proof eventually_elim
+ case (elim x)
+ also have "norm (f x) * K \<le> norm (f x) * 0"
using K norm_ge_zero by (rule mult_left_mono)
- finally show "norm (g x) < r"
+ finally show ?case
using `0 < r` by simp
qed
qed
@@ -474,14 +491,13 @@
using g r by (rule ZfunD)
ultimately
show "eventually (\<lambda>x. norm (f x + g x) < r) F"
- proof (rule eventually_elim2)
- fix x
- assume *: "norm (f x) < r/2" "norm (g x) < r/2"
+ proof eventually_elim
+ case (elim x)
have "norm (f x + g x) \<le> norm (f x) + norm (g x)"
by (rule norm_triangle_ineq)
also have "\<dots> < r/2 + r/2"
- using * by (rule add_strict_mono)
- finally show "norm (f x + g x) < r"
+ using elim by (rule add_strict_mono)
+ finally show ?case
by simp
qed
qed
@@ -522,16 +538,15 @@
using g K' by (rule ZfunD)
ultimately
show "eventually (\<lambda>x. norm (f x ** g x) < r) F"
- proof (rule eventually_elim2)
- fix x
- assume *: "norm (f x) < r" "norm (g x) < inverse K"
+ proof eventually_elim
+ case (elim x)
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K"
by (rule norm_le)
also have "norm (f x) * norm (g x) * K < r * inverse K * K"
- by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero * K)
+ by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K)
also from K have "r * inverse K * K = r"
by simp
- finally show "norm (f x ** g x) < r" .
+ finally show ?case .
qed
qed
@@ -635,11 +650,10 @@
using `(f ---> b) F` `open V` `b \<in> V` by (rule topological_tendstoD)
ultimately
have "eventually (\<lambda>x. False) F"
- proof (rule eventually_elim2)
- fix x
- assume "f x \<in> U" "f x \<in> V"
+ proof eventually_elim
+ case (elim x)
hence "f x \<in> U \<inter> V" by simp
- with `U \<inter> V = {}` show "False" by simp
+ with `U \<inter> V = {}` show ?case by simp
qed
with `\<not> trivial_limit F` show "False"
by (simp add: trivial_limit_def)
@@ -712,8 +726,8 @@
hence e2: "0 < e/2" by simp
from tendstoD [OF f e2] tendstoD [OF g e2]
show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) F"
- proof (rule eventually_elim2)
- fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2"
+ proof (eventually_elim)
+ case (elim x)
then show "dist (dist (f x) (g x)) (dist l m) < e"
unfolding dist_real_def
using dist_triangle2 [of "f x" "g x" "l"]
@@ -892,14 +906,13 @@
and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) F"
using g by (rule BfunE)
have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) F"
- using norm_g proof (rule eventually_elim1)
- fix x
- assume *: "norm (g x) \<le> B"
+ using norm_g proof eventually_elim
+ case (elim x)
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K"
by (rule norm_le)
also have "\<dots> \<le> norm (f x) * B * K"
by (intro mult_mono' order_refl norm_g norm_ge_zero
- mult_nonneg_nonneg K *)
+ mult_nonneg_nonneg K elim)
also have "\<dots> = norm (f x) * (B * K)"
by (rule mult_assoc)
finally show "norm (f x ** g x) \<le> norm (f x) * (B * K)" .
@@ -943,9 +956,8 @@
have "eventually (\<lambda>x. dist (f x) a < r) F"
using tendstoD [OF f r1] by fast
hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) F"
- proof (rule eventually_elim1)
- fix x
- assume "dist (f x) a < r"
+ proof eventually_elim
+ case (elim x)
hence 1: "norm (f x - a) < r"
by (simp add: dist_norm)
hence 2: "f x \<noteq> 0" using r2 by auto
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 12 21:42:40 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 12 22:11:10 2012 +0100
@@ -3175,8 +3175,8 @@
have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
using x(2) `d>0` by simp
hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
- proof (rule eventually_elim1)
- fix n assume "dist (x n) a < d" thus "(f \<circ> x) n \<in> T"
+ proof eventually_elim
+ case (elim n) thus ?case
using d x(1) `f a \<in> T` unfolding dist_nz[THEN sym] by auto
qed
}