src/HOL/Fun.thy
changeset 5305 513925de8962
parent 4830 bd73675adbed
child 5608 a82a038a3e7a
     1.1 --- a/src/HOL/Fun.thy	Wed Aug 12 16:21:18 1998 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Aug 12 16:23:25 1998 +0200
     1.3 @@ -12,15 +12,37 @@
     1.4                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
     1.5  consts
     1.6  
     1.7 +  Id          ::  'a => 'a
     1.8 +  o           :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
     1.9    inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
    1.10    inj_on      :: ['a => 'b, 'a set] => bool
    1.11    inv         :: ('a => 'b) => ('b => 'a)
    1.12 +  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    1.13 +
    1.14 +nonterminals
    1.15 +  updbinds  updbind
    1.16 +
    1.17 +syntax
    1.18 +
    1.19 +  (* Let expressions *)
    1.20 +
    1.21 +  "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
    1.22 +  ""               :: updbind => updbinds             ("_")
    1.23 +  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
    1.24 +  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
    1.25 +
    1.26 +translations
    1.27 +  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
    1.28 +  "f(x:=y)"                     == "fun_upd f x y"
    1.29  
    1.30  defs
    1.31  
    1.32 -  inj_def     "inj f          == ! x y. f(x)=f(y) --> x=y"
    1.33 -  inj_on_def  "inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.34 -  surj_def    "surj f         == ! y. ? x. y=f(x)"
    1.35 -  inv_def     "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
    1.36 +  Id_def	"Id             == %x. x"
    1.37 +  o_def   	"f o g          == %x. f(g(x))"
    1.38 +  inj_def	"inj f          == ! x y. f(x)=f(y) --> x=y"
    1.39 +  inj_on_def	"inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.40 +  surj_def	"surj f         == ! y. ? x. y=f(x)"
    1.41 +  inv_def	"inv(f::'a=>'b) == % y. @x. f(x)=y"
    1.42 +  fun_upd_def	"f(a:=b)        == % x. if x=a then b else f x"
    1.43  
    1.44  end