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