# HG changeset patch
# User wenzelm
# Date 1378238663 -7200
# Node ID 355a4cac5440109da1c60ba081f7a94027c3efc4
# Parent  08f3491c50bf3b5987d5329a425cc7632098d674
tuned proofs -- less guessing;

diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Deriv.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -1319,7 +1319,8 @@
     and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
     and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
     and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
-  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)"
+  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)"
 proof -
   let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
   from assms have "a < b" by simp
@@ -1466,7 +1467,7 @@
     ultimately show "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y"
       using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c])
   qed
-  then guess \<zeta> ..
+  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)" ..
   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)"
     unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
   moreover
@@ -1582,9 +1583,10 @@
 
     have "\<exists>y. t < y \<and> y < a \<and> (g a - g t) * f' y = (f a - f t) * g' y"
       using f0 g0 t(1,2) by (intro GMVT') (force intro!: DERIV_isCont)+
-    then guess y ..
-    from this
-    have [arith]: "t < y" "y < a" and D_eq: "(f t - f a) / (g t - g a) = f' y / g' y"
+    then obtain y where [arith]: "t < y" "y < a"
+      and D_eq0: "(g a - g t) * f' y = (f a - f t) * g' y"
+      by blast
+    from D_eq0 have D_eq: "(f t - f a) / (g t - g a) = f' y / g' y"
       using `g a < g t` g'_neq_0[of y] by (auto simp add: field_simps)
 
     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"
diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -55,7 +55,8 @@
   assumes "countable S" "infinite S"
   obtains e :: "'a \<Rightarrow> nat" where "bij_betw e S UNIV"
 proof -
-  from `countable S`[THEN countableE] guess f .
+  obtain f :: "'a \<Rightarrow> nat" where "inj_on f S"
+    using `countable S` by (rule countableE)
   then have "bij_betw f S (f`S)"
     unfolding bij_betw_def by simp
   moreover
@@ -169,9 +170,12 @@
   "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"
   by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)
 
-lemma countable_image[intro, simp]: assumes A: "countable A" shows "countable (f`A)"
+lemma countable_image[intro, simp]:
+  assumes "countable A"
+  shows "countable (f`A)"
 proof -
-  from A guess g by (rule countableE)
+  obtain g :: "'a \<Rightarrow> nat" where "inj_on g A"
+    using assms by (rule countableE)
   moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
     by (auto intro: inj_on_inv_into inv_into_into)
   ultimately show ?thesis
diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -1368,7 +1368,8 @@
   next
     case (real r)
     with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)" by auto
-    moreover from assms[of n] guess i ..
+    moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
+      using assms ..
     ultimately show ?thesis
       by (auto intro!: bexI[of _ i])
   qed
@@ -1383,11 +1384,12 @@
   proof
     fix n ::nat have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
       using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def)
-    then guess x ..
+    then obtain x where "x \<in> A" "Sup A - 1 / ereal (real n) < x" ..
     then show "\<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
       by (auto intro!: exI[of _ x] simp: ereal_minus_less_iff)
   qed
-  from choice[OF this] guess f .. note f = this
+  from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
+    where f: "\<forall>x. f x \<in> A \<and> Sup A < f x + 1 / ereal (real x)" ..
   have "SUPR UNIV f = Sup A"
   proof (rule SUP_eqI)
     fix i show "f i \<le> Sup A" using f
@@ -1433,10 +1435,12 @@
       then show False using `x \<in> A` `\<infinity> \<notin> A` PInf
         by(cases x) auto
     qed
-    from choice[OF this] guess f .. note f = this
+    from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
+      where f: "\<forall>z. f z \<in> A \<and> x + ereal (real z) \<le> f z" ..
     have "SUPR UNIV f = \<infinity>"
     proof (rule SUP_PInfty)
-      fix n :: nat show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
+      fix n :: nat
+      show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
         using f[THEN spec, of n] `0 \<le> x`
         by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n])
     qed
