author  wenzelm 
Thu, 13 Jul 2000 23:13:52 +0200  
changeset 9316  e58778cc4d22 
parent 9190  b86ff604729f 
child 10186  499637e8f2c6 
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 

9100  9 
(*These two are cited in Benzmueller and Kohlhase's system description of LEO, 
8266  10 
CADE15, 1998 (page 139143) as theorems LEO could not prove.*) 
11 

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

13 
by (Blast_tac 1); 

9100  14 
qed ""; 
8266  15 

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

17 
by (Blast_tac 1); 

9100  18 
qed ""; 
8266  19 

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

22 
by (Blast_tac 1); 

9100  23 
qed ""; 
5432  24 

5724  25 
(** Examples for the Blast_tac paper **) 
26 

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

6146  28 
Goal "(UN x:C. f(x) Un g(x)) = Union(f``C) Un Union(g``C)"; 
5724  29 
by (Blast_tac 1); 
9100  30 
qed ""; 
5724  31 

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

6146  33 
Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)"; 
5724  34 
by (Blast_tac 1); 
9100  35 
qed ""; 
5724  36 

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

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

9100  41 
qed ""; 
4153  42 

5724  43 
(*Singleton II. variant of the benchmark above*) 
5432  44 
Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"; 
4324  45 
by (blast_tac (claset() delrules [UNIV_I]) 1); 
5432  46 
(*just Blast_tac takes 5 seconds instead of 1*) 
9100  47 
qed ""; 
2998  48 

969  49 
(*** A unique fixpoint theorem  fast/best/meson all fail ***) 
50 

9166  51 
Goal "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y"; 
5432  52 
by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong, 
969  53 
rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]); 
9100  54 
qed ""; 
55 

969  56 

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

58 

9166  59 
Goal "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)"; 
969  60 
(*requires bestfirst search because it is undirectional*) 
4089  61 
by (best_tac (claset() addSEs [equalityCE]) 1); 
969  62 
qed "cantor1"; 
63 

64 
(*This form displays the diagonal term*) 

9166  65 
Goal "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)"; 
4089  66 
by (best_tac (claset() addSEs [equalityCE]) 1); 
969  67 
uresult(); 
68 

69 
(*This form exploits the set constructs*) 

9100  70 
Goal "?S ~: range(f :: 'a=>'a set)"; 
969  71 
by (rtac notI 1); 
72 
by (etac rangeE 1); 

73 
by (etac equalityCE 1); 

74 
by (dtac CollectD 1); 

75 
by (contr_tac 1); 

76 
by (swap_res_tac [CollectI] 1); 

77 
by (assume_tac 1); 

78 

79 
choplev 0; 

4089  80 
by (best_tac (claset() addSEs [equalityCE]) 1); 
9100  81 
qed ""; 
969  82 

6236  83 

9316  84 
(*** The SchroederBerstein Theorem ***) 
969  85 

6236  86 
Goal "[ (f``X) = g``(X); f(a)=g(b); a:X ] ==> b:X"; 
9190  87 
by (Blast_tac 1); 
969  88 
qed "disj_lemma"; 
89 

5490  90 
Goal "(f``X) = g``(X) ==> surj(%z. if z:X then f(z) else g(z))"; 
6236  91 
by (asm_simp_tac (simpset() addsimps [surj_def]) 1); 
9190  92 
by (Blast_tac 1); 
969  93 
qed "surj_if_then_else"; 
94 

6171  95 
Goalw [inj_on_def] 
96 
"[ 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

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

98 
\ ==> inj(h) & surj(h)"; 
6171  99 
by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1); 
9166  100 
by (blast_tac (claset() addDs [disj_lemma, sym]) 1); 
969  101 
qed "bij_if_then_else"; 
102 

9166  103 
Goal "EX X. X =  (g``( (f``X)))"; 
969  104 
by (rtac exI 1); 
105 
by (rtac lfp_Tarski 1); 

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

107 
qed "decomposition"; 

108 

9100  109 
val [injf,injg] = goal (the_context ()) 
9166  110 
"[ inj (f:: 'a=>'b); inj (g:: 'b=>'a) ] \ 
111 
\ ==> EX h:: 'a=>'b. inj(h) & surj(h)"; 

969  112 
by (rtac (decomposition RS exE) 1); 
113 
by (rtac exI 1); 

114 
by (rtac bij_if_then_else 1); 

6171  115 
by (rtac refl 4); 
6236  116 
by (rtac inj_on_inv 2); 
117 
by (rtac ([subset_UNIV, injf] MRS subset_inj_on) 1); 

118 
(**tricky variable instantiations!**) 

969  119 
by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, 
1465  120 
etac imageE, etac ssubst, rtac rangeI]); 
969  121 
by (EVERY1 [etac ssubst, stac double_complement, 
1465  122 
rtac (injg RS inv_image_comp RS sym)]); 
969  123 
qed "schroeder_bernstein"; 