Commit 6ecf1ff2 authored by Andrei Paskevich's avatar Andrei Paskevich

in ordered rings, 0 <= 1

parent 31cb5c6a
......@@ -65,6 +65,7 @@ theory int.Int
remove prop Antisymm
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
......@@ -110,6 +111,7 @@ theory real.Real
remove prop Inverse
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
......
......@@ -62,6 +62,7 @@ theory int.Int
remove prop Antisymm
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
......@@ -106,6 +107,7 @@ theory real.Real
remove prop Inverse
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
......
......@@ -72,6 +72,7 @@ theory int.Int
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
remove prop ZeroLessOne
end
......@@ -168,6 +169,7 @@ theory real.Real
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
remove prop ZeroLessOne
remove prop Refl
remove prop Trans
remove prop Antisymm
......
......@@ -65,6 +65,7 @@ theory int.Int
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
......@@ -103,6 +104,7 @@ theory real.Real
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
......
......@@ -69,6 +69,7 @@ theory int.Int
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
......
......@@ -63,6 +63,7 @@ theory int.Int
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
......@@ -101,6 +102,7 @@ theory real.Real
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
......
......@@ -63,6 +63,7 @@ theory int.Int
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
......@@ -103,6 +104,7 @@ theory real.Real
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
......
......@@ -65,6 +65,7 @@ theory int.Int
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
......@@ -103,6 +104,7 @@ theory real.Real
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
......
......@@ -64,6 +64,7 @@ theory int.Int
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
......@@ -102,6 +103,7 @@ theory real.Real
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
......
......@@ -83,6 +83,8 @@ theory OrderedUnitaryCommutativeRing
predicate (>=) (x y : t) = y <= x
clone export relations.TotalOrder with type t = t, predicate rel = (<=)
axiom ZeroLessOne : zero <= one
axiom CompatOrderAdd :
forall x y z : t. x <= y -> x + z <= y + z
axiom CompatOrderMult :
......@@ -116,6 +118,8 @@ theory OrderedField
predicate (>=) (x y : t) = y <= x
clone export relations.TotalOrder with type t = t, predicate rel = (<=)
axiom ZeroLessOne : zero <= one
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
......@@ -128,6 +132,5 @@ end
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
*)
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