examples_in_progress/avl/preorder.mlw

   1
   2 (* Full preorder theory,
   3    containing lt and eq as well. *)
   4 theory FullParam
   5
   6   type t 'a
   7   type order 'a
   8   predicate le (order 'a) (t 'a) (t 'a)
   9   clone export relations_params.PreOrderParam with type t = t,
  10     type param = order, predicate rel = le
  11   predicate eq (order 'a) (t 'a) (t 'a)
  12   axiom eq_def : forall o:order 'a,x y:t 'a.
  13     correct_for o x /\ correct_for o y ->
  14       (eq o x y <-> le o x y /\ le o y x)
  15   predicate lt (order 'a) (t 'a) (t 'a)
  16   axiom lt_def : forall o:order 'a,x y:t 'a.
  17     correct_for o x /\ correct_for o y ->
  18       (lt o x y <-> le o x y /\ not le o y x)
  19
  20   clone relations_params.EquivalenceParam as Eq with type t = t,
  21     type param = order, predicate correct_for = correct_for,
  22     predicate rel = eq, lemma trans, lemma refl, lemma symm
  23
  24   clone relations_params.PartialStrictOrderParam as Lt with type t = t,
  25     type param = order, predicate correct_for = correct_for,
  26     predicate rel = lt, lemma trans, lemma asymm
  27
  28 end
  29
  30 theory TotalFullParam
  31
  32   clone export FullParam
  33   clone export relations_params.TotalParam with type t = t,
  34     type param = order, predicate correct_for = correct_for,
  35     predicate rel = le
  36   clone relations_params.TotalParam as Lt with type t = t,
  37     type param = order, predicate correct_for = correct_for,
  38     predicate rel = le, goal total
  39   lemma lt_def2 : forall o:order 'a,x y:t 'a.
  40     correct_for o x /\ correct_for o y -> lt o x y <-> not le o y x
  41
  42 end
  43
  44 (* Total preorder + corresponding program types and computable comparison. *)
  45 module ComputableParam
  46
  47   use int.Int
  48   use program_type.TypeParams
  49   clone program_type.Type1 as T
  50   clone program_type.Type1 as O
  51   clone export TotalFullParam with type t = T.m, type order = O.m
  52
  53   (* Comparison is computable. *)
  54   val compare (ghost p:type_params 'a 'b) (o:O.t 'a 'b) (x y:T.t 'a 'b) : int
  55     requires { let op = O.make_params p in let tp = T.make_params p in
  56       op.inv o /\ tp.inv x /\ tp.inv y /\
  57       correct_for (op.mdl o) (tp.mdl x) /\
  58       correct_for (op.mdl o) (tp.mdl y) }
  59     ensures { let om = p.O.make_params.mdl o in
  60       let mt = p.T.make_params.mdl in let xm = mt x in let ym = mt y in
  61         (result > 0 <-> lt om ym xm) /\
  62         (result < 0 <-> lt om xm ym) /\
  63         (result = 0 <-> eq om xm ym) }
  64
  65 end
  66