equal
deleted
inserted
replaced
10 |
10 |
11 instance set :: (term) order |
11 instance set :: (term) order |
12 (subset_refl,subset_trans,subset_antisym,psubset_eq) |
12 (subset_refl,subset_trans,subset_antisym,psubset_eq) |
13 consts |
13 consts |
14 |
14 |
15 Id :: 'a => 'a |
15 id :: 'a => 'a |
16 o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) |
16 o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) |
17 inj, surj :: ('a => 'b) => bool (*inj/surjective*) |
17 inj, surj :: ('a => 'b) => bool (*inj/surjective*) |
18 inj_on :: ['a => 'b, 'a set] => bool |
18 inj_on :: ['a => 'b, 'a set] => bool |
19 inv :: ('a => 'b) => ('b => 'a) |
19 inv :: ('a => 'b) => ('b => 'a) |
20 fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" |
20 fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" |
35 "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs" |
35 "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs" |
36 "f(x:=y)" == "fun_upd f x y" |
36 "f(x:=y)" == "fun_upd f x y" |
37 |
37 |
38 defs |
38 defs |
39 |
39 |
40 Id_def "Id == %x. x" |
40 id_def "id == %x. x" |
41 o_def "f o g == %x. f(g(x))" |
41 o_def "f o g == %x. f(g(x))" |
42 inj_def "inj f == ! x y. f(x)=f(y) --> x=y" |
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" |
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)" |
44 surj_def "surj f == ! y. ? x. y=f(x)" |
45 inv_def "inv(f::'a=>'b) == % y. @x. f(x)=y" |
45 inv_def "inv(f::'a=>'b) == % y. @x. f(x)=y" |