# HG changeset patch
# User nipkow
# Date 1488707871 -3600
# Node ID a79c1080f1e98cec789d9b9de4f4afc1d7d65877
# Parent  30d0b2f1df768f398c6a36da855205aa866a99a9
added numeral_powr_numeral

diff -r 30d0b2f1df76 -r a79c1080f1e9 src/HOL/Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Mar 02 21:16:02 2017 +0100
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Sun Mar 05 10:57:51 2017 +0100
@@ -533,7 +533,7 @@
 lemma euler_mascheroni_gt_19_over_33: "(euler_mascheroni :: real) > 19/33" (is ?th1)
   and euler_mascheroni_less_13_over_22: "(euler_mascheroni :: real) < 13/22" (is ?th2)
 proof -
-  have "ln (real (Suc 7)) = 3 * ln 2" by (simp add: ln_powr [symmetric] powr_numeral)
+  have "ln (real (Suc 7)) = 3 * ln 2" by (simp add: ln_powr [symmetric])
   also from ln_approx_bounds[of 2 3] have "\<dots> \<in> {3*307/443<..<3*4615/6658}"
     by (simp add: eval_nat_numeral)
   finally have "ln (real (Suc 7)) \<in> \<dots>" .
diff -r 30d0b2f1df76 -r a79c1080f1e9 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Mar 02 21:16:02 2017 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Mar 05 10:57:51 2017 +0100
@@ -12,7 +12,6 @@
 keywords "approximate" :: diag
 begin
 
-declare powr_numeral [simp]
 declare powr_neg_one [simp]
 declare powr_neg_numeral [simp]
 
diff -r 30d0b2f1df76 -r a79c1080f1e9 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Thu Mar 02 21:16:02 2017 +0100
+++ b/src/HOL/Library/Float.thy	Sun Mar 05 10:57:51 2017 +0100
@@ -1646,7 +1646,7 @@
       powr_realpow[symmetric] powr_mult_base)
 
   have "\<bar>?m2\<bar> * 2 < 2 powr (bitlen \<bar>m2\<bar> + ?shift + 1)"
-    by (auto simp: field_simps powr_add powr_mult_base powr_numeral powr_divide2[symmetric] abs_mult)
+    by (auto simp: field_simps powr_add powr_mult_base powr_divide2[symmetric] abs_mult)
   also have "\<dots> \<le> 2 powr 0"
     using H by (intro powr_mono) auto
   finally have abs_m2_less_half: "\<bar>?m2\<bar> < 1 / 2"
@@ -1657,7 +1657,7 @@
   also have "\<dots> \<le> 2 powr real_of_int (e1 - e2 - 2)"
     by simp
   finally have b_less_quarter: "\<bar>?b\<bar> < 1/4 * 2 powr real_of_int e1"
-    by (simp add: powr_add field_simps powr_divide2[symmetric] powr_numeral abs_mult)
+    by (simp add: powr_add field_simps powr_divide2[symmetric] abs_mult)
   also have "1/4 < \<bar>real_of_int m1\<bar> / 2" using \<open>m1 \<noteq> 0\<close> by simp
   finally have b_less_half_a: "\<bar>?b\<bar> < 1/2 * \<bar>?a\<bar>"
     by (simp add: algebra_simps powr_mult_base abs_mult)
diff -r 30d0b2f1df76 -r a79c1080f1e9 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Mar 02 21:16:02 2017 +0100
+++ b/src/HOL/Transcendental.thy	Sun Mar 05 10:57:51 2017 +0100
@@ -2694,6 +2694,10 @@
 lemma powr_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   by (metis of_nat_numeral powr_realpow)
 
+lemma numeral_powr_numeral[simp]:
+  "(numeral m :: real) powr (numeral n :: real) = numeral m ^ (numeral n)"
+by(simp add: powr_numeral)
+
 lemma powr_real_of_int:
   "x > 0 \<Longrightarrow> x powr real_of_int n = (if n \<ge> 0 then x ^ nat n else inverse (x ^ nat (- n)))"
   using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]
@@ -2755,7 +2759,7 @@
   by (simp add: root_powr_inverse ln_powr)
 
 lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
-  by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult.commute)
+  by (simp add: ln_powr ln_powr[symmetric] mult.commute)
 
 lemma log_root: "n > 0 \<Longrightarrow> a > 0 \<Longrightarrow> log b (root n a) =  log b a / n"
   by (simp add: log_def ln_root)