stdlib/relations.mlw

   1
   2 (** {1 Relations} *)
   3
   4 (** {2 Relations and orders} *)
   5
   6 module EndoRelation
   7   type t
   8   predicate rel t t
   9 end
  10
  11 module Reflexive
  12   clone export EndoRelation
  13   axiom Refl : forall x:t. rel x x
  14 end
  15
  16 module Irreflexive
  17   clone export EndoRelation
  18   axiom Strict : forall x:t. not rel x x
  19 end
  20
  21 module Transitive
  22   clone export EndoRelation
  23   axiom Trans : forall x y z:t. rel x y -> rel y z -> rel x z
  24 end
  25
  26 module Symmetric
  27   clone export EndoRelation
  28   axiom Symm : forall x y:t. rel x y -> rel y x
  29 end
  30
  31 module Asymmetric
  32   clone export EndoRelation
  33   axiom Asymm : forall x y:t. rel x y -> not rel y x
  34 end
  35
  36 module Antisymmetric
  37   clone export EndoRelation
  38   axiom Antisymm : forall x y:t. rel x y -> rel y x -> x = y
  39 end
  40
  41 module Total
  42   clone export EndoRelation
  43   axiom Total : forall x y:t. rel x y \/ rel y x
  44 end
  45
  46 module PreOrder
  47   clone export Reflexive with axiom Refl
  48   clone export Transitive with type t = t, predicate rel = rel, axiom Trans
  49 end
  50
  51 module Equivalence
  52   clone export PreOrder with axiom Refl, axiom Trans
  53   clone export Symmetric with type t = t, predicate rel = rel, axiom Symm
  54 end
  55
  56 module TotalPreOrder
  57   clone export PreOrder with axiom Refl, axiom Trans
  58   clone export Total with type t = t, predicate rel = rel, axiom Total
  59 end
  60
  61 module PartialOrder
  62   clone export PreOrder with axiom Refl, axiom Trans
  63   clone export Antisymmetric with
  64     type t = t, predicate rel = rel, axiom Antisymm
  65 end
  66
  67 module TotalOrder
  68   clone export PartialOrder with axiom .
  69   clone export Total with type t = t, predicate rel = rel, axiom Total
  70 end
  71
  72 module PartialStrictOrder
  73   clone export Transitive with axiom Trans
  74   clone export Asymmetric with type t = t, predicate rel = rel, axiom Asymm
  75 end
  76
  77 module TotalStrictOrder
  78   clone export PartialStrictOrder with axiom Trans, axiom Asymm
  79   axiom Trichotomy : forall x y:t. rel x y \/ rel y x \/ x = y
  80 end
  81
  82 module Inverse
  83   clone export EndoRelation
  84
  85   predicate inv_rel (x y : t) = rel y x
  86 end
  87
  88 (** {2 Closures} *)
  89
  90 module ReflClosure
  91   clone export EndoRelation
  92
  93   inductive relR t t =
  94   | BaseRefl : forall x:t. relR x x
  95   | StepRefl : forall x y:t. rel x y -> relR x y
  96 end
  97
  98 module TransClosure
  99   clone export EndoRelation
 100
 101   inductive relT t t =
 102   | BaseTrans : forall x y:t. rel x y -> relT x y
 103   | StepTrans : forall x y z:t. relT x y -> rel y z -> relT x z
 104
 105   lemma relT_transitive:
 106     forall x y z: t. relT x y -> relT y z -> relT x z
 107 end
 108
 109 module ReflTransClosure
 110   clone export EndoRelation
 111
 112   inductive relTR t t =
 113   | BaseTransRefl : forall x:t. relTR x x
 114   | StepTransRefl : forall x y z:t. relTR x y -> rel y z -> relTR x z
 115
 116   lemma relTR_transitive:
 117     forall x y z: t. relTR x y -> relTR y z -> relTR x z
 118 end
 119
 120 (** {2 Lexicographic ordering} *)
 121
 122 module Lex
 123
 124   type t1
 125   type t2
 126
 127   predicate rel1 t1 t1
 128   predicate rel2 t2 t2
 129
 130   inductive lex (t1, t2) (t1, t2) =
 131   | Lex_1: forall x1 x2 : t1, y1 y2 : t2.
 132        rel1 x1 x2 -> lex (x1,y1) (x2,y2)
 133   | Lex_2: forall x : t1, y1 y2 : t2.
 134        rel2 y1 y2 -> lex (x,y1) (x,y2)
 135
 136 end
 137
 138 (** {2 Minimum and maximum for total orders} *)
 139
 140 module MinMax
 141
 142   type t
 143   predicate le t t
 144
 145   clone TotalOrder as TO with type t = t, predicate rel = le, axiom .
 146
 147   function min (x y : t) : t = if le x y then x else y
 148   function max (x y : t) : t = if le x y then y else x
 149
 150   lemma Min_r : forall x y:t. le y x -> min x y = y
 151   lemma Max_l : forall x y:t. le y x -> max x y = x
 152
 153   lemma Min_comm : forall x y:t. min x y = min y x
 154   lemma Max_comm : forall x y:t. max x y = max y x
 155
 156   lemma Min_assoc : forall x y z:t. min (min x y) z = min x (min y z)
 157   lemma Max_assoc : forall x y z:t. max (max x y) z = max x (max y z)
 158
 159 end
 160
 161 (** {2 Well-founded relation} *)
 162
 163 module WellFounded
 164
 165 use export why3.WellFounded.WellFounded
 166
 167 (** This is now part of the built-in theories. The contents is reproduced here for information
 168 {h <pre>
 169
 170   inductive acc (r: 'a -> 'a -> bool) (x: 'a) =
 171   | acc_x: forall r, x: 'a. (forall y. r y x -> acc r y) -> acc r x
 172
 173   predicate well_founded (r: 'a -> 'a -> bool) =
 174     forall x. acc r x
 175
 176 end
 177 </pre>}
 178
 179 *)
 180
 181 end