src/HOL/Isar_Examples/Cantor.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 37671 fa53d267dab3
child 55640 abc140f21caa
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 31758
diff changeset
     1
(*  Title:      HOL/Isar_Examples/Cantor.thy
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     3
*)
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     4
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
     5
header {* Cantor's Theorem *}
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     6
31758
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 23373
diff changeset
     7
theory Cantor
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 23373
diff changeset
     8
imports Main
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 23373
diff changeset
     9
begin
7955
wenzelm
parents: 7874
diff changeset
    10
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    11
text_raw {* \footnote{This is an Isar version of the final example of
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    12
  the Isabelle/HOL manual \cite{isabelle-HOL}.}  *}
7819
6dd018b6cf3f tuned presentation;
wenzelm
parents: 7800
diff changeset
    13
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    14
text {* Cantor's Theorem states that every set has more subsets than
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    15
  it has elements.  It has become a favorite basic example in pure
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    16
  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
    17
  \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    18
  \all{x::\alpha} f \ap x \not= S\]
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    19
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    20
  Viewing types as sets, $\alpha \To \idt{bool}$ represents the
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    21
  powerset of $\alpha$.  This version of the theorem states that for
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    22
  every function from $\alpha$ to its powerset, some subset is outside
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    23
  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
    24
  with the type $\alpha \ap \idt{set}$ and the operator
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    25
  $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *}
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    26
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    27
theorem "EX S. S ~: range (f :: 'a => 'a set)"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    28
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    29
  let ?S = "{x. x ~: f x}"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    30
  show "?S ~: range f"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    31
  proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    32
    assume "?S : range f"
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    33
    then obtain y where "?S = f y" ..
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    34
    then show False
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    35
    proof (rule equalityCE)
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    36
      assume "y : f y"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    37
      assume "y : ?S" then have "y ~: f y" ..
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    38
      with `y : f y` show ?thesis by contradiction
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    39
    next
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    40
      assume "y ~: ?S"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    41
      assume "y ~: f y" then have "y : ?S" ..
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    42
      with `y ~: ?S` show ?thesis by contradiction
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    43
    qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    44
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    45
qed
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    46
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    47
text {* How much creativity is required?  As it happens, Isabelle can
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    48
  prove this theorem automatically using best-first search.
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    49
  Depth-first search would diverge, but best-first search successfully
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    50
  navigates through the large search space.  The context of Isabelle's
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    51
  classical prover contains rules for the relevant constructs of HOL's
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    52
  set theory.  *}
6505
2863855a6902 elaborated;
wenzelm
parents: 6494
diff changeset
    53
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    54
theorem "EX S. S ~: range (f :: 'a => 'a set)"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    55
  by best
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    56
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    57
text {* While this establishes the same theorem internally, we do not
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    58
  get any idea of how the proof actually works.  There is currently no
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    59
  way to transform internal system-level representations of Isabelle
12388
c845fec1ac94 simplified proof (no longer use swapped rules);
wenzelm
parents: 10007
diff changeset
    60
  proofs back into Isar text.  Writing intelligible proof documents
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    61
  really is a creative process, after all. *}
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    62
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9474
diff changeset
    63
end