1.1 --- a/src/HOL/Isar_examples/Group.thy Thu Oct 28 19:53:24 1999 +0200
1.2 +++ b/src/HOL/Isar_examples/Group.thy Thu Oct 28 19:57:34 1999 +0200
1.3 @@ -10,10 +10,10 @@
1.4 subsection {* Groups and calculational reasoning *};
1.5
1.6 text {*
1.7 - We define an axiomatic type class of groups over signature $({\times}
1.8 - :: \alpha \To \alpha \To \alpha, \idt{one} :: \alpha, \idt{inv} ::
1.9 - \alpha \To \alpha)$. Note that the parent class $\idt{times}$ is
1.10 - provided by the basic HOL theory.
1.11 + Groups over signature $({\times} :: \alpha \To \alpha \To \alpha,
1.12 + \idt{one} :: \alpha, \idt{inv} :: \alpha \To \alpha)$ are defined as
1.13 + an axiomatic type class as follows. Note that the parent class
1.14 + $\idt{times}$ is provided by the basic HOL theory.
1.15 *};
1.16
1.17 consts
2.1 --- a/src/HOL/Isar_examples/MultisetOrder.thy Thu Oct 28 19:53:24 1999 +0200
2.2 +++ b/src/HOL/Isar_examples/MultisetOrder.thy Thu Oct 28 19:57:34 1999 +0200
2.3 @@ -3,15 +3,17 @@
2.4 Author: Markus Wenzel
2.5
2.6 Wellfoundedness proof for the multiset order.
2.7 -
2.8 -Original tactic script by Tobias Nipkow (see also
2.9 -HOL/Induct/Multiset). Pen-and-paper proof by Wilfried Buchholz.
2.10 *)
2.11
2.12 header {* Wellfoundedness of multiset ordering *};
2.13
2.14 theory MultisetOrder = Multiset:;
2.15
2.16 +text_raw {*
2.17 + \footnote{Original tactic script by Tobias Nipkow (see also
2.18 + \url{http://isabelle.in.tum.de/library/HOL/Induct/Multiset.html}),
2.19 + based on a pen-and-paper proof due to Wilfried Buchholz.}
2.20 +*};
2.21
2.22 subsection {* A technical lemma *};
2.23
3.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Thu Oct 28 19:53:24 1999 +0200
3.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Thu Oct 28 19:57:34 1999 +0200
3.3 @@ -2,18 +2,18 @@
3.4 ID: $Id$
3.5 Author: Markus Wenzel, TU Muenchen (Isar document)
3.6 Lawrence C Paulson, Cambridge University Computer Laboratory (original scripts)
3.7 -
3.8 -The Mutilated Checker Board Problem, formalized inductively.
3.9 - Originator is Max Black, according to J A Robinson.
3.10 - Popularized as the Mutilated Checkerboard Problem by J McCarthy.
3.11 -
3.12 -See also HOL/Induct/Mutil for the original Isabelle tactic scripts.
3.13 *)
3.14
3.15 header {* The Mutilated Checker Board Problem *};
3.16
3.17 theory MutilatedCheckerboard = Main:;
3.18
3.19 +text {*
3.20 + The Mutilated Checker Board Problem, formalized inductively. See
3.21 + \cite{paulson-mutilated-board} and
3.22 + \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for the
3.23 + original tactic script version.
3.24 +*};
3.25
3.26 subsection {* Tilings *};
3.27
4.1 --- a/src/HOL/Isar_examples/Summation.thy Thu Oct 28 19:53:24 1999 +0200
4.2 +++ b/src/HOL/Isar_examples/Summation.thy Thu Oct 28 19:57:34 1999 +0200
4.3 @@ -1,19 +1,38 @@
4.4 (* Title: HOL/Isar_examples/Summation.thy
4.5 ID: $Id$
4.6 Author: Markus Wenzel
4.7 -
4.8 -Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the
4.9 -original scripts). Demonstrates mathematical induction together with
4.10 -calculational proof.
4.11 *)
4.12
4.13 header {* Summing natural numbers *};
4.14
4.15 theory Summation = Main:;
4.16
4.17 +text_raw {*
4.18 + \footnote{This example is somewhat reminiscent of the
4.19 + \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
4.20 + discussed in \cite{isabelle-ref} in the context of permutative
4.21 + rewrite rules and ordered rewriting.}
4.22 +*};
4.23 +
4.24 +text {*
4.25 + Subsequently, we prove some summation laws of natural numbers
4.26 + (including odds, squares and cubes). These examples demonstrate how
4.27 + plain natural deduction (including induction) may be combined with
4.28 + calculational proof.
4.29 +*};
4.30 +
4.31
4.32 subsection {* A summation operator *};
4.33
4.34 +text {*
4.35 + The binder operator $\idt{sum} :: (\idt{nat} \To \idt{nat}) \To
4.36 + \idt{nat} \To \idt{nat}$ formalizes summation from $0$ up to $k$
4.37 + (excluding the bound).
4.38 + \[
4.39 + \sum\limits_{i < k} f(i) = \idt{sum} \ap (\lam i f \ap i) \ap k
4.40 + \]
4.41 +*};
4.42 +
4.43 consts
4.44 sum :: "[nat => nat, nat] => nat";
4.45
4.46 @@ -48,6 +67,11 @@
4.47
4.48 text_raw {* \end{comment} *};
4.49
4.50 +text {*
4.51 + The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
4.52 + 1)/2$. In order to avoid formal reasoning about division, we just
4.53 + show $2 \times \Sigma_{i < n} i = n \times (n + 1)$.
4.54 +*};
4.55
4.56 theorem sum_of_naturals:
4.57 "2 * (SUM i < n + 1. i) = n * (n + 1)"
4.58 @@ -62,6 +86,51 @@
4.59 finally; show "?P (Suc n)"; by simp;
4.60 qed;
4.61
4.62 +text {*
4.63 + The above proof is a typical instance of mathematical induction. The
4.64 + main statement is viewed as some $\var{P} \ap n$ that is split by the
4.65 + induction method into base case $\var{P} \ap 0$, and step case
4.66 + $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for any $n$.
4.67 +
4.68 + The step case is established by a short calculation in forward
4.69 + manner. Starting from the left-hand side $\var{S} \ap (n + 1)$ of
4.70 + the thesis, the final result is achieved by basic transformations
4.71 + involving arithmetic reasoning (using the Simplifier). The main
4.72 + point is where the induction hypothesis $\var{S} \ap n = n \times (n
4.73 + + 1)$ is introduced in order to replace a certain subterm. So the
4.74 + ``transitivity'' rule involved here is actual \emph{substitution}.
4.75 + Also note how the occurrence of ``\dots'' in the subsequent step
4.76 + documents the position where the right-hand side of the hypotheses
4.77 + got filled in.
4.78 +
4.79 + \medskip A further notable point here is integration of calculations
4.80 + with plain natural deduction. This works works quite well in Isar
4.81 + for two reasons.
4.82 +
4.83 + \begin{enumerate}
4.84 +
4.85 + \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
4.86 + calculational chains may be just anything. There is nothing special
4.87 + about \isakeyword{have}, so the natural deduction element
4.88 + \isakeyword{assume} works just as well.
4.89 +
4.90 + \item There are two \emph{separate} primitives for building natural
4.91 + deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
4.92 + Thus it is possible to start reasoning with new ``arbitrary, but
4.93 + fixed'' elements before bringing in the actual assumptions.
4.94 + Occasionally, natural deduction is formalized with basic context
4.95 + elements of the form $x:A$; this would rule out mixing with
4.96 + calculations as done here.
4.97 +
4.98 + \end{enumerate}
4.99 +*};
4.100 +
4.101 +text {*
4.102 + \medskip We derive further summation laws for odds, squares, cubes as
4.103 + follows. The basic technique of induction plus calculation is the
4.104 + same.
4.105 +*};
4.106 +
4.107 theorem sum_of_odds:
4.108 "(SUM i < n. 2 * i + 1) = n^2"
4.109 (is "?P n" is "?S n = _");
4.110 @@ -103,4 +172,25 @@
4.111 finally; show "?P (Suc n)"; by simp;
4.112 qed;
4.113
4.114 +text {*
4.115 + Comparing these examples with the tactic script version
4.116 + \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
4.117 + an important difference how of induction vs.\ simplification is
4.118 + applied. While \cite[\S10]{isabelle-ref} advises for these examples
4.119 + that ``induction should not be applied until the goal is in the
4.120 + simplest form'' this would be a very bad idea in our setting.
4.121 +
4.122 + Simplification normalizes all arithmetic expressions involved,
4.123 + producing huge intermediate goals. Applying induction afterwards,
4.124 + the Isar document would then have to reflect the emerging
4.125 + configuration by appropriate the sub-proofs. This would result in
4.126 + badly structured, low-level technical reasoning, without any good
4.127 + idea of the actual point.
4.128 +
4.129 + \medskip As a general rule of good proof style, automatic methods
4.130 + such as $\idt{simp}$ or $\idt{auto}$ should normally never used as
4.131 + initial proof methods, but only as terminal ones, solving certain
4.132 + goals completely.
4.133 +*};
4.134 +
4.135 end;
5.1 --- a/src/HOL/Isar_examples/W_correct.thy Thu Oct 28 19:53:24 1999 +0200
5.2 +++ b/src/HOL/Isar_examples/W_correct.thy Thu Oct 28 19:57:34 1999 +0200
5.3 @@ -3,13 +3,17 @@
5.4 Author: Markus Wenzel, TU Muenchen
5.5
5.6 Correctness of Milner's type inference algorithm W (let-free version).
5.7 -Based upon HOL/W0 by Dieter Nazareth and Tobias Nipkow.
5.8 *)
5.9
5.10 header {* Milner's type inference algorithm~W (let-free version) *};
5.11
5.12 theory W_correct = Main + Type:;
5.13
5.14 +text_raw {*
5.15 + \footnote{Based upon \url{http://isabelle.in.tum.de/library/HOL/W0}
5.16 + by Dieter Nazareth and Tobias Nipkow.}
5.17 +*};
5.18 +
5.19
5.20 subsection "Mini ML with type inference rules";
5.21
6.1 --- a/src/HOL/Isar_examples/document/root.bib Thu Oct 28 19:53:24 1999 +0200
6.2 +++ b/src/HOL/Isar_examples/document/root.bib Thu Oct 28 19:57:34 1999 +0200
6.3 @@ -5,6 +5,11 @@
6.4 @string{TUM="TU Munich"}
6.5
6.6
6.7 +@InProceedings{Wenzel:1999:TPHOL,
6.8 + author = {Markus Wenzel},
6.9 + title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
6.10 + crossref = {tphols99}}
6.11 +
6.12 @Book{davey-priestley,
6.13 author = {B. A. Davey and H. A. Priestley},
6.14 title = {Introduction to Lattices and Order},
6.15 @@ -24,13 +29,22 @@
6.16
6.17 @manual{isabelle-isar-ref,
6.18 author = {Markus Wenzel},
6.19 - title = {The {Isabelle Isar} Reference Manual},
6.20 + title = {The {Isabelle/Isar} Reference Manual},
6.21 institution = TUM}
6.22
6.23 -@InProceedings{Wenzel:1999:TPHOL,
6.24 - author = {Markus Wenzel},
6.25 - title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
6.26 - crossref = {tphols99}}
6.27 +@manual{isabelle-ref,
6.28 + author = {Lawrence C. Paulson},
6.29 + title = {The {Isabelle} Reference Manual},
6.30 + institution = CUCL}
6.31 +
6.32 +@TechReport{paulson-mutilated-board,
6.33 + author = {Lawrence C. Paulson},
6.34 + title = {A Simple Formalization and Proof for the Mutilated Chess Board},
6.35 + institution = CUCL,
6.36 + year = 1996,
6.37 + number = 394,
6.38 + note = {\url{http://www.ftp.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.pdf}}
6.39 +}
6.40
6.41 @Proceedings{tphols99,
6.42 title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
7.1 --- a/src/HOL/Isar_examples/document/style.tex Thu Oct 28 19:53:24 1999 +0200
7.2 +++ b/src/HOL/Isar_examples/document/style.tex Thu Oct 28 19:57:34 1999 +0200
7.3 @@ -22,6 +22,7 @@
7.4 \newcommand{\impl}{\rightarrow}
7.5 \newcommand{\conj}{\land}
7.6 \newcommand{\disj}{\lor}
7.7 +\newcommand{\Impl}{\Longrightarrow}
7.8
7.9 %%% Local Variables:
7.10 %%% mode: latex