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" .
```