author wenzelm Thu, 28 Oct 1999 19:57:34 +0200 changeset 7968 964b65b4e433 parent 7967 942274e0f7a8 child 7969 7a20317850ab
improved presentation;
 src/HOL/Isar_examples/Group.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/MultisetOrder.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/MutilatedCheckerboard.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Summation.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/W_correct.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/document/root.bib file | annotate | diff | comparison | revisions src/HOL/Isar_examples/document/style.tex file | annotate | diff | comparison | revisions
--- 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.
-
-HOL/Induct/Multiset).  Pen-and-paper proof by Wilfried Buchholz.
*)

header {* Wellfoundedness of multiset ordering *};

theory MultisetOrder = Multiset:;

+text_raw {*
+ \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.
-
*)

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