src/HOL/ex/set.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10198 2b255b772585
child 10834 a7897aebbffc
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 969
diff changeset
     1
(*  Title:      HOL/ex/set.ML
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 969
diff changeset
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
969
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
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
     9
(*These two are cited in Benzmueller and Kohlhase's system description of LEO,
8266
4bc79ed1233b new examples that cannot be done in LEO
paulson
parents: 7377
diff changeset
    10
  CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*)
4bc79ed1233b new examples that cannot be done in LEO
paulson
parents: 7377
diff changeset
    11
4bc79ed1233b new examples that cannot be done in LEO
paulson
parents: 7377
diff changeset
    12
Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))";
4bc79ed1233b new examples that cannot be done in LEO
paulson
parents: 7377
diff changeset
    13
by (Blast_tac 1);
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
    14
qed "";
8266
4bc79ed1233b new examples that cannot be done in LEO
paulson
parents: 7377
diff changeset
    15
4bc79ed1233b new examples that cannot be done in LEO
paulson
parents: 7377
diff changeset
    16
Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))";
4bc79ed1233b new examples that cannot be done in LEO
paulson
parents: 7377
diff changeset
    17
by (Blast_tac 1);
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
    18
qed "";
8266
4bc79ed1233b new examples that cannot be done in LEO
paulson
parents: 7377
diff changeset
    19
5432
983b9bf8e89f new example; tidying
paulson
parents: 4831
diff changeset
    20
(*trivial example of term synthesis: apparently hard for some provers!*)
983b9bf8e89f new example; tidying
paulson
parents: 4831
diff changeset
    21
Goal "a ~= b ==> a:?X & b ~: ?X";
983b9bf8e89f new example; tidying
paulson
parents: 4831
diff changeset
    22
by (Blast_tac 1);
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
    23
qed "";
5432
983b9bf8e89f new example; tidying
paulson
parents: 4831
diff changeset
    24
5724
a9f8cb9b5b5d standard Blast_tac demos
paulson
parents: 5490
diff changeset
    25
(** Examples for the Blast_tac paper **)
a9f8cb9b5b5d standard Blast_tac demos
paulson
parents: 5490
diff changeset
    26
a9f8cb9b5b5d standard Blast_tac demos
paulson
parents: 5490
diff changeset
    27
(*Union-image, called Un_Union_image on equalities.ML*)
6146
00f3324048a7 renamed variables for clarity
paulson
parents: 5786
diff changeset
    28
Goal "(UN x:C. f(x) Un g(x)) = Union(f``C)  Un  Union(g``C)";
5724
a9f8cb9b5b5d standard Blast_tac demos
paulson
parents: 5490
diff changeset
    29
by (Blast_tac 1);
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
    30
qed "";
5724
a9f8cb9b5b5d standard Blast_tac demos
paulson
parents: 5490
diff changeset
    31
a9f8cb9b5b5d standard Blast_tac demos
paulson
parents: 5490
diff changeset
    32
(*Inter-image, called Int_Inter_image on equalities.ML*)
6146
00f3324048a7 renamed variables for clarity
paulson
parents: 5786
diff changeset
    33
Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)";
5724
a9f8cb9b5b5d standard Blast_tac demos
paulson
parents: 5490
diff changeset
    34
by (Blast_tac 1);
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
    35
qed "";
5724
a9f8cb9b5b5d standard Blast_tac demos
paulson
parents: 5490
diff changeset
    36
a9f8cb9b5b5d standard Blast_tac demos
paulson
parents: 5490
diff changeset
    37
(*Singleton I.  Nice demonstration of blast_tac--and its limitations*)
5432
983b9bf8e89f new example; tidying
paulson
parents: 4831
diff changeset
    38
Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4109
diff changeset
    39
(*for some unfathomable reason, UNIV_I increases the search space greatly*)
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4109
diff changeset
    40
by (blast_tac (claset() delrules [UNIV_I]) 1);
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
    41
qed "";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4109
diff changeset
    42
5724
a9f8cb9b5b5d standard Blast_tac demos
paulson
parents: 5490
diff changeset
    43
(*Singleton II.  variant of the benchmark above*)
5432
983b9bf8e89f new example; tidying
paulson
parents: 4831
diff changeset
    44
Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
4324
9bfac4684f2f New example
paulson
parents: 4153
diff changeset
    45
by (blast_tac (claset() delrules [UNIV_I]) 1);
5432
983b9bf8e89f new example; tidying
paulson
parents: 4831
diff changeset
    46
(*just Blast_tac takes 5 seconds instead of 1*)
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
    47
qed "";
2998
62a5230883bb New blast_tac demo
paulson
parents: 2935
diff changeset
    48
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    49
(*** A unique fixpoint theorem --- fast/best/meson all fail ***)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    50
9166
paulson
parents: 9100
diff changeset
    51
