function.mlw 586 Bytes
Newer Older
1
module Injective
2

François Bobot's avatar
François Bobot committed
3 4
  type a
  type v
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6
  function to_ a : v
  function from v : a
François Bobot's avatar
François Bobot committed
7

8
  axiom Inj : forall x : a. from(to_ x) = x
François Bobot's avatar
François Bobot committed
9

10 11
  goal G1 : forall x y : a. to_(x)=to_(y) -> x = y
  goal G2 : forall y : a. exists x : v. from(x)=y
François Bobot's avatar
François Bobot committed
12 13 14

end

15
module Surjective
16

François Bobot's avatar
François Bobot committed
17 18
  type a
  type v
Andrei Paskevich's avatar
Andrei Paskevich committed
19 20
  function to_ a : v
  function from v : a
François Bobot's avatar
François Bobot committed
21

22
  clone export Injective with type v = a, type a = v,
23
    function to_ = from, function from = to_, axiom Inj
François Bobot's avatar
François Bobot committed
24 25 26

end

27
module Bijective
François Bobot's avatar
François Bobot committed
28

29
  clone export Injective
30
  clone Surjective as S with type v = v, type a = a,
31
    function to_ = to_, function from = from, axiom Inj
François Bobot's avatar
François Bobot committed
32

33
end