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