17 |
17 |
18 consts |
18 consts |
19 |
19 |
20 (* Constants *) |
20 (* Constants *) |
21 |
21 |
22 Collect :: "('a => bool) => 'a set" (*comprehension*) |
22 Collect :: "('a => bool) => 'a set" (*comprehension*) |
23 Compl :: "('a set) => 'a set" (*complement*) |
23 Compl :: "('a set) => 'a set" (*complement*) |
24 Int :: "['a set, 'a set] => 'a set" (infixl 70) |
24 Int :: "['a set, 'a set] => 'a set" (infixl 70) |
25 Un :: "['a set, 'a set] => 'a set" (infixl 65) |
25 Un :: "['a set, 'a set] => 'a set" (infixl 65) |
26 UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) |
26 UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) |
27 UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10) |
27 UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10) |
28 INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10) |
28 INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10) |
29 Union, Inter :: "(('a set)set) => 'a set" (*of a set*) |
29 Union, Inter :: "(('a set)set) => 'a set" (*of a set*) |
30 range :: "('a => 'b) => 'b set" (*of function*) |
30 range :: "('a => 'b) => 'b set" (*of function*) |
31 Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*) |
31 Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*) |
32 inj, surj :: "('a => 'b) => bool" (*injective/surjective*) |
32 inj, surj :: "('a => 'b) => bool" (*injective/surjective*) |
33 inj_onto :: "['a => 'b, 'a set] => bool" |
33 inj_onto :: "['a => 'b, 'a set] => bool" |
34 "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90) |
34 "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90) |
35 ":" :: "['a, 'a set] => bool" (infixl 50) (*membership*) |
35 ":" :: "['a, 'a set] => bool" (infixl 50) (*membership*) |
36 |
36 |
37 (* Finite Sets *) |
37 (* Finite Sets *) |
38 |
38 |
39 insert :: "['a, 'a set] => 'a set" |
39 insert :: "['a, 'a set] => 'a set" |
40 "{}" :: "'a set" ("{}") |
40 "{}" :: "'a set" ("{}") |
41 "@Finset" :: "args => 'a set" ("{(_)}") |
41 "@Finset" :: "args => 'a set" ("{(_)}") |
42 |
42 |
43 |
43 |
44 (** Binding Constants **) |
44 (** Binding Constants **) |
45 |
45 |
46 "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*) |
46 "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*) |
47 |
47 |
48 (* Big Intersection / Union *) |
48 (* Big Intersection / Union *) |
49 |
49 |
50 "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(3INT _:_./ _)" 10) |
50 "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(3INT _:_./ _)" 10) |
51 "@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(3UN _:_./ _)" 10) |
51 "@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(3UN _:_./ _)" 10) |
52 |
52 |
53 (* Bounded Quantifiers *) |
53 (* Bounded Quantifiers *) |
54 |
54 |
55 "@Ball" :: "[idt, 'a set, bool] => bool" ("(3! _:_./ _)" 10) |
55 "@Ball" :: "[idt, 'a set, bool] => bool" ("(3! _:_./ _)" 10) |
56 "@Bex" :: "[idt, 'a set, bool] => bool" ("(3? _:_./ _)" 10) |
56 "@Bex" :: "[idt, 'a set, bool] => bool" ("(3? _:_./ _)" 10) |
57 "*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10) |
57 "*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10) |
58 "*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10) |
58 "*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10) |
59 |
59 |
60 |
60 |
61 translations |
61 translations |
62 "{x. P}" == "Collect(%x. P)" |
62 "{x. P}" == "Collect(%x. P)" |
63 "INT x:A. B" == "INTER(A, %x. B)" |
63 "INT x:A. B" == "INTER(A, %x. B)" |