author  wenzelm 
Sun, 28 Oct 2001 22:59:12 +0100  
changeset 11979  0a3dace545c5 
parent 11752  8941d8d15dc8 
child 11982  65e2822d83dd 
permissions  rwrr 
923  1 
(* Title: HOL/Set.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1993 University of Cambridge 

5 
*) 

6 

11979  7 
header {* Set theory for higherorder logic *} 
8 

9 
theory Set = HOL 

10 
files ("subset.ML") ("equalities.ML") ("mono.ML"): 

11 

12 
text {* A set in HOL is simply a predicate. *} 

923  13 

2261  14 

11979  15 
subsection {* Basic syntax *} 
2261  16 

3947  17 
global 
18 

11979  19 
typedecl 'a set 
20 
arities set :: ("term") "term" 

3820  21 

923  22 
consts 
11979  23 
"{}" :: "'a set" ("{}") 
24 
UNIV :: "'a set" 

25 
insert :: "'a => 'a set => 'a set" 

26 
Collect :: "('a => bool) => 'a set"  "comprehension" 

27 
Int :: "'a set => 'a set => 'a set" (infixl 70) 

28 
Un :: "'a set => 'a set => 'a set" (infixl 65) 

29 
UNION :: "'a set => ('a => 'b set) => 'b set"  "general union" 

30 
INTER :: "'a set => ('a => 'b set) => 'b set"  "general intersection" 

31 
Union :: "'a set set => 'a set"  "union of a set" 

32 
Inter :: "'a set set => 'a set"  "intersection of a set" 

33 
Pow :: "'a set => 'a set set"  "powerset" 

34 
Ball :: "'a set => ('a => bool) => bool"  "bounded universal quantifiers" 

35 
Bex :: "'a set => ('a => bool) => bool"  "bounded existential quantifiers" 

36 
image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) 

37 

38 
syntax 

39 
"op :" :: "'a => 'a set => bool" ("op :") 

40 
consts 

41 
"op :" :: "'a => 'a set => bool" ("(_/ : _)" [50, 51] 50)  "membership" 

42 

43 
local 

44 

45 
instance set :: ("term") ord .. 

46 
instance set :: ("term") minus .. 

923  47 

48 

11979  49 
subsection {* Additional concrete syntax *} 
2261  50 

923  51 
syntax 
11979  52 
range :: "('a => 'b) => 'b set"  "of function" 
923  53 

11979  54 
"op ~:" :: "'a => 'a set => bool" ("op ~:")  "nonmembership" 
55 
"op ~:" :: "'a => 'a set => bool" ("(_/ ~: _)" [50, 51] 50) 

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

56 

11979  57 
"@Finset" :: "args => 'a set" ("{(_)}") 
58 
"@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})") 

59 
"@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ /_./ _})") 

923  60 

11979  61 
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" 10) 
62 
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" 10) 

63 
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" 10) 

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

923  65 

11979  66 
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10) 
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) 
11979  70 
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10) 
71 
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10) 

923  72 

73 
translations 

10832  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) 
11979  89 
"_setle" :: "'a set => 'a set => bool" ("op <=") 
90 
"_setle" :: "'a set => 'a set => bool" ("(_/ <= _)" [50, 51] 50) 

91 
"_setless" :: "'a set => 'a set => bool" ("op <") 

92 
"_setless" :: "'a set => 'a set => bool" ("(_/ < _)" [50, 51] 50) 

923  93 

2261  94 
syntax (symbols) 
11979  95 
"_setle" :: "'a set => 'a set => bool" ("op \<subseteq>") 
96 
"_setle" :: "'a set => 'a set => bool" ("(_/ \<subseteq> _)" [50, 51] 50) 

97 
"_setless" :: "'a set => 'a set => bool" ("op \<subset>") 

98 
"_setless" :: "'a set => 'a set => bool" ("(_/ \<subset> _)" [50, 51] 50) 

99 
"op Int" :: "'a set => 'a set => 'a set" (infixl "\<inter>" 70) 

100 
"op Un" :: "'a set => 'a set => 'a set" (infixl "\<union>" 65) 

