Preorders

Author: Martin Clochard

theory Full

Extended preorder theory

  type t
  predicate le t t
  clone export relations.PreOrder with type t = t, predicate rel = le, axiom .

Standard preorder theory.

Definable symbols for equality and strict ordering.

  predicate eq t t
  axiom eq_def : forall x y. eq x y <-> le x y /\ le y x
  predicate lt t t
  axiom lt_def : forall x y. lt x y <-> le x y /\ not le y x

  clone relations.Equivalence as Eq with type t = t,
    predicate rel = eq, lemma Trans, lemma Refl, lemma Symm

Equality is provably an equivalence relation.

  clone relations.PartialStrictOrder as Lt with type t = t,
    predicate rel = lt, lemma Trans, lemma Asymm

Strict ordering is indeed a strict partial order.

end

theory TotalFull

Total preorder

  clone export Full with axiom .
  clone export relations.Total with type t = t, predicate rel = le, axiom Total
  clone relations.Total as Lt with type t = t, predicate rel = le, goal Total
  lemma lt_def2 : forall x y. lt x y <-> not le y x

end

module Computable

Computable total preorder

  use int.Int
  clone export TotalFull with axiom .

  val compare (x y:t) : int
    ensures { result > 0 <-> lt y x }
    ensures { result < 0 <-> lt x y }
    ensures { result = 0 <-> eq x y }

Comparison is computable.

end