Commit 8788a7a2 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

minor + define 'abs' via if-then-else

parent f1b3c54e
theory Int
logic zero : int = 0
logic one : int = 1
clone export algebra.UnitaryCommutativeRing with
type t = int, logic zero = zero, logic one = one
logic (< ) (int, int)
logic (<=) (x:int, y:int) = x < y or x = y
logic (> ) (x:int, y:int) = y < x
......@@ -9,11 +15,6 @@ theory Int
clone export relations.TotalOrder with
type t = int, logic rel = (<=)
logic zero : int = 0
logic one : int = 1
clone export algebra.UnitaryCommutativeRing with
type t = int, logic zero = zero, logic one = one
end
......
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:real, y:real) = x < y or x = y
logic (> )(x:real, y:real) = y < x
......@@ -10,21 +15,13 @@ theory Real
clone export relations.TotalOrder with
type t = real, logic rel = (<=)
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
logic abs(real) : real = if x >= 0.0 then x else -x
lemma Abs_le: forall x,y:real. abs(x) <= y <-> -y <= x <= y
......
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