author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8148  5ef0b624aadb 
child 10106  1b63e30437ee 
permissions  rwrr 
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 

3947  12 
global 
13 

923  14 
types 
15 
'a set 

16 

17 
arities 

18 
set :: (term) term 

19 

20 
instance 

5780
0187f936685a
Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
paulson
parents:
5492
diff
changeset

21 
set :: (term) {ord, minus} 
923  22 

3820  23 
syntax 
24 
"op :" :: ['a, 'a set] => bool ("op :") 

25 

923  26 
consts 
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

27 
"{}" :: 'a set ("{}") 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset

28 
UNIV :: 'a set 
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

29 
insert :: ['a, 'a set] => 'a set 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

30 
Collect :: ('a => bool) => 'a set (*comprehension*) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

31 
Int :: ['a set, 'a set] => 'a set (infixl 70) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

32 
Un :: ['a set, 'a set] => 'a set (infixl 65) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

33 
UNION, INTER :: ['a set, 'a => 'b set] => 'b set (*general*) 
2261  34 
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

35 
Pow :: 'a set => 'a set set (*powerset*) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

36 
range :: ('a => 'b) => 'b set (*of function*) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

37 
Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) 
8005  38 
"image" :: ['a => 'b, 'a set] => ('b set) (infixr "``" 90) 
2261  39 
(*membership*) 
40 
"op :" :: ['a, 'a set] => bool ("(_/ : _)" [50, 51] 50) 

923  41 

42 

2261  43 
(** Additional concrete syntax **) 
44 

923  45 
syntax 
46 

2261  47 
(* Infix syntax for nonmembership *) 
923  48 

3820  49 
"op ~:" :: ['a, 'a set] => bool ("op ~:") 
2261  50 
"op ~:" :: ['a, 'a set] => bool ("(_/ ~: _)" [50, 51] 50) 
923  51 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

52 

2261  53 
"@Finset" :: args => 'a set ("{(_)}") 
54 
"@Coll" :: [pttrn, bool] => 'a set ("(1{_./ _})") 

55 
"@SetCompr" :: ['a, idts, bool] => 'a set ("(1{_ /_./ _})") 

923  56 

57 
(* Big Intersection / Union *) 

58 

7358
9e95b846ad42
a little tidying; also FIXED BAD TYPE in INTER1, UNION1
paulson
parents:
7238
diff
changeset

59 
"@INTER1" :: [pttrns, 'b set] => 'b set ("(3INT _./ _)" 10) 
9e95b846ad42
a little tidying; also FIXED BAD TYPE in INTER1, UNION1
paulson
parents:
7238
diff
changeset

60 
"@UNION1" :: [pttrns, 'b set] => 'b set ("(3UN _./ _)" 10) 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset

61 

1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

62 
"@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

63 
"@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3UN _:_./ _)" 10) 
923  64 

65 
(* Bounded Quantifiers *) 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

66 
"_Ball" :: [pttrn, 'a set, bool] => bool ("(3ALL _:_./ _)" [0, 0, 10] 10) 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

67 
"_Bex" :: [pttrn, 'a set, bool] => bool ("(3EX _:_./ _)" [0, 0, 10] 10) 
923  68 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

69 
syntax (HOL) 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

70 
"_Ball" :: [pttrn, 'a set, bool] => bool ("(3! _:_./ _)" [0, 0, 10] 10) 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

71 
"_Bex" :: [pttrn, 'a set, bool] => bool ("(3? _:_./ _)" [0, 0, 10] 10) 
923  72 

73 
translations 

2261  74 
"range f" == "f``UNIV" 
923  75 
"x ~: y" == "~ (x : y)" 
76 
"{x, xs}" == "insert x {xs}" 

77 
"{x}" == "insert x {}" 

78 
"{x. P}" == "Collect (%x. P)" 

4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset

79 
"UN x y. B" == "UN x. UN y. B" 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset

80 
"UN x. B" == "UNION UNIV (%x. B)" 
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

81 
"INT x y. B" == "INT x. INT y. B" 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset

82 
"INT x. B" == "INTER UNIV (%x. B)" 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset

83 
"UN x:A. B" == "UNION A (%x. B)" 
923  84 
"INT x:A. B" == "INTER A (%x. B)" 
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

85 
"ALL x:A. P" == "Ball A (%x. P)" 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

86 
"EX x:A. P" == "Bex A (%x. P)" 
923  87 

2388  88 
syntax ("" output) 
3820  89 
"_setle" :: ['a set, 'a set] => bool ("op <=") 
2388  90 
"_setle" :: ['a set, 'a set] => bool ("(_/ <= _)" [50, 51] 50) 
3820  91 
"_setless" :: ['a set, 'a set] => bool ("op <") 
2684  92 
"_setless" :: ['a set, 'a set] => bool ("(_/ < _)" [50, 51] 50) 
923  93 

2261  94 
syntax (symbols) 
3820  95 
"_setle" :: ['a set, 'a set] => bool ("op \\<subseteq>") 
2388  96 
"_setle" :: ['a set, 'a set] => bool ("(_/ \\<subseteq> _)" [50, 51] 50) 
3820  97 
"_setless" :: ['a set, 'a set] => bool ("op \\<subset>") 
2684  98 
"_setless" :: ['a set, 'a set] => bool ("(_/ \\<subset> _)" [50, 51] 50) 
2261  99 
"op Int" :: ['a set, 'a set] => 'a set (infixl "\\<inter>" 70) 
100 
"op Un" :: ['a set, 'a set] => 'a set (infixl "\\<union>" 65) 

3820  101 
"op :" :: ['a, 'a set] => bool ("op \\<in>") 
2261  102 
"op :" :: ['a, 'a set] => bool ("(_/ \\<in> _)" [50, 51] 50) 
3820  103 
"op ~:" :: ['a, 'a set] => bool ("op \\<notin>") 
2261  104 
"op ~:" :: ['a, 'a set] => bool ("(_/ \\<notin> _)" [50, 51] 50) 
8148
5ef0b624aadb
beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents:
8005
diff
changeset

105 
"UN " :: [idts, bool] => bool ("(3\\<Union>_./ _)" 10) 
5ef0b624aadb
beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents:
8005
diff
changeset

106 
"INT " :: [idts, bool] => bool ("(3\\<Inter>_./ _)" 10) 
5ef0b624aadb
beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents:
8005
diff
changeset

107 
"@UNION1" :: [pttrn, 'b set] => 'b set ("(3\\<Union>_./ _)" 10) 
5ef0b624aadb
beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents:
8005
diff
changeset

108 
"@INTER1" :: [pttrn, 'b set] => 'b set ("(3\\<Inter>_./ _)" 10) 
5ef0b624aadb
beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents:
8005
diff
changeset

109 
"@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Union>_\\<in>_./ _)" 10) 
5ef0b624aadb
beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents:
8005
diff
changeset

110 
"@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Inter>_\\<in>_./ _)" 10) 
5ef0b624aadb
beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents:
8005
diff
changeset

111 
Union :: (('a set) set) => 'a set ("\\<Union>_" [90] 90) 
5ef0b624aadb
beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents:
8005
diff
changeset

112 
Inter :: (('a set) set) => 'a set ("\\<Inter>_" [90] 90) 
5ef0b624aadb
beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents:
8005
diff
changeset

113 
"_Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall>_\\<in>_./ _)" [0, 0, 10] 10) 
5ef0b624aadb
beautified spacing for binders with symbols syntax, analogous to HOL.thy
oheimb
parents:
8005
diff
changeset

114 
"_Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists>_\\<in>_./ _)" [0, 0, 10] 10) 
2261  115 

2412  116 
translations 
2965
afbda7e26f15
improved translations for subset symbols syntax: constraints;
wenzelm
parents:
2912
diff
changeset

117 
"op \\<subseteq>" => "op <= :: [_ set, _ set] => bool" 
afbda7e26f15
improved translations for subset symbols syntax: constraints;
wenzelm
parents:
2912
diff
changeset

118 
"op \\<subset>" => "op < :: [_ set, _ set] => bool" 
2412  119 

2261  120 

121 

122 
(** Rules and definitions **) 

123 

3947  124 
local 
125 

923  126 
rules 
127 

128 
(* Isomorphisms between Predicates and Sets *) 

129 

3842  130 
mem_Collect_eq "(a : {x. P(x)}) = P(a)" 
131 
Collect_mem_eq "{x. x:A} = A" 

923  132 

133 

134 
defs 

135 
Ball_def "Ball A P == ! x. x:A > P(x)" 

136 
Bex_def "Bex A P == ? x. x:A & P(x)" 

137 
subset_def "A <= B == ! x:A. x:B" 

3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2965
diff
changeset

138 
psubset_def "A < B == (A::'a set) <= B & ~ A=B" 
5492  139 
Compl_def " A == {x. ~x:A}" 
3842  140 
Un_def "A Un B == {x. x:A  x:B}" 
141 
Int_def "A Int B == {x. x:A & x:B}" 

923  142 
set_diff_def "A  B == {x. x:A & ~x:B}" 
143 
INTER_def "INTER A B == {y. ! x:A. y: B(x)}" 

144 
UNION_def "UNION A B == {y. ? x:A. y: B(x)}" 

2393  145 
Inter_def "Inter S == (INT x:S. x)" 
146 
Union_def "Union S == (UN x:S. x)" 

147 
Pow_def "Pow A == {B. B <= A}" 

923  148 
empty_def "{} == {x. False}" 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset

149 
UNIV_def "UNIV == {x. True}" 
3842  150 
insert_def "insert a B == {x. x=a} Un B" 
923  151 
image_def "f``A == {y. ? x:A. y=f(x)}" 
1273  152 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

153 

923  154 
end 
155 

2261  156 

923  157 
ML 
158 

159 
local 

160 

2388  161 
(* Set inclusion *) 
162 

4151  163 
fun le_tr' _ (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts = 
2388  164 
list_comb (Syntax.const "_setle", ts) 
4151  165 
 le_tr' _ (*op <=*) _ _ = raise Match; 
2388  166 

4151  167 
fun less_tr' _ (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts = 
2684  168 
list_comb (Syntax.const "_setless", ts) 
4151  169 
 less_tr' _ (*op <*) _ _ = raise Match; 
2684  170 

2388  171 

923  172 
(* Translates between { e  x1..xn. P} and {u. ? x1..xn. u=e & P} *) 
173 
(* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *) 

174 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

175 
val ex_tr = snd(mk_binder_tr("EX ","Ex")); 
923  176 

177 
fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1 

178 
 nvars(_) = 1; 

179 

180 
fun setcompr_tr[e,idts,b] = 

181 
let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e 

182 
val P = Syntax.const("op &") $ eq $ b 

183 
val exP = ex_tr [idts,P] 

184 
in Syntax.const("Collect") $ Abs("",dummyT,exP) end; 

185 

186 
val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY")); 

187 

188 
fun setcompr_tr'[Abs(_,_,P)] = 

189 
let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1) 

190 
 ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) = 

191 
if n>0 andalso m=n andalso 

192 
((0 upto (n1)) subset add_loose_bnos(e,0,[])) 

193 
then () else raise Match 

194 

195 
fun tr'(_ $ abs) = 

196 
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs] 

197 
in Syntax.const("@SetCompr") $ e $ idts $ Q end 

198 
in ok(P,0); tr'(P) end; 

199 

200 
in 

201 

202 
val parse_translation = [("@SetCompr", setcompr_tr)]; 

203 
val print_translation = [("Collect", setcompr_tr')]; 

2684  204 
val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')]; 
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

205 

923  206 

207 
end; 