summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_examples/Cantor.thy

author | wenzelm |

Sat Sep 04 21:13:01 1999 +0200 (1999-09-04) | |

changeset 7480 | 0a0e0dbe1269 |

parent 6746 | cf6ad8d22793 |

child 7748 | 5b9c45b21782 |

permissions | -rw-r--r-- |

replaced ?? by ?;

1 (* Title: HOL/Isar_examples/Cantor.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

5 Cantor's theorem -- Isar'ized version of the final section of the HOL

6 chapter of "Isabelle's Object-Logics" (Larry Paulson).

7 *)

9 theory Cantor = Main:;

12 section {* Example: Cantor's Theorem *};

14 text {*

15 Cantor's Theorem states that every set has more subsets than it has

16 elements. It has become a favourite example in higher-order logic

17 since it is so easily expressed: @{display term[show_types] "ALL f

18 :: 'a => 'a => bool. EX S :: 'a => bool. ALL x::'a. f x ~= S"}

20 Viewing types as sets, @{type "'a => bool"} represents the powerset

21 of @{type 'a}. This version states that for every function from

22 @{type 'a} to its powerset, some subset is outside its range.

24 The Isabelle/Isar proofs below use HOL's set theory, with the type

25 @{type "'a set"} and the operator @{term range}.

26 *};

29 text {*

30 We first consider a rather verbose version of the proof, with the

31 reasoning expressed quite naively. We only make use of the pure

32 core of the Isar proof language.

33 *};

35 theorem "EX S. S ~: range(f :: 'a => 'a set)";

36 proof;

37 let ?S = "{x. x ~: f x}";

38 show "?S ~: range f";

39 proof;

40 assume "?S : range f";

41 then; show False;

42 proof;

43 fix y;

44 assume "?S = f y";

45 then; show ?thesis;

46 proof (rule equalityCE);

47 assume y_in_S: "y : ?S";

48 assume y_in_fy: "y : f y";

49 from y_in_S; have y_notin_fy: "y ~: f y"; ..;

50 from y_notin_fy y_in_fy; show ?thesis; by contradiction;

51 next;

52 assume y_notin_S: "y ~: ?S";

53 assume y_notin_fy: "y ~: f y";

54 from y_notin_S; have y_in_fy: "y : f y"; ..;

55 from y_notin_fy y_in_fy; show ?thesis; by contradiction;

56 qed;

57 qed;

58 qed;

59 qed;

62 text {*

63 The following version essentially does the same reasoning, only that

64 it is expressed more neatly, with some derived Isar language

65 elements involved.

66 *};

68 theorem "EX S. S ~: range(f :: 'a => 'a set)";

69 proof;

70 let ?S = "{x. x ~: f x}";

71 show "?S ~: range f";

72 proof;

73 assume "?S : range f";

74 thus False;

75 proof;

76 fix y;

77 assume "?S = f y";

78 thus ?thesis;

79 proof (rule equalityCE);

80 assume "y : f y";

81 assume "y : ?S"; hence "y ~: f y"; ..;

82 thus ?thesis; by contradiction;

83 next;

84 assume "y ~: f y";

85 assume "y ~: ?S"; hence "y : f y"; ..;

86 thus ?thesis; by contradiction;

87 qed;

88 qed;

89 qed;

90 qed;

93 text {*

94 How much creativity is required? As it happens, Isabelle can prove

95 this theorem automatically. The default classical set contains

96 rules for most of the constructs of HOL's set theory. We must

97 augment it with @{thm equalityCE} to break up set equalities, and

98 then apply best-first search. Depth-first search would diverge, but

99 best-first search successfully navigates through the large search

100 space.

101 *};

103 theorem "EX S. S ~: range(f :: 'a => 'a set)";

104 by (best elim: equalityCE);

106 text {*

107 While this establishes the same theorem internally, we do not get

108 any idea of how the proof actually works. There is currently no way

109 to transform internal system-level representations of Isabelle

110 proofs back into Isar documents. Writing Isabelle/Isar proof

111 documents actually \emph{is} a creative process.

112 *};

115 end;