Quelle NSCA.thy Sprache: Isabelle

(*  Title:      HOL/Nonstandard_Analysis/NSCA.thy
    Author:     Jacques D. Fleuriot
    Copyright:  2001, 2002 University of Edinburgh
*)

section\<open>Non-Standard Complex Analysis\<close>

theory NSCA
imports NSComplex HTranscendental
begin

abbreviation
   (* standard complex numbers reagarded as an embedded subset of NS complex *)
   SComplex  :: "hcomplex set" where
   "SComplex \ Standard"

definition \<comment> \<open>standard part map\<close>
  stc :: "hcomplex => hcomplex" where
  "stc x = (SOME r. x \ HFinite \ r\SComplex \ r \ x)"

subsection\<open>Closure Laws for SComplex, the Standard Complex Numbers\<close>

lemma SComplex_minus_iff [simp]: "(-x \ SComplex) = (x \ SComplex)"
  using Standard_minus by fastforce

lemma SComplex_add_cancel:
  "\x + y \ SComplex; y \ SComplex\ \ x \ SComplex"
  using Standard_diff by fastforce

lemma SReal_hcmod_hcomplex_of_complex [simp]:
  "hcmod (hcomplex_of_complex r) \ \"
  by (simp add: Reals_eq_Standard)

lemma SReal_hcmod_numeral: "hcmod (numeral w ::hcomplex) \ \"
  by simp

lemma SReal_hcmod_SComplex: "x \ SComplex \ hcmod x \ \"
  by (simp add: Reals_eq_Standard)

lemma SComplex_divide_numeral:
  "r \ SComplex \ r/(numeral w::hcomplex) \ SComplex"
  by simp

lemma SComplex_UNIV_complex:
  "{x. hcomplex_of_complex x \ SComplex} = (UNIV::complex set)"
  by simp

lemma SComplex_iff: "(x \ SComplex) = (\y. x = hcomplex_of_complex y)"
  by (simp add: Standard_def image_def)

lemma hcomplex_of_complex_image:
  "range hcomplex_of_complex = SComplex"
  by (simp add: Standard_def)

lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV"
by (auto simp add: Standard_def image_def) (metis inj_star_of inv_f_f)

lemma SComplex_hcomplex_of_complex_image:
      "\\x. x \ P; P \ SComplex\ \ \Q. P = hcomplex_of_complex ` Q"
  by (metis Standard_def subset_imageE)

lemma SComplex_SReal_dense:
     "\x \ SComplex; y \ SComplex; hcmod x < hcmod y
      \<rbrakk> \<Longrightarrow> \<exists>r \<in> Reals. hcmod x< r \<and> r < hcmod y"
  by (simp add: SReal_dense SReal_hcmod_SComplex)

subsection\<open>The Finite Elements form a Subring\<close>

lemma HFinite_hcmod_hcomplex_of_complex [simp]:
  "hcmod (hcomplex_of_complex r) \ HFinite"
  by (auto intro!: SReal_subset_HFinite [THEN subsetD])

lemma HFinite_hcmod_iff [simp]: "hcmod x \ HFinite \ x \ HFinite"
  by (simp add: HFinite_def)

lemma HFinite_bounded_hcmod:
  "\x \ HFinite; y \ hcmod x; 0 \ y\ \ y \ HFinite"
  using HFinite_bounded HFinite_hcmod_iff by blast

subsection\<open>The Complex Infinitesimals form a Subring\<close>

lemma Infinitesimal_hcmod_iff:
  "(z \ Infinitesimal) = (hcmod z \ Infinitesimal)"
  by (simp add: Infinitesimal_def)

lemma HInfinite_hcmod_iff: "(z \ HInfinite) = (hcmod z \ HInfinite)"
  by (simp add: HInfinite_def)

lemma HFinite_diff_Infinitesimal_hcmod:
  "x \ HFinite - Infinitesimal \ hcmod x \ HFinite - Infinitesimal"
  by (simp add: Infinitesimal_hcmod_iff)

lemma hcmod_less_Infinitesimal:
  "\e \ Infinitesimal; hcmod x < hcmod e\ \ x \ Infinitesimal"
  by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff)

lemma hcmod_le_Infinitesimal:
  "\e \ Infinitesimal; hcmod x \ hcmod e\ \ x \ Infinitesimal"
  by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff)

subsection\<open>The ``Infinitely Close'' Relation\<close>

lemma approx_SComplex_mult_cancel_zero:
  "\a \ SComplex; a \ 0; a*x \ 0\ \ x \ 0"
  by (metis Infinitesimal_mult_disj SComplex_iff mem_infmal_iff star_of_Infinitesimal_iff_0 star_zero_def)

lemma approx_mult_SComplex1: "\a \ SComplex; x \ 0\ \ x*a \ 0"
  using SComplex_iff approx_mult_subst_star_of by fastforce

lemma approx_mult_SComplex2: "\a \ SComplex; x \ 0\ \ a*x \ 0"
  by (metis approx_mult_SComplex1 mult.commute)

lemma approx_mult_SComplex_zero_cancel_iff [simp]:
  "\a \ SComplex; a \ 0\ \ (a*x \ 0) = (x \ 0)"
  using approx_SComplex_mult_cancel_zero approx_mult_SComplex2 by blast

lemma approx_SComplex_mult_cancel:
     "\a \ SComplex; a \ 0; a*w \ a*z\ \ w \ z"
  by (metis approx_SComplex_mult_cancel_zero approx_minus_iff right_diff_distrib)

lemma approx_SComplex_mult_cancel_iff1 [simp]:
     "\a \ SComplex; a \ 0\ \ (a*w \ a*z) = (w \ z)"
  by (metis HFinite_star_of SComplex_iff approx_SComplex_mult_cancel approx_mult2)

(* TODO: generalize following theorems: hcmod -> hnorm *)

lemma approx_hcmod_approx_zero: "(x \ y) = (hcmod (y - x) \ 0)"
  by (simp add: Infinitesimal_hcmod_iff approx_def hnorm_minus_commute)

lemma approx_approx_zero_iff: "(x \ 0) = (hcmod x \ 0)"
by (simp add: approx_hcmod_approx_zero)

lemma approx_minus_zero_cancel_iff [simp]: "(-x \ 0) = (x \ 0)"
by (simp add: approx_def)

lemma Infinitesimal_hcmod_add_diff:
     "u \ 0 \ hcmod(x + u) - hcmod x \ Infinitesimal"
  by (metis add.commute add.left_neutral approx_add_right_iff approx_def approx_hnorm)

lemma approx_hcmod_add_hcmod: "u \ 0 \ hcmod(x + u) \ hcmod x"
  using Infinitesimal_hcmod_add_diff approx_def by blast

subsection\<open>Zero is the Only Infinitesimal Complex Number\<close>

lemma Infinitesimal_less_SComplex:
  "\x \ SComplex; y \ Infinitesimal; 0 < hcmod x\ \ hcmod y < hcmod x"
  by (auto intro: Infinitesimal_less_SReal SReal_hcmod_SComplex simp add: Infinitesimal_hcmod_iff)

lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}"
  by (auto simp add: Standard_def Infinitesimal_hcmod_iff)

lemma SComplex_Infinitesimal_zero:
  "\x \ SComplex; x \ Infinitesimal\ \ x = 0"
  using SComplex_iff by auto

lemma SComplex_HFinite_diff_Infinitesimal:
  "\x \ SComplex; x \ 0\ \ x \ HFinite - Infinitesimal"
  using SComplex_iff by auto

lemma numeral_not_Infinitesimal [simp]:
  "numeral w \ (0::hcomplex) \ (numeral w::hcomplex) \ Infinitesimal"
  by (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero])

lemma approx_SComplex_not_zero:
  "\y \ SComplex; x \ y; y\ 0\ \ x \ 0"
  by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]])

lemma SComplex_approx_iff:
  "\x \ SComplex; y \ SComplex\ \ (x \ y) = (x = y)"
  by (auto simp add: Standard_def)

lemma approx_unique_complex:
  "\r \ SComplex; s \ SComplex; r \ x; s \ x\ \ r = s"
  by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2)

subsection \<open>Properties of \<^term>\<open>hRe\<close>, \<^term>\<open>hIm\<close> and \<^term>\<open>HComplex\<close>\<close>

lemma abs_hRe_le_hcmod: "\x. \hRe x\ \ hcmod x"
  by transfer (rule abs_Re_le_cmod)

lemma abs_hIm_le_hcmod: "\x. \hIm x\ \ hcmod x"
  by transfer (rule abs_Im_le_cmod)

lemma Infinitesimal_hRe: "x \ Infinitesimal \ hRe x \ Infinitesimal"
  using Infinitesimal_hcmod_iff abs_hRe_le_hcmod hrabs_le_Infinitesimal by blast

lemma Infinitesimal_hIm: "x \ Infinitesimal \ hIm x \ Infinitesimal"
  using Infinitesimal_hcmod_iff abs_hIm_le_hcmod hrabs_le_Infinitesimal by blast

lemma Infinitesimal_HComplex:
  assumes x: "x \ Infinitesimal" and y: "y \ Infinitesimal"
  shows "HComplex x y \ Infinitesimal"
