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

src/HOL/Isar_examples/Cantor.thy

author | oheimb |

Wed Jan 31 10:15:55 2001 +0100 (2001-01-31) | |

changeset 11008 | f7333f055ef6 |

parent 10007 | 64bf7da1994a |

child 12388 | c845fec1ac94 |

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

improved theory reference in comment

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 using best-first search. Depth-first

99 search would diverge, but best-first search successfully navigates

100 through the large search space. The context of Isabelle's classical

101 prover contains rules for the relevant constructs of HOL's set

102 theory.

103 *}

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

106 by best

108 text {*

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

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

111 transform internal system-level representations of Isabelle proofs

112 back into Isar text. Writing intelligible proof documents

113 really is a creative process, after all.

114 *}

116 end