--- a/src/HOL/Real/RealVector.thy Wed Sep 27 01:35:25 2006 +0200
+++ b/src/HOL/Real/RealVector.thy Wed Sep 27 01:48:30 2006 +0200
@@ -209,12 +209,16 @@
"y \<noteq> 0 \<Longrightarrow> of_real (x / y) =
(of_real x / of_real y :: 'a::real_field)"
by (simp add: divide_inverse nonzero_of_real_inverse)
-
-lemma of_real_divide:
+
+lemma of_real_divide [simp]:
"of_real (x / y) =
(of_real x / of_real y :: 'a::{real_field,division_by_zero})"
by (simp add: divide_inverse)
+lemma of_real_power [simp]:
+ "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n"
+by (induct n, simp_all add: power_Suc)
+
lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
by (simp add: of_real_def scaleR_cancel_right)
@@ -325,6 +329,14 @@
apply (rule of_real_divide [symmetric])
done
+lemma Reals_power [simp]:
+ fixes a :: "'a::{real_algebra_1,recpower}"
+ shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals"
+apply (auto simp add: Reals_def)
+apply (rule range_eqI)
+apply (rule of_real_power [symmetric])
+done
+
lemma Reals_cases [cases set: Reals]:
assumes "q \<in> \<real>"
obtains (of_real) r where "q = of_real r"