101 
"op :" :: "'a => 'a set => bool" ("op \<in>") 

102 
"op :" :: "'a => 'a set => bool" ("(_/ \<in> _)" [50, 51] 50) 

103 
"op ~:" :: "'a => 'a set => bool" ("op \<notin>") 

104 
"op ~:" :: "'a => 'a set => bool" ("(_/ \<notin> _)" [50, 51] 50) 

105 
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" 10) 

106 
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" 10) 

107 
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" 10) 

108 
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" 10) 

109 
Union :: "'a set set => 'a set" ("\<Union>_" [90] 90) 

110 
Inter :: "'a set set => 'a set" ("\<Inter>_" [90] 90) 

111 
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10) 

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

2261  113 

2412  114 
translations 
11979  115 
"op \<subseteq>" => "op <= :: _ set => _ set => bool" 
116 
"op \<subset>" => "op < :: _ set => _ set => bool" 

2261  117 

118 

11979  119 
typed_print_translation {* 
120 
let 

121 
fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts = 

122 
list_comb (Syntax.const "_setle", ts) 

123 
 le_tr' _ _ _ = raise Match; 

124 

125 
fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts = 

126 
list_comb (Syntax.const "_setless", ts) 

127 
 less_tr' _ _ _ = raise Match; 

128 
in [("op <=", le_tr'), ("op <", less_tr')] end 

129 
*} 

2261  130 

11979  131 
text {* 
132 
\medskip Translate between @{text "{e  x1...xn. P}"} and @{text 

133 
"{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is 

134 
only translated if @{text "[0..n] subset bvs(e)"}. 

135 
*} 

136 

137 
parse_translation {* 

138 
let 

139 
val ex_tr = snd (mk_binder_tr ("EX ", "Ex")); 

3947  140 

11979  141 
fun nvars (Const ("_idts", _) $ _ $ idts) = nvars idts + 1 
142 
 nvars _ = 1; 

143 

144 
fun setcompr_tr [e, idts, b] = 

145 
let 

146 
val eq = Syntax.const "op =" $ Bound (nvars idts) $ e; 

147 
val P = Syntax.const "op &" $ eq $ b; 

148 
val exP = ex_tr [idts, P]; 

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

150 

151 
in [("@SetCompr", setcompr_tr)] end; 

152 
*} 

923  153 

11979  154 
print_translation {* 
155 
let 

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

157 

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

159 
let 

160 
fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1) 

161 
 check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) = 

162 
if n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso 

163 
((0 upto (n  1)) subset add_loose_bnos (e, 0, [])) then () 

164 
else raise Match; 

923  165 

11979  166 
fun tr' (_ $ abs) = 
167 
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs] 

168 
in Syntax.const "@SetCompr" $ e $ idts $ Q end; 

169 
in check (P, 0); tr' P end; 

170 
in [("Collect", setcompr_tr')] end; 

171 
*} 

172 

173 

174 
subsection {* Rules and definitions *} 

175 

176 
text {* Isomorphisms between predicates and sets. *} 

923  177 

11979  178 
axioms 
179 
mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)" 

180 
Collect_mem_eq [simp]: "{x. x:A} = A" 

181 

182 
defs 

183 
Ball_def: "Ball A P == ALL x. x:A > P(x)" 

184 
Bex_def: "Bex A P == EX x. x:A & P(x)" 

185 

186 
defs (overloaded) 

187 
subset_def: "A <= B == ALL x:A. x:B" 

188 
psubset_def: "A < B == (A::'a set) <= B & ~ A=B" 

189 
Compl_def: " A == {x. ~x:A}" 

923  190 

191 
defs 

11979  192 
Un_def: "A Un B == {x. x:A  x:B}" 
193 
Int_def: "A Int B == {x. x:A & x:B}" 

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

195 
INTER_def: "INTER A B == {y. ALL x:A. y: B(x)}" 

196 
UNION_def: "UNION A B == {y. EX x:A. y: B(x)}" 

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

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

199 
Pow_def: "Pow A == {B. B <= A}" 

200 
empty_def: "{} == {x. False}" 

201 
UNIV_def: "UNIV == {x. True}" 

202 
insert_def: "insert a B == {x. x=a} Un B" 

203 
image_def: "f`A == {y. EX x:A. y = f(x)}" 

204 

205 

206 
subsection {* Lemmas and proof tool setup *} 

207 

208 
subsubsection {* Relating predicates and sets *} 

209 

210 
lemma CollectI [intro!]: "P(a) ==> a : {x. P(x)}" 

211 
by simp 

212 

213 
lemma CollectD: "a : {x. P(x)} ==> P(a)" 

214 
by simp 

215 

216 
lemma set_ext: "(!!x. (x:A) = (x:B)) ==> A = B" 

217 
proof  

218 
case rule_context 

219 
show ?thesis 

220 
apply (rule prems [THEN ext, THEN arg_cong, THEN box_equals]) 

221 
apply (rule Collect_mem_eq) 

222 
apply (rule Collect_mem_eq) 

223 
done 

224 
qed 

225 

226 
lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}" 

227 
by simp 

228 

229 
lemmas CollectE [elim!] = CollectD [elim_format] 

230 

231 

232 
subsubsection {* Bounded quantifiers *} 

233 

234 
lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x" 

235 
by (simp add: Ball_def) 

236 

237 
lemmas strip = impI allI ballI 

238 

239 
lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x" 

240 
by (simp add: Ball_def) 

241 

242 
lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q" 

243 
by (unfold Ball_def) blast 

244 

245 
text {* 

246 
\medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and 

247 
@{prop "a:A"}; creates assumption @{prop "P a"}. 

248 
*} 

249 

250 
ML {* 

251 
local val ballE = thm "ballE" 

252 
in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end; 

253 
*} 

254 

255 
text {* 

256 
Gives better instantiation for bound: 

257 
*} 

258 

259 
ML_setup {* 

260 
claset_ref() := claset() addbefore ("bspec", datac (thm "bspec") 1); 

261 
*} 

262 

263 
lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x" 

264 
 {* Normally the best argument order: @{prop "P x"} constrains the 

265 
choice of @{prop "x:A"}. *} 

266 
by (unfold Bex_def) blast 

267 

268 
lemma rev_bexI: "x:A ==> P x ==> EX x:A. P x" 

269 
 {* The best argument order when there is only one @{prop "x:A"}. *} 

270 
by (unfold Bex_def) blast 

271 

272 
lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x" 

273 
by (unfold Bex_def) blast 

274 

275 
lemma bexE [elim!]: "EX x:A. P x ==> (!!x. x:A ==> P x ==> Q) ==> Q" 

276 
by (unfold Bex_def) blast 

277 

278 
lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) > P)" 

279 
 {* Trival rewrite rule. *} 

280 
by (simp add: Ball_def) 

281 

282 
lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)" 

283 
 {* Dual form for existentials. *} 

284 
by (simp add: Bex_def) 

285 

286 
lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)" 

287 
by blast 

288 

289 
lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)" 

290 
by blast 

291 

292 
lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)" 

293 
by blast 

294 

295 
lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)" 

296 
by blast 

297 

298 
lemma ball_one_point1 [simp]: "(ALL x:A. x = a > P x) = (a:A > P a)" 

299 
by blast 

300 

301 
lemma ball_one_point2 [simp]: "(ALL x:A. a = x > P x) = (a:A > P a)" 

302 
by blast 

303 

304 
ML_setup {* 

305 
let 

306 
val Ball_def = thm "Ball_def"; 

307 
val Bex_def = thm "Bex_def"; 

308 

309 
val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) 

310 
("EX x:A. P x & Q x", HOLogic.boolT); 

311 

312 
val prove_bex_tac = 

313 
rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac; 

314 
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; 

315 

316 
val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) 

317 
("ALL x:A. P x > Q x", HOLogic.boolT); 

318 

319 
val prove_ball_tac = 

320 
rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac; 

321 
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; 

322 

323 
val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex; 

324 
val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball; 

325 
in 

326 
Addsimprocs [defBALL_regroup, defBEX_regroup] 

327 
end; 

328 
*} 

329 

330 

331 
subsubsection {* Congruence rules *} 

332 

333 
lemma ball_cong [cong]: 

334 
"A = B ==> (!!x. x:B ==> P x = Q x) ==> 

335 
(ALL x:A. P x) = (ALL x:B. Q x)" 

336 
by (simp add: Ball_def) 

337 

338 
lemma bex_cong [cong]: 

339 
"A = B ==> (!!x. x:B ==> P x = Q x) ==> 

340 
(EX x:A. P x) = (EX x:B. Q x)" 

341 
by (simp add: Bex_def cong: conj_cong) 

1273  342 

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

343 

11979  344 
subsubsection {* Subsets *} 
345 

346 
lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A <= B" 

347 
by (simp add: subset_def) 

348 

349 
text {* 

350 
\medskip Map the type @{text "'a set => anything"} to just @{typ 

351 
'a}; for overloading constants whose first argument has type @{typ 

352 
"'a set"}. 

353 
*} 

354 

355 
ML {* 

356 
fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type); 

357 
*} 

358 

359 
ML " 

360 
(* While (:) is not, its type must be kept 

361 
for overloading of = to work. *) 

362 
Blast.overloaded (\"op :\", domain_type); 

363 

364 
overload_1st_set \"Ball\"; (*need UNION, INTER also?*) 

365 
overload_1st_set \"Bex\"; 

366 

367 
(*Image: retain the type of the set being expressed*) 

368 
Blast.overloaded (\"image\", domain_type); 

369 
" 

370 

371 
lemma subsetD [elim]: "A <= B ==> c:A ==> c:B" 

372 
 {* Rule in Modus Ponens style. *} 

373 
by (unfold subset_def) blast 

374 

375 
declare subsetD [intro?]  FIXME 

376 

377 
lemma rev_subsetD: "c:A ==> A <= B ==> c:B" 

378 
 {* The same, with reversed premises for use with @{text erule}  

379 
cf @{text rev_mp}. *} 

380 
by (rule subsetD) 

381 

382 
declare rev_subsetD [intro?]  FIXME 

383 

384 
text {* 

385 
\medskip Converts @{prop "A <= B"} to @{prop "x:A ==> x:B"}. 

386 
*} 

387 

388 
ML {* 

389 
local val rev_subsetD = thm "rev_subsetD" 

390 
in fun impOfSubs th = th RSN (2, rev_subsetD) end; 

391 
*} 

392 

393 
lemma subsetCE [elim]: "A <= B ==> (c~:A ==> P) ==> (c:B ==> P) ==> P" 

394 
 {* Classical elimination rule. *} 

395 
by (unfold subset_def) blast 

396 

397 
text {* 

398 
\medskip Takes assumptions @{prop "A <= B"}; @{prop "c:A"} and 

399 
creates the assumption @{prop "c:B"}. 

400 
*} 

401 

402 
ML {* 

403 
local val subsetCE = thm "subsetCE" 

404 
in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end; 

405 
*} 

406 

407 
lemma contra_subsetD: "A <= B ==> c ~: B ==> c ~: A" 

408 
by blast 

409 

410 
lemma subset_refl: "A <= (A::'a set)" 

411 
by fast 

412 

413 
lemma subset_trans: "A <= B ==> B <= C ==> A <= (C::'a set)" 

414 
by blast 

923  415 

2261  416 

11979  417 
subsubsection {* Equality *} 
418 

419 
lemma subset_antisym [intro!]: "A <= B ==> B <= A ==> A = (B::'a set)" 

420 
 {* Antisymmetry of the subset relation. *} 

421 
by (rule set_ext) (blast intro: subsetD) 

422 

423 
lemmas equalityI = subset_antisym 

424 

425 
text {* 

426 
\medskip Equality rules from ZF set theory  are they appropriate 

427 
here? 

428 
*} 

429 

430 
lemma equalityD1: "A = B ==> A <= (B::'a set)" 

431 
by (simp add: subset_refl) 

432 

433 
lemma equalityD2: "A = B ==> B <= (A::'a set)" 

434 
by (simp add: subset_refl) 

435 

436 
text {* 

437 
\medskip Be careful when adding this to the claset as @{text 

438 
subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{} 

439 
<= A"} and @{prop "A <= {}"} and then back to @{prop "A = {}"}! 

440 
*} 

441 

442 
lemma equalityE: "A = B ==> (A <= B ==> B <= (A::'a set) ==> P) ==> P" 

443 
by (simp add: subset_refl) 

923  444 

11979  445 
lemma equalityCE [elim]: 
446 
"A = B ==> (c:A ==> c:B ==> P) ==> (c~:A ==> c~:B ==> P) ==> P" 

447 
by blast 

448 

449 
text {* 

450 
\medskip Lemma for creating induction formulae  for "pattern 

451 
matching" on @{text p}. To make the induction hypotheses usable, 

452 
apply @{text spec} or @{text bspec} to put universal quantifiers over the free 

453 
variables in @{text p}. 

454 
*} 

455 

456 
lemma setup_induction: "p:A ==> (!!z. z:A ==> p = z > R) ==> R" 

457 
by simp 

923  458 

11979  459 
lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)" 
460 
by simp 

461 

462 

463 
subsubsection {* The universal set  UNIV *} 

464 

465 
lemma UNIV_I [simp]: "x : UNIV" 

466 
by (simp add: UNIV_def) 

467 

468 
declare UNIV_I [intro]  {* unsafe makes it less likely to cause problems *} 

469 

470 
lemma UNIV_witness [intro?]: "EX x. x : UNIV" 

471 
by simp 

472 

473 
lemma subset_UNIV: "A <= UNIV" 

474 
by (rule subsetI) (rule UNIV_I) 

2388  475 

11979  476 
text {* 
477 
\medskip Etacontracting these two rules (to remove @{text P}) 

478 
causes them to be ignored because of their interaction with 

479 
congruence rules. 

480 
*} 

481 

482 
lemma ball_UNIV [simp]: "Ball UNIV P = All P" 

483 
by (simp add: Ball_def) 

484 

485 
lemma bex_UNIV [simp]: "Bex UNIV P = Ex P" 

486 
by (simp add: Bex_def) 

487 

488 

489 
subsubsection {* The empty set *} 

490 

491 
lemma empty_iff [simp]: "(c : {}) = False" 

492 
by (simp add: empty_def) 

493 

494 
lemma emptyE [elim!]: "a : {} ==> P" 

495 
by simp 

496 

497 
lemma empty_subsetI [iff]: "{} <= A" 

498 
 {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *} 

499 
by blast 

500 

501 
lemma equals0I: "(!!y. y:A ==> False) ==> A = {}" 

502 
by blast 

2388  503 

11979  504 
lemma equals0D: "A={} ==> a ~: A" 
505 
 {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *} 

506 
by blast 

507 

508 
lemma ball_empty [simp]: "Ball {} P = True" 

509 
by (simp add: Ball_def) 

510 

511 
lemma bex_empty [simp]: "Bex {} P = False" 

512 
by (simp add: Bex_def) 

513 

514 
lemma UNIV_not_empty [iff]: "UNIV ~= {}" 

515 
by (blast elim: equalityE) 

516 

517 

518 
section {* The Powerset operator  Pow *} 

519 

520 
lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)" 

521 
by (simp add: Pow_def) 

522 

523 
lemma PowI: "A <= B ==> A : Pow B" 

524 
by (simp add: Pow_def) 

525 

526 
lemma PowD: "A : Pow B ==> A <= B" 

527 
by (simp add: Pow_def) 

528 

529 
lemma Pow_bottom: "{}: Pow B" 

530 
by simp 

531 

532 
lemma Pow_top: "A : Pow A" 

533 
by (simp add: subset_refl) 

2684  534 

2388  535 

11979  536 
subsubsection {* Set complement *} 
537 

538 
lemma Compl_iff [simp]: "(c : A) = (c~:A)" 

539 
by (unfold Compl_def) blast 

540 

541 
lemma ComplI [intro!]: "(c:A ==> False) ==> c : A" 

542 
by (unfold Compl_def) blast 

543 

544 
text {* 

545 
\medskip This form, with negated conclusion, works well with the 

546 
Classical prover. Negated assumptions behave like formulae on the 

547 
right side of the notional turnstile ... *} 

548 

549 
lemma ComplD: "c : A ==> c~:A" 

550 
by (unfold Compl_def) blast 

551 

552 
lemmas ComplE [elim!] = ComplD [elim_format] 

553 

554 

555 
subsubsection {* Binary union  Un *} 

923  556 

11979  557 
lemma Un_iff [simp]: "(c : A Un B) = (c:A  c:B)" 
558 
by (unfold Un_def) blast 

559 

560 
lemma UnI1 [elim?]: "c:A ==> c : A Un B" 

561 
by simp 

562 

563 
lemma UnI2 [elim?]: "c:B ==> c : A Un B" 

564 
by simp 

923  565 

11979  566 
text {* 
567 
\medskip Classical introduction rule: no commitment to @{prop A} vs 

568 
@{prop B}. 

569 
*} 

570 

571 
lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B" 

572 
by auto 

573 

574 
lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P" 

575 
by (unfold Un_def) blast 

576 

577 

578 
section {* Binary intersection  Int *} 

923  579 

11979  580 
lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)" 
581 
by (unfold Int_def) blast 

582 

583 
lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B" 

584 
by simp 

585 

586 
lemma IntD1: "c : A Int B ==> c:A" 

587 
by simp 

588 

589 
lemma IntD2: "c : A Int B ==> c:B" 

590 
by simp 

591 

592 
lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P" 

593 
by simp 

594 

595 

596 
section {* Set difference *} 

597 

598 
lemma Diff_iff [simp]: "(c : A  B) = (c:A & c~:B)" 

599 
by (unfold set_diff_def) blast 

923  600 

11979  601 
lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A  B" 
602 
by simp 

603 

604 
lemma DiffD1: "c : A  B ==> c : A" 

605 
by simp 

606 

607 
lemma DiffD2: "c : A  B ==> c : B ==> P" 

608 
by simp 

609 

610 
lemma DiffE [elim!]: "c : A  B ==> (c:A ==> c~:B ==> P) ==> P" 

611 
by simp 

612 

613 

614 
subsubsection {* Augmenting a set  insert *} 

615 

616 
lemma insert_iff [simp]: "(a : insert b A) = (a = b  a:A)" 

617 
by (unfold insert_def) blast 

618 

619 
lemma insertI1: "a : insert a B" 

620 
by simp 

621 

622 
lemma insertI2: "a : B ==> a : insert b B" 

623 
by simp 

923  624 

11979  625 
lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P" 
626 
by (unfold insert_def) blast 

627 

628 
lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B" 

629 
 {* Classical introduction rule. *} 

630 
by auto 

631 

632 
lemma subset_insert_iff: "(A <= insert x B) = (if x:A then A  {x} <= B else A <= B)" 

633 
by auto 

634 

635 

636 
subsubsection {* Singletons, using insert *} 

637 

638 
lemma singletonI [intro!]: "a : {a}" 

639 
 {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *} 

640 
by (rule insertI1) 

641 

642 
lemma singletonD: "b : {a} ==> b = a" 

643 
by blast 

644 

645 
lemmas singletonE [elim!] = singletonD [elim_format] 

646 

647 
lemma singleton_iff: "(b : {a}) = (b = a)" 

648 
by blast 

649 

650 
lemma singleton_inject [dest!]: "{a} = {b} ==> a = b" 

651 
by blast 

652 

653 
lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A <= {b})" 

654 
by blast 

655 

656 
lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A <= {b})" 

657 
by blast 

658 

659 
lemma subset_singletonD: "A <= {x} ==> A={}  A = {x}" 

660 
by fast 

661 

662 
lemma singleton_conv [simp]: "{x. x = a} = {a}" 

663 
by blast 

664 

665 
lemma singleton_conv2 [simp]: "{x. a = x} = {a}" 

666 
by blast 

923  667 

