--- a/src/HOL/Library/ContNotDenum.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/ContNotDenum.thy Tue Apr 26 22:44:31 2016 +0200
@@ -41,9 +41,10 @@
by (auto simp add: not_le cong: conj_cong)
(metis dense le_less_linear less_linear less_trans order_refl)
then obtain i j where ij:
- "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
- "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
- "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
+ "a < b \<Longrightarrow> i a b c < j a b c"
+ "a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
+ "a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
+ for a b c :: real
by metis
define ivl where "ivl =
@@ -78,7 +79,7 @@
finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
by auto
qed (auto simp: I_def)
- then obtain x where "\<And>n. x \<in> I n"
+ then obtain x where "x \<in> I n" for n
by blast
moreover from \<open>surj f\<close> obtain j where "x = f j"
by blast
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Tue Apr 26 22:44:31 2016 +0200
@@ -1483,7 +1483,7 @@
case (real r)
then have "\<forall>x. \<exists>q\<ge>0. g x \<le> c \<longrightarrow> (g x = ennreal q \<and> q \<le> r)"
by (auto simp: le_ennreal_iff)
- then obtain f where *: "\<And>x. g x \<le> c \<Longrightarrow> 0 \<le> f x" "\<And>x. g x \<le> c \<Longrightarrow> g x = ennreal (f x)" "\<And>x. g x \<le> c \<Longrightarrow> f x \<le> r"
+ then obtain f where *: "0 \<le> f x" "g x = ennreal (f x)" "f x \<le> r" if "g x \<le> c" for x
by metis
from ae have ae2: "\<forall>\<^sub>F x in F. c - g x = ennreal (r - f x) \<and> f x \<le> r \<and> g x = ennreal (f x) \<and> 0 \<le> f x"
proof eventually_elim
--- a/src/HOL/Library/Extended_Real.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Tue Apr 26 22:44:31 2016 +0200
@@ -1696,7 +1696,7 @@
shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
proof (cases "\<exists>x. \<forall>a\<in>S. a \<le> ereal x")
case True
- then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y"
+ then obtain y where y: "a \<le> ereal y" if "a\<in>S" for a
by auto
then have "\<infinity> \<notin> S"
by force
@@ -1705,7 +1705,7 @@
case True
with \<open>\<infinity> \<notin> S\<close> obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
by auto
- obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "\<And>z. (\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z"
+ obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "(\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z" for z
proof (atomize_elim, rule complete_real)
show "\<exists>x. x \<in> ereal -` S"
using x by auto
@@ -1919,7 +1919,7 @@
assumes *: "bdd_below A" "A \<noteq> {}"
shows "ereal (Inf A) = (INF a:A. ereal a)"
proof (rule ereal_Inf)
- from * obtain l u where "\<And>x. x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A"
+ from * obtain l u where "x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A" for x
by (auto simp: bdd_below_def)
then have "l \<le> (INF x:A. ereal x)" "(INF x:A. ereal x) \<le> u"
by (auto intro!: INF_greatest INF_lower)
@@ -2193,7 +2193,7 @@
by (auto intro!: exI[of _ "\<lambda>_. -\<infinity>"] simp: bot_ereal_def)
next
assume "Sup A \<noteq> -\<infinity>"
- then obtain l where "incseq l" and l: "\<And>i::nat. l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A"
+ then obtain l where "incseq l" and l: "l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A" for i :: nat
by (auto dest: countable_approach)
have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))"
@@ -2456,7 +2456,7 @@
from \<open>open S\<close>
have "open (ereal -` S)"
by (rule ereal_openE)
- then obtain e where "e > 0" and e: "\<And>y. dist y (real_of_ereal x) < e \<Longrightarrow> ereal y \<in> S"
+ then obtain e where "e > 0" and e: "dist y (real_of_ereal x) < e \<Longrightarrow> ereal y \<in> S" for y
using assms unfolding open_dist by force
show thesis
proof (intro that subsetI)
@@ -2830,11 +2830,12 @@
assume "open S" and "x \<in> S"
then have "open (ereal -` S)"
unfolding open_ereal_def by auto
- with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
+ with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "dist y rx < r \<Longrightarrow> ereal y \<in> S" for y
unfolding open_dist rx by auto
- then obtain n where
- upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
- lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
+ then obtain n
+ where upper: "u N < x + ereal r"
+ and lower: "x < u N + ereal r"
+ if "n \<le> N" for N
using assms(2)[of "ereal r"] by auto
show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"
proof (safe intro!: exI[of _ n])
--- a/src/HOL/Library/Fun_Lexorder.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Fun_Lexorder.thy Tue Apr 26 22:44:31 2016 +0200
@@ -24,9 +24,9 @@
assumes "less_fun f g"
shows "\<not> less_fun g f"
proof
- from assms obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
+ from assms obtain k1 where k1: "f k1 < g k1" "k' < k1 \<Longrightarrow> f k' = g k'" for k'
by (blast elim!: less_funE)
- assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = f k'"
+ assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "k' < k2 \<Longrightarrow> g k' = f k'" for k'
by (blast elim!: less_funE)
show False proof (cases k1 k2 rule: linorder_cases)
case equal with k1 k2 show False by simp
@@ -52,9 +52,9 @@
assumes "less_fun f g" and "less_fun g h"
shows "less_fun f h"
proof (rule less_funI)
- from \<open>less_fun f g\<close> obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
- by (blast elim!: less_funE)
- from \<open>less_fun g h\<close> obtain k2 where k2: "g k2 < h k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = h k'"
+ from \<open>less_fun f g\<close> obtain k1 where k1: "f k1 < g k1" "k' < k1 \<Longrightarrow> f k' = g k'" for k'
+ by (blast elim!: less_funE)
+ from \<open>less_fun g h\<close> obtain k2 where k2: "g k2 < h k2" "k' < k2 \<Longrightarrow> g k' = h k'" for k'
by (blast elim!: less_funE)
show "\<exists>k. f k < h k \<and> (\<forall>k'<k. f k' = h k')"
proof (cases k1 k2 rule: linorder_cases)
--- a/src/HOL/Library/FuncSet.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/FuncSet.thy Tue Apr 26 22:44:31 2016 +0200
@@ -96,9 +96,9 @@
assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i"
by auto
- from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)"
+ from bchoice[OF this] obtain n where n: "f i \<in> A (n i) i" if "i \<in> I" for i
by auto
- obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
+ obtain k where k: "n i \<le> k" if "i \<in> I" for i
using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto
have "f \<in> Pi I (A k)"
proof (intro Pi_I)
--- a/src/HOL/Library/Function_Growth.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Function_Growth.thy Tue Apr 26 22:44:31 2016 +0200
@@ -163,7 +163,7 @@
and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
proof -
from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
- from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
+ from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "m > n \<Longrightarrow> f m \<le> c * g m" for m
by (rule less_eq_funE) blast
{ fix c n :: nat
assume "c > 0"
@@ -202,8 +202,8 @@
shows "f \<prec> g"
proof (rule less_funI)
have "1 > (0::nat)" by simp
- from assms \<open>1 > 0\<close> have "\<exists>n. \<forall>m>n. 1 * f m < g m" .
- then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" by blast
+ with assms [OF this] obtain n where *: "m > n \<Longrightarrow> 1 * f m < g m" for m
+ by blast
have "\<forall>m>n. f m \<le> 1 * g m"
proof (rule allI, rule impI)
fix m
@@ -214,7 +214,7 @@
with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
fix c n :: nat
assume "c > 0"
- with assms obtain q where "\<And>m. m > q \<Longrightarrow> c * f m < g m" by blast
+ with assms obtain q where "m > q \<Longrightarrow> c * f m < g m" for m by blast
then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
moreover have "Suc (q + n) > n" by simp
ultimately show "\<exists>m>n. c * f m < g m" by blast
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Apr 26 22:44:31 2016 +0200
@@ -312,7 +312,7 @@
assumes ep: "e > 0"
shows "\<exists>d >0. \<forall>w. 0 < norm (w - z) \<and> norm (w - z) < d \<longrightarrow> norm (poly p w - poly p z) < e"
proof -
- obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
+ obtain q where q: "degree q = degree p" "poly q x = poly p (z + x)" for x
proof
show "degree (offset_poly p z) = degree p"
by (rule degree_offset_poly)
@@ -329,7 +329,7 @@
next
case (pCons c cs)
from poly_bound_exists[of 1 "cs"]
- obtain m where m: "m > 0" "\<And>z. norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m"
+ obtain m where m: "m > 0" "norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m" for z
by blast
from ep m(1) have em0: "e/m > 0"
by (simp add: field_simps)
@@ -535,12 +535,14 @@
proof (cases "cs = 0")
case False
from poly_infinity[OF False, of "cmod (poly (pCons c cs) 0)" c]
- obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
+ obtain r where r: "cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
+ if "r \<le> cmod z" for z
by blast
have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>"
by arith
from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
- obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
+ obtain v where v: "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
+ if "cmod w \<le> \<bar>r\<bar>" for w
by blast
have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)" if z: "r \<le> cmod z" for z
using v[of 0] r[OF z] by simp
--- a/src/HOL/Library/Multiset.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Apr 26 22:44:31 2016 +0200
@@ -2075,7 +2075,7 @@
"a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
proof -
from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K"
- "\<And>b. b \<in># K \<Longrightarrow> b < a" by (blast elim: mult1E)
+ "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
moreover from this(3) [of a] have "a \<notin># K" by auto
ultimately show thesis by (auto intro: that)
qed
--- a/src/HOL/Library/Polynomial.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy Tue Apr 26 22:44:31 2016 +0200
@@ -3353,7 +3353,7 @@
fix p assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
define cs where "cs = coeffs p"
from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'" unfolding Rats_def by blast
- then obtain f where f: "\<And>i. coeff p i = of_rat (f (coeff p i))"
+ then obtain f where f: "coeff p i = of_rat (f (coeff p i))" for i
by (subst (asm) bchoice_iff) blast
define cs' where "cs' = map (quotient_of \<circ> f) (coeffs p)"
define d where "d = Lcm (set (map snd cs'))"
@@ -3392,9 +3392,8 @@
moreover from root have "poly p' x = 0" by (simp add: p'_def)
ultimately show "algebraic x" unfolding algebraic_def by blast
next
-
assume "algebraic x"
- then obtain p where p: "\<And>i. coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0"
+ then obtain p where p: "coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" for i
by (force simp: algebraic_def)
moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i by (elim Ints_cases) simp
ultimately show "(\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)" by auto
--- a/src/HOL/Library/Ramsey.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Library/Ramsey.thy Tue Apr 26 22:44:31 2016 +0200
@@ -231,8 +231,8 @@
qed
qed
from dependent_choice [OF transr propr0 proprstep]
- obtain g where pg: "!!n::nat. ?propr (g n)"
- and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
+ obtain g where pg: "?propr (g n)" and rg: "n<m ==> (g n, g m) \<in> ?ramr" for n m :: nat
+ by blast
let ?gy = "fst o g"
let ?gt = "snd o snd o g"
have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
--- a/src/HOL/Number_Theory/Factorial_Ring.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy Tue Apr 26 22:44:31 2016 +0200
@@ -609,12 +609,13 @@
next
case False then have "a \<noteq> 0" and "b \<noteq> 0" and "c \<noteq> 0"
by simp_all
- then obtain A B C where fact:
- "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
+ then obtain A B C
+ where fact: "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
and norm: "normalize a = msetprod A" "normalize b = msetprod B" "normalize c = msetprod C"
- and A: "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
- and B: "0 \<notin># B" "\<And>p. p \<in># B \<Longrightarrow> normalize p = p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
- and C: "0 \<notin># C" "\<And>p. p \<in># C \<Longrightarrow> normalize p = p" "\<And>p. p \<in># C \<Longrightarrow> is_prime p"
+ and A: "0 \<notin># A" "p \<in># A \<Longrightarrow> normalize p = p" "p \<in># A \<Longrightarrow> is_prime p"
+ and B: "0 \<notin># B" "p \<in># B \<Longrightarrow> normalize p = p" "p \<in># B \<Longrightarrow> is_prime p"
+ and C: "0 \<notin># C" "p \<in># C \<Longrightarrow> normalize p = p" "p \<in># C \<Longrightarrow> is_prime p"
+ for p
by (blast elim!: factorizationE)
moreover from that have "normalize c dvd normalize a" and "normalize c dvd normalize b"
by simp_all
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Apr 26 22:44:31 2016 +0200
@@ -40,9 +40,9 @@
by (rule types_snocE)
from snoc have "listall ?R bs" by simp
with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
- then obtain bs' where
- bsred: "\<And>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
- and bsNF: "\<And>j. NF (Var j \<degree>\<degree> map f bs')" by iprover
+ then obtain bs' where bsred: "Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
+ and bsNF: "NF (Var j \<degree>\<degree> map f bs')" for j
+ by iprover
from snoc have "?R b" by simp
with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'"
by iprover
--- a/src/HOL/ex/Gauge_Integration.thy Tue Apr 26 22:39:17 2016 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy Tue Apr 26 22:44:31 2016 +0200
@@ -133,7 +133,7 @@
proof (cases "b < x")
case True
with 2 obtain N where *: "N < length D"
- and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
+ and **: "D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" for d t e by auto
hence "Suc N < length ((a,t,b)#D) \<and>
(\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
thus ?thesis by auto
@@ -372,11 +372,11 @@
hence "a < b" and "b < c" by auto
obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
- and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)"
+ and I1: "fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" for D
using IntegralE [OF \<open>Integral (a, b) f x1\<close> \<open>0 < \<epsilon>/2\<close>] by auto
obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
- and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)"
+ and I2: "fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" for D
using IntegralE [OF \<open>Integral (b, c) f x2\<close> \<open>0 < \<epsilon>/2\<close>] by auto
define \<delta> where "\<delta> x =
@@ -541,7 +541,7 @@
then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
by (simp add: DERIV_iff2 LIM_eq)
with \<open>0 < e\<close> obtain s
- where "\<And>z. z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
+ where "z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s" for z
by (drule_tac x="e/2" in spec, auto)
with strad1 [of x s f f' e] have strad:
"\<And>z. \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
@@ -586,8 +586,8 @@
from lemma_straddle [OF f' this]
obtain \<delta> where "gauge {a..b} \<delta>"
- and \<delta>: "\<And>x u v. \<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
- \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" by auto
+ and \<delta>: "\<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
+ \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" for x u v by auto
have "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e"
proof (clarify)