(* Title: HOL/Nonstandard_Analysis/CStar.thy
Author: Jacques D. Fleuriot
Copyright: 2001 University of Edinburgh
*)
section \<open>Star-transforms in NSA, Extending Sets of Complex Numbers and Complex Functions\<close>
theory CStar
imports NSCA
begin
subsection \<open>Properties of the \<open>*\<close>-Transform Applied to Sets of Reals\<close>
lemma STARC_hcomplex_of_complex_Int: "*s* X \ SComplex = hcomplex_of_complex ` X"
by (auto simp: Standard_def)
lemma lemma_not_hcomplexA: "x \ hcomplex_of_complex ` A \ \y \ A. x \ hcomplex_of_complex y"
by auto
subsection \<open>Theorems about Nonstandard Extensions of Functions\<close>
lemma starfunC_hcpow: "\Z. ( *f* (\z. z ^ n)) Z = Z pow hypnat_of_nat n"
by transfer (rule refl)
lemma starfunCR_cmod: "*f* cmod = hcmod"
by transfer (rule refl)
subsection \<open>Internal Functions - Some Redundancy With \<open>*f*\<close> Now\<close>
(** subtraction: ( *fn) - ( *gn) = *(fn - gn) **)
(*
lemma starfun_n_diff:
"( *fn* f) z - ( *fn* g) z = ( *fn* (\<lambda>i x. f i x - g i x)) z"
apply (cases z)
apply (simp add: starfun_n star_n_diff)
done
*)
(** composition: ( *fn) o ( *gn) = *(fn o gn) **)
lemma starfun_Re: "( *f* (\x. Re (f x))) = (\x. hRe (( *f* f) x))"
by transfer (rule refl)
lemma starfun_Im: "( *f* (\x. Im (f x))) = (\x. hIm (( *f* f) x))"
by transfer (rule refl)
lemma starfunC_eq_Re_Im_iff:
"( *f* f) x = z \ ( *f* (\x. Re (f x))) x = hRe z \ ( *f* (\x. Im (f x))) x = hIm z"
by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im)
lemma starfunC_approx_Re_Im_iff:
"( *f* f) x \ z \ ( *f* (\x. Re (f x))) x \ hRe z \ ( *f* (\x. Im (f x))) x \ hIm z"
by (simp add: hcomplex_approx_iff starfun_Re starfun_Im)
end
¤ Dauer der Verarbeitung: 0.25 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
