--- 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"
--- 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
--- 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)
--- 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
--- 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)
--- 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"
--- 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
--- 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:
--- 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])
--- 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