HasCASL/test/BoundedOrd.hascasl

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
class Ord {
vars  a: Ord; x: a
op    __<=__ : Pred (a * a)
. x <= x  }

classes BoundedOrd < Ord

vars  a: Ord; b: BoundedOrd
op    __<=__ : Pred (a * a);
      bot, top: b
vars  x, y, z: a; v: b
. x <= x
. x <= y /\ y <= z => x <= z
. x <= y /\ y <= x => x = y
. bot <= v
. v <= top

vars  a, b: Ord
type  instances a * b: Ord
vars  x, y: a; v, w: b
. (x, v) <= (y, w) <=> x <= y /\ v <= w

class instance DiscreteOrd < Ord
vars  a: DiscreteOrd; x, y: a
. x <= y <=> x = y

class Num
vars  a: Ord; b: Num
ops   min: a * a ->? a;
      min: b * b ->? b

vars  a: Ord; b: Ord
op    __<=__ : Pred ((a ->? b) * (a ->? b))
type  instance a ->? b: Ord

type  instance Unit: Ord
. () <= ()

type  instance ?a: Ord
vars  x, y: ?a
. x <= y <=> def x() => x() <= y()

class Cpo < Ord
var a : Cpo
op    __<=__ : Pred (a * a)

var x:?a
. x <=[?a] x