author  paulson 
Mon, 21 Feb 2000 11:15:43 +0100  
changeset 8266  4bc79ed1233b 
parent 7377  2ad85e036c21 
child 9100  9e081c812338 
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 

8266  14 
(*These two are cited in Benzmueller and Kohlhash's system description of LEO, 
15 
CADE15, 1998 (page 139143) as theorems LEO could not prove.*) 

16 

17 
Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V > X<=V))"; 

18 
by (Blast_tac 1); 

19 
result(); 

20 

21 
Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z > V<=X))"; 

22 
by (Blast_tac 1); 

23 
result(); 

24 

5432  25 
(*trivial example of term synthesis: apparently hard for some provers!*) 
26 
Goal "a ~= b ==> a:?X & b ~: ?X"; 

27 
by (Blast_tac 1); 

28 
result(); 

29 

5724  30 
(** Examples for the Blast_tac paper **) 
31 

32 
(*Unionimage, called Un_Union_image on equalities.ML*) 

6146  33 
Goal "(UN x:C. f(x) Un g(x)) = Union(f``C) Un Union(g``C)"; 
5724  34 
by (Blast_tac 1); 
35 
result(); 

36 

37 
(*Interimage, called Int_Inter_image on equalities.ML*) 

6146  38 
Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)"; 
5724  39 
by (Blast_tac 1); 
40 
result(); 

41 

42 
(*Singleton I. Nice demonstration of blast_tacand its limitations*) 

5432  43 
Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; 
4153  44 
(*for some unfathomable reason, UNIV_I increases the search space greatly*) 
45 
by (blast_tac (claset() delrules [UNIV_I]) 1); 

46 
result(); 

47 

5724  48 
(*Singleton II. variant of the benchmark above*) 
5432  49 
Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"; 
4324  50 
by (blast_tac (claset() delrules [UNIV_I]) 1); 
5432  51 
(*just Blast_tac takes 5 seconds instead of 1*) 
4324  52 
result(); 
2998  53 

969  54 
(*** A unique fixpoint theorem  fast/best/meson all fail ***) 
55 

5432  56 
Goal "?!x. f(g(x))=x ==> ?!y. g(f(y))=y"; 
57 
by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong, 

969  58 
rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]); 
59 
result(); 

60 

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

62 

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

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

4089  65 
by (best_tac (claset() addSEs [equalityCE]) 1); 
969  66 
qed "cantor1"; 
67 

68 
(*This form displays the diagonal term*) 

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

4089  70 
by (best_tac (claset() addSEs [equalityCE]) 1); 
969  71 
uresult(); 
72 

73 
(*This form exploits the set constructs*) 

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

75 
by (rtac notI 1); 

76 
by (etac rangeE 1); 

77 
by (etac equalityCE 1); 

78 
by (dtac CollectD 1); 

79 
by (contr_tac 1); 

80 
by (swap_res_tac [CollectI] 1); 

81 
by (assume_tac 1); 

82 

83 
choplev 0; 

4089  84 
by (best_tac (claset() addSEs [equalityCE]) 1); 
969  85 

6236  86 

969  87 
(*** The SchroderBerstein Theorem ***) 
88 

6236  89 
Goal "[ (f``X) = g``(X); f(a)=g(b); a:X ] ==> b:X"; 
90 
by (blast_tac (claset() addEs [equalityE]) 1); 

969  91 
qed "disj_lemma"; 
92 

5490  93 
Goal "(f``X) = g``(X) ==> surj(%z. if z:X then f(z) else g(z))"; 
6236  94 
by (asm_simp_tac (simpset() addsimps [surj_def]) 1); 
95 
by (blast_tac (claset() addEs [equalityE]) 1); 

969  96 
qed "surj_if_then_else"; 
97 

6171  98 
Goalw [inj_on_def] 
99 
"[ 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

100 
\ 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

101 
\ ==> inj(h) & surj(h)"; 
6171  102 
by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1); 
103 
(*PROOF FAILED if inj_onD*) 

104 
by (blast_tac (claset() addDs [disj_lemma, sym RSN (2,disj_lemma)]) 1); 

969  105 
qed "bij_if_then_else"; 
106 

5786
9a2c90bdadfe
increased precedence of unary minus from 80 to 100
paulson
parents:
5724
diff
changeset

107 
Goal "? X. X =  (g``( (f``X)))"; 
969  108 
by (rtac exI 1); 
109 
by (rtac lfp_Tarski 1); 

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

111 
qed "decomposition"; 

112 

5432  113 
val [injf,injg] = goal Lfp.thy 
6171  114 
"[ inj (f:: 'a=>'b); inj (g:: 'b=>'a) ] ==> \ 
969  115 
\ ? h:: 'a=>'b. inj(h) & surj(h)"; 
116 
by (rtac (decomposition RS exE) 1); 

117 
by (rtac exI 1); 

118 
by (rtac bij_if_then_else 1); 

6171  119 
by (rtac refl 4); 
6236  120 
by (rtac inj_on_inv 2); 
121 
by (rtac ([subset_UNIV, injf] MRS subset_inj_on) 1); 

122 
(**tricky variable instantiations!**) 

969  123 
by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, 
1465  124 
etac imageE, etac ssubst, rtac rangeI]); 
969  125 
by (EVERY1 [etac ssubst, stac double_complement, 
1465  126 
rtac (injg RS inv_image_comp RS sym)]); 
969  127 
qed "schroeder_bernstein"; 
128 

129 
writeln"Reached end of file."; 