why3/stdlib/function.mlw

(** {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