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"