src/HOL/Real_Vector_Spaces.thy
 changeset 61649 268d88ec9087 parent 61609 77b453bd616f child 61762 d50b993b4fb9
```     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Nov 12 11:22:26 2015 +0100
1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Fri Nov 13 12:27:13 2015 +0000
1.3 @@ -1062,7 +1062,7 @@
1.4  subclass topological_space
1.5  proof
1.6    have "\<exists>e::real. 0 < e"
1.7 -    by (fast intro: zero_less_one)
1.8 +    by (blast intro: zero_less_one)
1.9    then show "open UNIV"
1.10      unfolding open_dist by simp
1.11  next
1.12 @@ -1076,7 +1076,7 @@
1.13      done
1.14  next
1.15    fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
1.16 -    unfolding open_dist by fast
1.17 +    unfolding open_dist by (meson UnionE UnionI)
1.18  qed
1.19
1.20  lemma open_ball: "open {y. dist x y < d}"
1.21 @@ -1260,26 +1260,14 @@
1.22  by (simp add: sgn_div_norm norm_mult mult.commute)
1.23
1.24  lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>"
1.25 -by (simp add: sgn_div_norm divide_inverse)
1.26 -
1.27 -lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
1.28 -unfolding real_sgn_eq by simp
1.29 -
1.30 -lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
1.31 -unfolding real_sgn_eq by simp
1.32 +  by (simp add: sgn_div_norm divide_inverse)
1.33
1.34  lemma zero_le_sgn_iff [simp]: "0 \<le> sgn x \<longleftrightarrow> 0 \<le> (x::real)"
1.35    by (cases "0::real" x rule: linorder_cases) simp_all
1.36
1.37 -lemma zero_less_sgn_iff [simp]: "0 < sgn x \<longleftrightarrow> 0 < (x::real)"
1.38 -  by (cases "0::real" x rule: linorder_cases) simp_all
1.39 -
1.40  lemma sgn_le_0_iff [simp]: "sgn x \<le> 0 \<longleftrightarrow> (x::real) \<le> 0"
1.41    by (cases "0::real" x rule: linorder_cases) simp_all
1.42
1.43 -lemma sgn_less_0_iff [simp]: "sgn x < 0 \<longleftrightarrow> (x::real) < 0"
1.44 -  by (cases "0::real" x rule: linorder_cases) simp_all
1.45 -
1.46  lemma norm_conv_dist: "norm x = dist x 0"
1.47    unfolding dist_norm by simp
1.48
1.49 @@ -1321,7 +1309,7 @@
1.50    "\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K"
1.51  proof -
1.52    obtain K where K: "\<And>x. norm (f x) \<le> norm x * K"
1.53 -    using bounded by fast
1.54 +    using bounded by blast
1.55    show ?thesis
1.56    proof (intro exI impI conjI allI)
1.57      show "0 < max 1 K"
1.58 @@ -1351,7 +1339,7 @@
1.59    assumes "\<And>r x. f (scaleR r x) = scaleR r (f x)"
1.60    assumes "\<And>x. norm (f x) \<le> norm x * K"
1.61    shows "bounded_linear f"
1.62 -  by standard (fast intro: assms)+
1.63 +  by standard (blast intro: assms)+
1.64
1.65  locale bounded_bilinear =
1.66    fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
1.67 @@ -1481,9 +1469,9 @@
1.68        by (simp only: f.scaleR g.scaleR)
1.69    next
1.70      from f.pos_bounded
1.71 -    obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
1.72 +    obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by blast
1.73      from g.pos_bounded
1.74 -    obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
1.75 +    obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by blast
1.76      show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
1.77      proof (intro exI allI)
1.78        fix x
1.79 @@ -1735,7 +1723,7 @@
1.80    proof (intro allI impI)
1.81      fix e :: real assume e: "e > 0"
1.82      with `Cauchy f` obtain M where "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (f m) (f n) < e"
1.83 -      unfolding Cauchy_def by fast
1.84 +      unfolding Cauchy_def by blast
1.85      thus "\<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e" by (intro exI[of _ M]) force
1.86    qed
1.87  qed
1.88 @@ -1783,9 +1771,9 @@
1.89    show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
1.90    proof (intro exI allI impI)
1.91      fix m assume "N \<le> m"
1.92 -    hence m: "dist (X m) a < e/2" using N by fast
1.93 +    hence m: "dist (X m) a < e/2" using N by blast
1.94      fix n assume "N \<le> n"
1.95 -    hence n: "dist (X n) a < e/2" using N by fast
1.96 +    hence n: "dist (X n) a < e/2" using N by blast
1.97      have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
1.98        by (rule dist_triangle2)
1.99      also from m n have "\<dots> < e" by simp
1.100 @@ -1805,7 +1793,7 @@
1.101  lemma Cauchy_convergent_iff:
1.102    fixes X :: "nat \<Rightarrow> 'a::complete_space"
1.103    shows "Cauchy X = convergent X"
1.104 -by (fast intro: Cauchy_convergent convergent_Cauchy)
1.105 +by (blast intro: Cauchy_convergent convergent_Cauchy)
1.106
1.107  subsection \<open>The set of real numbers is a complete metric space\<close>
1.108
1.109 @@ -1881,11 +1869,11 @@
1.110    hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
1.111      by (simp only: dist_real_def abs_diff_less_iff)
1.112
1.113 -  from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
1.114 +  from N have "\<forall>n\<ge>N. X N - r/2 < X n" by blast
1.115    hence "X N - r/2 \<in> S" by (rule mem_S)
1.116    hence 1: "X N - r/2 \<le> Sup S" by (simp add: cSup_upper)
1.117
1.118 -  from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
1.119 +  from N have "\<forall>n\<ge>N. X n < X N + r/2" by blast
1.120    from bound_isUb[OF this]
1.121    have 2: "Sup S \<le> X N + r/2"
1.122      by (intro cSup_least) simp_all
1.123 @@ -1953,7 +1941,7 @@
1.124        using ex_le_of_nat[of x] ..
1.125      note monoD[OF mono this]
1.126      also have "f (real_of_nat n) \<le> y"
1.127 -      by (rule LIMSEQ_le_const[OF limseq]) (auto intro: exI[of _ n] monoD[OF mono])
1.128 +      by (rule LIMSEQ_le_const[OF limseq]) (auto intro!: exI[of _ n] monoD[OF mono])
1.129      finally have "f x \<le> y" . }
1.130    note le = this
1.131    have "eventually (\<lambda>x. real N \<le> x) at_top"
```