author  paulson 
Mon, 09 Sep 1996 11:08:01 +0200  
changeset 1962  e60a230da179 
parent 1883  00b4b6992945 
child 2006  72754e060aa2 
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 

9 
types 

10 
'a set 

11 

12 
arities 

13 
set :: (term) term 

14 

15 
instance 

16 
set :: (term) {ord, minus} 

17 

18 
consts 

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

19 
"{}" :: 'a set ("{}") 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

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

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

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

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

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

25 
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

26 
UNION1 :: ['a => 'b set] => 'b set (binder "UN " 10) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

27 
INTER1 :: ['a => 'b set] => 'b set (binder "INT " 10) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

28 
Union, Inter :: (('a set)set) => 'a set (*of a set*) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

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

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

31 
Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

32 
inj, surj :: ('a => 'b) => bool (*inj/surjective*) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

33 
inj_onto :: ['a => 'b, 'a set] => bool 
1962
e60a230da179
Corrected associativity: must be to right, as the type dictatess
paulson
parents:
1883
diff
changeset

34 
"``" :: ['a => 'b, 'a set] => ('b set) (infixr 90) 
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

35 
":" :: ['a, 'a set] => bool (infixl 50) (*membership*) 
923  36 

37 

38 
syntax 

39 

1531  40 
UNIV :: 'a set 
41 

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

42 
"~:" :: ['a, 'a set] => bool (infixl 50) 
923  43 

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

44 
"@Finset" :: args => 'a set ("{(_)}") 
923  45 

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

46 
"@Coll" :: [pttrn, bool] => 'a set ("(1{_./ _})") 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

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

49 
(* Big Intersection / Union *) 

50 

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

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

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

54 
(* Bounded Quantifiers *) 

55 

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

56 
"@Ball" :: [pttrn, 'a set, bool] => bool ("(3! _:_./ _)" 10) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

57 
"@Bex" :: [pttrn, 'a set, bool] => bool ("(3? _:_./ _)" 10) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

58 
"*Ball" :: [pttrn, 'a set, bool] => bool ("(3ALL _:_./ _)" 10) 
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1273
diff
changeset

59 
"*Bex" :: [pttrn, 'a set, bool] => bool ("(3EX _:_./ _)" 10) 
923  60 

61 
translations 

1531  62 
"UNIV" == "Compl {}" 
1883  63 
"range(f)" == "f``UNIV" 
923  64 
"x ~: y" == "~ (x : y)" 
65 
"{x, xs}" == "insert x {xs}" 

66 
"{x}" == "insert x {}" 

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

68 
"INT x:A. B" == "INTER A (%x. B)" 

69 
"UN x:A. B" == "UNION A (%x. B)" 

70 
"! x:A. P" == "Ball A (%x. P)" 

71 
"? x:A. P" == "Bex A (%x. P)" 

72 
"ALL x:A. P" => "Ball A (%x. P)" 

73 
"EX x:A. P" => "Bex A (%x. P)" 

74 

75 

76 
rules 

77 

78 
(* Isomorphisms between Predicates and Sets *) 

79 

80 
mem_Collect_eq "(a : {x.P(x)}) = P(a)" 

81 
Collect_mem_eq "{x.x:A} = A" 

82 

83 

84 
defs 

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

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

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

88 
Compl_def "Compl(A) == {x. ~x:A}" 

89 
Un_def "A Un B == {x.x:A  x:B}" 

90 
Int_def "A Int B == {x.x:A & x:B}" 

91 
set_diff_def "A  B == {x. x:A & ~x:B}" 

92 
INTER_def "INTER A B == {y. ! x:A. y: B(x)}" 

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

94 
INTER1_def "INTER1(B) == INTER {x.True} B" 

95 
UNION1_def "UNION1(B) == UNION {x.True} B" 

96 
Inter_def "Inter(S) == (INT x:S. x)" 

97 
Union_def "Union(S) == (UN x:S. x)" 

98 
Pow_def "Pow(A) == {B. B <= A}" 

99 
empty_def "{} == {x. False}" 

100 
insert_def "insert a B == {x.x=a} Un B" 

101 
image_def "f``A == {y. ? x:A. y=f(x)}" 

102 
inj_def "inj(f) == ! x y. f(x)=f(y) > x=y" 

103 
inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) > x=y" 

104 
surj_def "surj(f) == ! y. ? x. y=f(x)" 

105 

1273  106 
(* start 8bit 1 *) 
107 
(* end 8bit 1 *) 

108 

923  109 
end 
110 

111 
ML 

112 

113 
local 

114 

115 
(* Translates between { e  x1..xn. P} and {u. ? x1..xn. u=e & P} *) 

116 
(* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *) 

117 

118 
val ex_tr = snd(mk_binder_tr("? ","Ex")); 

119 

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

121 
 nvars(_) = 1; 

122 

123 
fun setcompr_tr[e,idts,b] = 

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

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

126 
val exP = ex_tr [idts,P] 

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

128 

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

130 

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

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

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

134 
if n>0 andalso m=n andalso 

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

136 
then () else raise Match 

137 

138 
fun tr'(_ $ abs) = 

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

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

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

142 

143 
in 

144 

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

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

147 
val print_ast_translation = 

148 
map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")]; 

149 

150 
end; 

151 