|
1 (* Title: CCL/set.thy |
|
2 ID: $Id$ |
|
3 |
|
4 Modified version of HOL/set.thy that extends FOL |
|
5 |
|
6 *) |
|
7 |
|
8 Set = FOL + |
|
9 |
|
10 types |
|
11 set 1 |
|
12 |
|
13 arities |
|
14 set :: (term) term |
|
15 |
|
16 consts |
|
17 Collect :: "['a => o] => 'a set" (*comprehension*) |
|
18 Compl :: "('a set) => 'a set" (*complement*) |
|
19 Int :: "['a set, 'a set] => 'a set" (infixl 70) |
|
20 Un :: "['a set, 'a set] => 'a set" (infixl 65) |
|
21 Union, Inter :: "(('a set)set) => 'a set" (*...of a set*) |
|
22 UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) |
|
23 Ball, Bex :: "['a set, 'a => o] => o" (*bounded quants*) |
|
24 mono :: "['a set => 'b set] => o" (*monotonicity*) |
|
25 ":" :: "['a, 'a set] => o" (infixl 50) (*membership*) |
|
26 "<=" :: "['a set, 'a set] => o" (infixl 50) |
|
27 singleton :: "'a => 'a set" ("{_}") |
|
28 empty :: "'a set" ("{}") |
|
29 "oo" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) (*composition*) |
|
30 |
|
31 "@Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*) |
|
32 |
|
33 (* Big Intersection / Union *) |
|
34 |
|
35 "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) |
|
36 "@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(UN _:_./ _)" [0, 0, 0] 10) |
|
37 |
|
38 (* Bounded Quantifiers *) |
|
39 |
|
40 "@Ball" :: "[idt, 'a set, o] => o" ("(ALL _:_./ _)" [0, 0, 0] 10) |
|
41 "@Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10) |
|
42 |
|
43 |
|
44 translations |
|
45 "{x. P}" == "Collect(%x. P)" |
|
46 "INT x:A. B" == "INTER(A, %x. B)" |
|
47 "UN x:A. B" == "UNION(A, %x. B)" |
|
48 "ALL x:A. P" == "Ball(A, %x. P)" |
|
49 "EX x:A. P" == "Bex(A, %x. P)" |
|
50 |
|
51 |
|
52 rules |
|
53 mem_Collect_iff "(a : {x.P(x)}) <-> P(a)" |
|
54 set_extension "A=B <-> (ALL x.x:A <-> x:B)" |
|
55 |
|
56 Ball_def "Ball(A, P) == ALL x. x:A --> P(x)" |
|
57 Bex_def "Bex(A, P) == EX x. x:A & P(x)" |
|
58 mono_def "mono(f) == (ALL A B. A <= B --> f(A) <= f(B))" |
|
59 subset_def "A <= B == ALL x:A. x:B" |
|
60 singleton_def "{a} == {x.x=a}" |
|
61 empty_def "{} == {x.False}" |
|
62 Un_def "A Un B == {x.x:A | x:B}" |
|
63 Int_def "A Int B == {x.x:A & x:B}" |
|
64 Compl_def "Compl(A) == {x. ~x:A}" |
|
65 INTER_def "INTER(A, B) == {y. ALL x:A. y: B(x)}" |
|
66 UNION_def "UNION(A, B) == {y. EX x:A. y: B(x)}" |
|
67 Inter_def "Inter(S) == (INT x:S. x)" |
|
68 Union_def "Union(S) == (UN x:S. x)" |
|
69 |
|
70 end |
|
71 |