src/HOL/Complex/NSComplex.thy
author paulson
Mon May 05 18:22:31 2003 +0200 (2003-05-05)
changeset 13957 10dbf16be15f
child 14314 314da085adf3
permissions -rw-r--r--
new session Complex for the complex numbers
paulson@13957
     1
(*  Title:       NSComplex.thy
paulson@13957
     2
    Author:      Jacques D. Fleuriot
paulson@13957
     3
    Copyright:   2001  University of Edinburgh
paulson@13957
     4
    Description: Nonstandard Complex numbers
paulson@13957
     5
*)
paulson@13957
     6
paulson@13957
     7
NSComplex = NSInduct + 
paulson@13957
     8
paulson@13957
     9
constdefs
paulson@13957
    10
    hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
paulson@13957
    11
    "hcomplexrel == {p. EX X Y. p = ((X::nat=>complex),Y) & 
paulson@13957
    12
                        {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
paulson@13957
    13
paulson@13957
    14
typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel"      (quotient_def)
paulson@13957
    15
paulson@13957
    16
instance
paulson@13957
    17
   hcomplex  :: {zero,one,plus,times,minus,power,inverse}
paulson@13957
    18
  
paulson@13957
    19
defs
paulson@13957
    20
  hcomplex_zero_def 
paulson@13957
    21
  "0 == Abs_hcomplex(hcomplexrel `` {%n. (0::complex)})"
paulson@13957
    22
  
paulson@13957
    23
  hcomplex_one_def  
paulson@13957
    24
  "1 == Abs_hcomplex(hcomplexrel `` {%n. (1::complex)})"
paulson@13957
    25
paulson@13957
    26
paulson@13957
    27
  hcomplex_minus_def
paulson@13957
    28
  "- z == Abs_hcomplex(UN X: Rep_hcomplex(z). hcomplexrel `` {%n::nat. - (X n)})"
paulson@13957
    29
paulson@13957
    30
  hcomplex_diff_def
paulson@13957
    31
  "w - z == w + -(z::hcomplex)"
paulson@13957
    32
  
paulson@13957
    33
constdefs
paulson@13957
    34
paulson@13957
    35
  hcomplex_of_complex :: complex => hcomplex
paulson@13957
    36
  "hcomplex_of_complex z == Abs_hcomplex(hcomplexrel `` {%n. z})"
paulson@13957
    37
 
paulson@13957
    38
  hcinv  :: hcomplex => hcomplex
paulson@13957
    39
  "inverse(P)   == Abs_hcomplex(UN X: Rep_hcomplex(P). 
paulson@13957
    40
                    hcomplexrel `` {%n. inverse(X n)})"
paulson@13957
    41
paulson@13957
    42
  (*--- real and Imaginary parts ---*)
paulson@13957
    43
  
paulson@13957
    44
  hRe :: hcomplex => hypreal
paulson@13957
    45
  "hRe(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Re (X n)})"
paulson@13957
    46
paulson@13957
    47
  hIm :: hcomplex => hypreal
paulson@13957
    48
  "hIm(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Im (X n)})"   
paulson@13957
    49
paulson@13957
    50
paulson@13957
    51
  (*----------- modulus ------------*)
paulson@13957
    52
paulson@13957
    53
  hcmod :: hcomplex => hypreal
paulson@13957
    54
  "hcmod z == Abs_hypreal(UN X: Rep_hcomplex(z).
paulson@13957
    55
			  hyprel `` {%n. cmod (X n)})"
paulson@13957
    56
paulson@13957
    57
  (*------ imaginary unit ----------*)					 
paulson@13957
    58
			      
paulson@13957
    59
  iii :: hcomplex			      
paulson@13957
    60
  "iii == Abs_hcomplex(hcomplexrel `` {%n. ii})"
paulson@13957
    61
paulson@13957
    62
  (*------- complex conjugate ------*)
paulson@13957
    63
paulson@13957
    64
  hcnj :: hcomplex => hcomplex
paulson@13957
    65
  "hcnj z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. cnj (X n)})"
paulson@13957
    66
paulson@13957
    67
  (*------------ Argand -------------*)		       
paulson@13957
    68
paulson@13957
    69
  hsgn :: hcomplex => hcomplex
paulson@13957
    70
  "hsgn z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. sgn(X n)})"
paulson@13957
    71
paulson@13957
    72
  harg :: hcomplex => hypreal
paulson@13957
    73
  "harg z == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. arg(X n)})"
paulson@13957
    74
paulson@13957
    75
  (* abbreviation for (cos a + i sin a) *)
paulson@13957
    76
  hcis :: hypreal => hcomplex
paulson@13957
    77
  "hcis a == Abs_hcomplex(UN X:Rep_hypreal(a). hcomplexrel `` {%n. cis (X n)})"
paulson@13957
    78
paulson@13957
    79
  (* abbreviation for r*(cos a + i sin a) *)
paulson@13957
    80
  hrcis :: [hypreal, hypreal] => hcomplex
paulson@13957
    81
  "hrcis r a == hcomplex_of_hypreal r * hcis a"
paulson@13957
    82
paulson@13957
    83
  (*----- injection from hyperreals -----*)			   
paulson@13957
    84
 
paulson@13957
    85
  hcomplex_of_hypreal :: hypreal => hcomplex
paulson@13957
    86
  "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_hypreal(r).
paulson@13957
    87
			       hcomplexrel `` {%n. complex_of_real (X n)})"
paulson@13957
    88
paulson@13957
    89
  (*------------ e ^ (x + iy) ------------*)
paulson@13957
    90
paulson@13957
    91
  hexpi :: hcomplex => hcomplex
paulson@13957
    92
  "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
paulson@13957
    93
   
paulson@13957
    94
paulson@13957
    95
defs  
paulson@13957
    96
paulson@13957
    97
paulson@13957
    98
  (*----------- division ----------*)
paulson@13957
    99
paulson@13957
   100
  hcomplex_divide_def
paulson@13957
   101
  "w / (z::hcomplex) == w * inverse z"
paulson@13957
   102
    
paulson@13957
   103
  hcomplex_add_def
paulson@13957
   104
  "w + z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
paulson@13957
   105
		      hcomplexrel `` {%n. X n + Y n})"
paulson@13957
   106
paulson@13957
   107
  hcomplex_mult_def
paulson@13957
   108
  "w * z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
paulson@13957
   109
		      hcomplexrel `` {%n. X n * Y n})"    
paulson@13957
   110
paulson@13957
   111
paulson@13957
   112
primrec
paulson@13957
   113
     hcomplexpow_0   "z ^ 0       = 1"
paulson@13957
   114
     hcomplexpow_Suc "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
paulson@13957
   115
paulson@13957
   116
paulson@13957
   117
consts
paulson@13957
   118
  "hcpow"  :: [hcomplex,hypnat] => hcomplex     (infixr 80)
paulson@13957
   119
paulson@13957
   120
defs
paulson@13957
   121
  (* hypernatural powers of nonstandard complex numbers *)
paulson@13957
   122
  hcpow_def
paulson@13957
   123
  "(z::hcomplex) hcpow (n::hypnat) 
paulson@13957
   124
      == Abs_hcomplex(UN X:Rep_hcomplex(z). UN Y: Rep_hypnat(n).
paulson@13957
   125
             hcomplexrel `` {%n. (X n) ^ (Y n)})"
paulson@13957
   126
paulson@13957
   127
end