equal
deleted
inserted
replaced
95 by transfer (rule refl) |
95 by transfer (rule refl) |
96 |
96 |
97 lemma starfun_pow3: "\<And>R. ( *f* (\<lambda>r. r ^ n)) R = R pow hypnat_of_nat n" |
97 lemma starfun_pow3: "\<And>R. ( *f* (\<lambda>r. r ^ n)) R = R pow hypnat_of_nat n" |
98 by transfer (rule refl) |
98 by transfer (rule refl) |
99 |
99 |
100 text \<open>The @{term hypreal_of_hypnat} function as a nonstandard extension of |
100 text \<open>The \<^term>\<open>hypreal_of_hypnat\<close> function as a nonstandard extension of |
101 @{term real_of_nat}.\<close> |
101 \<^term>\<open>real_of_nat\<close>.\<close> |
102 lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat" |
102 lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat" |
103 by transfer (simp add: fun_eq_iff) |
103 by transfer (simp add: fun_eq_iff) |
104 |
104 |
105 lemma starfun_inverse_real_of_nat_eq: |
105 lemma starfun_inverse_real_of_nat_eq: |
106 "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x::nat. inverse (real x))) N = inverse (hypreal_of_hypnat N)" |
106 "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x::nat. inverse (real x))) N = inverse (hypreal_of_hypnat N)" |