src/HOL/Isar_examples/Cantor.thy
author wenzelm
Fri, 23 Apr 1999 11:50:35 +0200
changeset 6494 ab1442d2e4e1
parent 6444 2ebe9e630cab
child 6505 2863855a6902
permissions -rw-r--r--
detailed proofs;
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
Cantor's theorem (see also 'Isabelle's Object-Logics').
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     6
*)
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
theory Cantor = Main:;
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     9
6494
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    10
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    11
theorem "EX S. S ~: range(f :: 'a => 'a set)";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    12
proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    13
  let ??S = "{x. x ~: f x}";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    14
  show "??S ~: range f";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    15
  proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    16
    assume "??S : range f";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    17
    then; show False;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    18
    proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    19
      fix y; 
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    20
      assume "??S = f y";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    21
      then; show ??thesis;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    22
      proof (rule equalityCE);
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    23
        assume y_in_S: "y : ??S";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    24
        assume y_in_fy: "y : f y";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    25
        from y_in_S; have y_notin_fy: "y ~: f y"; ..;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    26
        from y_notin_fy y_in_fy; show ??thesis; ..;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    27
      next;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    28
        assume y_notin_S: "y ~: ??S";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    29
        assume y_notin_fy: "y ~: f y";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    30
        from y_notin_S; have y_in_fy: "y : f y"; ..;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    31
        from y_notin_fy y_in_fy; show ??thesis; ..;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    32
      qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    33
    qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    34
  qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    35
qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    36
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    37
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    38
theorem "EX S. S ~: range(f :: 'a => 'a set)";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    39
proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    40
  let ??S = "{x. x ~: f x}";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    41
  show "??S ~: range f";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    42
  proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    43
    assume "??S : range f";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    44
    then; show False;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    45
    proof;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    46
      fix y; 
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    47
      assume "??S = f y";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    48
      then; show ??thesis;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    49
      proof (rule equalityCE);
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    50
        assume "y : ??S"; then; have y_notin_fy: "y ~: f y"; ..;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    51
        assume "y : f y";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    52
        from y_notin_fy it; show ??thesis; ..;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    53
      next;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    54
        assume "y ~: ??S"; then; have y_in_fy: "y : f y"; ..;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    55
        assume "y ~: f y";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    56
        from it y_in_fy; show ??thesis; ..;
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
qed;
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    61
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    62
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    63
theorem "EX S. S ~: range(f :: 'a => 'a set)";
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    64
  by (best elim: equalityCE);
ab1442d2e4e1 detailed proofs;
wenzelm
parents: 6444
diff changeset
    65
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    66
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    67
end;