proof -
  have "hcmod (HComplex 0 y) \ Infinitesimal"
    by (simp add: hcmod_i y)
  moreover have "hcmod (hcomplex_of_hypreal x) \ Infinitesimal"
    using Infinitesimal_hcmod_iff Infinitesimal_of_hypreal_iff x by blast
  ultimately have "hcmod (HComplex x y) \ Infinitesimal"
    by (metis Infinitesimal_add Infinitesimal_hcmod_iff add.right_neutral hcomplex_of_hypreal_add_HComplex)
  then show ?thesis
    by (simp add: Infinitesimal_hnorm_iff)
qed

lemma hcomplex_Infinitesimal_iff:
  "(x \ Infinitesimal) \ (hRe x \ Infinitesimal \ hIm x \ Infinitesimal)"
  using Infinitesimal_HComplex Infinitesimal_hIm Infinitesimal_hRe by fastforce

lemma hRe_diff [simp]: "\x y. hRe (x - y) = hRe x - hRe y"
  by transfer simp

lemma hIm_diff [simp]: "\x y. hIm (x - y) = hIm x - hIm y"
  by transfer simp

lemma approx_hRe: "x \ y \ hRe x \ hRe y"
  unfolding approx_def by (drule Infinitesimal_hRe) simp

lemma approx_hIm: "x \ y \ hIm x \ hIm y"
  unfolding approx_def by (drule Infinitesimal_hIm) simp

lemma approx_HComplex:
  "\a \ b; c \ d\ \ HComplex a c \ HComplex b d"
  unfolding approx_def by (simp add: Infinitesimal_HComplex)

lemma hcomplex_approx_iff:
  "(x \ y) = (hRe x \ hRe y \ hIm x \ hIm y)"
  unfolding approx_def by (simp add: hcomplex_Infinitesimal_iff)

lemma HFinite_hRe: "x \ HFinite \ hRe x \ HFinite"
  using HFinite_bounded_hcmod abs_ge_zero abs_hRe_le_hcmod by blast

lemma HFinite_hIm: "x \ HFinite \ hIm x \ HFinite"
  using HFinite_bounded_hcmod abs_ge_zero abs_hIm_le_hcmod by blast

lemma HFinite_HComplex:
  assumes "x \ HFinite" "y \ HFinite"
  shows "HComplex x y \ HFinite"
proof -
  have "HComplex x 0 \ HFinite" "HComplex 0 y \ HFinite"
    using HFinite_hcmod_iff assms hcmod_i by fastforce+
  then have "HComplex x 0 + HComplex 0 y \ HFinite"
    using HFinite_add by blast
  then show ?thesis
    by simp
qed

lemma hcomplex_HFinite_iff:
  "(x \ HFinite) = (hRe x \ HFinite \ hIm x \ HFinite)"
  using HFinite_HComplex HFinite_hIm HFinite_hRe by fastforce

lemma hcomplex_HInfinite_iff:
  "(x \ HInfinite) = (hRe x \ HInfinite \ hIm x \ HInfinite)"
  by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff)

lemma hcomplex_of_hypreal_approx_iff [simp]:
  "(hcomplex_of_hypreal x \ hcomplex_of_hypreal z) = (x \ z)"
  by (simp add: hcomplex_approx_iff)

(* Here we go - easy proof now!! *)
lemma stc_part_Ex:
  assumes "x \ HFinite"
  shows "\t \ SComplex. x \ t"
proof -
  let ?t = "HComplex (st (hRe x)) (st (hIm x))"
  have "?t \ SComplex"
    using HFinite_hIm HFinite_hRe Reals_eq_Standard assms st_SReal by auto
  moreover have "x \ ?t"
    by (simp add: HFinite_hIm HFinite_hRe assms hcomplex_approx_iff st_HFinite st_eq_approx)
  ultimately show ?thesis ..
qed

lemma stc_part_Ex1: "x \ HFinite \ \!t. t \ SComplex \ x \ t"
  using approx_sym approx_unique_complex stc_part_Ex by blast

subsection\<open>Theorems About Monads\<close>

lemma monad_zero_hcmod_iff: "(x \ monad 0) = (hcmod x \ monad 0)"
  by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff)

subsection\<open>Theorems About Standard Part\<close>

lemma stc_approx_self: "x \ HFinite \ stc x \ x"
  unfolding stc_def
  by (metis (no_types, lifting) approx_reorient someI_ex stc_part_Ex1)

lemma stc_SComplex: "x \ HFinite \ stc x \ SComplex"
  unfolding stc_def
  by (metis (no_types, lifting) SComplex_iff approx_sym someI_ex stc_part_Ex)

