--- a/src/HOL/Isar_examples/Group.thy Thu Oct 28 19:53:24 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy Thu Oct 28 19:57:34 1999 +0200
@@ -10,10 +10,10 @@
subsection {* Groups and calculational reasoning *};
text {*
- We define an axiomatic type class of groups over signature $({\times}
- :: \alpha \To \alpha \To \alpha, \idt{one} :: \alpha, \idt{inv} ::
- \alpha \To \alpha)$. Note that the parent class $\idt{times}$ is
- provided by the basic HOL theory.
+ Groups over signature $({\times} :: \alpha \To \alpha \To \alpha,
+ \idt{one} :: \alpha, \idt{inv} :: \alpha \To \alpha)$ are defined as
+ an axiomatic type class as follows. Note that the parent class
+ $\idt{times}$ is provided by the basic HOL theory.
*};
consts
--- a/src/HOL/Isar_examples/MultisetOrder.thy Thu Oct 28 19:53:24 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy Thu Oct 28 19:57:34 1999 +0200
@@ -3,15 +3,17 @@
Author: Markus Wenzel
Wellfoundedness proof for the multiset order.
-
-Original tactic script by Tobias Nipkow (see also
-HOL/Induct/Multiset). Pen-and-paper proof by Wilfried Buchholz.
*)
header {* Wellfoundedness of multiset ordering *};
theory MultisetOrder = Multiset:;
+text_raw {*
+ \footnote{Original tactic script by Tobias Nipkow (see also
+ \url{http://isabelle.in.tum.de/library/HOL/Induct/Multiset.html}),
+ based on a pen-and-paper proof due to Wilfried Buchholz.}
+*};
subsection {* A technical lemma *};
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Thu Oct 28 19:53:24 1999 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Thu Oct 28 19:57:34 1999 +0200
@@ -2,18 +2,18 @@
ID: $Id$
Author: Markus Wenzel, TU Muenchen (Isar document)
Lawrence C Paulson, Cambridge University Computer Laboratory (original scripts)
-
-The Mutilated Checker Board Problem, formalized inductively.
- Originator is Max Black, according to J A Robinson.
- Popularized as the Mutilated Checkerboard Problem by J McCarthy.
-
-See also HOL/Induct/Mutil for the original Isabelle tactic scripts.
*)
header {* The Mutilated Checker Board Problem *};
theory MutilatedCheckerboard = Main:;
+text {*
+ The Mutilated Checker Board Problem, formalized inductively. See
+ \cite{paulson-mutilated-board} and
+ \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for the
+ original tactic script version.
+*};
subsection {* Tilings *};
--- a/src/HOL/Isar_examples/Summation.thy Thu Oct 28 19:53:24 1999 +0200
+++ b/src/HOL/Isar_examples/Summation.thy Thu Oct 28 19:57:34 1999 +0200
@@ -1,19 +1,38 @@
(* Title: HOL/Isar_examples/Summation.thy
ID: $Id$
Author: Markus Wenzel
-
-Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the
-original scripts). Demonstrates mathematical induction together with
-calculational proof.
*)
header {* Summing natural numbers *};
theory Summation = Main:;
+text_raw {*
+ \footnote{This example is somewhat reminiscent of the
+ \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
+ discussed in \cite{isabelle-ref} in the context of permutative
+ rewrite rules and ordered rewriting.}
+*};
+
+text {*
+ Subsequently, we prove some summation laws of natural numbers
+ (including odds, squares and cubes). These examples demonstrate how
+ plain natural deduction (including induction) may be combined with
+ calculational proof.
+*};
+
subsection {* A summation operator *};
+text {*
+ The binder operator $\idt{sum} :: (\idt{nat} \To \idt{nat}) \To
+ \idt{nat} \To \idt{nat}$ formalizes summation from $0$ up to $k$
+ (excluding the bound).
+ \[
+ \sum\limits_{i < k} f(i) = \idt{sum} \ap (\lam i f \ap i) \ap k
+ \]
+*};
+
consts
sum :: "[nat => nat, nat] => nat";
@@ -48,6 +67,11 @@
text_raw {* \end{comment} *};
+text {*
+ The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
+ 1)/2$. In order to avoid formal reasoning about division, we just
+ show $2 \times \Sigma_{i < n} i = n \times (n + 1)$.
+*};
theorem sum_of_naturals:
"2 * (SUM i < n + 1. i) = n * (n + 1)"
@@ -62,6 +86,51 @@
finally; show "?P (Suc n)"; by simp;
qed;
+text {*
+ The above proof is a typical instance of mathematical induction. The
+ main statement is viewed as some $\var{P} \ap n$ that is split by the
+ induction method into base case $\var{P} \ap 0$, and step case
+ $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for any $n$.
+
+ The step case is established by a short calculation in forward
+ manner. Starting from the left-hand side $\var{S} \ap (n + 1)$ of
+ the thesis, the final result is achieved by basic transformations
+ involving arithmetic reasoning (using the Simplifier). The main
+ point is where the induction hypothesis $\var{S} \ap n = n \times (n
+ + 1)$ is introduced in order to replace a certain subterm. So the
+ ``transitivity'' rule involved here is actual \emph{substitution}.
+ Also note how the occurrence of ``\dots'' in the subsequent step
+ documents the position where the right-hand side of the hypotheses
+ got filled in.
+
+ \medskip A further notable point here is integration of calculations
+ with plain natural deduction. This works works quite well in Isar
+ for two reasons.
+
+ \begin{enumerate}
+
+ \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
+ calculational chains may be just anything. There is nothing special
+ about \isakeyword{have}, so the natural deduction element
+ \isakeyword{assume} works just as well.
+
+ \item There are two \emph{separate} primitives for building natural
+ deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
+ Thus it is possible to start reasoning with new ``arbitrary, but
+ fixed'' elements before bringing in the actual assumptions.
+ Occasionally, natural deduction is formalized with basic context
+ elements of the form $x:A$; this would rule out mixing with
+ calculations as done here.
+
+ \end{enumerate}
+*};
+
+text {*
+ \medskip We derive further summation laws for odds, squares, cubes as
+ follows. The basic technique of induction plus calculation is the
+ same.
+*};
+
theorem sum_of_odds:
"(SUM i < n. 2 * i + 1) = n^2"
(is "?P n" is "?S n = _");
@@ -103,4 +172,25 @@
finally; show "?P (Suc n)"; by simp;
qed;
+text {*
+ Comparing these examples with the tactic script version
+ \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
+ an important difference how of induction vs.\ simplification is
+ applied. While \cite[\S10]{isabelle-ref} advises for these examples
+ that ``induction should not be applied until the goal is in the
+ simplest form'' this would be a very bad idea in our setting.
+
+ Simplification normalizes all arithmetic expressions involved,
+ producing huge intermediate goals. Applying induction afterwards,
+ the Isar document would then have to reflect the emerging
+ configuration by appropriate the sub-proofs. This would result in
+ badly structured, low-level technical reasoning, without any good
+ idea of the actual point.
+
+ \medskip As a general rule of good proof style, automatic methods
+ such as $\idt{simp}$ or $\idt{auto}$ should normally never used as
+ initial proof methods, but only as terminal ones, solving certain
+ goals completely.
+*};
+
end;
--- a/src/HOL/Isar_examples/W_correct.thy Thu Oct 28 19:53:24 1999 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy Thu Oct 28 19:57:34 1999 +0200
@@ -3,13 +3,17 @@
Author: Markus Wenzel, TU Muenchen
Correctness of Milner's type inference algorithm W (let-free version).
-Based upon HOL/W0 by Dieter Nazareth and Tobias Nipkow.
*)
header {* Milner's type inference algorithm~W (let-free version) *};
theory W_correct = Main + Type:;
+text_raw {*
+ \footnote{Based upon \url{http://isabelle.in.tum.de/library/HOL/W0}
+ by Dieter Nazareth and Tobias Nipkow.}
+*};
+
subsection "Mini ML with type inference rules";
--- a/src/HOL/Isar_examples/document/root.bib Thu Oct 28 19:53:24 1999 +0200
+++ b/src/HOL/Isar_examples/document/root.bib Thu Oct 28 19:57:34 1999 +0200
@@ -5,6 +5,11 @@
@string{TUM="TU Munich"}
+@InProceedings{Wenzel:1999:TPHOL,
+ author = {Markus Wenzel},
+ title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
+ crossref = {tphols99}}
+
@Book{davey-priestley,
author = {B. A. Davey and H. A. Priestley},
title = {Introduction to Lattices and Order},
@@ -24,13 +29,22 @@
@manual{isabelle-isar-ref,
author = {Markus Wenzel},
- title = {The {Isabelle Isar} Reference Manual},
+ title = {The {Isabelle/Isar} Reference Manual},
institution = TUM}
-@InProceedings{Wenzel:1999:TPHOL,
- author = {Markus Wenzel},
- title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
- crossref = {tphols99}}
+@manual{isabelle-ref,
+ author = {Lawrence C. Paulson},
+ title = {The {Isabelle} Reference Manual},
+ institution = CUCL}
+
+@TechReport{paulson-mutilated-board,
+ author = {Lawrence C. Paulson},
+ title = {A Simple Formalization and Proof for the Mutilated Chess Board},
+ institution = CUCL,
+ year = 1996,
+ number = 394,
+ note = {\url{http://www.ftp.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.pdf}}
+}
@Proceedings{tphols99,
title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
--- a/src/HOL/Isar_examples/document/style.tex Thu Oct 28 19:53:24 1999 +0200
+++ b/src/HOL/Isar_examples/document/style.tex Thu Oct 28 19:57:34 1999 +0200
@@ -22,6 +22,7 @@
\newcommand{\impl}{\rightarrow}
\newcommand{\conj}{\land}
\newcommand{\disj}{\lor}
+\newcommand{\Impl}{\Longrightarrow}
%%% Local Variables:
%%% mode: latex