src/HOL/Isar_examples/Cantor.thy
author wenzelm
Fri, 28 May 1999 13:30:59 +0200
changeset 6746 cf6ad8d22793
parent 6744 9727e83f0578
child 7480 0a0e0dbe1269
permissions -rw-r--r--
tuned formal comments;
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
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
     5
Cantor's theorem -- Isar'ized version of the final section of the HOL
6507
wenzelm
parents: 6506
diff changeset
     6
chapter of "Isabelle's Object-Logics" (Larry Paulson).
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     7
*)
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     8
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     9
theory Cantor = Main:;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    10
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    11
6746
cf6ad8d22793 tuned formal comments;
wenzelm
parents: 6744
diff changeset
    12
section {* Example: Cantor's Theorem *};
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    13
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    14
text {*
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    15
  Cantor's Theorem states that every set has more subsets than it has
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    16
  elements.  It has become a favourite example in higher-order logic
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    17
  since it is so easily expressed: @{display term[show_types] "ALL f
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    18
  :: 'a => 'a => bool. EX S :: 'a => bool. ALL x::'a. f x ~= S"}
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    19
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    20
  Viewing types as sets, @{type "'a => bool"} represents the powerset
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    21
  of @{type 'a}.  This version states that for every function from
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    22
  @{type 'a} to its powerset, some subset is outside its range.
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    23
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    24
  The Isabelle/Isar proofs below use HOL's set theory, with the type
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    25
  @{type "'a set"} and the operator @{term range}.
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    26
*};
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    27
6506
wenzelm
parents: 6505
diff changeset
    28
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    29
text {*
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    30
  We first consider a rather verbose version of the proof, with the
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    31
  reasoning expressed quite naively.  We only make use of the pure
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    32
  core of the Isar proof language.
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    33
*};
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    34
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    35
theorem "EX S. S ~: range(f :: 'a => 'a set)";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    36
proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    37
  let ??S = "{x. x ~: f x}";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    38
  show "??S ~: range f";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    39
  proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    40
    assume "??S : range f";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    41
    then; show False;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    42
    proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    43
      fix y; 
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    44
      assume "??S = f y";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    45
      then; show ??thesis;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    46
      proof (rule equalityCE);
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    47
        assume y_in_S: "y : ??S";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    48
        assume y_in_fy: "y : f y";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    49
        from y_in_S; have y_notin_fy: "y ~: f y"; ..;
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    50
        from y_notin_fy y_in_fy; show ??thesis; by contradiction;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    51
      next;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    52
        assume y_notin_S: "y ~: ??S";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    53
        assume y_notin_fy: "y ~: f y";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    54
        from y_notin_S; have y_in_fy: "y : f y"; ..;
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    55
        from y_notin_fy y_in_fy; show ??thesis; by contradiction;
6494
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
  qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    59
qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    60
6506
wenzelm
parents: 6505
diff changeset
    61
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    62
text {*
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    63
  The following version essentially does the same reasoning, only that
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    64
  it is expressed more neatly, with some derived Isar language
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    65
  elements involved.
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    66
*};
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    67
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    68
theorem "EX S. S ~: range(f :: 'a => 'a set)";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    69
proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    70
  let ??S = "{x. x ~: f x}";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    71
  show "??S ~: range f";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    72
  proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    73
    assume "??S : range f";
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    74
    thus False;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    75
    proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    76
      fix y; 
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    77
      assume "??S = f y";
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    78
      thus ??thesis;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    79
      proof (rule equalityCE);
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    80
        assume "y : f y";
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    81
        assume "y : ??S"; hence "y ~: f y"; ..;
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    82
        thus ??thesis; by contradiction;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    83
      next;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    84
        assume "y ~: f y";
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    85
        assume "y ~: ??S"; hence "y : f y"; ..;
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    86
        thus ??thesis; by contradiction;
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    87
      qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    88
    qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    89
  qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    90
qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    91
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    92
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    93
text {*
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    94
  How much creativity is required?  As it happens, Isabelle can prove
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    95
  this theorem automatically.  The default classical set contains
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    96
  rules for most of the constructs of HOL's set theory.  We must
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    97
  augment it with @{thm equalityCE} to break up set equalities, and
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    98
  then apply best-first search.  Depth-first search would diverge, but
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    99
  best-first search successfully navigates through the large search
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
   100
  space.
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
   101
*};
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
   102
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
   103
theorem "EX S. S ~: range(f :: 'a => 'a set)";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
   104
  by (best elim: equalityCE);
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
   105
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
   106
text {*
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
   107
  While this establishes the same theorem internally, we do not get
6506
wenzelm
parents: 6505
diff changeset
   108
  any idea of how the proof actually works.  There is currently no way
wenzelm
parents: 6505
diff changeset
   109
  to transform internal system-level representations of Isabelle
wenzelm
parents: 6505
diff changeset
   110
  proofs back into Isar documents.  Writing Isabelle/Isar proof
6507
wenzelm
parents: 6506
diff changeset
   111
  documents actually \emph{is} a creative process.
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
   112
*};
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   113
6506
wenzelm
parents: 6505
diff changeset
   114
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   115
end;