0
|
1 |
(* Title: HOL/set.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
*)
|
|
6 |
|
|
7 |
Set = Ord +
|
|
8 |
|
|
9 |
types
|
49
|
10 |
'a set
|
0
|
11 |
|
|
12 |
arities
|
|
13 |
set :: (term) term
|
|
14 |
set :: (term) ord
|
|
15 |
set :: (term) minus
|
|
16 |
|
|
17 |
|
|
18 |
consts
|
|
19 |
|
|
20 |
(* Constants *)
|
|
21 |
|
12
|
22 |
Collect :: "('a => bool) => 'a set" (*comprehension*)
|
|
23 |
Compl :: "('a set) => 'a set" (*complement*)
|
|
24 |
Int :: "['a set, 'a set] => 'a set" (infixl 70)
|
|
25 |
Un :: "['a set, 'a set] => 'a set" (infixl 65)
|
|
26 |
UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*)
|
|
27 |
UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10)
|
|
28 |
INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10)
|
|
29 |
Union, Inter :: "(('a set)set) => 'a set" (*of a set*)
|
|
30 |
range :: "('a => 'b) => 'b set" (*of function*)
|
|
31 |
Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*)
|
|
32 |
inj, surj :: "('a => 'b) => bool" (*inj/surjective*)
|
0
|
33 |
inj_onto :: "['a => 'b, 'a set] => bool"
|
12
|
34 |
"``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90)
|
|
35 |
":" :: "['a, 'a set] => bool" (infixl 50) (*membership*)
|
|
36 |
"~:" :: "['a, 'a set] => bool" ("(_ ~:/ _)" [50, 51] 50)
|
0
|
37 |
|
|
38 |
(* Finite Sets *)
|
|
39 |
|
|
40 |
insert :: "['a, 'a set] => 'a set"
|
4
|
41 |
"{}" :: "'a set" ("{}")
|
|
42 |
"@Finset" :: "args => 'a set" ("{(_)}")
|
0
|
43 |
|
|
44 |
|
|
45 |
(** Binding Constants **)
|
|
46 |
|
12
|
47 |
"@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*)
|
0
|
48 |
|
|
49 |
(* Big Intersection / Union *)
|
|
50 |
|
4
|
51 |
"@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(3INT _:_./ _)" 10)
|
|
52 |
"@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(3UN _:_./ _)" 10)
|
0
|
53 |
|
|
54 |
(* Bounded Quantifiers *)
|
|
55 |
|
4
|
56 |
"@Ball" :: "[idt, 'a set, bool] => bool" ("(3! _:_./ _)" 10)
|
|
57 |
"@Bex" :: "[idt, 'a set, bool] => bool" ("(3? _:_./ _)" 10)
|
|
58 |
"*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10)
|
|
59 |
"*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10)
|
0
|
60 |
|
|
61 |
|
|
62 |
translations
|
12
|
63 |
"x ~: y" == "~ (x : y)"
|
|
64 |
"{x, xs}" == "insert(x, {xs})"
|
|
65 |
"{x}" == "insert(x, {})"
|
0
|
66 |
"{x. P}" == "Collect(%x. P)"
|
|
67 |
"INT x:A. B" == "INTER(A, %x. B)"
|
|
68 |
"UN x:A. B" == "UNION(A, %x. B)"
|
|
69 |
"! x:A. P" == "Ball(A, %x. P)"
|
|
70 |
"? x:A. P" == "Bex(A, %x. P)"
|
|
71 |
"ALL x:A. P" => "Ball(A, %x. P)"
|
|
72 |
"EX x:A. P" => "Bex(A, %x. P)"
|
|
73 |
|
|
74 |
|
|
75 |
rules
|
|
76 |
|
|
77 |
(* Isomorphisms between Predicates and Sets *)
|
|
78 |
|
|
79 |
mem_Collect_eq "(a : {x.P(x)}) = P(a)"
|
|
80 |
Collect_mem_eq "{x.x:A} = A"
|
|
81 |
|
|
82 |
(* Definitions *)
|
|
83 |
|
|
84 |
Ball_def "Ball(A, P) == ! x. x:A --> P(x)"
|
|
85 |
Bex_def "Bex(A, P) == ? x. x:A & P(x)"
|
|
86 |
subset_def "A <= B == ! x:A. x:B"
|
|
87 |
Compl_def "Compl(A) == {x. ~x:A}"
|
|
88 |
Un_def "A Un B == {x.x:A | x:B}"
|
|
89 |
Int_def "A Int B == {x.x:A & x:B}"
|
|
90 |
set_diff_def "A-B == {x. x:A & ~x:B}"
|
|
91 |
INTER_def "INTER(A, B) == {y. ! x:A. y: B(x)}"
|
|
92 |
UNION_def "UNION(A, B) == {y. ? x:A. y: B(x)}"
|
|
93 |
INTER1_def "INTER1(B) == INTER({x.True}, B)"
|
|
94 |
UNION1_def "UNION1(B) == UNION({x.True}, B)"
|
|
95 |
Inter_def "Inter(S) == (INT x:S. x)"
|
|
96 |
Union_def "Union(S) == (UN x:S. x)"
|
|
97 |
empty_def "{} == {x. False}"
|
|
98 |
insert_def "insert(a, B) == {x.x=a} Un B"
|
|
99 |
range_def "range(f) == {y. ? x. y=f(x)}"
|
|
100 |
image_def "f``A == {y. ? x:A. y=f(x)}"
|
|
101 |
inj_def "inj(f) == ! x y. f(x)=f(y) --> x=y"
|
|
102 |
inj_onto_def "inj_onto(f, A) == ! x:A. ! y:A. f(x)=f(y) --> x=y"
|
|
103 |
surj_def "surj(f) == ! y. ? x. y=f(x)"
|
|
104 |
|
|
105 |
end
|
|
106 |
|
|
107 |
|
|
108 |
ML
|
|
109 |
|
|
110 |
val print_ast_translation =
|
4
|
111 |
map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
|
0
|
112 |
|