969

1 
(* Title: HOL/ex/set.ML


2 
ID: $Id$


3 
Author: Tobias Nipkow, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
Cantor's Theorem; the SchroederBerstein Theorem.


7 
*)


8 


9 


10 
writeln"File HOL/ex/set.";


11 


12 
(*** A unique fixpoint theorem  fast/best/meson all fail ***)


13 


14 
val [prem] = goal HOL.thy "?!x.f(g(x))=x ==> ?!y.g(f(y))=y";


15 
by(EVERY1[rtac (prem RS ex1E), rtac ex1I, etac arg_cong,


16 
rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]);


17 
result();


18 


19 
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)


20 


21 
goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";


22 
(*requires bestfirst search because it is undirectional*)


23 
by (best_tac (set_cs addSEs [equalityCE]) 1);


24 
qed "cantor1";


25 


26 
(*This form displays the diagonal term*)


27 
goal Set.thy "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)";


28 
by (best_tac (set_cs addSEs [equalityCE]) 1);


29 
uresult();


30 


31 
(*This form exploits the set constructs*)


32 
goal Set.thy "?S ~: range(f :: 'a=>'a set)";


33 
by (rtac notI 1);


34 
by (etac rangeE 1);


35 
by (etac equalityCE 1);


36 
by (dtac CollectD 1);


37 
by (contr_tac 1);


38 
by (swap_res_tac [CollectI] 1);


39 
by (assume_tac 1);


40 


41 
choplev 0;


42 
by (best_tac (set_cs addSEs [equalityCE]) 1);


43 


44 
(*** The SchroderBerstein Theorem ***)


45 


46 
val prems = goalw Lfp.thy [image_def] "inj(f) ==> Inv(f)``(f``X) = X";


47 
by (cut_facts_tac prems 1);


48 
by (rtac equalityI 1);


49 
by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);


50 
by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);


51 
qed "inv_image_comp";


52 


53 
val prems = goal Set.thy "f(a) ~: (f``X) ==> a~:X";


54 
by (cfast_tac prems 1);


55 
qed "contra_imageI";


56 


57 
goal Lfp.thy "(a ~: Compl(X)) = (a:X)";


58 
by (fast_tac set_cs 1);


59 
qed "not_Compl";


60 


61 
(*Lots of backtracking in this proof...*)


62 
val [compl,fg,Xa] = goal Lfp.thy


63 
"[ Compl(f``X) = g``Compl(X); f(a)=g(b); a:X ] ==> b:X";


64 
by (EVERY1 [rtac (not_Compl RS subst), rtac contra_imageI,


65 
rtac (compl RS subst), rtac (fg RS subst), stac not_Compl,


66 
rtac imageI, rtac Xa]);


67 
qed "disj_lemma";


68 


69 
goal Lfp.thy "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";


70 
by (rtac equalityI 1);


71 
by (rewtac range_def);


72 
by (fast_tac (set_cs addIs [if_P RS sym, if_not_P RS sym]) 2);


73 
by (rtac subsetI 1);


74 
by (etac CollectE 1);


75 
by (etac exE 1);


76 
by (etac ssubst 1);


77 
by (rtac (excluded_middle RS disjE) 1);


78 
by (EVERY' [rtac (if_P RS ssubst), atac, fast_tac set_cs] 2);


79 
by (EVERY' [rtac (if_not_P RS ssubst), atac, fast_tac set_cs] 1);


80 
qed "range_if_then_else";


81 


82 
goal Lfp.thy "a : X Un Compl(X)";


83 
by (fast_tac set_cs 1);


84 
qed "X_Un_Compl";


85 


86 
goalw Lfp.thy [surj_def] "surj(f) = (!a. a : range(f))";


87 
by (fast_tac (set_cs addEs [ssubst]) 1);


88 
qed "surj_iff_full_range";


89 


90 
val [compl] = goal Lfp.thy


91 
"Compl(f``X) = g``Compl(X) ==> surj(%z. if z:X then f(z) else g(z))";


92 
by (sstac [surj_iff_full_range, range_if_then_else, compl RS sym] 1);


93 
by (rtac (X_Un_Compl RS allI) 1);


94 
qed "surj_if_then_else";


95 


96 
val [injf,injg,compl,bij] = goal Lfp.thy


97 
"[ inj_onto f X; inj_onto g (Compl X); Compl(f``X) = g``Compl(X); \


98 
\ bij = (%z. if z:X then f(z) else g(z)) ] ==> \


99 
\ inj(bij) & surj(bij)";


100 
val f_eq_gE = make_elim (compl RS disj_lemma);


101 
by (rtac (bij RS ssubst) 1);


102 
by (rtac conjI 1);


103 
by (rtac (compl RS surj_if_then_else) 2);


104 
by (rewtac inj_def);


105 
by (cut_facts_tac [injf,injg] 1);


106 
by (EVERY1 [rtac allI, rtac allI, stac expand_if, rtac conjI, stac expand_if]);


107 
by (fast_tac (set_cs addEs [inj_ontoD, sym RS f_eq_gE]) 1);


108 
by (stac expand_if 1);


109 
by (fast_tac (set_cs addEs [inj_ontoD, f_eq_gE]) 1);


110 
qed "bij_if_then_else";


111 


112 
goal Lfp.thy "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))";


113 
by (rtac exI 1);


114 
by (rtac lfp_Tarski 1);


115 
by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));


116 
qed "decomposition";


117 


118 
val [injf,injg] = goal Lfp.thy


119 
"[ inj(f:: 'a=>'b); inj(g:: 'b=>'a) ] ==> \


120 
\ ? h:: 'a=>'b. inj(h) & surj(h)";


121 
by (rtac (decomposition RS exE) 1);


122 
by (rtac exI 1);


123 
by (rtac bij_if_then_else 1);


124 
by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1,


125 
rtac (injg RS inj_onto_Inv) 1]);


126 
by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI,


127 
etac imageE, etac ssubst, rtac rangeI]);


128 
by (EVERY1 [etac ssubst, stac double_complement,


129 
rtac (injg RS inv_image_comp RS sym)]);


130 
qed "schroeder_bernstein";


131 


132 
writeln"Reached end of file.";
