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