add lemma Standard_hyperpow
authorhuffman
Tue May 08 23:52:15 2007 +0200 (2007-05-08)
changeset 228791ec078cca386
parent 22878 ca2eb5eb615b
child 22880 424d6fb67513
add lemma Standard_hyperpow
src/HOL/Hyperreal/HyperDef.thy
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue May 08 21:02:26 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue May 08 23:52:15 2007 +0200
     1.3 @@ -429,6 +429,10 @@
     1.4    hyperpow_def [transfer_unfold]:
     1.5    "R pow N = ( *f2* op ^) R N"
     1.6  
     1.7 +lemma Standard_hyperpow [simp]:
     1.8 +  "\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard"
     1.9 +unfolding hyperpow_def by simp
    1.10 +
    1.11  lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)"
    1.12  by (simp add: hyperpow_def starfun2_star_n)
    1.13  
    1.14 @@ -537,7 +541,7 @@
    1.15  
    1.16  lemma hyperpow_SReal [simp]:
    1.17       "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
    1.18 -by (simp add: hyperpow_def Reals_eq_Standard)
    1.19 +by (simp add: Reals_eq_Standard)
    1.20  
    1.21  lemma hyperpow_zero_HNatInfinite [simp]:
    1.22       "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"