Commit efcc1da1 authored by Andrei Paskevich's avatar Andrei Paskevich

add axioms for totally ordered rings and fields

parent 5efa52de
......@@ -59,7 +59,7 @@ parameter get_num_classes :
parameter rand : s:int -> {} int { 0 <= result < s }
{
axiom Ineq1 :
lemma Ineq1 :
forall n x y:int. 0 <= n -> 0 <= x < n -> 0 <= y < n -> 0 <= x*n+y < n*n
}
......
......@@ -72,9 +72,39 @@ theory UnitaryCommutativeRing
axiom NonTrivialRing : zero <> one
end
theory OrderedUnitaryCommutativeRing
clone export UnitaryCommutativeRing
logic (<=) t t
logic (>=) (x y : t) = y <= x
clone export relations.TotalOrder with type t = t, logic rel = (<=)
axiom CompatOrderAdd : forall x y z : t. x <= y -> x + z <= y + z
axiom CompatOrderMult : forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
(*
lemma InvMult : forall x y : t. (-x) * y = - (x * y) = x * (-y)
lemma InvSquare : forall x : t. x * x = (-x) * (-x)
lemma ZeroMult : forall x : t. x * zero = zero = zero * x
lemma SquareNonNeg1 : forall x : t. x <= zero -> zero <= x * x
lemma SquareNonNeg : forall x : t. zero <= x * x
lemma ZeroLessOne : zero <= one
*)
end
theory Field
clone export UnitaryCommutativeRing
logic inv t : t
axiom Inverse : forall x:t. x <> zero -> x * inv x = one
logic (/) (x y : t) : t = x * inv y
end
theory OrderedField
clone export Field
logic (<=) t t
logic (>=) (x y : t) = y <= x
clone export relations.TotalOrder with type t = t, logic rel = (<=)
axiom CompatOrderAdd : forall x y z : t. x <= y -> x + z <= y + z
axiom CompatOrderMult : forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
end
......@@ -4,16 +4,12 @@ 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 y : int) = x < y or x = y
logic (> ) (x y : int) = y < x
logic (>=) (x y : int) = y <= x
logic (<=) (x y : int) = x < y or x = y
clone export relations.TotalOrder with
type t = int, logic rel = (<=)
clone export algebra.OrderedUnitaryCommutativeRing with
type t = int, logic zero = zero, logic one = one, logic (<=) = (<=)
end
......
......@@ -4,16 +4,12 @@ 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
logic (<=) (x y : real) = x < y or x = y
clone export relations.TotalOrder with
type t = real, logic rel = (<=)
clone export algebra.OrderedField with
type t = real, logic zero = zero, logic one = one, logic (<=) = (<=)
end
......@@ -29,8 +25,8 @@ theory RealInfix
logic (<=.) (x:real) (y:real) = x <= y
logic (>=.) (x:real) (y:real) = x >= y
logic (<.) (x:real) (y:real) = x < y
logic (>.) (x:real) (y:real) = x > y
logic ( <.) (x:real) (y:real) = x < y
logic ( >.) (x:real) (y:real) = x > y
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