theory Real 

  logic (< )(real, real)
  logic (<=)(real, real)
  logic (> )(real, real)
  logic (>=)(real, real)
  
  (* TODO : they are total order relations *)

  logic zero : real = 0.0
  logic one  : real = 1.0
  
  clone export algebra.Field with 
     type t = real, logic zero = zero, logic one = one
end 

theory Abs

  use import Real

  logic abs(real) : real

  axiom Pos: forall x:real. x >= 0.0 -> abs(x) = x
  axiom Neg: forall x:real. x <= 0.0 -> abs(x) = -x

  lemma Abs_le: forall x,y:real. abs(x) <= y <-> -y <= x and x <= y

  lemma Abs_pos: forall x:real. abs(x) >= 0.0

end

theory MinMax

  use import Real

  logic min(real,real) : real
  logic max(real,real) : real

  axiom Max_is_ge   : forall x,y:real. max(x,y) >= x and max(x,y) >= y
  axiom Max_is_some : forall x,y:real. max(x,y) = x or max(x,y) = y
  axiom Min_is_le   : forall x,y:real. min(x,y) <= x and min(x,y) <= y
  axiom Min_is_some : forall x,y:real. min(x,y) = x or min(x,y) = y

end

theory FromInt

  use int.Int
  use import Real

  logic from_int(int) : real

  axiom Zero: from_int(0) = 0.0
  axiom One: from_int(1) = 1.0

  axiom Add: 
    forall x,y:int. from_int(Int.(+)(x,y)) = from_int(x) + from_int(y)
  axiom Sub: 
    forall x,y:int. from_int(Int.(-)(x,y)) = from_int(x) - from_int(y)
  axiom Mul: 
    forall x,y:int. from_int(Int.(*)(x,y)) = from_int(x) * from_int(y)
  axiom Neg: 
    forall x,y:int. from_int(Int.(-_)(x)) = - from_int(x)

  lemma Test: from_int(2) = 2.0

end

theory Truncate

  (* TODO: truncate, floor, ceil *)

end

theory Square

  use import Real

  logic sqr(x:real):real = x * x

  logic sqrt(real):real

  axiom Sqrt_positive: 
    forall x:real. x >= 0.0 -> sqrt(x) >= 0.0

  axiom Sqrt_square:  
    forall x:real. x >= 0.0 -> sqr(sqrt(x)) = x

  axiom Square_sqrt: 
    forall x:real. x >= 0.0 -> sqrt(x*x) = x

end

theory ExpLog

  use import Real

  logic exp(real) : real
  axiom Exp_zero : exp(0.0) = 1.0
  axiom Exp_sum : forall x,y:real. exp(x+y) = exp(x)*exp(y)

  logic e : real = exp(1.0)

  logic log(real) : real
  axiom Log_one : log(1.0) = 0.0
  axiom Log_mul : 
    forall x,y:real. x > 0.0 and y > 0.0 -> log(x*y) = log(x)+log(y)

  axiom Log_exp: forall x:real. log(exp(x)) = x

  lemma Log_e : log(e) = 1.0

  axiom Exp_log: forall x:real. x > 0.0 -> exp(log(x)) = x

  logic log2(x:real) : real = log(x)/log(2.0)
  logic log10(x:real) : real = log(x)/log(10.0)

end

theory Power 

  use import Real
  use import Square
  use import ExpLog

  logic pow(real,real) : real

  axiom Pow_zero_y:
    forall y:real. y <> 0.0 -> pow(0.0,y) = 0.0

  axiom Pow_x_zero:
    forall x:real. x <> 0.0 -> pow(x,0.0) = 1.0

  axiom Pow_x_one:
    forall x:real. pow(x,1.0) = x

  axiom Pow_one_y:
    forall y:real. pow(1.0,y) = 1.0

  axiom Pow_x_two:
    forall x:real. pow(x,2.0) = sqr(x)

  axiom Pow_half:
    forall x:real. x >= 0.0 -> pow(x,0.5) = sqrt(x)  

  axiom Pow_exp_log:
    forall x,y:real. x > 0.0 -> pow(x,y) = exp(y*log(x))

end

(** Trigonometric functions 
    [http://en.wikipedia.org/wiki/Trigonometric_function]
*)
theory Trigonometric

  use import Real
  use import Square
  use import Abs

  logic cos(real) : real
  logic sin(real) : real

  axiom Pythagorean_identity:
    forall x:real. sqr(cos(x))+sqr(sin(x)) = 1.0

  lemma Cos_le_one: forall x:real. abs(cos(x)) <= 1.0
  lemma Sin_le_one: forall x:real. abs(sin(x)) <= 1.0

  axiom Cos_0: cos(0.0) = 1.0
  axiom Sin_0: sin(0.0) = 0.0

  logic pi : real

  axiom Cos_pi: cos(pi) = -1.0
  axiom Sin_pi: sin(pi) = 0.0

  axiom Cos_pi2: cos(0.5*pi) = 0.0
  axiom Sin_pi2: sin(0.5*pi) = 1.0

  axiom Cos_plus_pi: forall x:real. cos(x+pi) = -cos(x)
  axiom Sin_plus_pi: forall x:real. sin(x+pi) = -sin(x)

  axiom Cos_plus_pi2: forall x:real. cos(x+0.5*pi) = -sin(x)
  axiom Sin_plus_pi2: forall x:real. sin(x+0.5*pi) = cos(x)

  axiom Cos_neg:
    forall x:real. cos(-x) = cos(x)
  axiom Sin_neg:
    forall x:real. sin(-x) = -sin(x)
 
  axiom Cos_sum:
    forall x,y:real. cos(x+y) = cos(x)*cos(y)-sin(x)*sin(y)
  axiom Sin_sum:
    forall x,y:real. sin(x+y) = sin(x)*cos(y)+cos(x)*sin(y)

  logic tan(x:real) : real = sin(x) / cos(x)
  logic atan(real) : real
  axiom Tan_atan:
    forall x:real. tan(atan(x)) = x

end

(** hyperbolic functions 
    [http://en.wikipedia.org/wiki/Hyperbolic_function]
*)
theory Hyperbolic

  use import Real
  use import Square
  use import ExpLog

  logic sinh(x:real) : real = 0.5*(exp(x) - exp(-x))
  logic cosh(x:real) : real = 0.5*(exp(x) + exp(-x))
  logic tanh(x:real) : real = sinh(x) / cosh(x)

  logic arsinh(x:real) : real = log(x+sqrt(sqr(x)+1.0))
  logic arcosh(x:real) : real
  axiom Arcosh_def:
    forall x:real. x >= 1.0 -> arcosh(x) = log(x+sqrt(sqr(x)-1.0))
  logic artanh(x:real) : real
  axiom Artanh_def:
    forall x:real. -1.0 < x and x < 1.0 -> artanh(x) = 0.5*log((1.0+x)/(1.0-x))

end

(** polar coordinates: atan2, hypot 
    [http://en.wikipedia.org/wiki/Atan2]
*)
theory Polar

  use import Real
  use import Square
  use import Trigonometric

  logic hypot(x:real,y:real) : real = sqrt(sqr(x)+sqr(y))
  logic atan2(real,real) : real
 
  axiom X_from_polar:
    forall x,y:real. x = hypot(x,y)*cos(atan2(y,x))

  axiom Y_from_polar:
    forall x,y:real. y = hypot(x,y)*sin(atan2(y,x))
end