stdlib/function.mlw

   1
   2 (** {1 Injections, surjections and bijections} *)
   3
   4 module Injective
   5
   6   type a
   7   type v
   8   function to_ a : v
   9   function from v : a
  10
  11   axiom Inj : forall x : a. from(to_ x) = x
  12
  13   goal G1 : forall x y : a. to_(x)=to_(y) -> x = y
  14   goal G2 : forall y : a. exists x : v. from(x)=y
  15
  16 end
  17
  18 module Surjective
  19
  20   type a
  21   type v
  22   function to_ a : v
  23   function from v : a
  24
  25   clone export Injective with type v = a, type a = v,
  26     function to_ = from, function from = to_, axiom Inj
  27
  28 end
  29
  30 module Bijective
  31
  32   clone export Injective
  33   clone Surjective as S with type v = v, type a = a,
  34     function to_ = to_, function from = from, axiom Inj
  35
  36 end