real.why

theory Real

  function zero : real = 0.0
  function one  : real = 1.0

  predicate (< ) real real
  predicate (> ) (x y : real) = y < x
  predicate (<=) (x y : real) = x < y \/ x = y

  clone export algebra.OrderedField with type t = real,
    function zero = zero, function one = one, predicate (<=) = (<=)

(*
  lemma sub_zero: forall x y:real. x - y = 0.0 -> x = y
*)

end

theory RealInfix

  use import Real

  function (+.) (x:real) (y:real) : real = x + y
  function (-.) (x:real) (y:real) : real = x - y
  function ( *.) (x:real) (y:real) : real = x * y
  function (/.) (x:real) (y:real) : real = x / y
  function (-._) (x:real) : real = - x

  predicate (<=.) (x:real) (y:real) = x <= y
  predicate (>=.) (x:real) (y:real) = x >= y
  predicate ( <.) (x:real) (y:real) = x < y
  predicate ( >.) (x:real) (y:real) = x > y

end

theory Abs

  use import Real

  function abs(x : real) : real = if x >= 0.0 then x else -x

  lemma Abs_le: forall x y:real. abs x <= y <-> -y <= x <= y

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

(*
  lemma Abs_zero: forall x:real. abs x = 0.0 -> x = 0.0
*)

end

theory MinMax

  use import Real

  function min real real : real
  function max real real : real

  axiom Max_is_ge   : forall x y:real. max x y >= x /\ max x y >= y
  axiom Max_is_some : forall x y:real. max x y = x \/ max x y = y
  axiom Min_is_le   : forall x y:real. min x y <= x /\ min x y <= y
  axiom Min_is_some : forall x y:real. min x y = x \/ min x y = y

end

theory FromInt

  use int.Int
  use import Real

  function 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

end

theory FromIntTest

  use import FromInt

  lemma Test1: from_int 2 = 2.0

end

theory Truncate

  use import Real
  use import FromInt

  (* truncate: rounds towards zero *)

  function truncate real : int

  axiom Truncate_int :
    forall i:int. truncate (from_int i) = i

  axiom Truncate_down_pos:
    forall x:real. x >= 0.0 ->
      from_int (truncate x) <= x < from_int (Int.(+) (truncate x) 1)

  axiom Truncate_up_neg:
    forall x:real. x <= 0.0 ->
      from_int (Int.(-) (truncate x) 1) < x <= from_int (truncate x)

  axiom Real_of_truncate:
    forall x:real. x - 1.0 <= from_int (truncate x) <= x + 1.0

  axiom Truncate_monotonic:
    forall x y:real. x <= y -> Int.(<=) (truncate x) (truncate y)

  axiom Truncate_monotonic_int1:
    forall x:real, i:int. x <= from_int i -> Int.(<=) (truncate x) i

  axiom Truncate_monotonic_int2:
    forall x:real, i:int. from_int i <= x -> Int.(<=) i (truncate x)

  (* roundings up and down *)

  function floor real : int
  function ceil real : int

  axiom Floor_int :
    forall i:int. floor (from_int i) = i

  axiom Ceil_int :
    forall i:int. floor (from_int i) = i

  axiom Floor_down:
    forall x:real. from_int (floor x) <= x < from_int (Int.(+) (floor x) 1)

  axiom Ceil_up:
    forall x:real. from_int (Int.(-) (ceil x) 1) < x <= from_int (ceil x)

  axiom Floor_monotonic:
    forall x y:real. x <= y -> Int.(<=) (floor x) (floor y)

  axiom Ceil_monotonic:
    forall x y:real. x <= y -> Int.(<=) (ceil x) (ceil y)

end


theory Square

  use import Real

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

  function 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 SquareTest

  use import Square

  lemma Sqrt_zero: sqrt 0.0 = 0.0
  lemma Sqrt_one: sqrt 1.0 = 1.0
  lemma Sqrt_four: sqrt 4.0 = 2.0

end

theory ExpLog

  use import Real

  function 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

  function e : real = exp 1.0

  function log real : real
  axiom Log_one : log 1.0 = 0.0
  axiom Log_mul :
    forall x y:real. x > 0.0 /\ y > 0.0 -> log (x*y) = log x + log y

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

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

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

end

theory ExpLogTest

  use import ExpLog

  lemma Log_e : log e = 1.0

end


theory Power

  use import Real
  use import Square
  use import ExpLog

  function 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

theory PowerTest

  use import Power

  lemma Pow_2_2 : pow 2.0 2.0 = 4.0

end



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

  use import Real
  use import Square
  use import Abs

  function cos real : real
  function 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

  function pi : real

  axiom Pi_interval:
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
   < pi <
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197

  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

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

end

theory TrigonometryTest

  use import Real
  use import Trigonometry
  use import Square

  lemma Cos_2_pi : cos (2.0 * pi) = 1.0
  lemma Sin_2_pi : sin (2.0 * pi) = 0.
  lemma Tan_pi_3 : tan (pi / 2.0) = sqrt 3.0
  lemma Atan_1   : atan 1.0 = pi / 4.0

end

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

  use import Real
  use import Square
  use import ExpLog

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

  function asinh (x : real) : real = log (x + sqrt (sqr x + 1.0))
  function acosh (x : real) : real
  axiom Acosh_def:
    forall x:real. x >= 1.0 -> acosh x = log (x + sqrt (sqr x - 1.0))
  function atanh (x : real) : real
  axiom Atanh_def:
    forall x:real. -1.0 < x < 1.0 -> atanh 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 Trigonometry

  function hypot (x y : real) : real = sqrt (sqr x + sqr y)
  function 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