# Theory NSCA

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

section‹Non-Standard Complex Analysis›

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 ― ‹standard part map›
stc :: "hcomplex => hcomplex" where
"stc x = (SOME r. x ∈ HFinite ∧ r∈SComplex ∧ r ≈ x)"

subsection‹Closure Laws for SComplex, the Standard Complex Numbers›

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

"⟦x + y ∈ SComplex; y ∈ SComplex⟧ ⟹ x ∈ SComplex"
using Standard_diff by fastforce

lemma SReal_hcmod_hcomplex_of_complex [simp]:
"hcmod (hcomplex_of_complex r) ∈ ℝ"

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

lemma SReal_hcmod_SComplex: "x ∈ SComplex ⟹ hcmod x ∈ ℝ"

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

lemma hcomplex_of_complex_image:
"range hcomplex_of_complex = SComplex"

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"

subsection‹The 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"

lemma HFinite_bounded_hcmod:
"⟦x ∈ HFinite; y ≤ hcmod x; 0 ≤ y⟧ ⟹ y ∈ HFinite"
using HFinite_bounded HFinite_hcmod_iff by blast

subsection‹The Complex Infinitesimals form a Subring›

lemma Infinitesimal_hcmod_iff:
"(z ∈ Infinitesimal) = (hcmod z ∈ Infinitesimal)"

lemma HInfinite_hcmod_iff: "(z ∈ HInfinite) = (hcmod z ∈ HInfinite)"

lemma HFinite_diff_Infinitesimal_hcmod:
"x ∈ HFinite - Infinitesimal ⟹ hcmod x ∈ HFinite - Infinitesimal"

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‹The ``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)"

lemma approx_minus_zero_cancel_iff [simp]: "(-x ≈ 0) = (x ≈ 0)"

"u ≈ 0 ⟹ hcmod(x + u) - hcmod x ∈ Infinitesimal"

lemma approx_hcmod_add_hcmod: "u ≈ 0 ⟹ hcmod(x + u) ≈ hcmod x"

subsection‹Zero 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)"

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 \<^term>‹hRe›, \<^term>‹hIm› and \<^term>‹HComplex››

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"
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"
then show ?thesis
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"
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)"

lemma hcomplex_of_hypreal_approx_iff [simp]:
"(hcomplex_of_hypreal x ≈ hcomplex_of_hypreal z) = (x ≈ z)"

(* 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

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"

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)

"⟦x ∈ SComplex; e ∈ Infinitesimal⟧ ⟹ stc(x + e) = x"

"⟦x ∈ SComplex; e ∈ Infinitesimal⟧ ⟹ stc(e + x) = x"

"x ∈ HFinite ⟹ ∃e ∈ Infinitesimal. x = stc(x) + e"
by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])

"⟦x ∈ HFinite; y ∈ HFinite⟧ ⟹ stc (x + y) = stc(x) + stc(y)"

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"

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"

lemma SComplex_SReal_hcomplex_of_hypreal:
"x ∈ ℝ ⟹  hcomplex_of_hypreal x ∈ SComplex"

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