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 <= 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) 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 *) logic 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 *) logic floor(real) : int logic 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 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 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 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 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 ExpLogTest use import ExpLog lemma Log_e : log(e) = 1.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 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 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 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 : cos(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 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 < 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 Trigonometry 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