src/HOL/Fun.thy
changeset 6171 cd237a10cbf8
parent 5852 4d7320490be4
child 7374 dec7b838f5cb
     1.1 --- a/src/HOL/Fun.thy	Wed Feb 03 13:23:24 1999 +0100
     1.2 +++ b/src/HOL/Fun.thy	Wed Feb 03 13:26:07 1999 +0100
     1.3 @@ -10,18 +10,12 @@
     1.4  
     1.5  instance set :: (term) order
     1.6                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
     1.7 -consts
     1.8 -
     1.9 -  id          ::  'a => 'a
    1.10 -  o           :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    1.11 -  inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
    1.12 -  inj_on      :: ['a => 'b, 'a set] => bool
    1.13 -  inv         :: ('a => 'b) => ('b => 'a)
    1.14 -  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    1.15 -
    1.16  nonterminals
    1.17    updbinds  updbind
    1.18  
    1.19 +consts
    1.20 +  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    1.21 +
    1.22  syntax
    1.23  
    1.24    (* Let expressions *)
    1.25 @@ -36,15 +30,32 @@
    1.26    "f(x:=y)"                     == "fun_upd f x y"
    1.27  
    1.28  defs
    1.29 +  fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
    1.30  
    1.31 -  id_def	"id             == %x. x"
    1.32 -  o_def   	"f o g          == %x. f(g(x))"
    1.33 -  inj_def	"inj f          == ! x y. f(x)=f(y) --> x=y"
    1.34 -  inj_on_def	"inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.35 -  surj_def	"surj f         == ! y. ? x. y=f(x)"
    1.36 -  inv_def	"inv(f::'a=>'b) == % y. @x. f(x)=y"
    1.37 -  fun_upd_def	"f(a:=b)        == % x. if x=a then b else f x"
    1.38 +  
    1.39 +constdefs
    1.40 +  id ::  'a => 'a
    1.41 +    "id == %x. x"
    1.42 +
    1.43 +  o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    1.44 +    "f o g == %x. f(g(x))"
    1.45 +
    1.46 +  inj_on :: ['a => 'b, 'a set] => bool
    1.47 +    "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.48  
    1.49 +  surj :: ('a => 'b) => bool                   (*surjective*)
    1.50 +    "surj f == ! y. ? x. y=f(x)"
    1.51 +  
    1.52 +  inv :: ('a => 'b) => ('b => 'a)
    1.53 +    "inv(f::'a=>'b) == % y. @x. f(x)=y"
    1.54 +  
    1.55 +
    1.56 +
    1.57 +syntax
    1.58 +  inj   :: ('a => 'b) => bool                   (*injective*)
    1.59 +
    1.60 +translations
    1.61 +  "inj f" == "inj_on f UNIV"
    1.62  
    1.63  (*The Pi-operator, by Florian Kammueller*)
    1.64