lemma stc_HFinite: "x \ HFinite \ stc x \ HFinite"
  by (erule stc_SComplex [THEN Standard_subset_HFinite [THEN subsetD]])

lemma stc_unique: "\y \ SComplex; y \ x\ \ stc x = y"
  by (metis SComplex_approx_iff SComplex_iff approx_monad_iff approx_star_of_HFinite stc_SComplex stc_approx_self)

lemma stc_SComplex_eq [simp]: "x \ SComplex \ stc x = x"
  by (simp add: stc_unique)

lemma stc_eq_approx:
  "\x \ HFinite; y \ HFinite; stc x = stc y\ \ x \ y"
  by (auto dest!: stc_approx_self elim!: approx_trans3)

lemma approx_stc_eq:
     "\x \ HFinite; y \ HFinite; x \ y\ \ stc x = stc y"
  by (metis approx_sym approx_trans3 stc_part_Ex1 stc_unique)

lemma stc_eq_approx_iff:
  "\x \ HFinite; y \ HFinite\ \ (x \ y) = (stc x = stc y)"
  by (blast intro: approx_stc_eq stc_eq_approx)

lemma stc_Infinitesimal_add_SComplex:
  "\x \ SComplex; e \ Infinitesimal\ \ stc(x + e) = x"
  using Infinitesimal_add_approx_self stc_unique by blast

lemma stc_Infinitesimal_add_SComplex2:
  "\x \ SComplex; e \ Infinitesimal\ \ stc(e + x) = x"
  using Infinitesimal_add_approx_self2 stc_unique by blast

lemma HFinite_stc_Infinitesimal_add:
  "x \ HFinite \ \e \ Infinitesimal. x = stc(x) + e"
  by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])

lemma stc_add:
  "\x \ HFinite; y \ HFinite\ \ stc (x + y) = stc(x) + stc(y)"
  by (simp add: stc_unique stc_SComplex stc_approx_self approx_add)

lemma stc_zero: "stc 0 = 0"
  by simp

lemma stc_one: "stc 1 = 1"
  by simp

lemma stc_minus: "y \ HFinite \ stc(-y) = -stc(y)"
  by (simp add: stc_unique stc_SComplex stc_approx_self approx_minus)

lemma stc_diff:
  "\x \ HFinite; y \ HFinite\ \ stc (x-y) = stc(x) - stc(y)"
  by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff)

lemma stc_mult:
  "\x \ HFinite; y \ HFinite\
               \<Longrightarrow> stc (x * y) = stc(x) * stc(y)"
  by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite)

lemma stc_Infinitesimal: "x \ Infinitesimal \ stc x = 0"
  by (simp add: stc_unique mem_infmal_iff)

lemma stc_not_Infinitesimal: "stc(x) \ 0 \ x \ Infinitesimal"
  by (fast intro: stc_Infinitesimal)

lemma stc_inverse:
  "\x \ HFinite; stc x \ 0\ \ stc(inverse x) = inverse (stc x)"
  by (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse stc_not_Infinitesimal)

lemma stc_divide [simp]:
  "\x \ HFinite; y \ HFinite; stc y \ 0\
      \<Longrightarrow> stc(x/y) = (stc x) / (stc y)"
  by (simp add: divide_inverse stc_mult stc_not_Infinitesimal HFinite_inverse stc_inverse)

lemma stc_idempotent [simp]: "x \ HFinite \ stc(stc(x)) = stc(x)"
  by (blast intro: stc_HFinite stc_approx_self approx_stc_eq)

lemma HFinite_HFinite_hcomplex_of_hypreal:
  "z \ HFinite \ hcomplex_of_hypreal z \ HFinite"
  by (simp add: hcomplex_HFinite_iff)

lemma SComplex_SReal_hcomplex_of_hypreal:
     "x \ \ \ hcomplex_of_hypreal x \ SComplex"
  by (simp add: Reals_eq_Standard)

lemma stc_hcomplex_of_hypreal:
"z \ HFinite \ stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
  by (simp add: SComplex_SReal_hcomplex_of_hypreal st_SReal st_approx_self stc_unique)

lemma hmod_stc_eq:
  assumes "x \ HFinite"
  shows "hcmod(stc x) = st(hcmod x)"
    by (metis SReal_hcmod_SComplex approx_HFinite approx_hnorm assms st_unique stc_SComplex_eq stc_eq_approx_iff stc_part_Ex)

lemma Infinitesimal_hcnj_iff [simp]:
  "(hcnj z \ Infinitesimal) \ (z \ Infinitesimal)"
  by (simp add: Infinitesimal_hcmod_iff)

end

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.