author  wenzelm 
Wed, 03 Nov 2010 21:53:56 +0100  
changeset 40335  3e4bb6e7c3ca 
parent 39128  93a7365fb4ee 
child 41526  54b4686704af 
permissions  rwrr 
17456  1 
header {* Extending FOL by a modified version of HOL set theory *} 
2 

3 
theory Set 

4 
imports FOL 

5 
begin 

0  6 

39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
38499
diff
changeset

7 
declare [[eta_contract]] 
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
38499
diff
changeset

8 

17456  9 
typedecl 'a set 
10 
arities set :: ("term") "term" 

0  11 

12 
consts 

13 
Collect :: "['a => o] => 'a set" (*comprehension*) 

14 
Compl :: "('a set) => 'a set" (*complement*) 

24825  15 
Int :: "['a set, 'a set] => 'a set" (infixl "Int" 70) 
16 
Un :: "['a set, 'a set] => 'a set" (infixl "Un" 65) 

17456  17 
Union :: "(('a set)set) => 'a set" (*...of a set*) 
18 
Inter :: "(('a set)set) => 'a set" (*...of a set*) 

19 
UNION :: "['a set, 'a => 'b set] => 'b set" (*general*) 

20 
INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) 

21 
Ball :: "['a set, 'a => o] => o" (*bounded quants*) 

22 
Bex :: "['a set, 'a => o] => o" (*bounded quants*) 

0  23 
mono :: "['a set => 'b set] => o" (*monotonicity*) 
24825  24 
mem :: "['a, 'a set] => o" (infixl ":" 50) (*membership*) 
25 
subset :: "['a set, 'a set] => o" (infixl "<=" 50) 

0  26 
singleton :: "'a => 'a set" ("{_}") 
27 
empty :: "'a set" ("{}") 

28 

3935  29 
syntax 
35113  30 
"_Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*) 
0  31 

32 
(* Big Intersection / Union *) 

33 

35113  34 
"_INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) 
35 
"_UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(UN _:_./ _)" [0, 0, 0] 10) 

0  36 

37 
(* Bounded Quantifiers *) 

38 

35113  39 
"_Ball" :: "[idt, 'a set, o] => o" ("(ALL _:_./ _)" [0, 0, 0] 10) 
40 
"_Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10) 

0  41 

42 
translations 

35054  43 
"{x. P}" == "CONST Collect(%x. P)" 
44 
"INT x:A. B" == "CONST INTER(A, %x. B)" 

45 
"UN x:A. B" == "CONST UNION(A, %x. B)" 

46 
"ALL x:A. P" == "CONST Ball(A, %x. P)" 

47 
"EX x:A. P" == "CONST Bex(A, %x. P)" 

0  48 

17456  49 
axioms 
50 
mem_Collect_iff: "(a : {x. P(x)}) <> P(a)" 

51 
set_extension: "A=B <> (ALL x. x:A <> x:B)" 

0  52 

17456  53 
defs 
54 
Ball_def: "Ball(A, P) == ALL x. x:A > P(x)" 

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

56 
mono_def: "mono(f) == (ALL A B. A <= B > f(A) <= f(B))" 

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

58 
singleton_def: "{a} == {x. x=a}" 

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

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

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

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

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

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

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

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

67 

20140  68 

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

70 
apply (rule mem_Collect_iff [THEN iffD2]) 

71 
apply assumption 

72 
done 

73 

74 
lemma CollectD: "[ a : {x. P(x)} ] ==> P(a)" 

75 
apply (erule mem_Collect_iff [THEN iffD1]) 

76 
done 

77 

78 
lemmas CollectE = CollectD [elim_format] 

79 

80 
lemma set_ext: "[ !!x. x:A <> x:B ] ==> A = B" 

81 
apply (rule set_extension [THEN iffD2]) 

82 
apply simp 

83 
done 

84 

85 

86 
subsection {* Bounded quantifiers *} 

87 

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

89 
by (simp add: Ball_def) 

90 

91 
lemma bspec: "[ ALL x:A. P(x); x:A ] ==> P(x)" 

92 
by (simp add: Ball_def) 

93 

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

95 
unfolding Ball_def by blast 

96 

97 
lemma bexI: "[ P(x); x:A ] ==> EX x:A. P(x)" 

98 
unfolding Bex_def by blast 

99 

100 
lemma bexCI: "[ EX x:A. ~P(x) ==> P(a); a:A ] ==> EX x:A. P(x)" 

101 
unfolding Bex_def by blast 

102 

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

104 
unfolding Bex_def by blast 

105 

106 
(*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) 

107 
lemma ball_rew: "(ALL x:A. True) <> True" 

108 
by (blast intro: ballI) 

109 

110 

111 
subsection {* Congruence rules *} 

112 

113 
lemma ball_cong: 

114 
"[ A=A'; !!x. x:A' ==> P(x) <> P'(x) ] ==> 

115 
(ALL x:A. P(x)) <> (ALL x:A'. P'(x))" 

116 
by (blast intro: ballI elim: ballE) 

117 

118 
lemma bex_cong: 

119 
"[ A=A'; !!x. x:A' ==> P(x) <> P'(x) ] ==> 

120 
(EX x:A. P(x)) <> (EX x:A'. P'(x))" 

121 
by (blast intro: bexI elim: bexE) 

122 

123 

124 
subsection {* Rules for subsets *} 

125 

126 
lemma subsetI: "(!!x. x:A ==> x:B) ==> A <= B" 

127 
unfolding subset_def by (blast intro: ballI) 

128 

129 
(*Rule in Modus Ponens style*) 

130 
lemma subsetD: "[ A <= B; c:A ] ==> c:B" 

131 
unfolding subset_def by (blast elim: ballE) 

132 

133 
(*Classical elimination rule*) 

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

135 
by (blast dest: subsetD) 

136 

137 
lemma subset_refl: "A <= A" 

138 
by (blast intro: subsetI) 

139 

140 
lemma subset_trans: "[ A<=B; B<=C ] ==> A<=C" 

141 
by (blast intro: subsetI dest: subsetD) 

142 

143 

144 
subsection {* Rules for equality *} 

145 

146 
(*Antisymmetry of the subset relation*) 

147 
lemma subset_antisym: "[ A <= B; B <= A ] ==> A = B" 

148 
by (blast intro: set_ext dest: subsetD) 

149 

150 
lemmas equalityI = subset_antisym 

151 

152 
(* Equality rules from ZF set theory  are they appropriate here? *) 

153 
lemma equalityD1: "A = B ==> A<=B" 

154 
and equalityD2: "A = B ==> B<=A" 

155 
by (simp_all add: subset_refl) 

156 

157 
lemma equalityE: "[ A = B; [ A<=B; B<=A ] ==> P ] ==> P" 

158 
by (simp add: subset_refl) 

159 

160 
lemma equalityCE: 

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

162 
by (blast elim: equalityE subsetCE) 

163 

164 
lemma trivial_set: "{x. x:A} = A" 

165 
by (blast intro: equalityI subsetI CollectI dest: CollectD) 

166 

167 

168 
subsection {* Rules for binary union *} 

169 

170 
lemma UnI1: "c:A ==> c : A Un B" 

171 
and UnI2: "c:B ==> c : A Un B" 

172 
unfolding Un_def by (blast intro: CollectI)+ 

173 

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

175 
lemma UnCI: "(~c:B ==> c:A) ==> c : A Un B" 

176 
by (blast intro: UnI1 UnI2) 

177 

178 
lemma UnE: "[ c : A Un B; c:A ==> P; c:B ==> P ] ==> P" 

179 
unfolding Un_def by (blast dest: CollectD) 

180 

181 

182 
subsection {* Rules for small intersection *} 

183 

184 
lemma IntI: "[ c:A; c:B ] ==> c : A Int B" 

185 
unfolding Int_def by (blast intro: CollectI) 

186 

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

188 
and IntD2: "c : A Int B ==> c:B" 

189 
unfolding Int_def by (blast dest: CollectD)+ 

190 

191 
lemma IntE: "[ c : A Int B; [ c:A; c:B ] ==> P ] ==> P" 

192 
by (blast dest: IntD1 IntD2) 

193 

194 

195 
subsection {* Rules for set complement *} 

196 

197 
lemma ComplI: "[ c:A ==> False ] ==> c : Compl(A)" 

198 
unfolding Compl_def by (blast intro: CollectI) 

199 

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

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

202 
turnstile...*) 

203 
lemma ComplD: "[ c : Compl(A) ] ==> ~c:A" 

204 
unfolding Compl_def by (blast dest: CollectD) 

205 

206 
lemmas ComplE = ComplD [elim_format] 

207 

208 

209 
subsection {* Empty sets *} 

210 

211 
lemma empty_eq: "{x. False} = {}" 

212 
by (simp add: empty_def) 

213 

214 
lemma emptyD: "a : {} ==> P" 

215 
unfolding empty_def by (blast dest: CollectD) 

216 

217 
lemmas emptyE = emptyD [elim_format] 

218 

219 
lemma not_emptyD: 

220 
assumes "~ A={}" 

221 
shows "EX x. x:A" 

222 
proof  

223 
have "\<not> (EX x. x:A) \<Longrightarrow> A = {}" 

224 
by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+ 

225 
with prems show ?thesis by blast 

226 
qed 

227 

228 

229 
subsection {* Singleton sets *} 

230 

231 
lemma singletonI: "a : {a}" 

232 
unfolding singleton_def by (blast intro: CollectI) 

233 

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

235 
unfolding singleton_def by (blast dest: CollectD) 

236 

237 
lemmas singletonE = singletonD [elim_format] 

238 

239 

240 
subsection {* Unions of families *} 

241 

242 
(*The order of the premises presupposes that A is rigid; b may be flexible*) 

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

244 
unfolding UNION_def by (blast intro: bexI CollectI) 

245 

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

247 
unfolding UNION_def by (blast dest: CollectD elim: bexE) 

248 

249 
lemma UN_cong: 

250 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> 

251 
(UN x:A. C(x)) = (UN x:B. D(x))" 

252 
by (simp add: UNION_def cong: bex_cong) 

253 

254 

255 
subsection {* Intersections of families *} 

256 

257 
lemma INT_I: "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))" 

258 
unfolding INTER_def by (blast intro: CollectI ballI) 

259 

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

261 
unfolding INTER_def by (blast dest: CollectD bspec) 

262 

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

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

265 
unfolding INTER_def by (blast dest: CollectD bspec) 

266 

267 
lemma INT_cong: 

268 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> 

269 
(INT x:A. C(x)) = (INT x:B. D(x))" 

270 
by (simp add: INTER_def cong: ball_cong) 

271 

272 

273 
subsection {* Rules for Unions *} 

274 

275 
(*The order of the premises presupposes that C is rigid; A may be flexible*) 

276 
lemma UnionI: "[ X:C; A:X ] ==> A : Union(C)" 

277 
unfolding Union_def by (blast intro: UN_I) 

278 

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

280 
unfolding Union_def by (blast elim: UN_E) 

281 

282 

283 
subsection {* Rules for Inter *} 

284 

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

286 
unfolding Inter_def by (blast intro: INT_I) 

287 

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

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

290 
lemma InterD: "[ A : Inter(C); X:C ] ==> A:X" 

291 
unfolding Inter_def by (blast dest: INT_D) 

292 

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

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

295 
unfolding Inter_def by (blast elim: INT_E) 

296 

297 

298 
section {* Derived rules involving subsets; Union and Intersection as lattice operations *} 

299 

300 
subsection {* Big Union  least upper bound of a set *} 

301 

302 
lemma Union_upper: "B:A ==> B <= Union(A)" 

303 
by (blast intro: subsetI UnionI) 

304 

305 
lemma Union_least: "[ !!X. X:A ==> X<=C ] ==> Union(A) <= C" 

306 
by (blast intro: subsetI dest: subsetD elim: UnionE) 

307 

308 

309 
subsection {* Big Intersection  greatest lower bound of a set *} 

310 

311 
lemma Inter_lower: "B:A ==> Inter(A) <= B" 

312 
by (blast intro: subsetI dest: InterD) 

313 

314 
lemma Inter_greatest: "[ !!X. X:A ==> C<=X ] ==> C <= Inter(A)" 

315 
by (blast intro: subsetI InterI dest: subsetD) 

316 

317 

318 
subsection {* Finite Union  the least upper bound of 2 sets *} 

319 

320 
lemma Un_upper1: "A <= A Un B" 

321 
by (blast intro: subsetI UnI1) 

322 

323 
lemma Un_upper2: "B <= A Un B" 

324 
by (blast intro: subsetI UnI2) 

325 

326 
lemma Un_least: "[ A<=C; B<=C ] ==> A Un B <= C" 

327 
by (blast intro: subsetI elim: UnE dest: subsetD) 

328 

329 

330 
subsection {* Finite Intersection  the greatest lower bound of 2 sets *} 

331 

332 
lemma Int_lower1: "A Int B <= A" 

333 
by (blast intro: subsetI elim: IntE) 

334 

335 
lemma Int_lower2: "A Int B <= B" 

336 
by (blast intro: subsetI elim: IntE) 

337 

338 
lemma Int_greatest: "[ C<=A; C<=B ] ==> C <= A Int B" 

339 
by (blast intro: subsetI IntI dest: subsetD) 

340 

341 

342 
subsection {* Monotonicity *} 

343 

344 
lemma monoI: "[ !!A B. A <= B ==> f(A) <= f(B) ] ==> mono(f)" 

345 
unfolding mono_def by blast 

346 

347 
lemma monoD: "[ mono(f); A <= B ] ==> f(A) <= f(B)" 

348 
unfolding mono_def by blast 

349 

350 
lemma mono_Un: "mono(f) ==> f(A) Un f(B) <= f(A Un B)" 

351 
by (blast intro: Un_least dest: monoD intro: Un_upper1 Un_upper2) 

352 

353 
lemma mono_Int: "mono(f) ==> f(A Int B) <= f(A) Int f(B)" 

354 
by (blast intro: Int_greatest dest: monoD intro: Int_lower1 Int_lower2) 

355 

356 

357 
subsection {* Automated reasoning setup *} 

358 

359 
lemmas [intro!] = ballI subsetI InterI INT_I CollectI ComplI IntI UnCI singletonI 

360 
and [intro] = bexI UnionI UN_I 

361 
and [elim!] = bexE UnionE UN_E CollectE ComplE IntE UnE emptyE singletonE 

362 
and [elim] = ballE InterD InterE INT_D INT_E subsetD subsetCE 

363 

364 
lemma mem_rews: 

365 
"(a : A Un B) <> (a:A  a:B)" 

366 
"(a : A Int B) <> (a:A & a:B)" 

367 
"(a : Compl(B)) <> (~a:B)" 

368 
"(a : {b}) <> (a=b)" 

369 
"(a : {}) <> False" 

370 
"(a : {x. P(x)}) <> P(a)" 

371 
by blast+ 

372 

373 
lemmas [simp] = trivial_set empty_eq mem_rews 

374 
and [cong] = ball_cong bex_cong INT_cong UN_cong 

375 

376 

377 
section {* Equalities involving union, intersection, inclusion, etc. *} 

378 

379 
subsection {* Binary Intersection *} 

380 

381 
lemma Int_absorb: "A Int A = A" 

382 
by (blast intro: equalityI) 

383 

384 
lemma Int_commute: "A Int B = B Int A" 

385 
by (blast intro: equalityI) 

386 

387 
lemma Int_assoc: "(A Int B) Int C = A Int (B Int C)" 

388 
by (blast intro: equalityI) 

389 

390 
lemma Int_Un_distrib: "(A Un B) Int C = (A Int C) Un (B Int C)" 

391 
by (blast intro: equalityI) 

392 

393 
lemma subset_Int_eq: "(A<=B) <> (A Int B = A)" 

394 
by (blast intro: equalityI elim: equalityE) 

395 

396 

397 
subsection {* Binary Union *} 

398 

399 
lemma Un_absorb: "A Un A = A" 

400 
by (blast intro: equalityI) 

401 

402 
lemma Un_commute: "A Un B = B Un A" 

403 
by (blast intro: equalityI) 

404 

405 
lemma Un_assoc: "(A Un B) Un C = A Un (B Un C)" 

406 
by (blast intro: equalityI) 

407 

408 
lemma Un_Int_distrib: "(A Int B) Un C = (A Un C) Int (B Un C)" 

409 
by (blast intro: equalityI) 

410 

411 
lemma Un_Int_crazy: 

412 
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)" 

413 
by (blast intro: equalityI) 

414 

415 
lemma subset_Un_eq: "(A<=B) <> (A Un B = B)" 

416 
by (blast intro: equalityI elim: equalityE) 

417 

418 

419 
subsection {* Simple properties of @{text "Compl"}  complement of a set *} 

420 

421 
lemma Compl_disjoint: "A Int Compl(A) = {x. False}" 

422 
by (blast intro: equalityI) 

423 

424 
lemma Compl_partition: "A Un Compl(A) = {x. True}" 

425 
by (blast intro: equalityI) 

426 

427 
lemma double_complement: "Compl(Compl(A)) = A" 

428 
by (blast intro: equalityI) 

429 

430 
lemma Compl_Un: "Compl(A Un B) = Compl(A) Int Compl(B)" 

431 
by (blast intro: equalityI) 

432 

433 
lemma Compl_Int: "Compl(A Int B) = Compl(A) Un Compl(B)" 

434 
by (blast intro: equalityI) 

435 

436 
lemma Compl_UN: "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))" 

437 
by (blast intro: equalityI) 

438 

439 
lemma Compl_INT: "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))" 

440 
by (blast intro: equalityI) 

441 

442 
(*Halmos, Naive Set Theory, page 16.*) 

443 
lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) <> (C<=A)" 

444 
by (blast intro: equalityI elim: equalityE) 

445 

446 

447 
subsection {* Big Union and Intersection *} 

448 

449 
lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)" 

450 
by (blast intro: equalityI) 

451 

452 
lemma Union_disjoint: 

453 
"(Union(C) Int A = {x. False}) <> (ALL B:C. B Int A = {x. False})" 

454 
by (blast intro: equalityI elim: equalityE) 

455 

456 
lemma Inter_Un_distrib: "Inter(A Un B) = Inter(A) Int Inter(B)" 

457 
by (blast intro: equalityI) 

458 

459 

460 
subsection {* Unions and Intersections of Families *} 

461 

462 
lemma UN_eq: "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})" 

463 
by (blast intro: equalityI) 

464 

465 
(*Look: it has an EXISTENTIAL quantifier*) 

466 
lemma INT_eq: "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})" 

467 
by (blast intro: equalityI) 

468 

469 
lemma Int_Union_image: "A Int Union(B) = (UN C:B. A Int C)" 

470 
by (blast intro: equalityI) 

471 

472 
lemma Un_Inter_image: "A Un Inter(B) = (INT C:B. A Un C)" 

473 
by (blast intro: equalityI) 

474 

475 

476 
section {* Monotonicity of various operations *} 

477 

478 
lemma Union_mono: "A<=B ==> Union(A) <= Union(B)" 

479 
by blast 

480 

481 
lemma Inter_anti_mono: "[ B<=A ] ==> Inter(A) <= Inter(B)" 

482 
by blast 

483 

484 
lemma UN_mono: 

485 
"[ A<=B; !!x. x:A ==> f(x)<=g(x) ] ==> 

486 
(UN x:A. f(x)) <= (UN x:B. g(x))" 

487 
by blast 

488 

489 
lemma INT_anti_mono: 

490 
"[ B<=A; !!x. x:A ==> f(x)<=g(x) ] ==> 

491 
(INT x:A. f(x)) <= (INT x:A. g(x))" 

492 
by blast 

493 

494 
lemma Un_mono: "[ A<=C; B<=D ] ==> A Un B <= C Un D" 

495 
by blast 

496 

497 
lemma Int_mono: "[ A<=C; B<=D ] ==> A Int B <= C Int D" 

498 
by blast 

499 

500 
lemma Compl_anti_mono: "[ A<=B ] ==> Compl(B) <= Compl(A)" 

501 
by blast 

0  502 

503 
end 