equal
deleted
inserted
replaced
4 Modified version of HOL/set.thy that extends FOL |
4 Modified version of HOL/set.thy that extends FOL |
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 Set = FOL + |
8 Set = FOL + |
|
9 |
|
10 global |
9 |
11 |
10 types |
12 types |
11 'a set |
13 'a set |
12 |
14 |
13 arities |
15 arities |
26 "<=" :: "['a set, 'a set] => o" (infixl 50) |
28 "<=" :: "['a set, 'a set] => o" (infixl 50) |
27 singleton :: "'a => 'a set" ("{_}") |
29 singleton :: "'a => 'a set" ("{_}") |
28 empty :: "'a set" ("{}") |
30 empty :: "'a set" ("{}") |
29 "oo" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) (*composition*) |
31 "oo" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) (*composition*) |
30 |
32 |
|
33 syntax |
31 "@Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*) |
34 "@Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*) |
32 |
35 |
33 (* Big Intersection / Union *) |
36 (* Big Intersection / Union *) |
34 |
37 |
35 "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) |
38 "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) |
46 "INT x:A. B" == "INTER(A, %x. B)" |
49 "INT x:A. B" == "INTER(A, %x. B)" |
47 "UN x:A. B" == "UNION(A, %x. B)" |
50 "UN x:A. B" == "UNION(A, %x. B)" |
48 "ALL x:A. P" == "Ball(A, %x. P)" |
51 "ALL x:A. P" == "Ball(A, %x. P)" |
49 "EX x:A. P" == "Bex(A, %x. P)" |
52 "EX x:A. P" == "Bex(A, %x. P)" |
50 |
53 |
|
54 local |
51 |
55 |
52 rules |
56 rules |
53 mem_Collect_iff "(a : {x. P(x)}) <-> P(a)" |
57 mem_Collect_iff "(a : {x. P(x)}) <-> P(a)" |
54 set_extension "A=B <-> (ALL x. x:A <-> x:B)" |
58 set_extension "A=B <-> (ALL x. x:A <-> x:B)" |
55 |
59 |