@@ -1714,8 +1718,9 @@
   fixes S :: "ereal set"
   assumes "open S" "x \<in> S" and x: "\<bar>x\<bar> \<noteq> \<infinity>"
   obtains a b where "a < x" "x < b" "{a <..< b} \<subseteq> S"
-proof-
-  guess e using ereal_open_cont_interval[OF assms] .
+proof -
+  obtain e where "0 < e" "{x - e<..<x + e} \<subseteq> S"
+    using assms by (rule ereal_open_cont_interval)
   with that[of "x-e" "x+e"] ereal_between[OF x, of e]
   show thesis by auto
 qed
@@ -1762,8 +1767,9 @@
 lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
   unfolding tendsto_def
 proof safe
-  fix S :: "ereal set" assume "open S" "-\<infinity> \<in> S"
-  from open_MInfty[OF this] guess B .. note B = this
+  fix S :: "ereal set"
+  assume "open S" "-\<infinity> \<in> S"
+  from open_MInfty[OF this] obtain B where "{..<ereal B} \<subseteq> S" ..
   moreover
   assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
   then have "eventually (\<lambda>z. f z \<in> {..< B}) F" by auto
@@ -1778,7 +1784,7 @@
   unfolding tendsto_PInfty eventually_sequentially
 proof safe
   fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
-  from this[rule_format, of "r+1"] guess N ..
+  then obtain N where "\<forall>n\<ge>N. ereal (r + 1) \<le> f n" by blast
   moreover have "ereal r < ereal (r + 1)" by auto
   ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
     by (blast intro: less_le_trans)
@@ -1788,7 +1794,7 @@
   unfolding tendsto_MInfty eventually_sequentially
 proof safe
   fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
-  from this[rule_format, of "r - 1"] guess N ..
+  then obtain N where "\<forall>n\<ge>N. f n \<le> ereal (r - 1)" by blast
   moreover have "ereal (r - 1) < ereal r" by auto
   ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
     by (blast intro: le_less_trans)
diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Library/Float.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -44,7 +44,7 @@
 
 lemma zero_float[simp]: "0 \<in> float" by (auto simp: float_def)
 lemma one_float[simp]: "1 \<in> float" by (intro floatI[of 1 0]) simp
-lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp  
+lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp
 lemma neg_numeral_float[simp]: "neg_numeral i \<in> float" by (intro floatI[of "neg_numeral i" 0]) simp
 lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp
 lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float" by (intro floatI[of x 0]) simp
@@ -175,7 +175,7 @@
 lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n"
   by (induct n) simp_all
 
-lemma fixes x y::float 
+lemma fixes x y::float
   shows real_of_float_min: "real (min x y) = min (real x) (real y)"
     and real_of_float_max: "real (max x y) = max (real x) (real y)"
   by (simp_all add: min_def max_def)
@@ -197,7 +197,7 @@
   then show "\<exists>c. a < c \<and> c < b"
     apply (intro exI[of _ "(a + b) * Float 1 -1"])
     apply transfer
-    apply (simp add: powr_neg_numeral) 
+    apply (simp add: powr_neg_numeral)
     done
 qed
 
@@ -222,14 +222,14 @@
                   plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float)
   done
 
-lemma transfer_numeral [transfer_rule]: 
+lemma transfer_numeral [transfer_rule]:
   "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
   unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
 
 lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
   by (simp add: minus_numeral[symmetric] del: minus_numeral)
 
-lemma transfer_neg_numeral [transfer_rule]: 
+lemma transfer_neg_numeral [transfer_rule]:
   "fun_rel (op =) pcr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
   unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
 
@@ -321,7 +321,7 @@
   "exponent f = snd (SOME p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0)
    \<or> (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p))"
 
-lemma 
+lemma
   shows exponent_0[simp]: "exponent (float_of 0) = 0" (is ?E)
     and mantissa_0[simp]: "mantissa (float_of 0) = 0" (is ?M)
 proof -
@@ -351,7 +351,7 @@
 lemma mantissa_noteq_0: "f \<noteq> float_of 0 \<Longrightarrow> mantissa f \<noteq> 0"
   using mantissa_not_dvd[of f] by auto
 