11979  668 
lemma diff_single_insert: "A  {x} <= B ==> x : A ==> A <= insert x B" 
669 
by blast 

670 

671 

672 
subsubsection {* Unions of families *} 

673 

674 
text {* 

675 
@{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}. 

676 
*} 

677 

678 
lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)" 

679 
by (unfold UNION_def) blast 

680 

681 
lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)" 

682 
 {* The order of the premises presupposes that @{term A} is rigid; 

683 
@{term b} may be flexible. *} 

684 
by auto 

685 

686 
lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R" 

687 
by (unfold UNION_def) blast 

923  688 

11979  689 
lemma UN_cong [cong]: 
690 
"A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)" 

691 
by (simp add: UNION_def) 

692 

693 

694 
subsubsection {* Intersections of families *} 

695 

696 
text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *} 

697 

698 
lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)" 

699 
by (unfold INTER_def) blast 

923  700 

11979  701 
lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)" 
702 
by (unfold INTER_def) blast 

703 

704 
lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a" 

705 
by auto 

706 

707 
lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R" 

708 
 {* "Classical" elimination  by the Excluded Middle on @{prop "a:A"}. *} 

709 
by (unfold INTER_def) blast 

710 

711 
lemma INT_cong [cong]: 

712 
"A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)" 

713 
by (simp add: INTER_def) 

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

714 

923  715 

11979  716 
subsubsection {* Union *} 
717 

718 
lemma Union_iff [simp]: "(A : Union C) = (EX X:C. A:X)" 

719 
by (unfold Union_def) blast 

720 

721 
lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C" 

722 
 {* The order of the premises presupposes that @{term C} is rigid; 

723 
@{term A} may be flexible. *} 

724 
by auto 

725 

726 
lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R" 

727 
by (unfold Union_def) blast 

728 

729 

730 
subsubsection {* Inter *} 

731 

732 
lemma Inter_iff [simp]: "(A : Inter C) = (ALL X:C. A:X)" 

733 
by (unfold Inter_def) blast 

734 

735 
lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C" 

736 
by (simp add: Inter_def) 

737 

738 
text {* 

739 
\medskip A ``destruct'' rule  every @{term X} in @{term C} 

740 
contains @{term A} as an element, but @{prop "A:X"} can hold when 

741 
@{prop "X:C"} does not! This rule is analogous to @{text spec}. 

742 
*} 

743 

744 
lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X" 

745 
by auto 

746 

747 
lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R" 

748 
 {* ``Classical'' elimination rule  does not require proving 

749 
@{prop "X:C"}. *} 

750 
by (unfold Inter_def) blast 

751 

752 
text {* 

753 
\medskip Image of a set under a function. Frequently @{term b} does 

754 
not have the syntactic form of @{term "f x"}. 

755 
*} 

756 

757 
lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A" 

758 
by (unfold image_def) blast 

759 

760 
lemma imageI: "x : A ==> f x : f ` A" 

761 
by (rule image_eqI) (rule refl) 

762 

763 
lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A" 

764 
 {* This version's more effective when we already have the 

765 
required @{term x}. *} 

766 
by (unfold image_def) blast 

767 

768 
lemma imageE [elim!]: 

769 
"b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P" 

770 
 {* The etaexpansion gives variablename preservation. *} 

771 
by (unfold image_def) blast 

772 

773 
lemma image_Un: "f`(A Un B) = f`A Un f`B" 

774 
by blast 

775 

776 
lemma image_iff: "(z : f`A) = (EX x:A. z = f x)" 

777 
by blast 

778 

779 
lemma image_subset_iff: "(f`A <= B) = (ALL x:A. f x: B)" 

780 
 {* This rewrite rule would confuse users if made default. *} 

781 
by blast 

782 

783 
lemma subset_image_iff: "(B <= f ` A) = (EX AA. AA <= A & B = f ` AA)" 

784 
apply safe 

785 
prefer 2 apply fast 

786 
apply (rule_tac x = "{a. a : A & f a : B}" in exI) 

787 
apply fast 

788 
done 

789 

790 
lemma image_subsetI: "(!!x. x:A ==> f x : B) ==> f`A <= B" 

791 
 {* Replaces the three steps @{text subsetI}, @{text imageE}, 

792 
@{text hypsubst}, but breaks too many existing proofs. *} 

793 
by blast 

794 

795 
text {* 

796 
\medskip Range of a function  just a translation for image! 

797 
*} 

798 

799 
lemma range_eqI: "b = f x ==> b : range f" 

800 
by simp 

801 

802 
lemma rangeI: "f x : range f" 

803 
by simp 

804 

805 
lemma rangeE [elim?]: "b : range (%x. f x) ==> (!!x. b = f x ==> P) ==> P" 

806 
by blast 

807 

808 

809 
subsubsection {* Set reasoning tools *} 

810 

811 
text {* 

812 
Rewrite rules for boolean casesplitting: faster than @{text 

813 
"split_if [split]"}. 

814 
*} 

815 

816 
lemma split_if_eq1: "((if Q then x else y) = b) = ((Q > x = b) & (~ Q > y = b))" 

817 
by (rule split_if) 

818 

819 
lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q > a = x) & (~ Q > a = y))" 

820 
by (rule split_if) 

821 

822 
text {* 

823 
Split ifs on either side of the membership relation. Not for @{text 

824 
"[simp]"}  can cause goals to blow up! 

825 
*} 

826 

827 
lemma split_if_mem1: "((if Q then x else y) : b) = ((Q > x : b) & (~ Q > y : b))" 

828 
by (rule split_if) 

829 

830 
lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q > a : x) & (~ Q > a : y))" 

831 
by (rule split_if) 

832 

833 
lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 

834 

835 
lemmas mem_simps = 

836 
insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff 

837 
mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff 

838 
 {* Each of these has ALREADY been added @{text "[simp]"} above. *} 

839 

840 
(*Would like to add these, but the existing code only searches for the 

841 
outerlevel constant, which in this case is just "op :"; we instead need 

842 
to use termnets to associate patterns with rules. Also, if a rule fails to 

843 
apply, then the formula should be kept. 

844 
[("uminus", Compl_iff RS iffD1), ("op ", [Diff_iff RS iffD1]), 

845 
("op Int", [IntD1,IntD2]), 

846 
("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])] 

847 
*) 

848 

849 
ML_setup {* 

850 
val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs; 

851 
simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs); 

852 
*} 

853 

854 
declare subset_UNIV [simp] subset_refl [simp] 

855 

856 

857 
subsubsection {* The ``proper subset'' relation *} 

858 

859 
lemma psubsetI [intro!]: "(A::'a set) <= B ==> A ~= B ==> A < B" 

860 
by (unfold psubset_def) blast 

861 

862 
lemma psubset_insert_iff: 

863 
"(A < insert x B) = (if x:B then A < B else if x:A then A  {x} < B else A <= B)" 

864 
apply (simp add: psubset_def subset_insert_iff) 

865 
apply blast 

866 
done 

867 

868 
lemma psubset_eq: "((A::'a set) < B) = (A <= B & A ~= B)" 

869 
by (simp only: psubset_def) 

870 

871 
lemma psubset_imp_subset: "(A::'a set) < B ==> A <= B" 

872 
by (simp add: psubset_eq) 

873 

874 
lemma psubset_subset_trans: "(A::'a set) < B ==> B <= C ==> A < C" 

875 
by (auto simp add: psubset_eq) 

876 

877 
lemma subset_psubset_trans: "(A::'a set) <= B ==> B < C ==> A < C" 

878 
by (auto simp add: psubset_eq) 

879 

880 
lemma psubset_imp_ex_mem: "A < B ==> EX b. b : (B  A)" 

881 
by (unfold psubset_def) blast 

882 

883 
lemma atomize_ball: 

884 
"(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)" 

885 
by (simp only: Ball_def atomize_all atomize_imp) 

886 

887 
declare atomize_ball [symmetric, rulify] 

888 

889 

890 
subsection {* Further settheory lemmas *} 

891 

892 
use "subset.ML" 

893 
use "equalities.ML" 

894 
use "mono.ML" 

895 

896 
end 