--- a/src/HOL/Analysis/Harmonic_Numbers.thy Sat Mar 04 22:07:31 2017 +0100
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy Sun Mar 05 12:07:36 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>" .
--- a/src/HOL/Decision_Procs/Approximation.thy Sat Mar 04 22:07:31 2017 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Sun Mar 05 12:07:36 2017 +0100
@@ -12,7 +12,6 @@
keywords "approximate" :: diag
begin
-declare powr_numeral [simp]
declare powr_neg_one [simp]
declare powr_neg_numeral [simp]
--- a/src/HOL/Library/Float.thy Sat Mar 04 22:07:31 2017 +0100
+++ b/src/HOL/Library/Float.thy Sun Mar 05 12:07:36 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)
--- a/src/HOL/Transcendental.thy Sat Mar 04 22:07:31 2017 +0100
+++ b/src/HOL/Transcendental.thy Sun Mar 05 12:07:36 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)