author | nipkow |
Fri, 04 Apr 1997 16:33:28 +0200 | |
changeset 2912 | 3fac3e8d5d3e |
parent 2684 | 9781d63ef063 |
child 2965 | afbda7e26f15 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/Set.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
*) |
|
6 |
||
7 |
Set = Ord + |
|
8 |
||
2261 | 9 |
|
10 |
(** Core syntax **) |
|
11 |
||
923 | 12 |
types |
13 |
'a set |
|
14 |
||
15 |
arities |
|
16 |
set :: (term) term |
|
17 |
||
18 |
instance |
|
19 |
set :: (term) {ord, minus} |
|
20 |
||
21 |
consts |
|
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
22 |
"{}" :: 'a set ("{}") |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
23 |
insert :: ['a, 'a set] => 'a set |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
24 |
Collect :: ('a => bool) => 'a set (*comprehension*) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
25 |
Compl :: ('a set) => 'a set (*complement*) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
26 |
Int :: ['a set, 'a set] => 'a set (infixl 70) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
27 |
Un :: ['a set, 'a set] => 'a set (infixl 65) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
28 |
UNION, INTER :: ['a set, 'a => 'b set] => 'b set (*general*) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
29 |
UNION1 :: ['a => 'b set] => 'b set (binder "UN " 10) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
30 |
INTER1 :: ['a => 'b set] => 'b set (binder "INT " 10) |
2261 | 31 |
Union, Inter :: (('a set) set) => 'a set (*of a set*) |
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
32 |
Pow :: 'a set => 'a set set (*powerset*) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
33 |
range :: ('a => 'b) => 'b set (*of function*) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
34 |
Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) |
1962
e60a230da179
Corrected associativity: must be to right, as the type dictatess
paulson
parents:
1883
diff
changeset
|
35 |
"``" :: ['a => 'b, 'a set] => ('b set) (infixr 90) |
2261 | 36 |
(*membership*) |
37 |
"op :" :: ['a, 'a set] => bool ("(_/ : _)" [50, 51] 50) |
|
923 | 38 |
|
39 |
||
2261 | 40 |
|
41 |
(** Additional concrete syntax **) |
|
42 |
||
923 | 43 |
syntax |
44 |
||
2261 | 45 |
"op :" :: ['a, 'a set] => bool ("op :") |
1531 | 46 |
|
2261 | 47 |
UNIV :: 'a set |
48 |
||
49 |
(* Infix syntax for non-membership *) |
|
923 | 50 |
|
2261 | 51 |
"op ~:" :: ['a, 'a set] => bool ("(_/ ~: _)" [50, 51] 50) |
52 |
"op ~:" :: ['a, 'a set] => bool ("op ~:") |
|
923 | 53 |
|
2261 | 54 |
"@Finset" :: args => 'a set ("{(_)}") |
55 |
||
56 |
"@Coll" :: [pttrn, bool] => 'a set ("(1{_./ _})") |
|
57 |
"@SetCompr" :: ['a, idts, bool] => 'a set ("(1{_ |/_./ _})") |
|
923 | 58 |
|
59 |
(* Big Intersection / Union *) |
|
60 |
||
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
61 |
"@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3INT _:_./ _)" 10) |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset
|
62 |
"@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3UN _:_./ _)" 10) |
923 | 63 |
|
64 |
(* Bounded Quantifiers *) |
|
65 |
||
2368 | 66 |
"@Ball" :: [pttrn, 'a set, bool] => bool ("(3! _:_./ _)" [0, 0, 10] 10) |
67 |
"@Bex" :: [pttrn, 'a set, bool] => bool ("(3? _:_./ _)" [0, 0, 10] 10) |
|
68 |
"*Ball" :: [pttrn, 'a set, bool] => bool ("(3ALL _:_./ _)" [0, 0, 10] 10) |
|
69 |
"*Bex" :: [pttrn, 'a set, bool] => bool ("(3EX _:_./ _)" [0, 0, 10] 10) |
|
923 | 70 |
|
71 |
translations |
|
1531 | 72 |
"UNIV" == "Compl {}" |
2261 | 73 |
"range f" == "f``UNIV" |
923 | 74 |
"x ~: y" == "~ (x : y)" |
75 |
"{x, xs}" == "insert x {xs}" |
|
76 |
"{x}" == "insert x {}" |
|
77 |
"{x. P}" == "Collect (%x. P)" |
|
78 |
"INT x:A. B" == "INTER A (%x. B)" |
|
79 |
"UN x:A. B" == "UNION A (%x. B)" |
|
80 |
"! x:A. P" == "Ball A (%x. P)" |
|
81 |
"? x:A. P" == "Bex A (%x. P)" |
|
82 |
"ALL x:A. P" => "Ball A (%x. P)" |
|
83 |
"EX x:A. P" => "Bex A (%x. P)" |
|
84 |
||
2388 | 85 |
syntax ("" output) |
86 |
"_setle" :: ['a set, 'a set] => bool ("(_/ <= _)" [50, 51] 50) |
|
87 |
"_setle" :: ['a set, 'a set] => bool ("op <=") |
|
2684 | 88 |
"_setless" :: ['a set, 'a set] => bool ("(_/ < _)" [50, 51] 50) |
89 |
"_setless" :: ['a set, 'a set] => bool ("op <") |
|
923 | 90 |
|
2261 | 91 |
syntax (symbols) |
2388 | 92 |
"_setle" :: ['a set, 'a set] => bool ("(_/ \\<subseteq> _)" [50, 51] 50) |
93 |
"_setle" :: ['a set, 'a set] => bool ("op \\<subseteq>") |
|
2684 | 94 |
"_setless" :: ['a set, 'a set] => bool ("(_/ \\<subset> _)" [50, 51] 50) |
95 |
"_setless" :: ['a set, 'a set] => bool ("op \\<subset>") |
|
2261 | 96 |
"op Int" :: ['a set, 'a set] => 'a set (infixl "\\<inter>" 70) |
97 |
"op Un" :: ['a set, 'a set] => 'a set (infixl "\\<union>" 65) |
|
98 |
"op :" :: ['a, 'a set] => bool ("(_/ \\<in> _)" [50, 51] 50) |
|
99 |
"op :" :: ['a, 'a set] => bool ("op \\<in>") |
|
100 |
"op ~:" :: ['a, 'a set] => bool ("(_/ \\<notin> _)" [50, 51] 50) |
|
101 |
"op ~:" :: ['a, 'a set] => bool ("op \\<notin>") |
|
102 |
"UN " :: [idts, bool] => bool ("(3\\<Union> _./ _)" 10) |
|
103 |
"INT " :: [idts, bool] => bool ("(3\\<Inter> _./ _)" 10) |
|
104 |
"@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Union> _\\<in>_./ _)" 10) |
|
105 |
"@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Inter> _\\<in>_./ _)" 10) |
|
106 |
Union :: (('a set) set) => 'a set ("\\<Union> _" [90] 90) |
|
107 |
Inter :: (('a set) set) => 'a set ("\\<Inter> _" [90] 90) |
|
2368 | 108 |
"@Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10) |
109 |
"@Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10) |
|
2372 | 110 |
|
111 |
syntax (symbols output) |
|
2368 | 112 |
"*Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10) |
113 |
"*Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10) |
|
2261 | 114 |
|
2412 | 115 |
translations |
116 |
"op \\<subseteq>" => "op <=" |
|
2684 | 117 |
"op \\<subset>" => "op <" |
2412 | 118 |
|
2261 | 119 |
|
120 |
||
121 |
(** Rules and definitions **) |
|
122 |
||
923 | 123 |
rules |
124 |
||
125 |
(* Isomorphisms between Predicates and Sets *) |
|
126 |
||
127 |
mem_Collect_eq "(a : {x.P(x)}) = P(a)" |
|
128 |
Collect_mem_eq "{x.x:A} = A" |
|
129 |
||
130 |
||
131 |
defs |
|
2261 | 132 |
|
923 | 133 |
Ball_def "Ball A P == ! x. x:A --> P(x)" |
134 |
Bex_def "Bex A P == ? x. x:A & P(x)" |
|
135 |
subset_def "A <= B == ! x:A. x:B" |
|
2393 | 136 |
Compl_def "Compl A == {x. ~x:A}" |
923 | 137 |
Un_def "A Un B == {x.x:A | x:B}" |
138 |
Int_def "A Int B == {x.x:A & x:B}" |
|
139 |
set_diff_def "A - B == {x. x:A & ~x:B}" |
|
140 |
INTER_def "INTER A B == {y. ! x:A. y: B(x)}" |
|
141 |
UNION_def "UNION A B == {y. ? x:A. y: B(x)}" |
|
2393 | 142 |
INTER1_def "INTER1 B == INTER {x.True} B" |
143 |
UNION1_def "UNION1 B == UNION {x.True} B" |
|
144 |
Inter_def "Inter S == (INT x:S. x)" |
|
145 |
Union_def "Union S == (UN x:S. x)" |
|
146 |
Pow_def "Pow A == {B. B <= A}" |
|
923 | 147 |
empty_def "{} == {x. False}" |
148 |
insert_def "insert a B == {x.x=a} Un B" |
|
149 |
image_def "f``A == {y. ? x:A. y=f(x)}" |
|
1273 | 150 |
|
923 | 151 |
end |
152 |
||
2261 | 153 |
|
923 | 154 |
ML |
155 |
||
156 |
local |
|
157 |
||
2388 | 158 |
(* Set inclusion *) |
159 |
||
160 |
fun le_tr' (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts = |
|
161 |
list_comb (Syntax.const "_setle", ts) |
|
162 |
| le_tr' (*op <=*) _ _ = raise Match; |
|
163 |
||
2684 | 164 |
fun less_tr' (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts = |
165 |
list_comb (Syntax.const "_setless", ts) |
|
166 |
| less_tr' (*op <*) _ _ = raise Match; |
|
167 |
||
2388 | 168 |
|
923 | 169 |
(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *) |
170 |
(* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *) |
|
171 |
||
172 |
val ex_tr = snd(mk_binder_tr("? ","Ex")); |
|
173 |
||
174 |
fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1 |
|
175 |
| nvars(_) = 1; |
|
176 |
||
177 |
fun setcompr_tr[e,idts,b] = |
|
178 |
let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e |
|
179 |
val P = Syntax.const("op &") $ eq $ b |
|
180 |
val exP = ex_tr [idts,P] |
|
181 |
in Syntax.const("Collect") $ Abs("",dummyT,exP) end; |
|
182 |
||
183 |
val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY")); |
|
184 |
||
185 |
fun setcompr_tr'[Abs(_,_,P)] = |
|
186 |
let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1) |
|
187 |
| ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) = |
|
188 |
if n>0 andalso m=n andalso |
|
189 |
((0 upto (n-1)) subset add_loose_bnos(e,0,[])) |
|
190 |
then () else raise Match |
|
191 |
||
192 |
fun tr'(_ $ abs) = |
|
193 |
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs] |
|
194 |
in Syntax.const("@SetCompr") $ e $ idts $ Q end |
|
195 |
in ok(P,0); tr'(P) end; |
|
196 |
||
197 |
in |
|
198 |
||
199 |
val parse_translation = [("@SetCompr", setcompr_tr)]; |
|
200 |
val print_translation = [("Collect", setcompr_tr')]; |
|
2684 | 201 |
val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')]; |
923 | 202 |
val print_ast_translation = |
203 |
map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")]; |
|
204 |
||
205 |
end; |