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