author  paulson 
Thu, 09 Jan 1997 10:23:39 +0100  
changeset 2499  0bc87b063447 
parent 2031  03a843f0f447 
child 2608  450c9b682a92 
permissions  rwrr 
1465  1 
(* Title: HOL/set 
923  2 
ID: $Id$ 
1465  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
923  4 
Copyright 1991 University of Cambridge 
5 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1937
diff
changeset

6 
Set theory for higherorder logic. A set is simply a predicate. 
923  7 
*) 
8 

9 
open Set; 

10 

1548  11 
section "Relating predicates and sets"; 
12 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

13 
AddIffs [mem_Collect_eq]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

14 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

15 
goal Set.thy "!!a. P(a) ==> a : {x.P(x)}"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

16 
by (Asm_simp_tac 1); 
923  17 
qed "CollectI"; 
18 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

19 
val prems = goal Set.thy "!!a. a : {x.P(x)} ==> P(a)"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

20 
by (Asm_full_simp_tac 1); 
923  21 
qed "CollectD"; 
22 

23 
val [prem] = goal Set.thy "[ !!x. (x:A) = (x:B) ] ==> A = B"; 

24 
by (rtac (prem RS ext RS arg_cong RS box_equals) 1); 

25 
by (rtac Collect_mem_eq 1); 

26 
by (rtac Collect_mem_eq 1); 

27 
qed "set_ext"; 

28 

29 
val [prem] = goal Set.thy "[ !!x. P(x)=Q(x) ] ==> {x. P(x)} = {x. Q(x)}"; 

30 
by (rtac (prem RS ext RS arg_cong) 1); 

31 
qed "Collect_cong"; 

32 

33 
val CollectE = make_elim CollectD; 

34 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

35 
AddSIs [CollectI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

36 
AddSEs [CollectE]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

37 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

38 

1548  39 
section "Bounded quantifiers"; 
923  40 

41 
val prems = goalw Set.thy [Ball_def] 

42 
"[ !!x. x:A ==> P(x) ] ==> ! x:A. P(x)"; 

43 
by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); 

44 
qed "ballI"; 

45 

46 
val [major,minor] = goalw Set.thy [Ball_def] 

47 
"[ ! x:A. P(x); x:A ] ==> P(x)"; 

48 
by (rtac (minor RS (major RS spec RS mp)) 1); 

49 
qed "bspec"; 

50 

51 
val major::prems = goalw Set.thy [Ball_def] 

52 
"[ ! x:A. P(x); P(x) ==> Q; x~:A ==> Q ] ==> Q"; 

53 
by (rtac (major RS spec RS impCE) 1); 

54 
by (REPEAT (eresolve_tac prems 1)); 

55 
qed "ballE"; 

56 

57 
(*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*) 

58 
fun ball_tac i = etac ballE i THEN contr_tac (i+1); 

59 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

60 
AddSIs [ballI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

61 
AddEs [ballE]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

62 

923  63 
val prems = goalw Set.thy [Bex_def] 
64 
"[ P(x); x:A ] ==> ? x:A. P(x)"; 

65 
by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)); 

66 
qed "bexI"; 

67 

68 
qed_goal "bexCI" Set.thy 

69 
"[ ! x:A. ~P(x) ==> P(a); a:A ] ==> ? x:A.P(x)" 

70 
(fn prems=> 

71 
[ (rtac classical 1), 

72 
(REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); 

73 

74 
val major::prems = goalw Set.thy [Bex_def] 

75 
"[ ? x:A. P(x); !!x. [ x:A; P(x) ] ==> Q ] ==> Q"; 

76 
by (rtac (major RS exE) 1); 

77 
by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); 

78 
qed "bexE"; 

79 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

80 
AddIs [bexI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

81 
AddSEs [bexE]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

82 

923  83 
(*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) 
1882  84 
goalw Set.thy [Ball_def] "(! x:A. True) = True"; 
85 
by (Simp_tac 1); 

1816  86 
qed "ball_True"; 
87 

1882  88 
(*Dual form for existentials*) 
89 
goalw Set.thy [Bex_def] "(? x:A. False) = False"; 

90 
by (Simp_tac 1); 

91 
qed "bex_False"; 

92 

93 
Addsimps [ball_True, bex_False]; 

923  94 

95 
(** Congruence rules **) 

96 

97 
val prems = goal Set.thy 

98 
"[ A=B; !!x. x:B ==> P(x) = Q(x) ] ==> \ 

99 
\ (! x:A. P(x)) = (! x:B. Q(x))"; 

100 
by (resolve_tac (prems RL [ssubst]) 1); 

101 
by (REPEAT (ares_tac [ballI,iffI] 1 

102 
ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1)); 

103 
qed "ball_cong"; 

104 

105 
val prems = goal Set.thy 

106 
"[ A=B; !!x. x:B ==> P(x) = Q(x) ] ==> \ 

107 
\ (? x:A. P(x)) = (? x:B. Q(x))"; 

108 
by (resolve_tac (prems RL [ssubst]) 1); 

109 
by (REPEAT (etac bexE 1 

110 
ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1)); 

111 
qed "bex_cong"; 

112 

1548  113 
section "Subsets"; 
923  114 

115 
val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B"; 

116 
by (REPEAT (ares_tac (prems @ [ballI]) 1)); 

117 
qed "subsetI"; 

118 

119 
(*Rule in Modus Ponens style*) 

120 
val major::prems = goalw Set.thy [subset_def] "[ A <= B; c:A ] ==> c:B"; 

121 
by (rtac (major RS bspec) 1); 

122 
by (resolve_tac prems 1); 

123 
qed "subsetD"; 

124 

125 
(*The same, with reversed premises for use with etac  cf rev_mp*) 

126 
qed_goal "rev_subsetD" Set.thy "[ c:A; A <= B ] ==> c:B" 

127 
(fn prems=> [ (REPEAT (resolve_tac (prems@[subsetD]) 1)) ]); 

128 

1920  129 
(*Converts A<=B to x:A ==> x:B*) 
130 
fun impOfSubs th = th RSN (2, rev_subsetD); 

131 

1841  132 
qed_goal "contra_subsetD" Set.thy "!!c. [ A <= B; c ~: B ] ==> c ~: A" 
133 
(fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]); 

134 

135 
qed_goal "rev_contra_subsetD" Set.thy "!!c. [ c ~: B; A <= B ] ==> c ~: A" 

136 
(fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]); 

137 

923  138 
(*Classical elimination rule*) 
139 
val major::prems = goalw Set.thy [subset_def] 

140 
"[ A <= B; c~:A ==> P; c:B ==> P ] ==> P"; 

141 
by (rtac (major RS ballE) 1); 

142 
by (REPEAT (eresolve_tac prems 1)); 

143 
qed "subsetCE"; 

144 

145 
(*Takes assumptions A<=B; c:A and creates the assumption c:B *) 

146 
fun set_mp_tac i = etac subsetCE i THEN mp_tac i; 

147 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

148 
AddSIs [subsetI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

149 
AddEs [subsetD, subsetCE]; 
923  150 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

151 
qed_goal "subset_refl" Set.thy "A <= (A::'a set)" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

152 
(fn _=> [Fast_tac 1]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

153 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

154 
val prems = goal Set.thy "!!B. [ A<=B; B<=C ] ==> A<=(C::'a set)"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

155 
by (Fast_tac 1); 
923  156 
qed "subset_trans"; 
157 

158 

1548  159 
section "Equality"; 
923  160 

161 
(*Antisymmetry of the subset relation*) 

162 
val prems = goal Set.thy "[ A <= B; B <= A ] ==> A = (B::'a set)"; 

163 
by (rtac (iffI RS set_ext) 1); 

164 
by (REPEAT (ares_tac (prems RL [subsetD]) 1)); 

165 
qed "subset_antisym"; 

166 
val equalityI = subset_antisym; 

167 

1762  168 
AddSIs [equalityI]; 
169 

923  170 
(* Equality rules from ZF set theory  are they appropriate here? *) 
171 
val prems = goal Set.thy "A = B ==> A<=(B::'a set)"; 

172 
by (resolve_tac (prems RL [subst]) 1); 

173 
by (rtac subset_refl 1); 

174 
qed "equalityD1"; 

175 

176 
val prems = goal Set.thy "A = B ==> B<=(A::'a set)"; 

177 
by (resolve_tac (prems RL [subst]) 1); 

178 
by (rtac subset_refl 1); 

179 
qed "equalityD2"; 

180 

181 
val prems = goal Set.thy 

182 
"[ A = B; [ A<=B; B<=(A::'a set) ] ==> P ] ==> P"; 

183 
by (resolve_tac prems 1); 

184 
by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); 

185 
qed "equalityE"; 

186 

187 
val major::prems = goal Set.thy 

188 
"[ A = B; [ c:A; c:B ] ==> P; [ c~:A; c~:B ] ==> P ] ==> P"; 

189 
by (rtac (major RS equalityE) 1); 

190 
by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); 

191 
qed "equalityCE"; 

192 

193 
(*Lemma for creating induction formulae  for "pattern matching" on p 

194 
To make the induction hypotheses usable, apply "spec" or "bspec" to 

195 
put universal quantifiers over the free variables in p. *) 

196 
val prems = goal Set.thy 

197 
"[ p:A; !!z. z:A ==> p=z > R ] ==> R"; 

198 
by (rtac mp 1); 

199 
by (REPEAT (resolve_tac (refl::prems) 1)); 

200 
qed "setup_induction"; 

201 

202 

1548  203 
section "Set complement  Compl"; 
923  204 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

205 
qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : Compl(A)) = (c~:A)" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

206 
(fn _ => [ (Fast_tac 1) ]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

207 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

208 
Addsimps [Compl_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

209 

923  210 
val prems = goalw Set.thy [Compl_def] 
211 
"[ c:A ==> False ] ==> c : Compl(A)"; 

212 
by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1)); 

213 
qed "ComplI"; 

214 

215 
(*This form, with negated conclusion, works well with the Classical prover. 

216 
Negated assumptions behave like formulae on the right side of the notional 

217 
turnstile...*) 

218 
val major::prems = goalw Set.thy [Compl_def] 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

219 
"c : Compl(A) ==> c~:A"; 
923  220 
by (rtac (major RS CollectD) 1); 
221 
qed "ComplD"; 

222 

223 
val ComplE = make_elim ComplD; 

224 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

