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

src/HOL/Isar_examples/Cantor.thy

changeset 7982 | d534b897ce39 |

parent 7955 | f30e08579481 |

child 9474 | b0ce3b7c9c26 |

1.1 --- a/src/HOL/Isar_examples/Cantor.thy Sat Oct 30 20:13:16 1999 +0200 1.2 +++ b/src/HOL/Isar_examples/Cantor.thy Sat Oct 30 20:20:48 1999 +0200 1.3 @@ -30,7 +30,7 @@ 1.4 with the innermost reasoning expressed quite naively. 1.5 *}; 1.6 1.7 -theorem "EX S. S ~: range(f :: 'a => 'a set)"; 1.8 +theorem "EX S. S ~: range (f :: 'a => 'a set)"; 1.9 proof; 1.10 let ?S = "{x. x ~: f x}"; 1.11 show "?S ~: range f"; 1.12 @@ -69,7 +69,7 @@ 1.13 introduced \emph{before} its corresponding \isacommand{show}.} 1.14 *}; 1.15 1.16 -theorem "EX S. S ~: range(f :: 'a => 'a set)"; 1.17 +theorem "EX S. S ~: range (f :: 'a => 'a set)"; 1.18 proof; 1.19 let ?S = "{x. x ~: f x}"; 1.20 show "?S ~: range f"; 1.21 @@ -95,22 +95,22 @@ 1.22 1.23 text {* 1.24 How much creativity is required? As it happens, Isabelle can prove 1.25 - this theorem automatically. The default context of the Isabelle's 1.26 - classical prover contains rules for most of the constructs of HOL's 1.27 - set theory. We must augment it with \name{equalityCE} to break up 1.28 - set equalities, and then apply best-first search. Depth-first search 1.29 - would diverge, but best-first search successfully navigates through 1.30 - the large search space. 1.31 + this theorem automatically. The context of Isabelle's classical 1.32 + prover contains rules for most of the constructs of HOL's set theory. 1.33 + We must augment it with \name{equalityCE} to break up set equalities, 1.34 + and then apply best-first search. Depth-first search would diverge, 1.35 + but best-first search successfully navigates through the large search 1.36 + space. 1.37 *}; 1.38 1.39 -theorem "EX S. S ~: range(f :: 'a => 'a set)"; 1.40 +theorem "EX S. S ~: range (f :: 'a => 'a set)"; 1.41 by (best elim: equalityCE); 1.42 1.43 text {* 1.44 While this establishes the same theorem internally, we do not get any 1.45 idea of how the proof actually works. There is currently no way to 1.46 transform internal system-level representations of Isabelle proofs 1.47 - back into Isar documents. Writing intelligible proof documents 1.48 + back into Isar text. Writing intelligible proof documents 1.49 really is a creative process, after all. 1.50 *}; 1.51