diff r b1c24adc1581 r 268d88ec9087 src/HOL/Real_Vector_Spaces.thy
 a/src/HOL/Real_Vector_Spaces.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Fri Nov 13 12:27:13 2015 +0000
@@ 1062,7 +1062,7 @@
subclass topological_space
proof
have "\e::real. 0 < e"
 by (fast intro: zero_less_one)
+ by (blast intro: zero_less_one)
then show "open UNIV"
unfolding open_dist by simp
next
@@ 1076,7 +1076,7 @@
done
next
fix K assume "\S\K. open S" thus "open (\K)"
 unfolding open_dist by fast
+ unfolding open_dist by (meson UnionE UnionI)
qed
lemma open_ball: "open {y. dist x y < d}"
@@ 1260,26 +1260,14 @@
by (simp add: sgn_div_norm norm_mult mult.commute)
lemma real_sgn_eq: "sgn (x::real) = x / \x\"
by (simp add: sgn_div_norm divide_inverse)

lemma real_sgn_pos: "0 < (x::real) \ sgn x = 1"
unfolding real_sgn_eq by simp

lemma real_sgn_neg: "(x::real) < 0 \ sgn x = 1"
unfolding real_sgn_eq by simp
+ by (simp add: sgn_div_norm divide_inverse)
lemma zero_le_sgn_iff [simp]: "0 \ sgn x \ 0 \ (x::real)"
by (cases "0::real" x rule: linorder_cases) simp_all
lemma zero_less_sgn_iff [simp]: "0 < sgn x \ 0 < (x::real)"
 by (cases "0::real" x rule: linorder_cases) simp_all

lemma sgn_le_0_iff [simp]: "sgn x \ 0 \ (x::real) \ 0"
by (cases "0::real" x rule: linorder_cases) simp_all
lemma sgn_less_0_iff [simp]: "sgn x < 0 \ (x::real) < 0"
 by (cases "0::real" x rule: linorder_cases) simp_all

lemma norm_conv_dist: "norm x = dist x 0"
unfolding dist_norm by simp
@@ 1321,7 +1309,7 @@
"\K>0. \x. norm (f x) \ norm x * K"
proof 
obtain K where K: "\x. norm (f x) \ norm x * K"
 using bounded by fast
+ using bounded by blast
show ?thesis
proof (intro exI impI conjI allI)
show "0 < max 1 K"
@@ 1351,7 +1339,7 @@
assumes "\r x. f (scaleR r x) = scaleR r (f x)"
assumes "\x. norm (f x) \ norm x * K"
shows "bounded_linear f"
 by standard (fast intro: assms)+
+ by standard (blast intro: assms)+
locale bounded_bilinear =
fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
@@ 1481,9 +1469,9 @@
by (simp only: f.scaleR g.scaleR)
next
from f.pos_bounded
 obtain Kf where f: "\x. norm (f x) \ norm x * Kf" and Kf: "0 < Kf" by fast
+ obtain Kf where f: "\x. norm (f x) \ norm x * Kf" and Kf: "0 < Kf" by blast
from g.pos_bounded
 obtain Kg where g: "\x. norm (g x) \ norm x * Kg" by fast
+ obtain Kg where g: "\x. norm (g x) \ norm x * Kg" by blast
show "\K. \x. norm (f (g x)) \ norm x * K"
proof (intro exI allI)
fix x
@@ 1735,7 +1723,7 @@
proof (intro allI impI)
fix e :: real assume e: "e > 0"
with `Cauchy f` obtain M where "\m n. m \ M \ n \ M \ dist (f m) (f n) < e"
 unfolding Cauchy_def by fast
+ unfolding Cauchy_def by blast
thus "\M. \m\M. \n>m. dist (f m) (f n) < e" by (intro exI[of _ M]) force
qed
qed
@@ 1783,9 +1771,9 @@
show "\N. \m\N. \n\N. dist (X m) (X n) < e"
proof (intro exI allI impI)
fix m assume "N \ m"
 hence m: "dist (X m) a < e/2" using N by fast
+ hence m: "dist (X m) a < e/2" using N by blast
fix n assume "N \ n"
 hence n: "dist (X n) a < e/2" using N by fast
+ hence n: "dist (X n) a < e/2" using N by blast
have "dist (X m) (X n) \ dist (X m) a + dist (X n) a"
by (rule dist_triangle2)
also from m n have "\ < e" by simp
@@ 1805,7 +1793,7 @@
lemma Cauchy_convergent_iff:
fixes X :: "nat \ 'a::complete_space"
shows "Cauchy X = convergent X"
by (fast intro: Cauchy_convergent convergent_Cauchy)
+by (blast intro: Cauchy_convergent convergent_Cauchy)
subsection \The set of real numbers is a complete metric space\
@@ 1881,11 +1869,11 @@
hence N: "\n\N. X N  r/2 < X n \ X n < X N + r/2"
by (simp only: dist_real_def abs_diff_less_iff)
 from N have "\n\N. X N  r/2 < X n" by fast
+ from N have "\n\N. X N  r/2 < X n" by blast
hence "X N  r/2 \ S" by (rule mem_S)
hence 1: "X N  r/2 \ Sup S" by (simp add: cSup_upper)
 from N have "\n\N. X n < X N + r/2" by fast
+ from N have "\n\N. X n < X N + r/2" by blast
from bound_isUb[OF this]
have 2: "Sup S \ X N + r/2"
by (intro cSup_least) simp_all
@@ 1953,7 +1941,7 @@
using ex_le_of_nat[of x] ..
note monoD[OF mono this]
also have "f (real_of_nat n) \ y"
 by (rule LIMSEQ_le_const[OF limseq]) (auto intro: exI[of _ n] monoD[OF mono])
+ by (rule LIMSEQ_le_const[OF limseq]) (auto intro!: exI[of _ n] monoD[OF mono])
finally have "f x \ y" . }
note le = this
have "eventually (\x. real N \ x) at_top"