-lemma 
+lemma
   fixes m e :: int
   defines "f \<equiv> float_of (m * 2 powr e)"
   assumes dvd: "\<not> 2 dvd m"
@@ -740,19 +740,23 @@
 qed
 
 lemma bitlen_Float:
-fixes m e
-defines "f \<equiv> Float m e"
-shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
-proof cases
-  assume "m \<noteq> 0"
+  fixes m e
+  defines "f \<equiv> Float m e"
+  shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
+proof (cases "m = 0")
+  case True
+  then show ?thesis by (simp add: f_def bitlen_def Float_def)
+next
+  case False
   hence "f \<noteq> float_of 0"
     unfolding real_of_float_eq by (simp add: f_def)
   hence "mantissa f \<noteq> 0"
     by (simp add: mantissa_noteq_0)
   moreover
-  from f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`] guess i .
+  obtain i where "m = mantissa f * 2 ^ i" "e = exponent f - int i"
+    by (rule f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`])
   ultimately show ?thesis by (simp add: abs_mult)
-qed (simp add: f_def bitlen_def Float_def)
+qed
 
 lemma compute_bitlen[code]:
   shows "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
@@ -865,9 +869,9 @@
   is "\<lambda>prec (x::nat) (y::nat). round_down (rat_precision prec x y) (x / y)" by simp
 
 lemma compute_lapprox_posrat[code]:
-  fixes prec x y 
-  shows "lapprox_posrat prec x y = 
-   (let 
+  fixes prec x y
+  shows "lapprox_posrat prec x y =
+   (let
        l = rat_precision prec x y;
        d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y
     in normfloat (Float d (- l)))"
@@ -948,7 +952,7 @@
   assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
   shows "real (rapprox_posrat n x y) < 1"
 proof -
-  have powr1: "2 powr real (rat_precision n (int x) (int y)) = 
+  have powr1: "2 powr real (rat_precision n (int x) (int y)) =
     2 ^ nat (rat_precision n (int x) (int y))" using rat_precision_pos[of x y n] assms
     by (simp add: powr_realpow[symmetric])
   have "x * 2 powr real (rat_precision n (int x) (int y)) / y = (x / y) *
@@ -978,7 +982,7 @@
     (if y = 0 then 0
     else if 0 \<le> x then
       (if 0 < y then lapprox_posrat prec (nat x) (nat y)
-      else - (rapprox_posrat prec (nat x) (nat (-y)))) 
+      else - (rapprox_posrat prec (nat x) (nat (-y))))
       else (if 0 < y
         then - (rapprox_posrat prec (nat (-x)) (nat y))
         else lapprox_posrat prec (nat (-x)) (nat (-y))))"
@@ -993,7 +997,7 @@
     (if y = 0 then 0
     else if 0 \<le> x then
       (if 0 < y then rapprox_posrat prec (nat x) (nat y)
-      else - (lapprox_posrat prec (nat x) (nat (-y)))) 
+      else - (lapprox_posrat prec (nat x) (nat (-y))))
       else (if 0 < y
         then - (lapprox_posrat prec (nat (-x)) (nat y))
         else rapprox_posrat prec (nat (-x)) (nat (-y))))"
@@ -1017,7 +1021,7 @@
     by (simp add: field_simps powr_divide2[symmetric])
 
   show ?thesis
-    using not_0 
+    using not_0
     by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift, simp add: field_simps)
 qed (transfer, auto)
 hide_fact (open) compute_float_divl
@@ -1037,7 +1041,7 @@
     by (simp add: field_simps powr_divide2[symmetric])
 
   show ?thesis
-    using not_0 
+    using not_0
     by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift, simp add: field_simps)
 qed (transfer, auto)
 hide_fact (open) compute_float_divr
@@ -1104,7 +1108,7 @@
        (simp add: powr_minus inverse_eq_divide)
 qed
 
-lemma rapprox_rat_nonneg_neg: 
+lemma rapprox_rat_nonneg_neg:
   "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
   unfolding rapprox_rat_def round_up_def
   by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff)
