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
|
(** {1 Injections, surjections and bijections} *)
module Injective
type a
type v
function to_ a : v
function from v : a
axiom Inj : forall x : a. from(to_ x) = x
goal G1 : forall x y : a. to_(x)=to_(y) -> x = y
goal G2 : forall y : a. exists x : v. from(x)=y
end
module Surjective
type a
type v
function to_ a : v
function from v : a
clone export Injective with type v = a, type a = v,
function to_ = from, function from = to_, axiom Inj
end
module Bijective
clone export Injective
clone Surjective as S with type v = v, type a = a,
function to_ = to_, function from = from, axiom Inj
end
|
