--- a/src/HOL/Fun.thy Wed Aug 12 16:21:18 1998 +0200
+++ b/src/HOL/Fun.thy Wed Aug 12 16:23:25 1998 +0200
@@ -12,15 +12,37 @@
(subset_refl,subset_trans,subset_antisym,psubset_eq)
consts
+ Id :: 'a => 'a
+ o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55)
inj, surj :: ('a => 'b) => bool (*inj/surjective*)
inj_on :: ['a => 'b, 'a set] => bool
inv :: ('a => 'b) => ('b => 'a)
+ fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+
+nonterminals
+ updbinds updbind
+
+syntax
+
+ (* Let expressions *)
+
+ "_updbind" :: ['a, 'a] => updbind ("(2_ :=/ _)")
+ "" :: updbind => updbinds ("_")
+ "_updbinds" :: [updbind, updbinds] => updbinds ("_,/ _")
+ "_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [900,0] 900)
+
+translations
+ "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
+ "f(x:=y)" == "fun_upd f x y"
defs
- inj_def "inj f == ! x y. f(x)=f(y) --> x=y"
- inj_on_def "inj_on 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)"
+ Id_def "Id == %x. x"
+ o_def "f o g == %x. f(g(x))"
+ inj_def "inj f == ! x y. f(x)=f(y) --> x=y"
+ inj_on_def "inj_on 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"
+ fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
end