@@ -1157,7 +1161,7 @@
   "0 < real x \<Longrightarrow> real x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
 proof transfer
   fix prec :: nat and x :: real assume x: "0 < x" "x < 1" "x \<in> float" and prec: "1 \<le> prec"
-  def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>" 
+  def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>"
   show "1 \<le> round_down (int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - \<lfloor>log 2 \<bar>1\<bar>\<rfloor>) (1 / x) "
   proof cases
     assume nonneg: "0 \<le> p"
@@ -1279,12 +1283,16 @@
 lemma int_floor_fl: "real (int_floor_fl x) \<le> real x" by transfer simp
 
 lemma floor_pos_exp: "exponent (floor_fl x) \<ge> 0"
-proof cases
-  assume nzero: "floor_fl x \<noteq> float_of 0"
-  have "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
-  from denormalize_shift[OF this[THEN eq_reflection] nzero] guess i . note i = this
-  thus ?thesis by simp
-qed (simp add: floor_fl_def)
+proof (cases "floor_fl x = float_of 0")
+  case True
+  then show ?thesis by (simp add: floor_fl_def)
+next
+  case False
+  have eq: "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
+  obtain i where "\<lfloor>real x\<rfloor> = mantissa (floor_fl x) * 2 ^ i" "0 = exponent (floor_fl x) - int i"
+    by (rule denormalize_shift[OF eq[THEN eq_reflection] False])
+  then show ?thesis by simp
+qed
 
 end
 
diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -375,7 +375,8 @@
   proof (rule ccontr)
     assume "\<not> ?thesis"
     then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
-    from choice[OF this] guess f ..
+    from choice[OF this]
+    obtain f where " \<forall>x. (x \<in> I \<longrightarrow> f x \<in> F x) \<and> (x \<notin> I \<longrightarrow> f x = undefined)" ..
     then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
     with `Pi\<^sub>E I F = {}` show False by auto
   qed
@@ -437,8 +438,10 @@
   shows "F i \<subseteq> F' i"
 proof
   fix x assume "x \<in> F i"
-  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
-  from choice[OF this] guess f .. note f = this
+  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
+  from choice[OF this] obtain f
+    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)" ..
   then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
   then have "f \<in> Pi\<^sub>E I F'" using assms by simp
   then show "x \<in> F' i" using f `i \<in> I` by (auto simp: PiE_def)
diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -169,15 +169,15 @@
   moreover
   { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
     have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
-    proof cases
-      assume "\<exists>z. y < z \<and> z < C"
-      then guess z .. note z = this
+    proof (cases "\<exists>z. y < z \<and> z < C")
+      case True
+      then obtain z where z: "y < z \<and> z < C" ..
       moreover from z have "z \<le> INFI {x. z < X x} X"
         by (auto intro!: INF_greatest)
       ultimately show ?thesis
         using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
     next
-      assume "\<not> (\<exists>z. y < z \<and> z < C)"
+      case False
       then have "C \<le> INFI {x. y < X x} X"
         by (intro INF_greatest) auto
       with `y < C` show ?thesis
@@ -240,22 +240,22 @@
 next
   fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
   show "y \<le> f0"
-  proof cases
-    assume "\<exists>z. f0 < z \<and> z < y"
-    then guess z ..
+  proof (cases "\<exists>z. f0 < z \<and> z < y")
+    case True
+    then obtain z where "f0 < z \<and> z < y" ..
     moreover have "SUPR {x. f x < z} f \<le> z"
       by (rule SUP_least) simp
     ultimately show ?thesis
       using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
   next
-    assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
+    case False
     show ?thesis
     proof (rule classical)
       assume "\<not> y \<le> f0"
       then have "eventually (\<lambda>x. f x < y) F"
         using lim[THEN topological_tendstoD, of "{..< y}"] by auto
       then have "eventually (\<lambda>x. f x \<le> f0) F"
-        using discrete by (auto elim!: eventually_elim1 simp: not_less)
+        using False by (auto elim!: eventually_elim1 simp: not_less)
       then have "y \<le> SUPR {x. f x \<le> f0} f"
         by (rule lower)
       moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -93,8 +93,9 @@
   next
     case (Suc k)
     hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1)
