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