Theory NSCA

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

sectionNon-Standard Complex Analysis

theory NSCA
imports NSComplex HTranscendental

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

definition ― ‹standard part map
  stc :: "hcomplex => hcomplex" where 
  "stc x = (SOME r. x  HFinite  rSComplex  r  x)"

subsectionClosure Laws for SComplex, the Standard Complex Numbers

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  
        r  Reals. hcmod x< r  r < hcmod y"
  by (simp add: SReal_dense SReal_hcmod_SComplex)

subsectionThe Finite Elements form a Subring

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

subsectionThe Complex Infinitesimals form a Subring

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)

subsectionThe ``Infinitely Close'' Relation

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

subsectionZero is the Only Infinitesimal Complex Number

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 Properties of termhRe, termhIm and termHComplex

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)

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

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 ..

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

subsectionTheorems About Monads

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

subsectionTheorems About Standard Part

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  
                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  
       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)