src/HOL/Complex/Complex.thy
author paulson
Mon May 05 18:22:31 2003 +0200 (2003-05-05)
changeset 13957 10dbf16be15f
child 14323 27724f528f82
permissions -rw-r--r--
new session Complex for the complex numbers
paulson@13957
     1
(*  Title:       Complex.thy
paulson@13957
     2
    Author:      Jacques D. Fleuriot
paulson@13957
     3
    Copyright:   2001 University of Edinburgh
paulson@13957
     4
    Description: Complex numbers
paulson@13957
     5
*)
paulson@13957
     6
paulson@13957
     7
Complex = HLog + 
paulson@13957
     8
paulson@13957
     9
typedef complex = "{p::(real*real). True}"
paulson@13957
    10
paulson@13957
    11
instance
paulson@13957
    12
  complex :: {ord,zero,one,plus,minus,times,power,inverse}
paulson@13957
    13
paulson@13957
    14
consts
paulson@13957
    15
  "ii"    :: complex        ("ii") 
paulson@13957
    16
paulson@13957
    17
constdefs
paulson@13957
    18
paulson@13957
    19
  (*--- real and Imaginary parts ---*)
paulson@13957
    20
  
paulson@13957
    21
  Re :: complex => real
paulson@13957
    22
  "Re(z) == fst(Rep_complex z)"
paulson@13957
    23
paulson@13957
    24
  Im :: complex => real
paulson@13957
    25
  "Im(z) == snd(Rep_complex z)"
paulson@13957
    26
paulson@13957
    27
  (*----------- modulus ------------*)
paulson@13957
    28
paulson@13957
    29
  cmod :: complex => real
paulson@13957
    30
  "cmod z == sqrt(Re(z) ^ 2 + Im(z) ^ 2)"			      
paulson@13957
    31
paulson@13957
    32
  (*----- injection from reals -----*)			   
paulson@13957
    33
 
paulson@13957
    34
  complex_of_real :: real => complex
paulson@13957
    35
  "complex_of_real r == Abs_complex(r,0::real)"
paulson@13957
    36
				    
paulson@13957
    37
  (*------- complex conjugate ------*)
paulson@13957
    38
paulson@13957
    39
  cnj :: complex => complex
paulson@13957
    40
  "cnj z == Abs_complex(Re z, -Im z)"
paulson@13957
    41
paulson@13957
    42
  (*------------ Argand -------------*)		       
paulson@13957
    43
paulson@13957
    44
  sgn :: complex => complex
paulson@13957
    45
  "sgn z == z / complex_of_real(cmod z)"
paulson@13957
    46
paulson@13957
    47
  arg :: complex => real
paulson@13957
    48
  "arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a <= pi"
paulson@13957
    49
									  
paulson@13957
    50
defs
paulson@13957
    51
paulson@13957
    52
  complex_zero_def
paulson@13957
    53
  "0 == Abs_complex(0::real,0)"
paulson@13957
    54
paulson@13957
    55
  complex_one_def
paulson@13957
    56
  "1 == Abs_complex(1,0::real)"
paulson@13957
    57
paulson@13957
    58
  (*------ imaginary unit ----------*)					 
paulson@13957
    59
			      
paulson@13957
    60
  i_def 
paulson@13957
    61
  "ii == Abs_complex(0::real,1)"
paulson@13957
    62
paulson@13957
    63
  (*----------- negation -----------*)
paulson@13957
    64
				     
paulson@13957
    65
  complex_minus_def
paulson@13957
    66
  "- (z::complex) == Abs_complex(-Re z, -Im z)"				     
paulson@13957
    67
paulson@13957
    68
  
paulson@13957
    69
  (*----------- inverse -----------*)
paulson@13957
    70
  complex_inverse_def
paulson@13957
    71
  "inverse (z::complex) == Abs_complex(Re(z)/(Re(z) ^ 2 + Im(z) ^ 2),
paulson@13957
    72
                            -Im(z)/(Re(z) ^ 2 + Im(z) ^ 2))"
paulson@13957
    73
paulson@13957
    74
  complex_add_def
paulson@13957
    75
  "w + (z::complex) == Abs_complex(Re(w) + Re(z),Im(w) + Im(z))"
paulson@13957
    76
paulson@13957
    77
  complex_diff_def
paulson@13957
    78
  "w - (z::complex) == w + -(z::complex)"
paulson@13957
    79
paulson@13957
    80
  complex_mult_def
paulson@13957
    81
  "w * (z::complex) == Abs_complex(Re(w) * Re(z) - Im(w) * Im(z),
paulson@13957
    82
			Re(w) * Im(z) + Im(w) * Re(z))"
paulson@13957
    83
paulson@13957
    84
paulson@13957
    85
  (*----------- division ----------*)
paulson@13957
    86
  complex_divide_def
paulson@13957
    87
  "w / (z::complex) == w * inverse z"
paulson@13957
    88
  
paulson@13957
    89
paulson@13957
    90
primrec
paulson@13957
    91
     complexpow_0   "z ^ 0       = complex_of_real 1"
paulson@13957
    92
     complexpow_Suc "z ^ (Suc n) = (z::complex) * (z ^ n)"
paulson@13957
    93
paulson@13957
    94
paulson@13957
    95
constdefs
paulson@13957
    96
paulson@13957
    97
  (* abbreviation for (cos a + i sin a) *)
paulson@13957
    98
  cis :: real => complex
paulson@13957
    99
  "cis a == complex_of_real(cos a) + ii * complex_of_real(sin a)"
paulson@13957
   100
paulson@13957
   101
  (* abbreviation for r*(cos a + i sin a) *)
paulson@13957
   102
  rcis :: [real, real] => complex
paulson@13957
   103
  "rcis r a == complex_of_real r * cis a"
paulson@13957
   104
paulson@13957
   105
  (* e ^ (x + iy) *)
paulson@13957
   106
  expi :: complex => complex
paulson@13957
   107
  "expi z == complex_of_real(exp (Re z)) * cis (Im z)"
paulson@13957
   108
   
paulson@13957
   109
end
paulson@13957
   110
paulson@13957
   111