Commit d3345843 authored by MARCHE Claude's avatar MARCHE Claude

more reals

parent 20ad5462
......@@ -24,6 +24,8 @@ theory Abs
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
end
theory MinMax
......@@ -94,6 +96,8 @@ theory ExpLog
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 :
......@@ -101,8 +105,11 @@ theory ExpLog
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
......@@ -138,21 +145,89 @@ theory Power
end
theory Trigonometry
(** 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
(* sin, cos, tan, atan *)
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
(* cosh, sinh, tanh *)
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 *)
theory Polar
(* atan2, hypot *)
use import Real
use import Square
logic hypot(x:real,y:real) : real = sqrt(sqr(x)+sqr(y))
logic atan2(real,real) : real
end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment