author  wenzelm 
Wed, 16 Apr 1997 18:46:01 +0200  
changeset 2965  afbda7e26f15 
parent 2912  3fac3e8d5d3e 
child 3222  726a9b069947 
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 

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 nonmembership *) 

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 
2965
afbda7e26f15
improved translations for subset symbols syntax: constraints;
wenzelm
parents:
2912
diff
changeset

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

117 
"op \\<subset>" => "op < :: [_ set, _ set] => bool" 
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 (n1)) 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; 