src/HOL/Fun.thy

Now Datatype.occs_in_prems prints the necessary warning ITSELF.

It is also easier to invoke and even works if the induction variable
is a parameter (rather than a free variable).

(*  Title:      HOL/Fun.thy
    ID:         $Id$
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

Notions about functions.
*)

Fun = Set +

consts

  inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
  inj_onto      :: ['a => 'b, 'a set] => bool
  inv           :: ('a => 'b) => ('b => 'a)

defs

  inj_def       "inj f          == ! x y. f(x)=f(y) --> x=y"
  inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
  surj_def      "surj f         == ! y. ? x. y=f(x)"
  inv_def       "inv(f::'a=>'b) == (% y. @x. f(x)=y)"

end