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

src/HOL/Isar_examples/Cantor.thy

author | wenzelm |

Sat Oct 30 20:20:48 1999 +0200 (1999-10-30) | |

changeset 7982 | d534b897ce39 |

parent 7955 | f30e08579481 |

child 9474 | b0ce3b7c9c26 |

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

improved presentation;

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

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

4 *)

6 header {* Cantor's Theorem *};

8 theory Cantor = Main:;

10 text_raw {*

11 \footnote{This is an Isar version of the final example of the

12 Isabelle/HOL manual \cite{isabelle-HOL}.}

13 *};

15 text {*

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

17 elements. It has become a favorite basic example in pure

18 higher-order logic since it is so easily expressed: \[\all{f::\alpha

19 \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}

20 \all{x::\alpha} f \ap x \not= S\]

22 Viewing types as sets, $\alpha \To \idt{bool}$ represents the

23 powerset of $\alpha$. This version of the theorem states that for

24 every function from $\alpha$ to its powerset, some subset is outside

25 its range. The Isabelle/Isar proofs below uses HOL's set theory,

26 with the type $\alpha \ap \idt{set}$ and the operator

27 $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.

29 \bigskip We first consider a slightly awkward version of the proof,

30 with the innermost reasoning expressed quite naively.

31 *};

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

34 proof;

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

36 show "?S ~: range f";

37 proof;

38 assume "?S : range f";

39 thus False;

40 proof;

41 fix y;

42 assume "?S = f y";

43 thus ?thesis;

44 proof (rule equalityCE);

45 assume in_S: "y : ?S";

46 assume in_fy: "y : f y";

47 from in_S; have notin_fy: "y ~: f y"; ..;

48 from notin_fy in_fy; show ?thesis; by contradiction;

49 next;

50 assume notin_S: "y ~: ?S";

51 assume notin_fy: "y ~: f y";

52 from notin_S; have in_fy: "y : f y"; ..;

53 from notin_fy in_fy; show ?thesis; by contradiction;

54 qed;

55 qed;

56 qed;

57 qed;

59 text {*

60 The following version of the proof essentially does the same

61 reasoning, only that it is expressed more neatly. In particular, we

62 change the order of assumptions introduced in the two cases of rule

63 \name{equalityCE}, streamlining the flow of intermediate facts and

64 avoiding explicit naming.\footnote{In general, neither the order of

65 assumptions as introduced by \isacommand{assume}, nor the order of

66 goals as solved by \isacommand{show} is of any significance. The

67 basic logical structure has to be left intact, though. In

68 particular, assumptions ``belonging'' to some goal have to be

69 introduced \emph{before} its corresponding \isacommand{show}.}

70 *};

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

73 proof;

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

75 show "?S ~: range f";

76 proof;

77 assume "?S : range f";

78 thus False;

79 proof;

80 fix y;

81 assume "?S = f y";

82 thus ?thesis;

83 proof (rule equalityCE);

84 assume "y : f y";

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

86 thus ?thesis; by contradiction;

87 next;

88 assume "y ~: f y";

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

90 thus ?thesis; by contradiction;

91 qed;

92 qed;

93 qed;

94 qed;

96 text {*

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

98 this theorem automatically. The context of Isabelle's classical

99 prover contains rules for most of the constructs of HOL's set theory.

100 We must augment it with \name{equalityCE} to break up set equalities,

101 and then apply best-first search. Depth-first search would diverge,

102 but best-first search successfully navigates through the large search

103 space.

104 *};

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

107 by (best elim: equalityCE);

109 text {*

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

111 idea of how the proof actually works. There is currently no way to

112 transform internal system-level representations of Isabelle proofs

113 back into Isar text. Writing intelligible proof documents

114 really is a creative process, after all.

115 *};

117 end;