equal
deleted
inserted
replaced
113 |
113 |
114 text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of |
114 text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of |
115 @{term real_of_nat} *} |
115 @{term real_of_nat} *} |
116 |
116 |
117 lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat" |
117 lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat" |
118 by transfer (simp add: fun_eq_iff real_of_nat_def) |
118 by transfer (simp add: fun_eq_iff) |
119 |
119 |
120 lemma starfun_inverse_real_of_nat_eq: |
120 lemma starfun_inverse_real_of_nat_eq: |
121 "N \<in> HNatInfinite |
121 "N \<in> HNatInfinite |
122 ==> ( *f* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)" |
122 ==> ( *f* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)" |
123 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst]) |
123 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst]) |