summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Isar_examples/Cantor.thy

changeset 7982 | d534b897ce39 |

parent 7955 | f30e08579481 |

child 9474 | b0ce3b7c9c26 |

equal
deleted
inserted
replaced

7981:5120a2a15d06 | 7982:d534b897ce39 |
---|---|

28 |
28 |

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

30 with the innermost reasoning expressed quite naively. |
30 with the innermost reasoning expressed quite naively. |

31 *}; |
31 *}; |

32 |
32 |

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

34 proof; |
34 proof; |

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

36 show "?S ~: range f"; |
36 show "?S ~: range f"; |

37 proof; |
37 proof; |

38 assume "?S : range f"; |
38 assume "?S : range f"; |

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

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

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

70 *}; |
70 *}; |

71 |
71 |

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

73 proof; |
73 proof; |

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

75 show "?S ~: range f"; |
75 show "?S ~: range f"; |

76 proof; |
76 proof; |

77 assume "?S : range f"; |
77 assume "?S : range f"; |

93 qed; |
93 qed; |

94 qed; |
94 qed; |

95 |
95 |

96 text {* |
96 text {* |

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

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

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

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

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

102 would diverge, but best-first search successfully navigates through |
102 but best-first search successfully navigates through the large search |

103 the large search space. |
103 space. |

104 *}; |
104 *}; |

105 |
105 |

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

107 by (best elim: equalityCE); |
107 by (best elim: equalityCE); |

108 |
108 |

109 text {* |
109 text {* |

110 While this establishes the same theorem internally, we do not get any |
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 |
111 idea of how the proof actually works. There is currently no way to |

112 transform internal system-level representations of Isabelle proofs |
112 transform internal system-level representations of Isabelle proofs |

113 back into Isar documents. Writing intelligible proof documents |
113 back into Isar text. Writing intelligible proof documents |

114 really is a creative process, after all. |
114 really is a creative process, after all. |

115 *}; |
115 *}; |

116 |
116 |

117 end; |
117 end; |