added lemma
authornipkow
Fri Jun 06 12:36:06 2014 +0200 (2014-06-06)
changeset 5718074c81a5b5a34
parent 57179 011955e7846b
child 57181 2d13bf9ea77b
added lemma
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Transcendental.thy	Thu Jun 05 14:37:44 2014 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Jun 06 12:36:06 2014 +0200
     1.3 @@ -1951,6 +1951,9 @@
     1.4  lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
     1.5    unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
     1.6  
     1.7 +lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
     1.8 +by(simp add: powr_realpow_numeral)
     1.9 +
    1.10  lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
    1.11    apply (case_tac "x = 0", simp, simp)
    1.12    apply (rule powr_realpow [THEN sym], simp)