-    then guess k by (rule exE[OF Suc.IH[of "c s"]])
-    with assms show ?case by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
+    from Suc.IH[OF this] obtain k where "\<not> b' ((c' ^^ k) (f (c s)))" ..
+    with assms show ?case
+      by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
   qed
 next
   fix k assume "\<not> b' ((c' ^^ k) (f s))"
@@ -107,8 +108,8 @@
     show ?case
     proof (cases "b s")
       case True
-      with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp 
-      then guess k by (rule exE[OF Suc.IH[of "c s"]])
+      with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp
+      from Suc.IH[OF this] obtain k where "\<not> b ((c ^^ k) (c s))" ..
       thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"])
     qed (auto intro: exI[of _ "0"])
   qed
diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Limits.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -33,16 +33,17 @@
   "(at_infinity \<Colon> real filter) = sup at_top at_bot"
   unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder
 proof (intro arg_cong[where f=Abs_filter] ext iffI)
-  fix P :: "real \<Rightarrow> bool" assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
-  then guess r ..
+  fix P :: "real \<Rightarrow> bool"
+  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
+  then obtain r where "\<forall>x. r \<le> norm x \<longrightarrow> P x" ..
   then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>-r. P x)" by auto
   then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto
 next
-  fix P :: "real \<Rightarrow> bool" assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
+  fix P :: "real \<Rightarrow> bool"
+  assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
   then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto
   then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
-    by (intro exI[of _ "max p (-q)"])
-       (auto simp: abs_real_def)
+    by (intro exI[of _ "max p (-q)"]) (auto simp: abs_real_def)
 qed
 
 lemma at_top_le_at_infinity:
diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -833,7 +833,8 @@
   show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
   proof (rule ext, safe)
     fix S :: "real set" assume "open S"
-    then guess f unfolding open_real_def bchoice_iff ..
+    then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
+      unfolding open_real_def bchoice_iff ..
     then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
       by (fastforce simp: dist_real_def)
     show "generate_topology (range lessThan \<union> range greaterThan) S"
@@ -1525,7 +1526,8 @@
   with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
     by (auto simp: LIMSEQ_def dist_real_def)
   { fix x :: real
-    from ex_le_of_nat[of x] guess n ..
+    obtain n where "x \<le> real_of_nat n"
+      using ex_le_of_nat[of x] ..
     note monoD[OF mono this]
     also have "f (real_of_nat n) \<le> y"
       by (rule LIMSEQ_le_const[OF limseq])
diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -215,14 +215,14 @@
 lemma (in linorder) less_separate:
   assumes "x < y"
   shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
-proof cases
-  assume "\<exists>z. x < z \<and> z < y"
-  then guess z ..
+proof (cases "\<exists>z. x < z \<and> z < y")
+  case True
+  then obtain z where "x < z \<and> z < y" ..
   then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"
     by auto
   then show ?thesis by blast
 next
-  assume "\<not> (\<exists>z. x < z \<and> z < y)"
+  case False
   with `x < y` have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}"
     by auto
   then show ?thesis by blast
@@ -570,10 +570,11 @@
 lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::unbounded_dense_linorder. \<forall>n>N. P n)"
   unfolding eventually_at_top_linorder
 proof safe
-  fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
+  fix N assume "\<forall>n\<ge>N. P n"
+  then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
 next
   fix N assume "\<forall>n>N. P n"
-  moreover from gt_ex[of N] guess y ..
+  moreover obtain y where "N < y" using gt_ex[of N] ..
   ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])
 qed
 
@@ -606,7 +607,7 @@
   fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
 next
   fix N assume "\<forall>n<N. P n" 
-  moreover from lt_ex[of N] guess y ..
+  moreover obtain y where "y < N" using lt_ex[of N] ..
   ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y])
 qed
 
@@ -765,7 +766,7 @@
   shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
   unfolding eventually_at_topological
 proof safe
-  from gt_ex[of x] guess y ..
+  obtain y where "x < y" using gt_ex[of x] ..
   moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
   moreover note gt_ex[of x]
   moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
