src/HOL/Fun.thy
author oheimb
Wed Aug 12 16:23:25 1998 +0200 (1998-08-12)
changeset 5305 513925de8962
parent 4830 bd73675adbed
child 5608 a82a038a3e7a
permissions -rw-r--r--
cleanup for Fun.thy:
merged Update.{thy|ML} into Fun.{thy|ML}
moved o_def from HOL.thy to Fun.thy
added Id_def to Fun.thy
moved image_compose from Set.ML to Fun.ML
moved o_apply and o_assoc from simpdata.ML to Fun.ML
moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML
added fun_upd_twist to Fun.ML
     1 (*  Title:      HOL/Fun.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Notions about functions.
     7 *)
     8 
     9 Fun = Vimage +
    10 
    11 instance set :: (term) order
    12                        (subset_refl,subset_trans,subset_antisym,psubset_eq)
    13 consts
    14 
    15   Id          ::  'a => 'a
    16   o           :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    17   inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
    18   inj_on      :: ['a => 'b, 'a set] => bool
    19   inv         :: ('a => 'b) => ('b => 'a)
    20   fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    21 
    22 nonterminals
    23   updbinds  updbind
    24 
    25 syntax
    26 
    27   (* Let expressions *)
    28 
    29   "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
    30   ""               :: updbind => updbinds             ("_")
    31   "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
    32   "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
    33 
    34 translations
    35   "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
    36   "f(x:=y)"                     == "fun_upd f x y"
    37 
    38 defs
    39 
    40   Id_def	"Id             == %x. x"
    41   o_def   	"f o g          == %x. f(g(x))"
    42   inj_def	"inj f          == ! x y. f(x)=f(y) --> x=y"
    43   inj_on_def	"inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    44   surj_def	"surj f         == ! y. ? x. y=f(x)"
    45   inv_def	"inv(f::'a=>'b) == % y. @x. f(x)=y"
    46   fun_upd_def	"f(a:=b)        == % x. if x=a then b else f x"
    47 
    48 end