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