src/HOL/Multivariate_Analysis/Linear_Algebra.thy
changeset 56480 093ea91498e6
parent 56479 91958d4b30f7
child 56536 aefb4a8da31f
     1.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Apr 09 09:37:47 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Apr 09 09:37:48 2014 +0200
     1.3 @@ -569,12 +569,8 @@
     1.4    unfolding real_of_nat_def by (rule ex_le_of_nat)
     1.5  
     1.6  lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
     1.7 -  using reals_Archimedean
     1.8 -  apply (auto simp add: field_simps)
     1.9 -  apply (subgoal_tac "inverse (real n) > 0")
    1.10 -  apply arith
    1.11 -  apply simp
    1.12 -  done
    1.13 +  using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
    1.14 +  by (auto simp add: field_simps cong: conj_cong)
    1.15  
    1.16  lemma real_pow_lbound: "0 \<le> x \<Longrightarrow> 1 + real n * x \<le> (1 + x) ^ n"
    1.17  proof (induct n)
    1.18 @@ -629,7 +625,7 @@
    1.19    from real_arch_pow[OF ix, of "1/y"]
    1.20    obtain n where n: "1/y < (1/x)^n" by blast
    1.21    then show ?thesis using y `x > 0`
    1.22 -    by (auto simp add: field_simps power_divide)
    1.23 +    by (auto simp add: field_simps)
    1.24  next
    1.25    case False
    1.26    with y x1 show ?thesis
    1.27 @@ -1147,7 +1143,7 @@
    1.28        using fS SP vS by auto
    1.29      have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S =
    1.30        setsum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
    1.31 -      using fS vS uv by (simp add: setsum_diff1 divide_inverse field_simps)
    1.32 +      using fS vS uv by (simp add: setsum_diff1 field_simps)
    1.33      also have "\<dots> = ?a"
    1.34        unfolding scaleR_right.setsum [symmetric] u using uv by simp
    1.35      finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .