author | paulson |
Fri, 05 Feb 1999 17:31:42 +0100 | |
changeset 6236 | 958f4fc3e8b8 |
parent 6171 | cd237a10cbf8 |
child 7377 | 2ad85e036c21 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/ex/set.ML |
969 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory |
969 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
Cantor's Theorem; the Schroeder-Berstein Theorem. |
|
7 |
*) |
|
8 |
||
9 |
||
10 |
writeln"File HOL/ex/set."; |
|
11 |
||
4153 | 12 |
context Lfp.thy; |
2998 | 13 |
|
5432 | 14 |
(*trivial example of term synthesis: apparently hard for some provers!*) |
15 |
Goal "a ~= b ==> a:?X & b ~: ?X"; |
|
16 |
by (Blast_tac 1); |
|
17 |
result(); |
|
18 |
||
5724 | 19 |
(** Examples for the Blast_tac paper **) |
20 |
||
21 |
(*Union-image, called Un_Union_image on equalities.ML*) |
|
6146 | 22 |
Goal "(UN x:C. f(x) Un g(x)) = Union(f``C) Un Union(g``C)"; |
5724 | 23 |
by (Blast_tac 1); |
24 |
result(); |
|
25 |
||
26 |
(*Inter-image, called Int_Inter_image on equalities.ML*) |
|
6146 | 27 |
Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)"; |
5724 | 28 |
by (Blast_tac 1); |
29 |
result(); |
|
30 |
||
31 |
(*Singleton I. Nice demonstration of blast_tac--and its limitations*) |
|
5432 | 32 |
Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; |
4153 | 33 |
(*for some unfathomable reason, UNIV_I increases the search space greatly*) |
34 |
by (blast_tac (claset() delrules [UNIV_I]) 1); |
|
35 |
result(); |
|
36 |
||
5724 | 37 |
(*Singleton II. variant of the benchmark above*) |
5432 | 38 |
Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"; |
4324 | 39 |
by (blast_tac (claset() delrules [UNIV_I]) 1); |
5432 | 40 |
(*just Blast_tac takes 5 seconds instead of 1*) |
4324 | 41 |
result(); |
2998 | 42 |
|
969 | 43 |
(*** A unique fixpoint theorem --- fast/best/meson all fail ***) |
44 |
||
5432 | 45 |
Goal "?!x. f(g(x))=x ==> ?!y. g(f(y))=y"; |
46 |
by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong, |
|
969 | 47 |
rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]); |
48 |
result(); |
|
49 |
||
50 |
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) |
|
51 |
||
52 |
goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)"; |
|
53 |
(*requires best-first search because it is undirectional*) |
|
4089 | 54 |
by (best_tac (claset() addSEs [equalityCE]) 1); |
969 | 55 |
qed "cantor1"; |
56 |
||
57 |
(*This form displays the diagonal term*) |
|
58 |
goal Set.thy "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)"; |
|
4089 | 59 |
by (best_tac (claset() addSEs [equalityCE]) 1); |
969 | 60 |
uresult(); |
61 |
||
62 |
(*This form exploits the set constructs*) |
|
63 |
goal Set.thy "?S ~: range(f :: 'a=>'a set)"; |
|
64 |
by (rtac notI 1); |
|
65 |
by (etac rangeE 1); |
|
66 |
by (etac equalityCE 1); |
|
67 |
by (dtac CollectD 1); |
|
68 |
by (contr_tac 1); |
|
69 |
by (swap_res_tac [CollectI] 1); |
|
70 |
by (assume_tac 1); |
|
71 |
||
72 |
choplev 0; |
|
4089 | 73 |
by (best_tac (claset() addSEs [equalityCE]) 1); |
969 | 74 |
|
6236 | 75 |
|
969 | 76 |
(*** The Schroder-Berstein Theorem ***) |
77 |
||
6236 | 78 |
Goal "[| -(f``X) = g``(-X); f(a)=g(b); a:X |] ==> b:X"; |
79 |
by (blast_tac (claset() addEs [equalityE]) 1); |
|
969 | 80 |
qed "disj_lemma"; |
81 |
||
5490 | 82 |
Goal "-(f``X) = g``(-X) ==> surj(%z. if z:X then f(z) else g(z))"; |
6236 | 83 |
by (asm_simp_tac (simpset() addsimps [surj_def]) 1); |
84 |
by (blast_tac (claset() addEs [equalityE]) 1); |
|
969 | 85 |
qed "surj_if_then_else"; |
86 |
||
6171 | 87 |
Goalw [inj_on_def] |
88 |
"[| inj_on f X; inj_on g (-X); -(f``X) = g``(-X); \ |
|
89 |
\ bij = (%z. if z:X then f(z) else g(z)) |] \ |
|
90 |
\ ==> inj(bij) & surj(bij)"; |
|
91 |
by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1); |
|
92 |
(*PROOF FAILED if inj_onD*) |
|
93 |
by (blast_tac (claset() addDs [disj_lemma, sym RSN (2,disj_lemma)]) 1); |
|
969 | 94 |
qed "bij_if_then_else"; |
95 |
||
5786
9a2c90bdadfe
increased precedence of unary minus from 80 to 100
paulson
parents:
5724
diff
changeset
|
96 |
Goal "? X. X = - (g``(- (f``X)))"; |
969 | 97 |
by (rtac exI 1); |
98 |
by (rtac lfp_Tarski 1); |
|
99 |
by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1)); |
|
100 |
qed "decomposition"; |
|
101 |
||
5432 | 102 |
val [injf,injg] = goal Lfp.thy |
6171 | 103 |
"[| inj (f:: 'a=>'b); inj (g:: 'b=>'a) |] ==> \ |
969 | 104 |
\ ? h:: 'a=>'b. inj(h) & surj(h)"; |
105 |
by (rtac (decomposition RS exE) 1); |
|
106 |
by (rtac exI 1); |
|
107 |
by (rtac bij_if_then_else 1); |
|
6171 | 108 |
by (rtac refl 4); |
6236 | 109 |
by (rtac inj_on_inv 2); |
110 |
by (rtac ([subset_UNIV, injf] MRS subset_inj_on) 1); |
|
111 |
(**tricky variable instantiations!**) |
|
969 | 112 |
by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, |
1465 | 113 |
etac imageE, etac ssubst, rtac rangeI]); |
969 | 114 |
by (EVERY1 [etac ssubst, stac double_complement, |
1465 | 115 |
rtac (injg RS inv_image_comp RS sym)]); |
969 | 116 |
qed "schroeder_bernstein"; |
117 |
||
118 |
writeln"Reached end of file."; |