# HG changeset patch
# User huffman
# Date 1159314510 -7200
# Node ID 741737aa70b26f7e12f9b16d59476e87462c7392
# Parent  54dd8f96235b75fd9836afc63d6d43201cf33900
add lemmas about of_real and power

diff -r 54dd8f96235b -r 741737aa70b2 src/HOL/Real/RealVector.thy
--- 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"