Complex

spec
       BasicComplex = 
       BasicReal 
then
       free
              type Complex ::= complex(real,imag:Real) 
       sort
              Real < Complex 
       ops
               i : 
                                  Complex; 
               __i: 
                                  Real -> Complex; 
               r, phi : 
                                  Complex -> Real; 
               +__,-__ : 
                                  Complex -> Complex; 
               __+__,__-__,__*__ : 
                                  Complex × Complex -> Complex; 
               __/__,__^ __ : 
                                  Complex × Complex ->? Complex; 
               exp,sqrt : 
                                  Complex -> Complex; 
               ln : 
                                  Complex ->? Complex; 
               sin, cos, sinh, cosh : 
                                  Complex -> Complex; 
               tan, cot, tanh, coth : 
                                  Complex ->? Complex; 

       vars
              t,u,v,w:Real; x,y: Complex 
       %%              Embedding of the reals: 
       .              t = complex(t,0) 
       %%              i: 
       .              i = complex(0,1) 
       .              t i = complex(0,t) 
       %%              Polar coordinates of a complex number: 
       .              r(complex(t,u)) = sqrt(t2+u2) 
       .              phi(complex(t,u)) = arctan(u/t) if not t=0 
       .              phi(complex(t,u)) = sign(u)*pi/2 if t=0 
       %%              arithmetic functions: 
       .              +x = x 
       .              -complex(t,u) = complex(-t,-u) 
       .              complex(t,u)+complex(v,w) = complex(t+v,u+w) 
       .              complex(t,u)-complex(v,w) = complex(t-v,u-w) 
       .              complex(t,u)*complex(v,w) = complex(t*v-u*w,t*w+v*u) 
       .              def x/y <=> not y=0 
       .               complex(t,u)/complex(v,w) = 
               complex( (t*v+u*w)/(v^ 2+w^ 2), (v*u-t*w)/(v^ 2+w^ 2)) 

       %%              exponential function and logarithm (using Euler's formula): 
       .              exp(complex(t,u)) = exp(t) * complex(cos(u),sin(u)) 
       .              def ln(x) <=> not x=0 
       .              ln(x) = complex(ln(r(x)),phi(x)) if def ln(x) 
       %%              power und square root defined using exp and ln: 
       .              def x ^ y <=> not x=0 
       .              x ^ y = exp(ln(x)*y) 
       .              sqrt(x) = x^ (1/2) if not x=0 
       .              sqrt(0) = 0 
       %%              trigonometric functions: 
       .              sin(complex(t,u)) = complex(sin(t)*cosh(u),cos(t)*sinh(u)) 
       .              cos(complex(t,u)) = complex(cos(t)*cosh(u),-sin(t)*sinh(u)) 
       .               tan(complex(t,u)) = 
               complex( sin(2*t), sinh(2*u))/(cos(2*t)+cosh(2*u)) 

       .               cot(complex(t,u)) = 
               complex( -sin(2*t), sinh(2*u))/(cos(2*t)-cosh(2*u)) 

       %%              hyperbolic functions: 
       .              sinh(complex(t,u)) = complex(sinh(t)*cos(u),cosh(t)*sin(u)) 
       .              cosh(complex(t,u)) = complex(cosh(t)*cos(u),sinh(t)*sin(u)) 
       .               tanh(complex(t,u)) = 
               complex( sinh(2*t), sin(2*u))/(cosh(2*t)+cos(2*u)) 

       .               coth(complex(t,u)) = 
               complex( sinh(2*t), -sin(2*u))/(cosh(2*t)-cos(2*u)) 

hide
       op complex 
end