author | paulson |
Wed, 20 Jan 1999 10:33:34 +0100 | |
changeset 6146 | 00f3324048a7 |
parent 5786 | 9a2c90bdadfe |
child 6171 | cd237a10cbf8 |
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 |
|
75 |
(*** The Schroder-Berstein Theorem ***) |
|
76 |
||
5432 | 77 |
Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X"; |
969 | 78 |
by (rtac equalityI 1); |
4089 | 79 |
by (fast_tac (claset() addEs [inv_f_f RS ssubst]) 1); |
80 |
by (fast_tac (claset() addEs [inv_f_f RS ssubst]) 1); |
|
969 | 81 |
qed "inv_image_comp"; |
82 |
||
5432 | 83 |
Goal "f(a) ~: (f``X) ==> a~:X"; |
2935 | 84 |
by (Blast_tac 1); |
969 | 85 |
qed "contra_imageI"; |
86 |
||
5490 | 87 |
Goal "(a ~: -(X)) = (a:X)"; |
2935 | 88 |
by (Blast_tac 1); |
969 | 89 |
qed "not_Compl"; |
90 |
||
91 |
(*Lots of backtracking in this proof...*) |
|
92 |
val [compl,fg,Xa] = goal Lfp.thy |
|
5490 | 93 |
"[| -(f``X) = g``(-X); f(a)=g(b); a:X |] ==> b:X"; |
969 | 94 |
by (EVERY1 [rtac (not_Compl RS subst), rtac contra_imageI, |
1465 | 95 |
rtac (compl RS subst), rtac (fg RS subst), stac not_Compl, |
96 |
rtac imageI, rtac Xa]); |
|
969 | 97 |
qed "disj_lemma"; |
98 |
||
5432 | 99 |
Goalw [image_def] |
5490 | 100 |
"range(%z. if z:X then f(z) else g(z)) = f``X Un g``(-X)"; |
4686 | 101 |
by (Simp_tac 1); |
2935 | 102 |
by (Blast_tac 1); |
969 | 103 |
qed "range_if_then_else"; |
104 |
||
5432 | 105 |
Goalw [surj_def] "surj(f) = (!a. a : range(f))"; |
4089 | 106 |
by (fast_tac (claset() addEs [ssubst]) 1); |
969 | 107 |
qed "surj_iff_full_range"; |
108 |
||
5490 | 109 |
Goal "-(f``X) = g``(-X) ==> surj(%z. if z:X then f(z) else g(z))"; |
1487 | 110 |
by (EVERY1[stac surj_iff_full_range, stac range_if_then_else, |
5432 | 111 |
etac subst]); |
5490 | 112 |
by (Blast_tac 1); |
969 | 113 |
qed "surj_if_then_else"; |
114 |
||
5432 | 115 |
val [injf,injg,compl,bij] = |
116 |
goal Lfp.thy |
|
5490 | 117 |
"[| inj_on f X; inj_on g (-X); -(f``X) = g``(-X); \ |
969 | 118 |
\ bij = (%z. if z:X then f(z) else g(z)) |] ==> \ |
119 |
\ inj(bij) & surj(bij)"; |
|
120 |
val f_eq_gE = make_elim (compl RS disj_lemma); |
|
2031 | 121 |
by (stac bij 1); |
969 | 122 |
by (rtac conjI 1); |
123 |
by (rtac (compl RS surj_if_then_else) 2); |
|
124 |
by (rewtac inj_def); |
|
125 |
by (cut_facts_tac [injf,injg] 1); |
|
4831 | 126 |
by (EVERY1 [rtac allI, rtac allI, stac split_if, rtac conjI, stac split_if]); |
127 |
by (fast_tac (claset() addEs [inj_onD, sym RS f_eq_gE]) 1); |
|
128 |
by (stac split_if 1); |
|
129 |
by (fast_tac (claset() addEs [inj_onD, f_eq_gE]) 1); |
|
969 | 130 |
qed "bij_if_then_else"; |
131 |
||
5786
9a2c90bdadfe
increased precedence of unary minus from 80 to 100
paulson
parents:
5724
diff
changeset
|
132 |
Goal "? X. X = - (g``(- (f``X)))"; |
969 | 133 |
by (rtac exI 1); |
134 |
by (rtac lfp_Tarski 1); |
|
135 |
by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1)); |
|
136 |
qed "decomposition"; |
|
137 |
||
5432 | 138 |
val [injf,injg] = goal Lfp.thy |
969 | 139 |
"[| inj(f:: 'a=>'b); inj(g:: 'b=>'a) |] ==> \ |
140 |
\ ? h:: 'a=>'b. inj(h) & surj(h)"; |
|
141 |
by (rtac (decomposition RS exE) 1); |
|
142 |
by (rtac exI 1); |
|
143 |
by (rtac bij_if_then_else 1); |
|
144 |
by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1, |
|
4831 | 145 |
rtac (injg RS inj_on_inv) 1]); |
969 | 146 |
by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, |
1465 | 147 |
etac imageE, etac ssubst, rtac rangeI]); |
969 | 148 |
by (EVERY1 [etac ssubst, stac double_complement, |
1465 | 149 |
rtac (injg RS inv_image_comp RS sym)]); |
969 | 150 |
qed "schroeder_bernstein"; |
151 |
||
152 |
writeln"Reached end of file."; |