Goal "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y";
5432
983b9bf8e89f new example; tidying
paulson
parents: 4831
diff changeset
    52
by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong,
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    53
          rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]);
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
    54
qed "";
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
    55
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    56
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    57
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    58
9166
paulson
parents: 9100
diff changeset
    59
Goal "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    60
(*requires best-first search because it is undirectional*)
10198
paulson
parents: 10186
diff changeset
    61
by (Best_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    62
qed "cantor1";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    63
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    64
(*This form displays the diagonal term*)
9166
paulson
parents: 9100
diff changeset
    65
Goal "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)";
10198
paulson
parents: 10186
diff changeset
    66
by (Best_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    67
uresult();
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    68
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    69
(*This form exploits the set constructs*)
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
    70
Goal "?S ~: range(f :: 'a=>'a set)";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    71
by (rtac notI 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    72
by (etac rangeE 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    73
by (etac equalityCE 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    74
by (dtac CollectD 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    75
by (contr_tac 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    76
by (swap_res_tac [CollectI] 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    77
by (assume_tac 1);
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    78
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    79
choplev 0;
10198
paulson
parents: 10186
diff changeset
    80
by (Best_tac 1);
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
    81
qed "";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    82
6236
958f4fc3e8b8 tidied Schroeder-Bernstein proof
paulson
parents: 6171
diff changeset
    83
9316
e58778cc4d22 fixed comment;
wenzelm
parents: 9190
diff changeset
    84
(*** The Schroeder-Berstein Theorem ***)
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    85
6236
958f4fc3e8b8 tidied Schroeder-Bernstein proof
paulson
parents: 6171
diff changeset
    86
Goal "[| -(f``X) = g``(-X);  f(a)=g(b);  a:X |] ==> b:X";
9190
b86ff604729f tidied proofs using default rule equalityCE
paulson
parents: 9166
diff changeset
    87
by (Blast_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    88
qed "disj_lemma";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    89
5490
85855f65d0c6 From Compl(A) to -A
paulson
parents: 5432
diff changeset
    90
Goal "-(f``X) = g``(-X) ==> surj(%z. if z:X then f(z) else g(z))";
6236
958f4fc3e8b8 tidied Schroeder-Bernstein proof
paulson
parents: 6171
diff changeset
    91
by (asm_simp_tac (simpset() addsimps [surj_def]) 1);
9190
b86ff604729f tidied proofs using default rule equalityCE
paulson
parents: 9166
diff changeset
    92
by (Blast_tac 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    93
qed "surj_if_then_else";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    94
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 6146
diff changeset
    95
Goalw [inj_on_def]
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 6146
diff changeset
    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
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 6146
diff changeset
    99
by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1);
9166
paulson
parents: 9100
diff changeset
   100
by (blast_tac (claset() addDs [disj_lemma, sym]) 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   101
qed "bij_if_then_else";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   102
9166
paulson
parents: 9100
diff changeset
   103
Goal "EX X. X = - (g``(- (f``X)))";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   104
by (rtac exI 1);
10186
499637e8f2c6 *** empty log message ***
nipkow
parents: 9316
diff changeset
   105
by (rtac lfp_unfold 1);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   106
by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   107
qed "decomposition";
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   108
9100
9e081c812338 fixed deps;
wenzelm
parents: 8266
diff changeset
   109
val [injf,injg] = goal (the_context ())
9166
paulson
parents: 9100
diff changeset
   110
   "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |] \
paulson
parents: 9100
diff changeset
   111
\   ==> EX h:: 'a=>'b. inj(h) & surj(h)";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   112
by (rtac (decomposition RS exE) 1);
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 bij_if_then_else 1);
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 6146
diff changeset
   115
by (rtac refl 4);
6236
958f4fc3e8b8 tidied Schroeder-Bernstein proof
paulson
parents: 6171
diff changeset
   116
by (rtac inj_on_inv 2);
958f4fc3e8b8 tidied Schroeder-Bernstein proof
paulson
parents: 6171
diff changeset
   117
by (rtac ([subset_UNIV, injf] MRS subset_inj_on) 1);
958f4fc3e8b8 tidied Schroeder-Bernstein proof
paulson
parents: 6171
diff changeset
   118
  (**tricky variable instantiations!**)
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   119
by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI,
1465
5d7a7e439cec expanded tabs
clasohm
parents: 969
diff changeset
   120
            etac imageE, etac ssubst, rtac rangeI]);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   121
by (EVERY1 [etac ssubst, stac double_complement, 
1465
5d7a7e439cec expanded tabs
clasohm
parents: 969
diff changeset
   122
            rtac (injg RS inv_image_comp RS sym)]);
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   123
qed "schroeder_bernstein";