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"