author  paulson 
Wed, 20 Jan 1999 10:33:34 +0100  
changeset 6146  00f3324048a7 
parent 5786  9a2c90bdadfe 
child 6171  cd237a10cbf8 
permissions  rwrr 
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 

5724  19 
(** Examples for the Blast_tac paper **) 
20 

21 
(*Unionimage, 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 
(*Interimage, 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_tacand 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 bestfirst 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 SchroderBerstein 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."; 