@@ -782,7 +783,7 @@
   shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
   unfolding eventually_at_topological
 proof safe
-  from lt_ex[of x] guess y ..
+  obtain y where "y < x" using lt_ex[of x] ..
   moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
   moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
   ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
@@ -1513,10 +1514,16 @@
     "\<And>i. open (A i)" "\<And>i. x \<in> A i"
     "\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F ----> x"
 proof atomize_elim
-  from countable_basis_at_decseq[of x] guess A . note A = this
-  { fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S"
+  obtain A :: "nat \<Rightarrow> 'a set" where A:
+    "\<And>i. open (A i)"
+    "\<And>i. x \<in> A i"
+    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
+    by (rule countable_basis_at_decseq) blast
+  {
+    fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S"
     with A(3)[of S] have "eventually (\<lambda>n. F n \<in> S) sequentially"
-      by (auto elim: eventually_elim1 simp: subset_eq) }
+      by (auto elim: eventually_elim1 simp: subset_eq)
+  }
   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)"
     by (intro exI[of _ A]) (auto simp: tendsto_def)
 qed
@@ -1525,13 +1532,16 @@
   assumes "\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
   shows "eventually P (inf (nhds a) (principal s))"
 proof (rule ccontr)
-  from countable_basis[of a] guess A . note A = this
-  assume "\<not> eventually P (inf (nhds a) (principal s))"
+  obtain A :: "nat \<Rightarrow> 'a set" where A:
+    "\<And>i. open (A i)"
+    "\<And>i. a \<in> A i"
+    "\<And>F. \<forall>n. F n \<in> A n \<Longrightarrow> F ----> a"
+    by (rule countable_basis) blast
+  assume "\<not> ?thesis"
   with A have P: "\<exists>F. \<forall>n. F n \<in> s \<and> F n \<in> A n \<and> \<not> P (F n)"
     unfolding eventually_inf_principal eventually_nhds by (intro choice) fastforce
-  then guess F ..
-  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)"
-    by fast+
+  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)"
+    by blast
   with A have "F ----> a" by auto
   hence "eventually (\<lambda>n. P (F n)) sequentially"
     using assms F0 by simp
@@ -1668,7 +1678,8 @@
   fix B :: "'b set" assume "continuous_on s f" "open B"
   then have "\<forall>x\<in>f -` B \<inter> s. (\<exists>A. open A \<and> x \<in> A \<and> s \<inter> A \<subseteq> f -` B)"
     by (auto simp: continuous_on_topological subset_eq Ball_def imp_conjL)
-  then guess A unfolding bchoice_iff ..
+  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"
+    unfolding bchoice_iff ..
   then show "\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s"
     by (intro exI[of _ "\<Union>x\<in>f -` B \<inter> s. A x"]) auto
 next
@@ -1883,7 +1894,7 @@
   moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
   ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
     using `compact s` unfolding compact_eq_heine_borel by auto
-  then guess D ..
+  then obtain D where "D \<subseteq> C \<union> {- t} \<and> finite D \<and> s \<subseteq> \<Union>D" ..
   then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
     by (intro exI[of _ "D - {-t}"]) auto
 qed
@@ -1925,7 +1936,8 @@
   fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
   with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
     unfolding continuous_on_open_invariant by blast
-  then guess A unfolding bchoice_iff .. note A = this
+  then obtain A where A: "\<forall>c\<in>C. open (A c) \<and> A c \<inter> s = f -` c \<inter> s"
+    unfolding bchoice_iff ..
   with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
     by (fastforce simp add: subset_eq set_eq_iff)+
   from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
@@ -2114,7 +2126,8 @@
 instance linear_continuum_topology \<subseteq> perfect_space
 proof
   fix x :: 'a
-  from ex_gt_or_lt [of x] guess y ..
+  obtain y where "x < y \<or> y < x"
+    using ex_gt_or_lt [of x] ..
   with Inf_notin_open[of "{x}" y] Sup_notin_open[of "{x}" y]
   show "\<not> open {x}"
     by auto