equal
deleted
inserted
replaced
45 |
45 |
46 instantiation star :: (scaleR) scaleR |
46 instantiation star :: (scaleR) scaleR |
47 begin |
47 begin |
48 |
48 |
49 definition |
49 definition |
50 star_scaleR_def [transfer_unfold, code func del]: "scaleR r \<equiv> *f* (scaleR r)" |
50 star_scaleR_def [transfer_unfold, code del]: "scaleR r \<equiv> *f* (scaleR r)" |
51 |
51 |
52 instance .. |
52 instance .. |
53 |
53 |
54 end |
54 end |
55 |
55 |
111 |
111 |
112 subsection {* Injection from @{typ hypreal} *} |
112 subsection {* Injection from @{typ hypreal} *} |
113 |
113 |
114 definition |
114 definition |
115 of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where |
115 of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where |
116 [transfer_unfold, code func del]: "of_hypreal = *f* of_real" |
116 [transfer_unfold, code del]: "of_hypreal = *f* of_real" |
117 |
117 |
118 lemma Standard_of_hypreal [simp]: |
118 lemma Standard_of_hypreal [simp]: |
119 "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard" |
119 "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard" |
120 by (simp add: of_hypreal_def) |
120 by (simp add: of_hypreal_def) |
121 |
121 |
426 *) |
426 *) |
427 |
427 |
428 subsection{*Powers with Hypernatural Exponents*} |
428 subsection{*Powers with Hypernatural Exponents*} |
429 |
429 |
430 definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where |
430 definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where |
431 hyperpow_def [transfer_unfold, code func del]: "R pow N = ( *f2* op ^) R N" |
431 hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N" |
432 (* hypernatural powers of hyperreals *) |
432 (* hypernatural powers of hyperreals *) |
433 |
433 |
434 lemma Standard_hyperpow [simp]: |
434 lemma Standard_hyperpow [simp]: |
435 "\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard" |
435 "\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard" |
436 unfolding hyperpow_def by simp |
436 unfolding hyperpow_def by simp |