src/HOL/Complex/CStar.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 21848 b35faf14a89f
permissions -rw-r--r--
avoid rebinding of existing facts;
     1 (*  Title       : CStar.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 2001 University of Edinburgh
     4 *)
     5 
     6 header{*Star-transforms in NSA, Extending Sets of Complex Numbers
     7       and Complex Functions*}
     8 
     9 theory CStar
    10 imports NSCA
    11 begin
    12 
    13 subsection{*Properties of the *-Transform Applied to Sets of Reals*}
    14 
    15 lemma STARC_hcomplex_of_complex_Int:
    16      "*s* X Int SComplex = hcomplex_of_complex ` X"
    17 by (auto simp add: Standard_def)
    18 
    19 lemma lemma_not_hcomplexA:
    20      "x \<notin> hcomplex_of_complex ` A ==> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"
    21 by auto
    22 
    23 subsection{*Theorems about Nonstandard Extensions of Functions*}
    24 
    25 lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z pow hypnat_of_nat n"
    26 by transfer (rule refl)
    27 
    28 lemma starfunCR_cmod: "*f* cmod = hcmod"
    29 by transfer (rule refl)
    30 
    31 subsection{*Internal Functions - Some Redundancy With *f* Now*}
    32 
    33 (** subtraction: ( *fn) - ( *gn) = *(fn - gn) **)
    34 (*
    35 lemma starfun_n_diff:
    36    "( *fn* f) z - ( *fn* g) z = ( *fn* (%i x. f i x - g i x)) z"
    37 apply (cases z)
    38 apply (simp add: starfun_n star_n_diff)
    39 done
    40 *)
    41 (** composition: ( *fn) o ( *gn) = *(fn o gn) **)
    42 
    43 lemma starfun_Re: "( *f* (\<lambda>x. Re (f x))) = (\<lambda>x. hRe (( *f* f) x))"
    44 by transfer (rule refl)
    45 
    46 lemma starfun_Im: "( *f* (\<lambda>x. Im (f x))) = (\<lambda>x. hIm (( *f* f) x))"
    47 by transfer (rule refl)
    48 
    49 lemma starfunC_eq_Re_Im_iff:
    50     "(( *f* f) x = z) = ((( *f* (%x. Re(f x))) x = hRe (z)) &
    51                           (( *f* (%x. Im(f x))) x = hIm (z)))"
    52 by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im)
    53 
    54 lemma starfunC_approx_Re_Im_iff:
    55     "(( *f* f) x @= z) = ((( *f* (%x. Re(f x))) x @= hRe (z)) &
    56                             (( *f* (%x. Im(f x))) x @= hIm (z)))"
    57 by (simp add: hcomplex_approx_iff starfun_Re starfun_Im)
    58 
    59 end