theory Real logic zero : real = 0.0 logic one : real = 1.0 clone export algebra.Field with type t = real, logic zero = zero, logic one = one logic (< ) real real logic (<=) (x y : real) = x < y or x = y logic (> ) (x y : real) = y < x logic (>=) (x y : real) = y <= x clone export relations.TotalOrder with type t = real, logic rel = (<=) end theory Abs use import Real logic 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 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 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 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 : 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 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 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