src/HOL/Fun.thy
author paulson
Sat Nov 01 12:59:06 1997 +0100 (1997-11-01)
changeset 4059 59c1422c9da5
parent 2912 3fac3e8d5d3e
child 4648 f04da668581c
permissions -rw-r--r--
New Blast_tac (and minor tidying...)
clasohm@1475
     1
(*  Title:      HOL/Fun.thy
clasohm@923
     2
    ID:         $Id$
clasohm@1475
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1994  University of Cambridge
clasohm@923
     5
nipkow@2912
     6
Notions about functions.
clasohm@923
     7
*)
clasohm@923
     8
nipkow@2912
     9
Fun = Set +
nipkow@2912
    10
paulson@4059
    11
instance set :: (term) order
paulson@4059
    12
                       (subset_refl,subset_trans,subset_antisym,psubset_eq)
nipkow@2912
    13
consts
nipkow@2912
    14
nipkow@2912
    15
  inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
nipkow@2912
    16
  inj_onto      :: ['a => 'b, 'a set] => bool
nipkow@2912
    17
  inv           :: ('a => 'b) => ('b => 'a)
nipkow@2912
    18
nipkow@2912
    19
defs
nipkow@2912
    20
nipkow@2912
    21
  inj_def       "inj f          == ! x y. f(x)=f(y) --> x=y"
nipkow@2912
    22
  inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
nipkow@2912
    23
  surj_def      "surj f         == ! y. ? x. y=f(x)"
nipkow@2912
    24
  inv_def       "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
nipkow@2912
    25
nipkow@2912
    26
end