# HG changeset patch # User wenzelm # Date 941133454 -7200 # Node ID 964b65b4e4331b29d4c219fbd39560f5d1b23a4e # Parent 942274e0f7a876d64d3f87f9ca1b8941cbef76bd improved presentation; diff -r 942274e0f7a8 -r 964b65b4e433 src/HOL/Isar_examples/Group.thy --- 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 diff -r 942274e0f7a8 -r 964b65b4e433 src/HOL/Isar_examples/MultisetOrder.thy --- 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 *}; diff -r 942274e0f7a8 -r 964b65b4e433 src/HOL/Isar_examples/MutilatedCheckerboard.thy --- 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 *}; diff -r 942274e0f7a8 -r 964b65b4e433 src/HOL/Isar_examples/Summation.thy --- 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; diff -r 942274e0f7a8 -r 964b65b4e433 src/HOL/Isar_examples/W_correct.thy --- 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"; diff -r 942274e0f7a8 -r 964b65b4e433 src/HOL/Isar_examples/document/root.bib --- 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}, diff -r 942274e0f7a8 -r 964b65b4e433 src/HOL/Isar_examples/document/style.tex --- 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