tuned proofs -- less guessing;
authorwenzelm
Tue Sep 03 22:04:23 2013 +0200 (2013-09-03)
changeset 53381355a4cac5440
parent 53380 08f3491c50bf
child 53382 344587a4d5cd
tuned proofs -- less guessing;
src/HOL/Deriv.thy
src/HOL/Library/Countable_Set.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Float.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Limits.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Deriv.thy	Tue Sep 03 19:58:00 2013 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Tue Sep 03 22:04:23 2013 +0200
     1.3 @@ -1319,7 +1319,8 @@
     1.4      and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
     1.5      and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
     1.6      and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
     1.7 -  shows "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
     1.8 +  shows "\<exists>g'c f'c c.
     1.9 +    DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
    1.10  proof -
    1.11    let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
    1.12    from assms have "a < b" by simp
    1.13 @@ -1466,7 +1467,7 @@
    1.14      ultimately show "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y"
    1.15        using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c])
    1.16    qed
    1.17 -  then guess \<zeta> ..
    1.18 +  then obtain \<zeta> where "\<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)" ..
    1.19    then have \<zeta>: "eventually (\<lambda>x. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)) (at_right 0)"
    1.20      unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
    1.21    moreover
    1.22 @@ -1582,9 +1583,10 @@
    1.23  
    1.24      have "\<exists>y. t < y \<and> y < a \<and> (g a - g t) * f' y = (f a - f t) * g' y"
    1.25        using f0 g0 t(1,2) by (intro GMVT') (force intro!: DERIV_isCont)+
    1.26 -    then guess y ..
    1.27 -    from this
    1.28 -    have [arith]: "t < y" "y < a" and D_eq: "(f t - f a) / (g t - g a) = f' y / g' y"
    1.29 +    then obtain y where [arith]: "t < y" "y < a"
    1.30 +      and D_eq0: "(g a - g t) * f' y = (f a - f t) * g' y"
    1.31 +      by blast
    1.32 +    from D_eq0 have D_eq: "(f t - f a) / (g t - g a) = f' y / g' y"
    1.33        using `g a < g t` g'_neq_0[of y] by (auto simp add: field_simps)
    1.34  
    1.35      have *: "f t / g t - x = ((f t - f a) / (g t - g a) - x) * (1 - g a / g t) + (f a - x * g a) / g t"
     2.1 --- a/src/HOL/Library/Countable_Set.thy	Tue Sep 03 19:58:00 2013 +0200
     2.2 +++ b/src/HOL/Library/Countable_Set.thy	Tue Sep 03 22:04:23 2013 +0200
     2.3 @@ -55,7 +55,8 @@
     2.4    assumes "countable S" "infinite S"
     2.5    obtains e :: "'a \<Rightarrow> nat" where "bij_betw e S UNIV"
     2.6  proof -
     2.7 -  from `countable S`[THEN countableE] guess f .
     2.8 +  obtain f :: "'a \<Rightarrow> nat" where "inj_on f S"
     2.9 +    using `countable S` by (rule countableE)
    2.10    then have "bij_betw f S (f`S)"
    2.11      unfolding bij_betw_def by simp
    2.12    moreover
    2.13 @@ -169,9 +170,12 @@
    2.14    "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"
    2.15    by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)
    2.16  
    2.17 -lemma countable_image[intro, simp]: assumes A: "countable A" shows "countable (f`A)"
    2.18 +lemma countable_image[intro, simp]:
    2.19 +  assumes "countable A"
    2.20 +  shows "countable (f`A)"
    2.21  proof -
    2.22 -  from A guess g by (rule countableE)
    2.23 +  obtain g :: "'a \<Rightarrow> nat" where "inj_on g A"
    2.24 +    using assms by (rule countableE)
    2.25    moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
    2.26      by (auto intro: inj_on_inv_into inv_into_into)
    2.27    ultimately show ?thesis
     3.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Sep 03 19:58:00 2013 +0200
     3.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Sep 03 22:04:23 2013 +0200
     3.3 @@ -1368,7 +1368,8 @@
     3.4    next
     3.5      case (real r)
     3.6      with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)" by auto
     3.7 -    moreover from assms[of n] guess i ..
     3.8 +    moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
     3.9 +      using assms ..
    3.10      ultimately show ?thesis
    3.11        by (auto intro!: bexI[of _ i])
    3.12    qed
    3.13 @@ -1383,11 +1384,12 @@
    3.14    proof
    3.15      fix n ::nat have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
    3.16        using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def)
    3.17 -    then guess x ..
    3.18 +    then obtain x where "x \<in> A" "Sup A - 1 / ereal (real n) < x" ..
    3.19      then show "\<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
    3.20        by (auto intro!: exI[of _ x] simp: ereal_minus_less_iff)
    3.21    qed
    3.22 -  from choice[OF this] guess f .. note f = this
    3.23 +  from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
    3.24 +    where f: "\<forall>x. f x \<in> A \<and> Sup A < f x + 1 / ereal (real x)" ..
    3.25    have "SUPR UNIV f = Sup A"
    3.26    proof (rule SUP_eqI)
    3.27      fix i show "f i \<le> Sup A" using f
    3.28 @@ -1433,10 +1435,12 @@
    3.29        then show False using `x \<in> A` `\<infinity> \<notin> A` PInf
    3.30          by(cases x) auto
    3.31      qed
    3.32 -    from choice[OF this] guess f .. note f = this
    3.33 +    from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
    3.34 +      where f: "\<forall>z. f z \<in> A \<and> x + ereal (real z) \<le> f z" ..
    3.35      have "SUPR UNIV f = \<infinity>"
    3.36      proof (rule SUP_PInfty)
    3.37 -      fix n :: nat show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
    3.38 +      fix n :: nat
    3.39 +      show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
    3.40          using f[THEN spec, of n] `0 \<le> x`
    3.41          by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n])
    3.42      qed
    3.43 @@ -1714,8 +1718,9 @@
    3.44    fixes S :: "ereal set"
    3.45    assumes "open S" "x \<in> S" and x: "\<bar>x\<bar> \<noteq> \<infinity>"
    3.46    obtains a b where "a < x" "x < b" "{a <..< b} \<subseteq> S"
    3.47 -proof-
    3.48 -  guess e using ereal_open_cont_interval[OF assms] .
    3.49 +proof -
    3.50 +  obtain e where "0 < e" "{x - e<..<x + e} \<subseteq> S"
    3.51 +    using assms by (rule ereal_open_cont_interval)
    3.52    with that[of "x-e" "x+e"] ereal_between[OF x, of e]
    3.53    show thesis by auto
    3.54  qed
    3.55 @@ -1762,8 +1767,9 @@
    3.56  lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
    3.57    unfolding tendsto_def
    3.58  proof safe
    3.59 -  fix S :: "ereal set" assume "open S" "-\<infinity> \<in> S"
    3.60 -  from open_MInfty[OF this] guess B .. note B = this
    3.61 +  fix S :: "ereal set"
    3.62 +  assume "open S" "-\<infinity> \<in> S"
    3.63 +  from open_MInfty[OF this] obtain B where "{..<ereal B} \<subseteq> S" ..
    3.64    moreover
    3.65    assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
    3.66    then have "eventually (\<lambda>z. f z \<in> {..< B}) F" by auto
    3.67 @@ -1778,7 +1784,7 @@
    3.68    unfolding tendsto_PInfty eventually_sequentially
    3.69  proof safe
    3.70    fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
    3.71 -  from this[rule_format, of "r+1"] guess N ..
    3.72 +  then obtain N where "\<forall>n\<ge>N. ereal (r + 1) \<le> f n" by blast
    3.73    moreover have "ereal r < ereal (r + 1)" by auto
    3.74    ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
    3.75      by (blast intro: less_le_trans)
    3.76 @@ -1788,7 +1794,7 @@
    3.77    unfolding tendsto_MInfty eventually_sequentially
    3.78  proof safe
    3.79    fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
    3.80 -  from this[rule_format, of "r - 1"] guess N ..
    3.81 +  then obtain N where "\<forall>n\<ge>N. f n \<le> ereal (r - 1)" by blast
    3.82    moreover have "ereal (r - 1) < ereal r" by auto
    3.83    ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
    3.84      by (blast intro: le_less_trans)
     4.1 --- a/src/HOL/Library/Float.thy	Tue Sep 03 19:58:00 2013 +0200
     4.2 +++ b/src/HOL/Library/Float.thy	Tue Sep 03 22:04:23 2013 +0200
     4.3 @@ -44,7 +44,7 @@
     4.4  
     4.5  lemma zero_float[simp]: "0 \<in> float" by (auto simp: float_def)
     4.6  lemma one_float[simp]: "1 \<in> float" by (intro floatI[of 1 0]) simp
     4.7 -lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp  
     4.8 +lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp
     4.9  lemma neg_numeral_float[simp]: "neg_numeral i \<in> float" by (intro floatI[of "neg_numeral i" 0]) simp
    4.10  lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp
    4.11  lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float" by (intro floatI[of x 0]) simp
    4.12 @@ -175,7 +175,7 @@
    4.13  lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n"
    4.14    by (induct n) simp_all
    4.15  
    4.16 -lemma fixes x y::float 
    4.17 +lemma fixes x y::float
    4.18    shows real_of_float_min: "real (min x y) = min (real x) (real y)"
    4.19      and real_of_float_max: "real (max x y) = max (real x) (real y)"
    4.20    by (simp_all add: min_def max_def)
    4.21 @@ -197,7 +197,7 @@
    4.22    then show "\<exists>c. a < c \<and> c < b"
    4.23      apply (intro exI[of _ "(a + b) * Float 1 -1"])
    4.24      apply transfer
    4.25 -    apply (simp add: powr_neg_numeral) 
    4.26 +    apply (simp add: powr_neg_numeral)
    4.27      done
    4.28  qed
    4.29  
    4.30 @@ -222,14 +222,14 @@
    4.31                    plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float)
    4.32    done
    4.33  
    4.34 -lemma transfer_numeral [transfer_rule]: 
    4.35 +lemma transfer_numeral [transfer_rule]:
    4.36    "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
    4.37    unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
    4.38  
    4.39  lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
    4.40    by (simp add: minus_numeral[symmetric] del: minus_numeral)
    4.41  
    4.42 -lemma transfer_neg_numeral [transfer_rule]: 
    4.43 +lemma transfer_neg_numeral [transfer_rule]:
    4.44    "fun_rel (op =) pcr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
    4.45    unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
    4.46  
    4.47 @@ -321,7 +321,7 @@
    4.48    "exponent f = snd (SOME p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0)
    4.49     \<or> (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p))"
    4.50  
    4.51 -lemma 
    4.52 +lemma
    4.53    shows exponent_0[simp]: "exponent (float_of 0) = 0" (is ?E)
    4.54      and mantissa_0[simp]: "mantissa (float_of 0) = 0" (is ?M)
    4.55  proof -
    4.56 @@ -351,7 +351,7 @@
    4.57  lemma mantissa_noteq_0: "f \<noteq> float_of 0 \<Longrightarrow> mantissa f \<noteq> 0"
    4.58    using mantissa_not_dvd[of f] by auto
    4.59  
    4.60 -lemma 
    4.61 +lemma
    4.62    fixes m e :: int
    4.63    defines "f \<equiv> float_of (m * 2 powr e)"
    4.64    assumes dvd: "\<not> 2 dvd m"
    4.65 @@ -740,19 +740,23 @@
    4.66  qed
    4.67  
    4.68  lemma bitlen_Float:
    4.69 -fixes m e
    4.70 -defines "f \<equiv> Float m e"
    4.71 -shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
    4.72 -proof cases
    4.73 -  assume "m \<noteq> 0"
    4.74 +  fixes m e
    4.75 +  defines "f \<equiv> Float m e"
    4.76 +  shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
    4.77 +proof (cases "m = 0")
    4.78 +  case True
    4.79 +  then show ?thesis by (simp add: f_def bitlen_def Float_def)
    4.80 +next
    4.81 +  case False
    4.82    hence "f \<noteq> float_of 0"
    4.83      unfolding real_of_float_eq by (simp add: f_def)
    4.84    hence "mantissa f \<noteq> 0"
    4.85      by (simp add: mantissa_noteq_0)
    4.86    moreover
    4.87 -  from f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`] guess i .
    4.88 +  obtain i where "m = mantissa f * 2 ^ i" "e = exponent f - int i"
    4.89 +    by (rule f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`])
    4.90    ultimately show ?thesis by (simp add: abs_mult)
    4.91 -qed (simp add: f_def bitlen_def Float_def)
    4.92 +qed
    4.93  
    4.94  lemma compute_bitlen[code]:
    4.95    shows "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
    4.96 @@ -865,9 +869,9 @@
    4.97    is "\<lambda>prec (x::nat) (y::nat). round_down (rat_precision prec x y) (x / y)" by simp
    4.98  
    4.99  lemma compute_lapprox_posrat[code]:
   4.100 -  fixes prec x y 
   4.101 -  shows "lapprox_posrat prec x y = 
   4.102 -   (let 
   4.103 +  fixes prec x y
   4.104 +  shows "lapprox_posrat prec x y =
   4.105 +   (let
   4.106         l = rat_precision prec x y;
   4.107         d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y
   4.108      in normfloat (Float d (- l)))"
   4.109 @@ -948,7 +952,7 @@
   4.110    assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
   4.111    shows "real (rapprox_posrat n x y) < 1"
   4.112  proof -
   4.113 -  have powr1: "2 powr real (rat_precision n (int x) (int y)) = 
   4.114 +  have powr1: "2 powr real (rat_precision n (int x) (int y)) =
   4.115      2 ^ nat (rat_precision n (int x) (int y))" using rat_precision_pos[of x y n] assms
   4.116      by (simp add: powr_realpow[symmetric])
   4.117    have "x * 2 powr real (rat_precision n (int x) (int y)) / y = (x / y) *
   4.118 @@ -978,7 +982,7 @@
   4.119      (if y = 0 then 0
   4.120      else if 0 \<le> x then
   4.121        (if 0 < y then lapprox_posrat prec (nat x) (nat y)
   4.122 -      else - (rapprox_posrat prec (nat x) (nat (-y)))) 
   4.123 +      else - (rapprox_posrat prec (nat x) (nat (-y))))
   4.124        else (if 0 < y
   4.125          then - (rapprox_posrat prec (nat (-x)) (nat y))
   4.126          else lapprox_posrat prec (nat (-x)) (nat (-y))))"
   4.127 @@ -993,7 +997,7 @@
   4.128      (if y = 0 then 0
   4.129      else if 0 \<le> x then
   4.130        (if 0 < y then rapprox_posrat prec (nat x) (nat y)
   4.131 -      else - (lapprox_posrat prec (nat x) (nat (-y)))) 
   4.132 +      else - (lapprox_posrat prec (nat x) (nat (-y))))
   4.133        else (if 0 < y
   4.134          then - (lapprox_posrat prec (nat (-x)) (nat y))
   4.135          else rapprox_posrat prec (nat (-x)) (nat (-y))))"
   4.136 @@ -1017,7 +1021,7 @@
   4.137      by (simp add: field_simps powr_divide2[symmetric])
   4.138  
   4.139    show ?thesis
   4.140 -    using not_0 
   4.141 +    using not_0
   4.142      by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift, simp add: field_simps)
   4.143  qed (transfer, auto)
   4.144  hide_fact (open) compute_float_divl
   4.145 @@ -1037,7 +1041,7 @@
   4.146      by (simp add: field_simps powr_divide2[symmetric])
   4.147  
   4.148    show ?thesis
   4.149 -    using not_0 
   4.150 +    using not_0
   4.151      by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift, simp add: field_simps)
   4.152  qed (transfer, auto)
   4.153  hide_fact (open) compute_float_divr
   4.154 @@ -1104,7 +1108,7 @@
   4.155         (simp add: powr_minus inverse_eq_divide)
   4.156  qed
   4.157  
   4.158 -lemma rapprox_rat_nonneg_neg: 
   4.159 +lemma rapprox_rat_nonneg_neg:
   4.160    "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
   4.161    unfolding rapprox_rat_def round_up_def
   4.162    by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff)
   4.163 @@ -1157,7 +1161,7 @@
   4.164    "0 < real x \<Longrightarrow> real x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
   4.165  proof transfer
   4.166    fix prec :: nat and x :: real assume x: "0 < x" "x < 1" "x \<in> float" and prec: "1 \<le> prec"
   4.167 -  def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>" 
   4.168 +  def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>"
   4.169    show "1 \<le> round_down (int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - \<lfloor>log 2 \<bar>1\<bar>\<rfloor>) (1 / x) "
   4.170    proof cases
   4.171      assume nonneg: "0 \<le> p"
   4.172 @@ -1279,12 +1283,16 @@
   4.173  lemma int_floor_fl: "real (int_floor_fl x) \<le> real x" by transfer simp
   4.174  
   4.175  lemma floor_pos_exp: "exponent (floor_fl x) \<ge> 0"
   4.176 -proof cases
   4.177 -  assume nzero: "floor_fl x \<noteq> float_of 0"
   4.178 -  have "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
   4.179 -  from denormalize_shift[OF this[THEN eq_reflection] nzero] guess i . note i = this
   4.180 -  thus ?thesis by simp
   4.181 -qed (simp add: floor_fl_def)
   4.182 +proof (cases "floor_fl x = float_of 0")
   4.183 +  case True
   4.184 +  then show ?thesis by (simp add: floor_fl_def)
   4.185 +next
   4.186 +  case False
   4.187 +  have eq: "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
   4.188 +  obtain i where "\<lfloor>real x\<rfloor> = mantissa (floor_fl x) * 2 ^ i" "0 = exponent (floor_fl x) - int i"
   4.189 +    by (rule denormalize_shift[OF eq[THEN eq_reflection] False])
   4.190 +  then show ?thesis by simp
   4.191 +qed
   4.192  
   4.193  end
   4.194  
     5.1 --- a/src/HOL/Library/FuncSet.thy	Tue Sep 03 19:58:00 2013 +0200
     5.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Sep 03 22:04:23 2013 +0200
     5.3 @@ -375,7 +375,8 @@
     5.4    proof (rule ccontr)
     5.5      assume "\<not> ?thesis"
     5.6      then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
     5.7 -    from choice[OF this] guess f ..
     5.8 +    from choice[OF this]
     5.9 +    obtain f where " \<forall>x. (x \<in> I \<longrightarrow> f x \<in> F x) \<and> (x \<notin> I \<longrightarrow> f x = undefined)" ..
    5.10      then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
    5.11      with `Pi\<^sub>E I F = {}` show False by auto
    5.12    qed
    5.13 @@ -437,8 +438,10 @@
    5.14    shows "F i \<subseteq> F' i"
    5.15  proof
    5.16    fix x assume "x \<in> F i"
    5.17 -  with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))" by auto
    5.18 -  from choice[OF this] guess f .. note f = this
    5.19 +  with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))"
    5.20 +    by auto
    5.21 +  from choice[OF this] obtain f
    5.22 +    where f: " \<forall>j. (j \<in> I \<longrightarrow> f j \<in> F j \<and> (i = j \<longrightarrow> x = f j)) \<and> (j \<notin> I \<longrightarrow> f j = undefined)" ..
    5.23    then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
    5.24    then have "f \<in> Pi\<^sub>E I F'" using assms by simp
    5.25    then show "x \<in> F' i" using f `i \<in> I` by (auto simp: PiE_def)
     6.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Tue Sep 03 19:58:00 2013 +0200
     6.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Sep 03 22:04:23 2013 +0200
     6.3 @@ -169,15 +169,15 @@
     6.4    moreover
     6.5    { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
     6.6      have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
     6.7 -    proof cases
     6.8 -      assume "\<exists>z. y < z \<and> z < C"
     6.9 -      then guess z .. note z = this
    6.10 +    proof (cases "\<exists>z. y < z \<and> z < C")
    6.11 +      case True
    6.12 +      then obtain z where z: "y < z \<and> z < C" ..
    6.13        moreover from z have "z \<le> INFI {x. z < X x} X"
    6.14          by (auto intro!: INF_greatest)
    6.15        ultimately show ?thesis
    6.16          using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
    6.17      next
    6.18 -      assume "\<not> (\<exists>z. y < z \<and> z < C)"
    6.19 +      case False
    6.20        then have "C \<le> INFI {x. y < X x} X"
    6.21          by (intro INF_greatest) auto
    6.22        with `y < C` show ?thesis
    6.23 @@ -240,22 +240,22 @@
    6.24  next
    6.25    fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
    6.26    show "y \<le> f0"
    6.27 -  proof cases
    6.28 -    assume "\<exists>z. f0 < z \<and> z < y"
    6.29 -    then guess z ..
    6.30 +  proof (cases "\<exists>z. f0 < z \<and> z < y")
    6.31 +    case True
    6.32 +    then obtain z where "f0 < z \<and> z < y" ..
    6.33      moreover have "SUPR {x. f x < z} f \<le> z"
    6.34        by (rule SUP_least) simp
    6.35      ultimately show ?thesis
    6.36        using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
    6.37    next
    6.38 -    assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
    6.39 +    case False
    6.40      show ?thesis
    6.41      proof (rule classical)
    6.42        assume "\<not> y \<le> f0"
    6.43        then have "eventually (\<lambda>x. f x < y) F"
    6.44          using lim[THEN topological_tendstoD, of "{..< y}"] by auto
    6.45        then have "eventually (\<lambda>x. f x \<le> f0) F"
    6.46 -        using discrete by (auto elim!: eventually_elim1 simp: not_less)
    6.47 +        using False by (auto elim!: eventually_elim1 simp: not_less)
    6.48        then have "y \<le> SUPR {x. f x \<le> f0} f"
    6.49          by (rule lower)
    6.50        moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
     7.1 --- a/src/HOL/Library/While_Combinator.thy	Tue Sep 03 19:58:00 2013 +0200
     7.2 +++ b/src/HOL/Library/While_Combinator.thy	Tue Sep 03 22:04:23 2013 +0200
     7.3 @@ -93,8 +93,9 @@
     7.4    next
     7.5      case (Suc k)
     7.6      hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1)
     7.7 -    then guess k by (rule exE[OF Suc.IH[of "c s"]])
     7.8 -    with assms show ?case by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
     7.9 +    from Suc.IH[OF this] obtain k where "\<not> b' ((c' ^^ k) (f (c s)))" ..
    7.10 +    with assms show ?case
    7.11 +      by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
    7.12    qed
    7.13  next
    7.14    fix k assume "\<not> b' ((c' ^^ k) (f s))"
    7.15 @@ -107,8 +108,8 @@
    7.16      show ?case
    7.17      proof (cases "b s")
    7.18        case True
    7.19 -      with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp 
    7.20 -      then guess k by (rule exE[OF Suc.IH[of "c s"]])
    7.21 +      with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp
    7.22 +      from Suc.IH[OF this] obtain k where "\<not> b ((c ^^ k) (c s))" ..
    7.23        thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"])
    7.24      qed (auto intro: exI[of _ "0"])
    7.25    qed
     8.1 --- a/src/HOL/Limits.thy	Tue Sep 03 19:58:00 2013 +0200
     8.2 +++ b/src/HOL/Limits.thy	Tue Sep 03 22:04:23 2013 +0200
     8.3 @@ -33,16 +33,17 @@
     8.4    "(at_infinity \<Colon> real filter) = sup at_top at_bot"
     8.5    unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder
     8.6  proof (intro arg_cong[where f=Abs_filter] ext iffI)
     8.7 -  fix P :: "real \<Rightarrow> bool" assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
     8.8 -  then guess r ..
     8.9 +  fix P :: "real \<Rightarrow> bool"
    8.10 +  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
    8.11 +  then obtain r where "\<forall>x. r \<le> norm x \<longrightarrow> P x" ..
    8.12    then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>-r. P x)" by auto
    8.13    then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto
    8.14  next
    8.15 -  fix P :: "real \<Rightarrow> bool" assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
    8.16 +  fix P :: "real \<Rightarrow> bool"
    8.17 +  assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
    8.18    then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto
    8.19    then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
    8.20 -    by (intro exI[of _ "max p (-q)"])
    8.21 -       (auto simp: abs_real_def)
    8.22 +    by (intro exI[of _ "max p (-q)"]) (auto simp: abs_real_def)
    8.23  qed
    8.24  
    8.25  lemma at_top_le_at_infinity:
     9.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 19:58:00 2013 +0200
     9.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 22:04:23 2013 +0200
     9.3 @@ -833,7 +833,8 @@
     9.4    show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
     9.5    proof (rule ext, safe)
     9.6      fix S :: "real set" assume "open S"
     9.7 -    then guess f unfolding open_real_def bchoice_iff ..
     9.8 +    then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
     9.9 +      unfolding open_real_def bchoice_iff ..
    9.10      then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
    9.11        by (fastforce simp: dist_real_def)
    9.12      show "generate_topology (range lessThan \<union> range greaterThan) S"
    9.13 @@ -1525,7 +1526,8 @@
    9.14    with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
    9.15      by (auto simp: LIMSEQ_def dist_real_def)
    9.16    { fix x :: real
    9.17 -    from ex_le_of_nat[of x] guess n ..
    9.18 +    obtain n where "x \<le> real_of_nat n"
    9.19 +      using ex_le_of_nat[of x] ..
    9.20      note monoD[OF mono this]
    9.21      also have "f (real_of_nat n) \<le> y"
    9.22        by (rule LIMSEQ_le_const[OF limseq])
    10.1 --- a/src/HOL/Topological_Spaces.thy	Tue Sep 03 19:58:00 2013 +0200
    10.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Sep 03 22:04:23 2013 +0200
    10.3 @@ -215,14 +215,14 @@
    10.4  lemma (in linorder) less_separate:
    10.5    assumes "x < y"
    10.6    shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
    10.7 -proof cases
    10.8 -  assume "\<exists>z. x < z \<and> z < y"
    10.9 -  then guess z ..
   10.10 +proof (cases "\<exists>z. x < z \<and> z < y")
   10.11 +  case True
   10.12 +  then obtain z where "x < z \<and> z < y" ..
   10.13    then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"
   10.14      by auto
   10.15    then show ?thesis by blast
   10.16  next
   10.17 -  assume "\<not> (\<exists>z. x < z \<and> z < y)"
   10.18 +  case False
   10.19    with `x < y` have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}"
   10.20      by auto
   10.21    then show ?thesis by blast
   10.22 @@ -570,10 +570,11 @@
   10.23  lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::unbounded_dense_linorder. \<forall>n>N. P n)"
   10.24    unfolding eventually_at_top_linorder
   10.25  proof safe
   10.26 -  fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
   10.27 +  fix N assume "\<forall>n\<ge>N. P n"
   10.28 +  then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
   10.29  next
   10.30    fix N assume "\<forall>n>N. P n"
   10.31 -  moreover from gt_ex[of N] guess y ..
   10.32 +  moreover obtain y where "N < y" using gt_ex[of N] ..
   10.33    ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])
   10.34  qed
   10.35  
   10.36 @@ -606,7 +607,7 @@
   10.37    fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
   10.38  next
   10.39    fix N assume "\<forall>n<N. P n" 
   10.40 -  moreover from lt_ex[of N] guess y ..
   10.41 +  moreover obtain y where "y < N" using lt_ex[of N] ..
   10.42    ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y])
   10.43  qed
   10.44  
   10.45 @@ -765,7 +766,7 @@
   10.46    shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
   10.47    unfolding eventually_at_topological
   10.48  proof safe
   10.49 -  from gt_ex[of x] guess y ..
   10.50 +  obtain y where "x < y" using gt_ex[of x] ..
   10.51    moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
   10.52    moreover note gt_ex[of x]
   10.53    moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
   10.54 @@ -782,7 +783,7 @@
   10.55    shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
   10.56    unfolding eventually_at_topological
   10.57  proof safe
   10.58 -  from lt_ex[of x] guess y ..
   10.59 +  obtain y where "y < x" using lt_ex[of x] ..
   10.60    moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
   10.61    moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
   10.62    ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
   10.63 @@ -1513,10 +1514,16 @@
   10.64      "\<And>i. open (A i)" "\<And>i. x \<in> A i"
   10.65      "\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F ----> x"
   10.66  proof atomize_elim
   10.67 -  from countable_basis_at_decseq[of x] guess A . note A = this
   10.68 -  { fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S"
   10.69 +  obtain A :: "nat \<Rightarrow> 'a set" where A:
   10.70 +    "\<And>i. open (A i)"
   10.71 +    "\<And>i. x \<in> A i"
   10.72 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
   10.73 +    by (rule countable_basis_at_decseq) blast
   10.74 +  {
   10.75 +    fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S"
   10.76      with A(3)[of S] have "eventually (\<lambda>n. F n \<in> S) sequentially"
   10.77 -      by (auto elim: eventually_elim1 simp: subset_eq) }
   10.78 +      by (auto elim: eventually_elim1 simp: subset_eq)
   10.79 +  }
   10.80    with A show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and> (\<forall>F. (\<forall>n. F n \<in> A n) \<longrightarrow> F ----> x)"
   10.81      by (intro exI[of _ A]) (auto simp: tendsto_def)
   10.82  qed
   10.83 @@ -1525,13 +1532,16 @@
   10.84    assumes "\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
   10.85    shows "eventually P (inf (nhds a) (principal s))"
   10.86  proof (rule ccontr)
   10.87 -  from countable_basis[of a] guess A . note A = this
   10.88 -  assume "\<not> eventually P (inf (nhds a) (principal s))"
   10.89 +  obtain A :: "nat \<Rightarrow> 'a set" where A:
   10.90 +    "\<And>i. open (A i)"
   10.91 +    "\<And>i. a \<in> A i"
   10.92 +    "\<And>F. \<forall>n. F n \<in> A n \<Longrightarrow> F ----> a"
   10.93 +    by (rule countable_basis) blast
   10.94 +  assume "\<not> ?thesis"
   10.95    with A have P: "\<exists>F. \<forall>n. F n \<in> s \<and> F n \<in> A n \<and> \<not> P (F n)"
   10.96      unfolding eventually_inf_principal eventually_nhds by (intro choice) fastforce
   10.97 -  then guess F ..
   10.98 -  hence F0: "\<forall>n. F n \<in> s" and F2: "\<forall>n. F n \<in> A n" and F3: "\<forall>n. \<not> P (F n)"
   10.99 -    by fast+
  10.100 +  then obtain F where F0: "\<forall>n. F n \<in> s" and F2: "\<forall>n. F n \<in> A n" and F3: "\<forall>n. \<not> P (F n)"
  10.101 +    by blast
  10.102    with A have "F ----> a" by auto
  10.103    hence "eventually (\<lambda>n. P (F n)) sequentially"
  10.104      using assms F0 by simp
  10.105 @@ -1668,7 +1678,8 @@
  10.106    fix B :: "'b set" assume "continuous_on s f" "open B"
  10.107    then have "\<forall>x\<in>f -` B \<inter> s. (\<exists>A. open A \<and> x \<in> A \<and> s \<inter> A \<subseteq> f -` B)"
  10.108      by (auto simp: continuous_on_topological subset_eq Ball_def imp_conjL)
  10.109 -  then guess A unfolding bchoice_iff ..
  10.110 +  then obtain A where "\<forall>x\<in>f -` B \<inter> s. open (A x) \<and> x \<in> A x \<and> s \<inter> A x \<subseteq> f -` B"
  10.111 +    unfolding bchoice_iff ..
  10.112    then show "\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s"
  10.113      by (intro exI[of _ "\<Union>x\<in>f -` B \<inter> s. A x"]) auto
  10.114  next
  10.115 @@ -1883,7 +1894,7 @@
  10.116    moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
  10.117    ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
  10.118      using `compact s` unfolding compact_eq_heine_borel by auto
  10.119 -  then guess D ..
  10.120 +  then obtain D where "D \<subseteq> C \<union> {- t} \<and> finite D \<and> s \<subseteq> \<Union>D" ..
  10.121    then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
  10.122      by (intro exI[of _ "D - {-t}"]) auto
  10.123  qed
  10.124 @@ -1925,7 +1936,8 @@
  10.125    fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
  10.126    with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
  10.127      unfolding continuous_on_open_invariant by blast
  10.128 -  then guess A unfolding bchoice_iff .. note A = this
  10.129 +  then obtain A where A: "\<forall>c\<in>C. open (A c) \<and> A c \<inter> s = f -` c \<inter> s"
  10.130 +    unfolding bchoice_iff ..
  10.131    with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
  10.132      by (fastforce simp add: subset_eq set_eq_iff)+
  10.133    from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
  10.134 @@ -2114,7 +2126,8 @@
  10.135  instance linear_continuum_topology \<subseteq> perfect_space
  10.136  proof
  10.137    fix x :: 'a
  10.138 -  from ex_gt_or_lt [of x] guess y ..
  10.139 +  obtain y where "x < y \<or> y < x"
  10.140 +    using ex_gt_or_lt [of x] ..
  10.141    with Inf_notin_open[of "{x}" y] Sup_notin_open[of "{x}" y]
  10.142    show "\<not> open {x}"
  10.143      by auto