ex/set.ML
author clasohm
Wed, 02 Mar 1994 12:26:55 +0100
changeset 48 21291189b51e
parent 19 da15d528fb19
child 90 5c7a69cef18b
permissions -rw-r--r--
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	HOL/ex/set.ML
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     5
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     6
Cantor's Theorem; the Schroeder-Berstein Theorem.  
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     7
*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     8
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     9
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    10
writeln"File HOL/ex/set.";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    11
19
da15d528fb19 added "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"
nipkow
parents: 6
diff changeset
    12
(*** A unique fixpoint theorem --- fast/best/meson all fail ***)
da15d528fb19 added "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"
nipkow
parents: 6
diff changeset
    13
da15d528fb19 added "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"
nipkow
parents: 6
diff changeset
    14
val [prem] = goal HOL.thy "?!x.f(g(x))=x ==> ?!y.g(f(y))=y";
da15d528fb19 added "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"
nipkow
parents: 6
diff changeset
    15
by(EVERY1[rtac (prem RS ex1E), rtac ex1I, etac arg_cong,
da15d528fb19 added "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"
nipkow
parents: 6
diff changeset
    16
          rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]);
da15d528fb19 added "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"
nipkow
parents: 6
diff changeset
    17
result();
da15d528fb19 added "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"
nipkow
parents: 6
diff changeset
    18
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    19
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    20
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    21
goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    22
(*requires best-first search because it is undirectional*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    23
by (best_tac (set_cs addSEs [equalityCE]) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    24
val cantor1 = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    25
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    26
(*This form displays the diagonal term*)
6
4448d76f87ef used ~= for "not equals" and ~: for "not in"
lcp
parents: 0
diff changeset
    27
goal Set.thy "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)";
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    28
by (best_tac (set_cs addSEs [equalityCE]) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    29
uresult();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    30
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    31
(*This form exploits the set constructs*)
6
4448d76f87ef used ~= for "not equals" and ~: for "not in"
lcp
parents: 0
diff changeset
    32
goal Set.thy "?S ~: range(f :: 'a=>'a set)";
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    33
by (rtac notI 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    34
by (etac rangeE 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    35
by (etac equalityCE 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    36
by (dtac CollectD 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    37
by (contr_tac 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    38
by (swap_res_tac [CollectI] 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    39
by (assume_tac 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    40
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    41
choplev 0;
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    42
by (best_tac (set_cs addSEs [equalityCE]) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    43
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    44
(*** The Schroder-Berstein Theorem ***)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    45
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    46
val prems = goalw Lfp.thy [image_def] "inj(f) ==> Inv(f)``(f``X) = X";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    47
by (cut_facts_tac prems 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    48
by (rtac equalityI 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    49
by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    50
by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    51
val inv_image_comp = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    52
6
4448d76f87ef used ~= for "not equals" and ~: for "not in"
lcp
parents: 0
diff changeset
    53
val prems = goal Set.thy "f(a) ~: (f``X) ==> a~:X";
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    54
by (cfast_tac prems 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    55
val contra_imageI = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    56
6
4448d76f87ef used ~= for "not equals" and ~: for "not in"
lcp
parents: 0
diff changeset
    57
goal Lfp.thy "(a ~: Compl(X)) = (a:X)";
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    58
by (fast_tac set_cs 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    59
val not_Compl = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    60
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    61
(*Lots of backtracking in this proof...*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    62
val [compl,fg,Xa] = goal Lfp.thy
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    63
    "[| Compl(f``X) = g``Compl(X);  f(a)=g(b);  a:X |] ==> b:X";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    64
by (EVERY1 [rtac (not_Compl RS subst), rtac contra_imageI,
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    65
	    rtac (compl RS subst), rtac (fg RS subst), stac not_Compl,
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    66
	    rtac imageI, rtac Xa]);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    67
val disj_lemma = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    68
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    69
goal Lfp.thy "range(%z. if(z:X, f(z), g(z))) = f``X Un g``Compl(X)";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    70
by (rtac equalityI 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    71
by (rewtac range_def);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    72
by (fast_tac (set_cs addIs [if_P RS sym, if_not_P RS sym]) 2);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    73
by (rtac subsetI 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    74
by (etac CollectE 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    75
by (etac exE 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    76
by (etac ssubst 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    77
by (rtac (excluded_middle RS disjE) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    78
by (EVERY' [rtac (if_P     RS ssubst), atac, fast_tac set_cs] 2);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    79
by (EVERY' [rtac (if_not_P RS ssubst), atac, fast_tac set_cs] 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    80
val range_if_then_else = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    81
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    82
goal Lfp.thy "a : X Un Compl(X)";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    83
by (fast_tac set_cs 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    84
val X_Un_Compl = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    85
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    86
goalw Lfp.thy [surj_def] "surj(f) = (!a. a : range(f))";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    87
by (fast_tac (set_cs addEs [ssubst]) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    88
val surj_iff_full_range = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    89
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    90
val [compl] = goal Lfp.thy
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    91
    "Compl(f``X) = g``Compl(X) ==> surj(%z. if(z:X, f(z), g(z)))";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    92
by (sstac [surj_iff_full_range, range_if_then_else, compl RS sym] 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    93
by (rtac (X_Un_Compl RS allI) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    94
val surj_if_then_else = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    95
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    96
val [injf,injg,compl,bij] = goal Lfp.thy
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    97
    "[| inj_onto(f,X);  inj_onto(g,Compl(X));  Compl(f``X) = g``Compl(X); \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    98
\       bij = (%z. if(z:X, f(z), g(z))) |] ==> \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    99
\       inj(bij) & surj(bij)";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   100
val f_eq_gE = make_elim (compl RS disj_lemma);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   101
by (rtac (bij RS ssubst) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   102
by (rtac conjI 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   103
by (rtac (compl RS surj_if_then_else) 2);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   104
by (rewtac inj_def);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   105
by (cut_facts_tac [injf,injg] 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   106
by (EVERY1 [rtac allI, rtac allI, stac expand_if, rtac conjI, stac expand_if]);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   107
by (fast_tac (set_cs addEs  [inj_ontoD, sym RS f_eq_gE]) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   108
by (stac expand_if 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   109
by (fast_tac (set_cs addEs  [inj_ontoD, f_eq_gE]) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   110
val bij_if_then_else = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   111
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   112
goal Lfp.thy "? X. X = Compl(g``Compl(f:: 'a=>'b``X))";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   113
by (rtac exI 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   114
by (rtac lfp_Tarski 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   115
by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   116
val decomposition = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   117
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   118
val [injf,injg] = goal Lfp.thy
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   119
   "[| inj(f:: 'a=>'b);  inj(g:: 'b=>'a) |] ==> \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   120
\   ? h:: 'a=>'b. inj(h) & surj(h)";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   121
by (rtac (decomposition RS exE) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   122
by (rtac exI 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   123
by (rtac bij_if_then_else 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   124
by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1,
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   125
	   rtac (injg RS inj_onto_Inv) 1]);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   126
by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI,
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   127
	    etac imageE, etac ssubst, rtac rangeI]);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   128
by (EVERY1 [etac ssubst, stac double_complement, 
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   129
	    rtac (injg RS inv_image_comp RS sym)]);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   130
val schroeder_bernstein = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   131
7949f97df77a Initial revision
clasohm
parents:
diff changeset
   132
writeln"Reached end of file.";