src/HOL/Isar_examples/Cantor.thy
author wenzelm
Sat, 30 Oct 1999 20:20:48 +0200
changeset 7982 d534b897ce39
parent 7955 f30e08579481
child 9474 b0ce3b7c9c26
permissions -rw-r--r--
improved presentation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Isar_examples/Cantor.thy
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     4
*)
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     5
7800
8ee919e42174 improved presentation;
wenzelm
parents: 7748
diff changeset
     6
header {* Cantor's Theorem *};
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     7
7955
wenzelm
parents: 7874
diff changeset
     8
theory Cantor = Main:;
wenzelm
parents: 7874
diff changeset
     9
wenzelm
parents: 7874
diff changeset
    10
text_raw {*
wenzelm
parents: 7874
diff changeset
    11
 \footnote{This is an Isar version of the final example of the
wenzelm
parents: 7874
diff changeset
    12
 Isabelle/HOL manual \cite{isabelle-HOL}.}
7819
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    13
*};
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    14
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    15
text {*
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    16
 Cantor's Theorem states that every set has more subsets than it has
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    17
 elements.  It has become a favorite basic example in pure
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    18
 higher-order logic since it is so easily expressed: \[\all{f::\alpha
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    19
 \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
7874
180364256231 improved presentation;
wenzelm
parents: 7869
diff changeset
    20
 \all{x::\alpha} f \ap x \not= S\]
7748
5b9c45b21782 improved presentation;
wenzelm
parents: 7480
diff changeset
    21
  
7819
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    22
 Viewing types as sets, $\alpha \To \idt{bool}$ represents the
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    23
 powerset of $\alpha$.  This version of the theorem states that for
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    24
 every function from $\alpha$ to its powerset, some subset is outside
7860
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    25
 its range.  The Isabelle/Isar proofs below uses HOL's set theory,
7874
180364256231 improved presentation;
wenzelm
parents: 7869
diff changeset
    26
 with the type $\alpha \ap \idt{set}$ and the operator
180364256231 improved presentation;
wenzelm
parents: 7869
diff changeset
    27
 $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.
7748
5b9c45b21782 improved presentation;
wenzelm
parents: 7480
diff changeset
    28
  
7860
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    29
 \bigskip We first consider a slightly awkward version of the proof,
7874
180364256231 improved presentation;
wenzelm
parents: 7869
diff changeset
    30
 with the innermost reasoning expressed quite naively.
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    31
*};
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    32
7982
d534b897ce39 improved presentation;
wenzelm
parents: 7955
diff changeset
    33
theorem "EX S. S ~: range (f :: 'a => 'a set)";
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    34
proof;
7480
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    35
  let ?S = "{x. x ~: f x}";
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    36
  show "?S ~: range f";
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    37
  proof;
7480
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    38
    assume "?S : range f";
7860
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    39
    thus False;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    40
    proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    41
      fix y; 
7480
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    42
      assume "?S = f y";
7860
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    43
      thus ?thesis;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    44
      proof (rule equalityCE);
7860
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    45
        assume in_S: "y : ?S";
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    46
        assume in_fy: "y : f y";
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    47
        from in_S; have notin_fy: "y ~: f y"; ..;
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    48
        from notin_fy in_fy; show ?thesis; by contradiction;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    49
      next;
7860
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    50
        assume notin_S: "y ~: ?S";
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    51
        assume notin_fy: "y ~: f y";
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    52
        from notin_S; have in_fy: "y : f y"; ..;
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    53
        from notin_fy in_fy; show ?thesis; by contradiction;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    54
      qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    55
    qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    56
  qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    57
qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    58
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    59
text {*
7819
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    60
 The following version of the proof essentially does the same
7860
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    61
 reasoning, only that it is expressed more neatly.  In particular, we
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    62
 change the order of assumptions introduced in the two cases of rule
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    63
 \name{equalityCE}, streamlining the flow of intermediate facts and
7819547df4d8 improved presentation;
wenzelm
parents: 7833
diff changeset
    64
 avoiding explicit naming.\footnote{In general, neither the order of
7874
180364256231 improved presentation;
wenzelm
parents: 7869
diff changeset
    65
 assumptions as introduced by \isacommand{assume}, nor the order of
180364256231 improved presentation;
wenzelm
parents: 7869
diff changeset
    66
 goals as solved by \isacommand{show} is of any significance.  The
180364256231 improved presentation;
wenzelm
parents: 7869
diff changeset
    67
 basic logical structure has to be left intact, though.  In
180364256231 improved presentation;
wenzelm
parents: 7869
diff changeset
    68
 particular, assumptions ``belonging'' to some goal have to be
180364256231 improved presentation;
wenzelm
parents: 7869
diff changeset
    69
 introduced \emph{before} its corresponding \isacommand{show}.}
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    70
*};
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    71
7982
d534b897ce39 improved presentation;
wenzelm
parents: 7955
diff changeset
    72
theorem "EX S. S ~: range (f :: 'a => 'a set)";
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    73
proof;
7480
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    74
  let ?S = "{x. x ~: f x}";
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    75
  show "?S ~: range f";
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    76
  proof;
7480
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    77
    assume "?S : range f";
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    78
    thus False;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    79
    proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    80
      fix y; 
7480
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    81
      assume "?S = f y";
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    82
      thus ?thesis;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    83
      proof (rule equalityCE);
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    84
        assume "y : f y";
7480
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    85
        assume "y : ?S"; hence "y ~: f y"; ..;
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    86
        thus ?thesis; by contradiction;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    87
      next;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    88
        assume "y ~: f y";
7480
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    89
        assume "y ~: ?S"; hence "y : f y"; ..;
0a0e0dbe1269 replaced ?? by ?;
wenzelm
parents: 6746
diff changeset
    90
        thus ?thesis; by contradiction;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    91
      qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    92
    qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    93
  qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    94
qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    95
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    96
text {*
7819
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    97
 How much creativity is required?  As it happens, Isabelle can prove
7982
d534b897ce39 improved presentation;
wenzelm
parents: 7955
diff changeset
    98
 this theorem automatically.  The context of Isabelle's classical
d534b897ce39 improved presentation;
wenzelm
parents: 7955
diff changeset
    99
 prover contains rules for most of the constructs of HOL's set theory.
d534b897ce39 improved presentation;
wenzelm
parents: 7955
diff changeset
   100
 We must augment it with \name{equalityCE} to break up set equalities,
d534b897ce39 improved presentation;
wenzelm
parents: 7955
diff changeset
   101
 and then apply best-first search.  Depth-first search would diverge,
d534b897ce39 improved presentation;
wenzelm
parents: 7955
diff changeset
   102
 but best-first search successfully navigates through the large search
d534b897ce39 improved presentation;
wenzelm
parents: 7955
diff changeset
   103
 space.
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
   104
*};
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
   105
7982
d534b897ce39 improved presentation;
wenzelm
parents: 7955
diff changeset
   106
theorem "EX S. S ~: range (f :: 'a => 'a set)";
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
   107
  by (best elim: equalityCE);
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
   108
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
   109
text {*
7819
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
   110
 While this establishes the same theorem internally, we do not get any
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
   111
 idea of how the proof actually works.  There is currently no way to
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
   112
 transform internal system-level representations of Isabelle proofs
7982
d534b897ce39 improved presentation;
wenzelm
parents: 7955
diff changeset
   113
 back into Isar text.  Writing intelligible proof documents
7874
180364256231 improved presentation;
wenzelm
parents: 7869
diff changeset
   114
 really is a creative process, after all.
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
   115
*};
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   116
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   117
end;