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" (*inj/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) |
64 "UN x:A. B" == "UNION(A, %x. B)" |
64 "UN x:A. B" == "UNION(A, %x. B)" |
65 "! x:A. P" == "Ball(A, %x. P)" |
65 "! x:A. P" == "Ball(A, %x. P)" |
66 "? x:A. P" == "Bex(A, %x. P)" |
66 "? x:A. P" == "Bex(A, %x. P)" |
67 "ALL x:A. P" => "Ball(A, %x. P)" |
67 "ALL x:A. P" => "Ball(A, %x. P)" |
68 "EX x:A. P" => "Bex(A, %x. P)" |
68 "EX x:A. P" => "Bex(A, %x. P)" |
|
69 |
|
70 "x ~: y" == "~ (x:y)" |
69 |
71 |
70 "{x, xs}" == "insert(x, {xs})" |
72 "{x, xs}" == "insert(x, {xs})" |
71 "{x}" == "insert(x, {})" |
73 "{x}" == "insert(x, {})" |
72 |
74 |
73 |
75 |