some uses of 'obtain' with structure statement;
authorwenzelm
Tue Apr 26 22:44:31 2016 +0200 (2016-04-26)
changeset 63060293ede07b775
parent 63059 3f577308551e
child 63061 21ebc2f5c571
some uses of 'obtain' with structure statement;
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Fun_Lexorder.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Function_Growth.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Ramsey.thy
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Proofs/Lambda/WeakNorm.thy
src/HOL/ex/Gauge_Integration.thy
     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Tue Apr 26 22:39:17 2016 +0200
     1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Tue Apr 26 22:44:31 2016 +0200
     1.3 @@ -41,9 +41,10 @@
     1.4      by (auto simp add: not_le cong: conj_cong)
     1.5         (metis dense le_less_linear less_linear less_trans order_refl)
     1.6    then obtain i j where ij:
     1.7 -    "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
     1.8 -    "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
     1.9 -    "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
    1.10 +      "a < b \<Longrightarrow> i a b c < j a b c"
    1.11 +      "a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
    1.12 +      "a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
    1.13 +    for a b c :: real
    1.14      by metis
    1.15  
    1.16    define ivl where "ivl =
    1.17 @@ -78,7 +79,7 @@
    1.18      finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
    1.19        by auto
    1.20    qed (auto simp: I_def)
    1.21 -  then obtain x where "\<And>n. x \<in> I n"
    1.22 +  then obtain x where "x \<in> I n" for n
    1.23      by blast
    1.24    moreover from \<open>surj f\<close> obtain j where "x = f j"
    1.25      by blast
     2.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Apr 26 22:39:17 2016 +0200
     2.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Apr 26 22:44:31 2016 +0200
     2.3 @@ -1483,7 +1483,7 @@
     2.4    case (real r)
     2.5    then have "\<forall>x. \<exists>q\<ge>0. g x \<le> c \<longrightarrow> (g x = ennreal q \<and> q \<le> r)"
     2.6      by (auto simp: le_ennreal_iff)
     2.7 -  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"
     2.8 +  then obtain f where *: "0 \<le> f x" "g x = ennreal (f x)" "f x \<le> r" if "g x \<le> c" for x
     2.9      by metis
    2.10    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"
    2.11    proof eventually_elim
     3.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Apr 26 22:39:17 2016 +0200
     3.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Apr 26 22:44:31 2016 +0200
     3.3 @@ -1696,7 +1696,7 @@
     3.4    shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
     3.5  proof (cases "\<exists>x. \<forall>a\<in>S. a \<le> ereal x")
     3.6    case True
     3.7 -  then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y"
     3.8 +  then obtain y where y: "a \<le> ereal y" if "a\<in>S" for a
     3.9      by auto
    3.10    then have "\<infinity> \<notin> S"
    3.11      by force
    3.12 @@ -1705,7 +1705,7 @@
    3.13      case True
    3.14      with \<open>\<infinity> \<notin> S\<close> obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
    3.15        by auto
    3.16 -    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"
    3.17 +    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
    3.18      proof (atomize_elim, rule complete_real)
    3.19        show "\<exists>x. x \<in> ereal -` S"
    3.20          using x by auto
    3.21 @@ -1919,7 +1919,7 @@
    3.22    assumes *: "bdd_below A" "A \<noteq> {}"
    3.23    shows "ereal (Inf A) = (INF a:A. ereal a)"
    3.24  proof (rule ereal_Inf)
    3.25 -  from * obtain l u where "\<And>x. x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A"
    3.26 +  from * obtain l u where "x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A" for x
    3.27      by (auto simp: bdd_below_def)
    3.28    then have "l \<le> (INF x:A. ereal x)" "(INF x:A. ereal x) \<le> u"
    3.29      by (auto intro!: INF_greatest INF_lower)
    3.30 @@ -2193,7 +2193,7 @@
    3.31      by (auto intro!: exI[of _ "\<lambda>_. -\<infinity>"] simp: bot_ereal_def)
    3.32  next
    3.33    assume "Sup A \<noteq> -\<infinity>"
    3.34 -  then obtain l where "incseq l" and l: "\<And>i::nat. l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A"
    3.35 +  then obtain l where "incseq l" and l: "l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A" for i :: nat
    3.36      by (auto dest: countable_approach)
    3.37  
    3.38    have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))"
    3.39 @@ -2456,7 +2456,7 @@
    3.40    from \<open>open S\<close>
    3.41    have "open (ereal -` S)"
    3.42      by (rule ereal_openE)
    3.43 -  then obtain e where "e > 0" and e: "\<And>y. dist y (real_of_ereal x) < e \<Longrightarrow> ereal y \<in> S"
    3.44 +  then obtain e where "e > 0" and e: "dist y (real_of_ereal x) < e \<Longrightarrow> ereal y \<in> S" for y
    3.45      using assms unfolding open_dist by force
    3.46    show thesis
    3.47    proof (intro that subsetI)
    3.48 @@ -2830,11 +2830,12 @@
    3.49    assume "open S" and "x \<in> S"
    3.50    then have "open (ereal -` S)"
    3.51      unfolding open_ereal_def by auto
    3.52 -  with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
    3.53 +  with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "dist y rx < r \<Longrightarrow> ereal y \<in> S" for y
    3.54      unfolding open_dist rx by auto
    3.55 -  then obtain n where
    3.56 -    upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
    3.57 -    lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
    3.58 +  then obtain n
    3.59 +    where upper: "u N < x + ereal r"
    3.60 +      and lower: "x < u N + ereal r"
    3.61 +      if "n \<le> N" for N
    3.62      using assms(2)[of "ereal r"] by auto
    3.63    show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"
    3.64    proof (safe intro!: exI[of _ n])
     4.1 --- a/src/HOL/Library/Fun_Lexorder.thy	Tue Apr 26 22:39:17 2016 +0200
     4.2 +++ b/src/HOL/Library/Fun_Lexorder.thy	Tue Apr 26 22:44:31 2016 +0200
     4.3 @@ -24,9 +24,9 @@
     4.4    assumes "less_fun f g"
     4.5    shows "\<not> less_fun g f"
     4.6  proof
     4.7 -  from assms obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
     4.8 +  from assms obtain k1 where k1: "f k1 < g k1" "k' < k1 \<Longrightarrow> f k' = g k'" for k'
     4.9      by (blast elim!: less_funE) 
    4.10 -  assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = f k'"
    4.11 +  assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "k' < k2 \<Longrightarrow> g k' = f k'" for k'
    4.12      by (blast elim!: less_funE) 
    4.13    show False proof (cases k1 k2 rule: linorder_cases)
    4.14      case equal with k1 k2 show False by simp
    4.15 @@ -52,9 +52,9 @@
    4.16    assumes "less_fun f g" and "less_fun g h"
    4.17    shows "less_fun f h"
    4.18  proof (rule less_funI)
    4.19 -  from \<open>less_fun f g\<close> obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
    4.20 -    by (blast elim!: less_funE) 
    4.21 -  from \<open>less_fun g h\<close> obtain k2 where k2: "g k2 < h k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = h k'"
    4.22 +  from \<open>less_fun f g\<close> obtain k1 where k1: "f k1 < g k1" "k' < k1 \<Longrightarrow> f k' = g k'" for k'
    4.23 +    by (blast elim!: less_funE)                          
    4.24 +  from \<open>less_fun g h\<close> obtain k2 where k2: "g k2 < h k2" "k' < k2 \<Longrightarrow> g k' = h k'" for k'
    4.25      by (blast elim!: less_funE) 
    4.26    show "\<exists>k. f k < h k \<and> (\<forall>k'<k. f k' = h k')"
    4.27    proof (cases k1 k2 rule: linorder_cases)
     5.1 --- a/src/HOL/Library/FuncSet.thy	Tue Apr 26 22:39:17 2016 +0200
     5.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Apr 26 22:44:31 2016 +0200
     5.3 @@ -96,9 +96,9 @@
     5.4    assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
     5.5    then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i"
     5.6      by auto
     5.7 -  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)"
     5.8 +  from bchoice[OF this] obtain n where n: "f i \<in> A (n i) i" if "i \<in> I" for i
     5.9      by auto
    5.10 -  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
    5.11 +  obtain k where k: "n i \<le> k" if "i \<in> I" for i
    5.12      using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto
    5.13    have "f \<in> Pi I (A k)"
    5.14    proof (intro Pi_I)
     6.1 --- a/src/HOL/Library/Function_Growth.thy	Tue Apr 26 22:39:17 2016 +0200
     6.2 +++ b/src/HOL/Library/Function_Growth.thy	Tue Apr 26 22:44:31 2016 +0200
     6.3 @@ -163,7 +163,7 @@
     6.4      and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
     6.5  proof -
     6.6    from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
     6.7 -  from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
     6.8 +  from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "m > n \<Longrightarrow> f m \<le> c * g m" for m
     6.9      by (rule less_eq_funE) blast
    6.10    { fix c n :: nat
    6.11      assume "c > 0"
    6.12 @@ -202,8 +202,8 @@
    6.13    shows "f \<prec> g"
    6.14  proof (rule less_funI)
    6.15    have "1 > (0::nat)" by simp
    6.16 -  from assms \<open>1 > 0\<close> have "\<exists>n. \<forall>m>n. 1 * f m < g m" .
    6.17 -  then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" by blast
    6.18 +  with assms [OF this] obtain n where *: "m > n \<Longrightarrow> 1 * f m < g m" for m
    6.19 +    by blast
    6.20    have "\<forall>m>n. f m \<le> 1 * g m"
    6.21    proof (rule allI, rule impI)
    6.22      fix m
    6.23 @@ -214,7 +214,7 @@
    6.24    with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
    6.25    fix c n :: nat
    6.26    assume "c > 0"
    6.27 -  with assms obtain q where "\<And>m. m > q \<Longrightarrow> c * f m < g m" by blast
    6.28 +  with assms obtain q where "m > q \<Longrightarrow> c * f m < g m" for m by blast
    6.29    then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
    6.30    moreover have "Suc (q + n) > n" by simp
    6.31    ultimately show "\<exists>m>n. c * f m < g m" by blast
     7.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Apr 26 22:39:17 2016 +0200
     7.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Apr 26 22:44:31 2016 +0200
     7.3 @@ -312,7 +312,7 @@
     7.4    assumes ep: "e > 0"
     7.5    shows "\<exists>d >0. \<forall>w. 0 < norm (w - z) \<and> norm (w - z) < d \<longrightarrow> norm (poly p w - poly p z) < e"
     7.6  proof -
     7.7 -  obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
     7.8 +  obtain q where q: "degree q = degree p" "poly q x = poly p (z + x)" for x
     7.9    proof
    7.10      show "degree (offset_poly p z) = degree p"
    7.11        by (rule degree_offset_poly)
    7.12 @@ -329,7 +329,7 @@
    7.13    next
    7.14      case (pCons c cs)
    7.15      from poly_bound_exists[of 1 "cs"]
    7.16 -    obtain m where m: "m > 0" "\<And>z. norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m"
    7.17 +    obtain m where m: "m > 0" "norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m" for z
    7.18        by blast
    7.19      from ep m(1) have em0: "e/m > 0"
    7.20        by (simp add: field_simps)
    7.21 @@ -535,12 +535,14 @@
    7.22    proof (cases "cs = 0")
    7.23      case False
    7.24      from poly_infinity[OF False, of "cmod (poly (pCons c cs) 0)" c]
    7.25 -    obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
    7.26 +    obtain r where r: "cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
    7.27 +      if "r \<le> cmod z" for z
    7.28        by blast
    7.29      have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>"
    7.30        by arith
    7.31      from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
    7.32 -    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)"
    7.33 +    obtain v where v: "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
    7.34 +      if "cmod w \<le> \<bar>r\<bar>" for w
    7.35        by blast
    7.36      have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)" if z: "r \<le> cmod z" for z
    7.37        using v[of 0] r[OF z] by simp
     8.1 --- a/src/HOL/Library/Multiset.thy	Tue Apr 26 22:39:17 2016 +0200
     8.2 +++ b/src/HOL/Library/Multiset.thy	Tue Apr 26 22:44:31 2016 +0200
     8.3 @@ -2075,7 +2075,7 @@
     8.4      "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
     8.5  proof -
     8.6    from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K"
     8.7 -    "\<And>b. b \<in># K \<Longrightarrow> b < a" by (blast elim: mult1E)
     8.8 +    "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
     8.9    moreover from this(3) [of a] have "a \<notin># K" by auto
    8.10    ultimately show thesis by (auto intro: that)
    8.11  qed
     9.1 --- a/src/HOL/Library/Polynomial.thy	Tue Apr 26 22:39:17 2016 +0200
     9.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Apr 26 22:44:31 2016 +0200
     9.3 @@ -3353,7 +3353,7 @@
     9.4    fix p assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
     9.5    define cs where "cs = coeffs p"
     9.6    from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'" unfolding Rats_def by blast
     9.7 -  then obtain f where f: "\<And>i. coeff p i = of_rat (f (coeff p i))" 
     9.8 +  then obtain f where f: "coeff p i = of_rat (f (coeff p i))" for i
     9.9      by (subst (asm) bchoice_iff) blast
    9.10    define cs' where "cs' = map (quotient_of \<circ> f) (coeffs p)"
    9.11    define d where "d = Lcm (set (map snd cs'))"
    9.12 @@ -3392,9 +3392,8 @@
    9.13    moreover from root have "poly p' x = 0" by (simp add: p'_def)
    9.14    ultimately show "algebraic x" unfolding algebraic_def by blast
    9.15  next
    9.16 -
    9.17    assume "algebraic x"
    9.18 -  then obtain p where p: "\<And>i. coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" 
    9.19 +  then obtain p where p: "coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" for i
    9.20      by (force simp: algebraic_def)
    9.21    moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i by (elim Ints_cases) simp
    9.22    ultimately show  "(\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)" by auto
    10.1 --- a/src/HOL/Library/Ramsey.thy	Tue Apr 26 22:39:17 2016 +0200
    10.2 +++ b/src/HOL/Library/Ramsey.thy	Tue Apr 26 22:44:31 2016 +0200
    10.3 @@ -231,8 +231,8 @@
    10.4        qed
    10.5      qed
    10.6      from dependent_choice [OF transr propr0 proprstep]
    10.7 -    obtain g where pg: "!!n::nat.  ?propr (g n)"
    10.8 -      and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
    10.9 +    obtain g where pg: "?propr (g n)" and rg: "n<m ==> (g n, g m) \<in> ?ramr" for n m :: nat
   10.10 +      by blast
   10.11      let ?gy = "fst o g"
   10.12      let ?gt = "snd o snd o g"
   10.13      have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
    11.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Tue Apr 26 22:39:17 2016 +0200
    11.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Tue Apr 26 22:44:31 2016 +0200
    11.3 @@ -609,12 +609,13 @@
    11.4    next
    11.5      case False then have "a \<noteq> 0" and "b \<noteq> 0" and "c \<noteq> 0"
    11.6        by simp_all
    11.7 -    then obtain A B C where fact:
    11.8 -      "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
    11.9 +    then obtain A B C
   11.10 +    where fact: "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
   11.11        and norm: "normalize a = msetprod A" "normalize b = msetprod B" "normalize c = msetprod C"
   11.12 -      and A: "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
   11.13 -      and B: "0 \<notin># B" "\<And>p. p \<in># B \<Longrightarrow> normalize p = p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
   11.14 -      and C: "0 \<notin># C" "\<And>p. p \<in># C \<Longrightarrow> normalize p = p" "\<And>p. p \<in># C \<Longrightarrow> is_prime p"
   11.15 +      and A: "0 \<notin># A" "p \<in># A \<Longrightarrow> normalize p = p" "p \<in># A \<Longrightarrow> is_prime p"
   11.16 +      and B: "0 \<notin># B" "p \<in># B \<Longrightarrow> normalize p = p" "p \<in># B \<Longrightarrow> is_prime p"
   11.17 +      and C: "0 \<notin># C" "p \<in># C \<Longrightarrow> normalize p = p" "p \<in># C \<Longrightarrow> is_prime p"
   11.18 +      for p
   11.19        by (blast elim!: factorizationE)
   11.20      moreover from that have "normalize c dvd normalize a" and "normalize c dvd normalize b"
   11.21        by simp_all
    12.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Apr 26 22:39:17 2016 +0200
    12.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Apr 26 22:44:31 2016 +0200
    12.3 @@ -40,9 +40,9 @@
    12.4      by (rule types_snocE)
    12.5    from snoc have "listall ?R bs" by simp
    12.6    with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
    12.7 -  then obtain bs' where
    12.8 -    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'"
    12.9 -    and bsNF: "\<And>j. NF (Var j \<degree>\<degree> map f bs')" by iprover
   12.10 +  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'"
   12.11 +    and bsNF: "NF (Var j \<degree>\<degree> map f bs')" for j
   12.12 +    by iprover
   12.13    from snoc have "?R b" by simp
   12.14    with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'"
   12.15      by iprover
    13.1 --- a/src/HOL/ex/Gauge_Integration.thy	Tue Apr 26 22:39:17 2016 +0200
    13.2 +++ b/src/HOL/ex/Gauge_Integration.thy	Tue Apr 26 22:44:31 2016 +0200
    13.3 @@ -133,7 +133,7 @@
    13.4    proof (cases "b < x")
    13.5      case True
    13.6      with 2 obtain N where *: "N < length D"
    13.7 -      and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
    13.8 +      and **: "D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" for d t e by auto
    13.9      hence "Suc N < length ((a,t,b)#D) \<and>
   13.10             (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
   13.11      thus ?thesis by auto
   13.12 @@ -372,11 +372,11 @@
   13.13    hence "a < b" and "b < c" by auto
   13.14  
   13.15    obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
   13.16 -    and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)"
   13.17 +    and I1: "fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" for D
   13.18      using IntegralE [OF \<open>Integral (a, b) f x1\<close> \<open>0 < \<epsilon>/2\<close>] by auto
   13.19  
   13.20    obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
   13.21 -    and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)"
   13.22 +    and I2: "fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" for D
   13.23      using IntegralE [OF \<open>Integral (b, c) f x2\<close> \<open>0 < \<epsilon>/2\<close>] by auto
   13.24  
   13.25    define \<delta> where "\<delta> x =
   13.26 @@ -541,7 +541,7 @@
   13.27      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"
   13.28        by (simp add: DERIV_iff2 LIM_eq)
   13.29      with \<open>0 < e\<close> obtain s
   13.30 -    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"
   13.31 +    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
   13.32        by (drule_tac x="e/2" in spec, auto)
   13.33      with strad1 [of x s f f' e] have strad:
   13.34          "\<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>"
   13.35 @@ -586,8 +586,8 @@
   13.36  
   13.37      from lemma_straddle [OF f' this]
   13.38      obtain \<delta> where "gauge {a..b} \<delta>"
   13.39 -      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>
   13.40 -           \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" by auto
   13.41 +      and \<delta>: "\<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
   13.42 +           \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" for x u v by auto
   13.43  
   13.44      have "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e"
   13.45      proof (clarify)