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 SchroederBerstein 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 

4153

19 
(*Nice demonstration of blast_tacand its limitations*)

5432

20 
Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";

4153

21 
(*for some unfathomable reason, UNIV_I increases the search space greatly*)


22 
by (blast_tac (claset() delrules [UNIV_I]) 1);


23 
result();


24 

4324

25 
(*variant of the benchmark above*)

5432

26 
Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";

4324

27 
by (blast_tac (claset() delrules [UNIV_I]) 1);

5432

28 
(*just Blast_tac takes 5 seconds instead of 1*)

4324

29 
result();

2998

30 

969

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


32 

5432

33 
Goal "?!x. f(g(x))=x ==> ?!y. g(f(y))=y";


34 
by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong,

969

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


36 
result();


37 


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


39 


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


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

4089

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

969

43 
qed "cantor1";


44 


45 
(*This form displays the diagonal term*)


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

4089

47 
by (best_tac (claset() addSEs [equalityCE]) 1);

969

48 
uresult();


49 


50 
(*This form exploits the set constructs*)


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


52 
by (rtac notI 1);


53 
by (etac rangeE 1);


54 
by (etac equalityCE 1);


55 
by (dtac CollectD 1);


56 
by (contr_tac 1);


57 
by (swap_res_tac [CollectI] 1);


58 
by (assume_tac 1);


59 


60 
choplev 0;

4089

61 
by (best_tac (claset() addSEs [equalityCE]) 1);

969

62 


63 
(*** The SchroderBerstein Theorem ***)


64 

5432

65 
Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X";

969

66 
by (rtac equalityI 1);

4089

67 
by (fast_tac (claset() addEs [inv_f_f RS ssubst]) 1);


68 
by (fast_tac (claset() addEs [inv_f_f RS ssubst]) 1);

969

69 
qed "inv_image_comp";


70 

5432

71 
Goal "f(a) ~: (f``X) ==> a~:X";

2935

72 
by (Blast_tac 1);

969

73 
qed "contra_imageI";


74 

5490

75 
Goal "(a ~: (X)) = (a:X)";

2935

76 
by (Blast_tac 1);

969

77 
qed "not_Compl";


78 


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


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

5490

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

969

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

1465

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


84 
rtac imageI, rtac Xa]);

969

85 
qed "disj_lemma";


86 

5432

87 
Goalw [image_def]

5490

88 
"range(%z. if z:X then f(z) else g(z)) = f``X Un g``(X)";

4686

89 
by (Simp_tac 1);

2935

90 
by (Blast_tac 1);

969

91 
qed "range_if_then_else";


92 

5432

93 
Goalw [surj_def] "surj(f) = (!a. a : range(f))";

4089

94 
by (fast_tac (claset() addEs [ssubst]) 1);

969

95 
qed "surj_iff_full_range";


96 

5490

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

1487

98 
by (EVERY1[stac surj_iff_full_range, stac range_if_then_else,

5432

99 
etac subst]);

5490

100 
by (Blast_tac 1);

969

101 
qed "surj_if_then_else";


102 

5432

103 
val [injf,injg,compl,bij] =


104 
goal Lfp.thy

5490

105 
"[ inj_on f X; inj_on g (X); (f``X) = g``(X); \

969

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


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


108 
val f_eq_gE = make_elim (compl RS disj_lemma);

2031

109 
by (stac bij 1);

969

110 
by (rtac conjI 1);


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


112 
by (rewtac inj_def);


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

4831

114 
by (EVERY1 [rtac allI, rtac allI, stac split_if, rtac conjI, stac split_if]);


115 
by (fast_tac (claset() addEs [inj_onD, sym RS f_eq_gE]) 1);


116 
by (stac split_if 1);


117 
by (fast_tac (claset() addEs [inj_onD, f_eq_gE]) 1);

969

118 
qed "bij_if_then_else";


119 

5490

120 
Goal "!!f:: 'a=>'b. ? X. X =  (g``( f``X))";

969

121 
by (rtac exI 1);


122 
by (rtac lfp_Tarski 1);


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


124 
qed "decomposition";


125 

5432

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

969

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


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


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


130 
by (rtac exI 1);


131 
by (rtac bij_if_then_else 1);


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

4831

133 
rtac (injg RS inj_on_inv) 1]);

969

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

1465

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

969

136 
by (EVERY1 [etac ssubst, stac double_complement,

1465

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

969

138 
qed "schroeder_bernstein";


139 


140 
writeln"Reached end of file.";
