src/HOL/Isar_examples/Cantor.thy
author haftmann
Mon, 29 Sep 2008 12:31:58 +0200
changeset 28401 d5f39173444c
parent 23373 ead82c82da9e
child 31758 3edd5f813f01
permissions -rw-r--r--
separate HOL-Main image
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
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
     6
header {* Cantor's Theorem *}
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12388
diff changeset
     8
theory Cantor imports Main begin
7955
wenzelm
parents: 7874
diff changeset
     9
wenzelm
parents: 7874
diff changeset
    10
text_raw {*
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    11
  \footnote{This is an Isar version of the final example of the
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    12
  Isabelle/HOL manual \cite{isabelle-HOL}.}
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    13
*}
7819
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    14
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    15
text {*
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    16
  Cantor's Theorem states that every set has more subsets than it has
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    17
  elements.  It has become a favorite basic example in pure
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    18
  higher-order logic since it is so easily expressed: \[\all{f::\alpha
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    19
  \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    20
  \all{x::\alpha} f \ap x \not= S\]
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    21
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    22
  Viewing types as sets, $\alpha \To \idt{bool}$ represents the
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    23
  powerset of $\alpha$.  This version of the theorem states that for
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    24
  every function from $\alpha$ to its powerset, some subset is outside
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    25
  its range.  The Isabelle/Isar proofs below uses HOL's set theory,
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    26
  with the type $\alpha \ap \idt{set}$ and the operator
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    27
  $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    28
*}
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    29
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    30
theorem "EX S. S ~: range (f :: 'a => 'a set)"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    31
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    32
  let ?S = "{x. x ~: f x}"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    33
  show "?S ~: range f"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    34
  proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    35
    assume "?S : range f"
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    36
    then obtain y where "?S = f y" ..
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    37
    then show False
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    38
    proof (rule equalityCE)
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    39
      assume "y : f y"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    40
      assume "y : ?S" then have "y ~: f y" ..
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    41
      with `y : f y` show ?thesis by contradiction
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    42
    next
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    43
      assume "y ~: ?S"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    44
      assume "y ~: f y" then have "y : ?S" ..
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    45
      with `y ~: ?S` show ?thesis by contradiction
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    46
    qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    47
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    48
qed
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    49
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    50
text {*
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    51
  How much creativity is required?  As it happens, Isabelle can prove
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    52
  this theorem automatically using best-first search.  Depth-first
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    53
  search would diverge, but best-first search successfully navigates
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    54
  through the large search space.  The context of Isabelle's classical
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    55
  prover contains rules for the relevant constructs of HOL's set
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    56
  theory.
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    57
*}
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    58
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    59
theorem "EX S. S ~: range (f :: 'a => 'a set)"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    60
  by best
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    61
6744
9727e83f0578 changed {| |} verbatim syntax to {* *};
wenzelm
parents: 6517
diff changeset
    62
text {*
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    63
  While this establishes the same theorem internally, we do not get
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    64
  any idea of how the proof actually works.  There is currently no way
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    65
  to transform internal system-level representations of Isabelle
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    66
  proofs back into Isar text.  Writing intelligible proof documents
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    67
  really is a creative process, after all.
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    68
*}
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    69
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    70
end