225 
AddSIs [ComplI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

226 
AddSEs [ComplE]; 
1640  227 

923  228 

1548  229 
section "Binary union  Un"; 
923  230 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

231 
qed_goalw "Un_iff" Set.thy [Un_def] "(c : A Un B) = (c:A  c:B)" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

232 
(fn _ => [ Fast_tac 1 ]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

233 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

234 
Addsimps [Un_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

235 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

236 
goal Set.thy "!!c. c:A ==> c : A Un B"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

237 
by (Asm_simp_tac 1); 
923  238 
qed "UnI1"; 
239 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

240 
goal Set.thy "!!c. c:B ==> c : A Un B"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

241 
by (Asm_simp_tac 1); 
923  242 
qed "UnI2"; 
243 

244 
(*Classical introduction rule: no commitment to A vs B*) 

245 
qed_goal "UnCI" Set.thy "(c~:B ==> c:A) ==> c : A Un B" 

246 
(fn prems=> 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

247 
[ (Simp_tac 1), 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

248 
(REPEAT (ares_tac (prems@[disjCI]) 1)) ]); 
923  249 

250 
val major::prems = goalw Set.thy [Un_def] 

251 
"[ c : A Un B; c:A ==> P; c:B ==> P ] ==> P"; 

252 
by (rtac (major RS CollectD RS disjE) 1); 

253 
by (REPEAT (eresolve_tac prems 1)); 

254 
qed "UnE"; 

255 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

256 
AddSIs [UnCI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

257 
AddSEs [UnE]; 
1640  258 

923  259 

1548  260 
section "Binary intersection  Int"; 
923  261 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

262 
qed_goalw "Int_iff" Set.thy [Int_def] "(c : A Int B) = (c:A & c:B)" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

263 
(fn _ => [ (Fast_tac 1) ]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

264 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

265 
Addsimps [Int_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

266 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

267 
goal Set.thy "!!c. [ c:A; c:B ] ==> c : A Int B"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

268 
by (Asm_simp_tac 1); 
923  269 
qed "IntI"; 
270 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

271 
goal Set.thy "!!c. c : A Int B ==> c:A"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

272 
by (Asm_full_simp_tac 1); 
923  273 
qed "IntD1"; 
274 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

275 
goal Set.thy "!!c. c : A Int B ==> c:B"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

276 
by (Asm_full_simp_tac 1); 
923  277 
qed "IntD2"; 
278 

279 
val [major,minor] = goal Set.thy 

280 
"[ c : A Int B; [ c:A; c:B ] ==> P ] ==> P"; 

281 
by (rtac minor 1); 

282 
by (rtac (major RS IntD1) 1); 

283 
by (rtac (major RS IntD2) 1); 

284 
qed "IntE"; 

285 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

286 
AddSIs [IntI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

287 
AddSEs [IntE]; 
923  288 

1548  289 
section "Set difference"; 
923  290 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

291 
qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : AB) = (c:A & c~:B)" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

292 
(fn _ => [ (Fast_tac 1) ]); 
923  293 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

294 
Addsimps [Diff_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

295 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

296 
qed_goal "DiffI" Set.thy "!!c. [ c : A; c ~: B ] ==> c : A  B" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

297 
(fn _=> [ Asm_simp_tac 1 ]); 
923  298 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

299 
qed_goal "DiffD1" Set.thy "!!c. c : A  B ==> c : A" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

300 
(fn _=> [ (Asm_full_simp_tac 1) ]); 
923  301 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

302 
qed_goal "DiffD2" Set.thy "!!c. [ c : A  B; c : B ] ==> P" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

303 
(fn _=> [ (Asm_full_simp_tac 1) ]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

304 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

305 
qed_goal "DiffE" Set.thy "[ c : A  B; [ c:A; c~:B ] ==> P ] ==> P" 
923  306 
(fn prems=> 
307 
[ (resolve_tac prems 1), 

308 
(REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]); 

309 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

310 
AddSIs [DiffI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

311 
AddSEs [DiffE]; 
923  312 

1548  313 
section "The empty set  {}"; 
923  314 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

315 
qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

316 
(fn _ => [ (Fast_tac 1) ]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

317 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

318 
Addsimps [empty_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

319 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

320 
qed_goal "emptyE" Set.thy "!!a. a:{} ==> P" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

321 
(fn _ => [Full_simp_tac 1]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

322 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

323 
AddSEs [emptyE]; 
923  324 

325 
qed_goal "empty_subsetI" Set.thy "{} <= A" 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

326 
(fn _ => [ (Fast_tac 1) ]); 
923  327 

328 
qed_goal "equals0I" Set.thy "[ !!y. y:A ==> False ] ==> A={}" 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

329 
(fn [prem]=> 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

330 
[ (fast_tac (!claset addIs [prem RS FalseE]) 1) ]); 
923  331 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

332 
qed_goal "equals0D" Set.thy "!!a. [ A={}; a:A ] ==> P" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

333 
(fn _ => [ (Fast_tac 1) ]); 
1640  334 

1816  335 
goal Set.thy "Ball {} P = True"; 
336 
by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Ball_def, empty_def]) 1); 

337 
qed "ball_empty"; 

338 

339 
goal Set.thy "Bex {} P = False"; 

340 
by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Bex_def, empty_def]) 1); 

341 
qed "bex_empty"; 

342 
Addsimps [ball_empty, bex_empty]; 

343 

923  344 

1548  345 
section "Augmenting a set  insert"; 
923  346 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

347 
qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b  a:A)" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

348 
(fn _ => [Fast_tac 1]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

349 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

350 
Addsimps [insert_iff]; 
923  351 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

352 
qed_goal "insertI1" Set.thy "a : insert a B" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

353 
(fn _ => [Simp_tac 1]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

354 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

355 
qed_goal "insertI2" Set.thy "!!a. a : B ==> a : insert b B" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

356 
(fn _=> [Asm_simp_tac 1]); 
923  357 

358 
qed_goalw "insertE" Set.thy [insert_def] 

359 
"[ a : insert b A; a=b ==> P; a:A ==> P ] ==> P" 

360 
(fn major::prems=> 

361 
[ (rtac (major RS UnE) 1), 

362 
(REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]); 

363 

364 
(*Classical introduction rule*) 

365 
qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B" 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

366 
(fn prems=> 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

367 
[ (Simp_tac 1), 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

368 
(REPEAT (ares_tac (prems@[disjCI]) 1)) ]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

369 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

370 
AddSIs [insertCI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

371 
AddSEs [insertE]; 
923  372 

1548  373 
section "Singletons, using insert"; 
923  374 

375 
qed_goal "singletonI" Set.thy "a : {a}" 

376 
(fn _=> [ (rtac insertI1 1) ]); 

377 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

378 
goal Set.thy "!!a. b : {a} ==> b=a"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

379 
by (Fast_tac 1); 
923  380 
qed "singletonD"; 
381 

1776
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

382 
bind_thm ("singletonE", make_elim singletonD); 
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

383 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

384 
qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

385 
(fn _ => [Fast_tac 1]); 
923  386 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

387 
goal Set.thy "!!a b. {a}={b} ==> a=b"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

388 
by (fast_tac (!claset addEs [equalityE]) 1); 
923  389 
qed "singleton_inject"; 
390 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

391 
AddSDs [singleton_inject]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

392 

1531  393 

1548  394 
section "The universal set  UNIV"; 
1531  395 

1882  396 
qed_goal "UNIV_I" Set.thy "x : UNIV" 
397 
(fn _ => [rtac ComplI 1, etac emptyE 1]); 

398 

1531  399 
qed_goal "subset_UNIV" Set.thy "A <= UNIV" 
1882  400 
(fn _ => [rtac subsetI 1, rtac UNIV_I 1]); 
1531  401 

402 

1548  403 
section "Unions of families  UNION x:A. B(x) is Union(B``A)"; 
923  404 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

405 
goalw Set.thy [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

406 
by (Fast_tac 1); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

407 
qed "UN_iff"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

408 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

409 
Addsimps [UN_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

410 

923  411 
(*The order of the premises presupposes that A is rigid; b may be flexible*) 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

412 
goal Set.thy "!!b. [ a:A; b: B(a) ] ==> b: (UN x:A. B(x))"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

413 
by (Auto_tac()); 
923  414 
qed "UN_I"; 
415 

416 
val major::prems = goalw Set.thy [UNION_def] 

417 
"[ b : (UN x:A. B(x)); !!x.[ x:A; b: B(x) ] ==> R ] ==> R"; 

418 
by (rtac (major RS CollectD RS bexE) 1); 

419 
by (REPEAT (ares_tac prems 1)); 

420 
qed "UN_E"; 

421 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

422 
AddIs [UN_I]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

423 
AddSEs [UN_E]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

424 

923  425 
val prems = goal Set.thy 
426 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> \ 

427 
\ (UN x:A. C(x)) = (UN x:B. D(x))"; 

428 
by (REPEAT (etac UN_E 1 

429 
ORELSE ares_tac ([UN_I,equalityI,subsetI] @ 

1465  430 
(prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); 
923  431 
qed "UN_cong"; 
432 

433 

1548  434 
section "Intersections of families  INTER x:A. B(x) is Inter(B``A)"; 
923  435 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

436 
goalw Set.thy [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

437 
by (Auto_tac()); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

438 
qed "INT_iff"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

439 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

440 
Addsimps [INT_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

441 

923  442 
val prems = goalw Set.thy [INTER_def] 
443 
"(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"; 

444 
by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1)); 

445 
qed "INT_I"; 

446 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

447 
goal Set.thy "!!b. [ b : (INT x:A. B(x)); a:A ] ==> b: B(a)"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

448 
by (Auto_tac()); 
923  449 
qed "INT_D"; 
450 

451 
(*"Classical" elimination  by the Excluded Middle on a:A *) 

452 
val major::prems = goalw Set.thy [INTER_def] 

453 
"[ b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R ] ==> R"; 

454 
by (rtac (major RS CollectD RS ballE) 1); 

455 
by (REPEAT (eresolve_tac prems 1)); 

456 
qed "INT_E"; 

457 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

458 
AddSIs [INT_I]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

459 
AddEs [INT_D, INT_E]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

460 

923  461 
val prems = goal Set.thy 
462 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> \ 

463 
\ (INT x:A. C(x)) = (INT x:B. D(x))"; 

464 
by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI])); 

465 
by (REPEAT (dtac INT_D 1 

466 
ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1)); 

467 
qed "INT_cong"; 

468 

469 

1548  470 
section "Unions over a type; UNION1(B) = Union(range(B))"; 
923  471 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

472 
goalw Set.thy [UNION1_def] "(b: (UN x. B(x))) = (EX x. b: B(x))"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

473 
by (Simp_tac 1); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

474 
by (Fast_tac 1); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

475 
qed "UN1_iff"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

476 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

477 
Addsimps [UN1_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

478 

923  479 
(*The order of the premises presupposes that A is rigid; b may be flexible*) 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

480 
goal Set.thy "!!b. b: B(x) ==> b: (UN x. B(x))"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

481 
by (Auto_tac()); 
923  482 
qed "UN1_I"; 
483 

484 
val major::prems = goalw Set.thy [UNION1_def] 

485 
"[ b : (UN x. B(x)); !!x. b: B(x) ==> R ] ==> R"; 

486 
by (rtac (major RS UN_E) 1); 

487 
by (REPEAT (ares_tac prems 1)); 

488 
qed "UN1_E"; 

489 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

490 
AddIs [UN1_I]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

491 
AddSEs [UN1_E]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

492 

923  493 

1548  494 
section "Intersections over a type; INTER1(B) = Inter(range(B))"; 
923  495 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

496 
goalw Set.thy [INTER1_def] "(b: (INT x. B(x))) = (ALL x. b: B(x))"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

497 
by (Simp_tac 1); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

498 
by (Fast_tac 1); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

499 
qed "INT1_iff"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

500 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

501 
Addsimps [INT1_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

502 

923  503 
val prems = goalw Set.thy [INTER1_def] 
504 
"(!!x. b: B(x)) ==> b : (INT x. B(x))"; 

505 
by (REPEAT (ares_tac (INT_I::prems) 1)); 

506 
qed "INT1_I"; 

507 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

508 
goal Set.thy "!!b. b : (INT x. B(x)) ==> b: B(a)"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

509 
by (Asm_full_simp_tac 1); 
923  510 
qed "INT1_D"; 
511 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

512 
AddSIs [INT1_I]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

513 
AddDs [INT1_D]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

514 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

515 

1548  516 
section "Union"; 
923  517 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

518 
goalw Set.thy [Union_def] "(A : Union(C)) = (EX X:C. A:X)"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

519 
by (Fast_tac 1); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

520 
qed "Union_iff"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

521 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

522 
Addsimps [Union_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

523 

923  524 
(*The order of the premises presupposes that C is rigid; A may be flexible*) 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

525 
goal Set.thy "!!X. [ X:C; A:X ] ==> A : Union(C)"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

526 
by (Auto_tac()); 
923  527 
qed "UnionI"; 
528 

529 
val major::prems = goalw Set.thy [Union_def] 

530 
"[ A : Union(C); !!X.[ A:X; X:C ] ==> R ] ==> R"; 

531 
by (rtac (major RS UN_E) 1); 

532 
by (REPEAT (ares_tac prems 1)); 

533 
qed "UnionE"; 

534 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

535 
AddIs [UnionI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

536 
AddSEs [UnionE]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

537 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

538 

1548  539 
section "Inter"; 
923  540 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

541 
goalw Set.thy [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

542 
by (Fast_tac 1); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

543 
qed "Inter_iff"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

544 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

545 
Addsimps [Inter_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

546 

923  547 
val prems = goalw Set.thy [Inter_def] 
548 
"[ !!X. X:C ==> A:X ] ==> A : Inter(C)"; 

549 
by (REPEAT (ares_tac ([INT_I] @ prems) 1)); 

550 
qed "InterI"; 

551 

552 
(*A "destruct" rule  every X in C contains A as an element, but 

553 
A:X can hold when X:C does not! This rule is analogous to "spec". *) 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

554 
goal Set.thy "!!X. [ A : Inter(C); X:C ] ==> A:X"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

555 
by (Auto_tac()); 
923  556 
qed "InterD"; 
557 

558 
(*"Classical" elimination rule  does not require proving X:C *) 

559 
val major::prems = goalw Set.thy [Inter_def] 

560 
"[ A : Inter(C); A:X ==> R; X~:C ==> R ] ==> R"; 

561 
by (rtac (major RS INT_E) 1); 

562 
by (REPEAT (eresolve_tac prems 1)); 

563 
qed "InterE"; 

564 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

565 
AddSIs [InterI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

566 
AddEs [InterD, InterE]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

567 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

568 

1548  569 
section "The Powerset operator  Pow"; 
923  570 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

571 
qed_goalw "Pow_iff" Set.thy [Pow_def] "(A : Pow(B)) = (A <= B)" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

572 
(fn _ => [ (Asm_simp_tac 1) ]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

573 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

574 
AddIffs [Pow_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

575 

923  576 
qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)" 
577 
(fn _ => [ (etac CollectI 1) ]); 

578 

579 
qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B" 

580 
(fn _=> [ (etac CollectD 1) ]); 

581 

582 
val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *) 

583 
val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) 

1776
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

584 

d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

585 

d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

586 

d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

587 
(*** Set reasoning tools ***) 
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

588 

d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

589 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

590 
(*Each of these has ALREADY been added to !simpset above.*) 
2024
909153d8318f
Rationalized the rewriting of membership for {} and insert
paulson
parents:
1985
diff
changeset

591 
val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

592 
mem_Collect_eq, 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

593 
UN_iff, UN1_iff, Union_iff, 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

594 
INT_iff, INT1_iff, Inter_iff]; 
1776
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

595 

1937  596 
(*Not for Addsimps  it can cause goals to blow up!*) 
597 
goal Set.thy "(a : (if Q then x else y)) = ((Q > a:x) & (~Q > a : y))"; 

598 
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); 

599 
qed "mem_if"; 

600 

1776
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

601 
val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs; 
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

602 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

603 
simpset := !simpset addcongs [ball_cong,bex_cong] 
1776
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

604 
setmksimps (mksimps mksimps_pairs); 