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

src/HOL/Isar_examples/Cantor.thy

changeset 6744 | 9727e83f0578 |

parent 6517 | 239c0eff6ce8 |

child 6746 | cf6ad8d22793 |

--- a/src/HOL/Isar_examples/Cantor.thy Thu May 27 20:47:30 1999 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Thu May 27 20:49:10 1999 +0200 @@ -11,7 +11,7 @@ section "Example: Cantor's Theorem"; -text {| +text {* Cantor's Theorem states that every set has more subsets than it has elements. It has become a favourite example in higher-order logic since it is so easily expressed: @{display term[show_types] "ALL f @@ -23,14 +23,14 @@ The Isabelle/Isar proofs below use HOL's set theory, with the type @{type "'a set"} and the operator @{term range}. -|}; +*}; -text {| +text {* We first consider a rather verbose version of the proof, with the reasoning expressed quite naively. We only make use of the pure core of the Isar proof language. -|}; +*}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; proof; @@ -59,11 +59,11 @@ qed; -text {| +text {* The following version essentially does the same reasoning, only that it is expressed more neatly, with some derived Isar language elements involved. -|}; +*}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; proof; @@ -90,7 +90,7 @@ qed; -text {| +text {* How much creativity is required? As it happens, Isabelle can prove this theorem automatically. The default classical set contains rules for most of the constructs of HOL's set theory. We must @@ -98,18 +98,18 @@ then apply best-first search. Depth-first search would diverge, but best-first search successfully navigates through the large search space. -|}; +*}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; by (best elim: equalityCE); -text {| +text {* While this establishes the same theorem internally, we do not get any idea of how the proof actually works. There is currently no way to transform internal system-level representations of Isabelle proofs back into Isar documents. Writing Isabelle/Isar proof documents actually \emph{is} a creative process. -|}; +*}; end;