src/HOL/Transcendental.thy
 changeset 54489 03ff4d1e6784 parent 54230 b1d955791529 child 54573 07864001495d
```     1.1 --- a/src/HOL/Transcendental.thy	Tue Nov 19 01:30:14 2013 +0100
1.2 +++ b/src/HOL/Transcendental.thy	Tue Nov 19 10:05:53 2013 +0100
1.3 @@ -2000,8 +2000,8 @@
1.4    apply (subst powr_add, simp, simp)
1.5    done
1.6
1.7 -lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x^(numeral n)"
1.8 -  unfolding real_of_nat_numeral[symmetric] by (rule powr_realpow)
1.9 +lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
1.10 +  unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
1.11
1.12  lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
1.13    apply (case_tac "x = 0", simp, simp)
1.14 @@ -2020,11 +2020,17 @@
1.15    then show ?thesis by (simp add: assms powr_realpow[symmetric])
1.16  qed
1.17
1.18 -lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x^numeral n"
1.19 -  using powr_realpow[of x "numeral n"] by simp
1.20 -
1.21 -lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr neg_numeral n = 1 / x^numeral n"
1.22 -  using powr_int[of x "neg_numeral n"] by simp
1.23 +lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
1.24 +  using powr_realpow [of x 1] by simp
1.25 +
1.26 +lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
1.27 +  by (fact powr_realpow_numeral)
1.28 +
1.29 +lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
1.30 +  using powr_int [of x "- 1"] by simp
1.31 +
1.32 +lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
1.33 +  using powr_int [of x "- numeral n"] by simp
1.34
1.35  lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
1.36    by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
1.37 @@ -4047,7 +4053,7 @@
1.38    show "sgn x * pi / 2 - arctan x < pi / 2"
1.39      using arctan_bounded [of "- x"] assms
1.40      unfolding sgn_real_def arctan_minus
1.41 -    by auto
1.42 +    by (auto simp add: algebra_simps)
1.43    show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
1.44      unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
1.45      unfolding sgn_real_def
```