src/HOL/Hyperreal/HyperPow.thy
changeset 21851 030f46b8c4b5
parent 21848 b35faf14a89f
equal deleted inserted replaced
21850:bf253f7075b4 21851:030f46b8c4b5
   200       ==> ALL n: Nats. r pow N \<le> r pow n"
   200       ==> ALL n: Nats. r pow N \<le> r pow n"
   201 by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff)
   201 by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff)
   202 
   202 
   203 lemma hyperpow_realpow:
   203 lemma hyperpow_realpow:
   204       "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
   204       "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
   205 by (simp add: star_of_def hypnat_of_nat_eq hyperpow)
   205 by transfer (rule refl)
   206 
   206 
   207 lemma hyperpow_SReal [simp]:
   207 lemma hyperpow_SReal [simp]:
   208      "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
   208      "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
   209 by (simp del: star_of_power add: hyperpow_realpow SReal_def)
   209 by (simp del: star_of_power add: hyperpow_realpow SReal_def)
   210 
   210