author | wenzelm |
Mon, 11 Feb 2002 10:56:33 +0100 | |
changeset 12873 | d7f8dfaad46d |
parent 10834 | a7897aebbffc |
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 |
||
9100 | 9 |
(*These two are cited in Benzmueller and Kohlhase's system description of LEO, |
8266 | 10 |
CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*) |
11 |
||
12 |
Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"; |
|
13 |
by (Blast_tac 1); |
|
9100 | 14 |
qed ""; |
8266 | 15 |
|
16 |
Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"; |
|
17 |
by (Blast_tac 1); |
|
9100 | 18 |
qed ""; |
8266 | 19 |
|
5432 | 20 |
(*trivial example of term synthesis: apparently hard for some provers!*) |
21 |
Goal "a ~= b ==> a:?X & b ~: ?X"; |
|
22 |
by (Blast_tac 1); |
|
9100 | 23 |
qed ""; |
5432 | 24 |
|
5724 | 25 |
(** Examples for the Blast_tac paper **) |
26 |
||
27 |
(*Union-image, called Un_Union_image on equalities.ML*) |
|
10834 | 28 |
Goal "(UN x:C. f(x) Un g(x)) = Union(f`C) Un Union(g`C)"; |
5724 | 29 |
by (Blast_tac 1); |
9100 | 30 |
qed ""; |
5724 | 31 |
|
32 |
(*Inter-image, called Int_Inter_image on equalities.ML*) |
|
10834 | 33 |
Goal "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)"; |
5724 | 34 |
by (Blast_tac 1); |
9100 | 35 |
qed ""; |
5724 | 36 |
|
37 |
(*Singleton I. Nice demonstration of blast_tac--and its limitations*) |
|
5432 | 38 |
Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; |
4153 | 39 |
(*for some unfathomable reason, UNIV_I increases the search space greatly*) |
40 |
by (blast_tac (claset() delrules [UNIV_I]) 1); |
|
9100 | 41 |
qed ""; |
4153 | 42 |
|
5724 | 43 |
(*Singleton II. variant of the benchmark above*) |
5432 | 44 |
Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"; |
4324 | 45 |
by (blast_tac (claset() delrules [UNIV_I]) 1); |
5432 | 46 |
(*just Blast_tac takes 5 seconds instead of 1*) |
9100 | 47 |
qed ""; |
2998 | 48 |
|
969 | 49 |
(*** A unique fixpoint theorem --- fast/best/meson all fail ***) |
50 |
||
9166 | 51 |
Goal "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y"; |
5432 | 52 |
by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong, |
969 | 53 |
rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]); |
9100 | 54 |
qed ""; |
55 |
||
969 | 56 |
|
57 |
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) |
|
58 |
||
9166 | 59 |
Goal "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)"; |
969 | 60 |
(*requires best-first search because it is undirectional*) |
10198 | 61 |
by (Best_tac 1); |
969 | 62 |
qed "cantor1"; |
63 |
||
64 |
(*This form displays the diagonal term*) |
|
9166 | 65 |
Goal "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)"; |
10198 | 66 |
by (Best_tac 1); |
969 | 67 |
uresult(); |
68 |
||
69 |
(*This form exploits the set constructs*) |
|
9100 | 70 |
Goal "?S ~: range(f :: 'a=>'a set)"; |
969 | 71 |
by (rtac notI 1); |
72 |
by (etac rangeE 1); |
|
73 |
by (etac equalityCE 1); |
|
74 |
by (dtac CollectD 1); |
|
75 |
by (contr_tac 1); |
|
76 |
by (swap_res_tac [CollectI] 1); |
|
77 |
by (assume_tac 1); |
|
78 |
||
79 |
choplev 0; |
|
10198 | 80 |
by (Best_tac 1); |
9100 | 81 |
qed ""; |
969 | 82 |
|
6236 | 83 |
|
9316 | 84 |
(*** The Schroeder-Berstein Theorem ***) |
969 | 85 |
|
10834 | 86 |
Goal "[| -(f`X) = g`(-X); f(a)=g(b); a:X |] ==> b:X"; |
9190 | 87 |
by (Blast_tac 1); |
969 | 88 |
qed "disj_lemma"; |
89 |
||
10834 | 90 |
Goal "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))"; |
6236 | 91 |
by (asm_simp_tac (simpset() addsimps [surj_def]) 1); |
9190 | 92 |
by (Blast_tac 1); |
969 | 93 |
qed "surj_if_then_else"; |
94 |
||
6171 | 95 |
Goalw [inj_on_def] |
10834 | 96 |
"[| inj_on f X; inj_on g (-X); -(f`X) = g`(-X); \ |
7377
2ad85e036c21
the bij predicate forced renaming of a variable bij
paulson
parents:
6236
diff
changeset
|
97 |
\ h = (%z. if z:X then f(z) else g(z)) |] \ |
2ad85e036c21
the bij predicate forced renaming of a variable bij
paulson
parents:
6236
diff
changeset
|
98 |
\ ==> inj(h) & surj(h)"; |
6171 | 99 |
by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1); |
9166 | 100 |
by (blast_tac (claset() addDs [disj_lemma, sym]) 1); |
969 | 101 |
qed "bij_if_then_else"; |
102 |
||
10834 | 103 |
Goal "EX X. X = - (g`(- (f`X)))"; |
969 | 104 |
by (rtac exI 1); |
10186 | 105 |
by (rtac lfp_unfold 1); |
969 | 106 |
by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1)); |
107 |
qed "decomposition"; |
|
108 |
||
9100 | 109 |
val [injf,injg] = goal (the_context ()) |
9166 | 110 |
"[| inj (f:: 'a=>'b); inj (g:: 'b=>'a) |] \ |
111 |
\ ==> EX h:: 'a=>'b. inj(h) & surj(h)"; |
|
969 | 112 |
by (rtac (decomposition RS exE) 1); |
113 |
by (rtac exI 1); |
|
114 |
by (rtac bij_if_then_else 1); |
|
6171 | 115 |
by (rtac refl 4); |
6236 | 116 |
by (rtac inj_on_inv 2); |
117 |
by (rtac ([subset_UNIV, injf] MRS subset_inj_on) 1); |
|
118 |
(**tricky variable instantiations!**) |
|
969 | 119 |
by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, |
1465 | 120 |
etac imageE, etac ssubst, rtac rangeI]); |
969 | 121 |
by (EVERY1 [etac ssubst, stac double_complement, |
1465 | 122 |
rtac (injg RS inv_image_comp RS sym)]); |
969 | 123 |
qed "schroeder_bernstein"; |