Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: _CoqProject Sprache: Isabelle

Original von: Isabelle^©

(*  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.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.