Commit d87eb15e authored by MARCHE Claude's avatar MARCHE Claude
Browse files

anomaly CannotInstantiate

parent e9a6fd45
......@@ -6,7 +6,11 @@ theory Int
logic (> ) (int, int)
logic (>=) (int, int)
(* TODO : < is a total order relation *)
clone import relations.TotalOrder with type t = int,
logic Equiv.eq = (=), logic PreOrder.le = (<=), logic lt = (<)
clone import relations.TotalOrder with type t = int,
logic eq = (=), logic le = (>=), logic lt = (>)
logic zero : int = 0
logic one : int = 1
......@@ -29,6 +33,7 @@ theory Abs
end
(*
theory MinMax
use import Int
......@@ -42,6 +47,7 @@ theory MinMax
axiom Min_is_some : forall x,y:int. min(x,y) = x or min(x,y) = y
end
*)
theory EuclideanDivision
......
theory PreOrder
type t
logic le(t,t)
axiom Refl : forall x:t. le(x,x)
axiom Trans : forall x,y,z:t. le(x,y) and le(y,z) -> le(x,z)
end
theory Equiv
type t
logic eq(t,t)
axiom Refl : forall x:t. eq(x,x)
axiom Symm : forall x,y:t. eq(x,y) -> eq(y,x)
axiom Trans : forall x,y,z:t. eq(x,y) and eq(y,z) -> eq(x,z)
end
type t
logic eq(t,t)
clone export PreOrder with type t = t, logic le = eq
theory Order
clone export Equiv
axiom Symm : forall x,y:t. eq(x,y) -> eq(y,x)
logic le(t,t)
axiom Le_refl : forall x:t. le(x,x)
axiom Le_trans : forall x,y,z:t. le(x,y) and le(y,z) -> le(x,z)
end
logic lt(x:t,y:t) = le(x,y) and not eq(x,y)
theory TotalOrder
lemma Lt_antirefl: forall x:t. not lt(x,x)
lemma Lt_trans: forall x,y,z:t. lt(x,y) and lt(y,z) -> lt(x,z)
lemma Le_lt_trans: forall x,y,z:t. le(x,y) and lt(y,z) -> lt(x,z)
lemma Lt_le_trans: forall x,y,z:t. lt(x,y) and le(y,z) -> lt(x,z)
end
type t
clone import Equiv with type t = t
clone import PreOrder with type t = t
theory StrictOrder
clone export Equiv
axiom Totality: forall x,y:t. eq(x,y) or le(x,y) or le(y,x)
logic lt(t,t)
axiom AntiRefl : forall x:t. not lt(x,x)
axiom Lt_trans : forall x,y,z:t. lt(x,y) and lt(y,z) -> lt(x,z)
logic lt(x:t,y:t) = le(x,y) and not eq(x,y)
logic le(x:t,y:t) = lt(x,y) or eq(x,y)
lemma Lt_antirefl: forall x:t. not lt(x,x)
lemma Lt_trans: forall x,y,z:t. lt(x,y) and lt(y,z) -> lt(x,z)
lemma Le_lt_trans: forall x,y,z:t. le(x,y) and lt(y,z) -> lt(x,z)
lemma Lt_le_trans: forall x,y,z:t. lt(x,y) and le(y,z) -> lt(x,z)
lemma Le_refl: forall x:t. le(x,x)
lemma Le_trans: forall x,y,z:t. le(x,y) and le(y,z) -> le(x,z)
lemma Le_lt_trans: forall x,y,z:t. le(x,y) and lt(y,z) -> lt(x,z)
lemma Lt_le_trans: forall x,y,z:t. lt(x,y) and le(y,z) -> lt(x,z)
end
theory MinMax
clone export TotalOrder
logic min(t,t) : t
logic max(t,t) : t
end
(*
Local Variables:
compile-command: "../bin/why.opt --output-dir goals --driver ../drivers/alt_ergo.drv -I ../theories/ relations.why"
compile-command: "make -C .. test"
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