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