author nipkow Tue, 13 Nov 2007 13:51:12 +0100 changeset 25427 8ba39d2d9d0b parent 25426 7ab693b8ee87 child 25428 95c0b4dc600b
updated
--- a/doc-src/IsarOverview/Isar/Induction.thy	Tue Nov 13 11:04:30 2007 +0100
+++ b/doc-src/IsarOverview/Isar/Induction.thy	Tue Nov 13 13:51:12 2007 +0100
@@ -81,10 +81,12 @@

We start with an inductive proof where both cases are proved automatically: *}
lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)"
-by (induct n, simp_all)
+by (induct n) simp_all

text{*\noindent The constraint @{text"::nat"} is needed because all of
+This proof also demonstrates that \isakeyword{by} can take two arguments,
+one to start and one to finish the proof --- the latter is optional.

If we want to expose more of the structure of the
proof, we can use pattern matching to avoid having to repeat the goal
@@ -136,12 +138,10 @@
proof and the quantifiers should not clutter the original claim. This
is how the quantification step can be combined with induction: *}
lemma "itrev xs ys = rev xs @ ys"
-by (induct xs arbitrary: ys) auto
+by (induct xs arbitrary: ys) simp_all
text{*\noindent The annotation @{text"arbitrary:"}~\emph{vars}
universally quantifies all \emph{vars} before the induction.  Hence
they can be replaced by \emph{arbitrary} values in the proof.
-This proof also demonstrates that \isakeyword{by} can take two arguments,
-one to start and one to finish the proof --- the latter is optional.

The nice thing about generalization via @{text"arbitrary:"} is that in
the induction step the claim is available in unquantified form but
@@ -159,7 +159,7 @@
*}

lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
-by (induct xs) auto
+by (induct xs) simp_all

text{*\noindent This is an improvement over that style the
@@ -178,7 +178,7 @@
thus ?thesis ..
next
case (Cons x xs')
-    with Asm(2) have "map f xs' = map f ys" by auto
+    with Asm(2) have "map f xs' = map f ys" by simp
from Asm(1)[OF this] xs = x#xs' show ?thesis by simp
qed
qed
--- a/doc-src/IsarOverview/Isar/Logic.thy	Tue Nov 13 11:04:30 2007 +0100
+++ b/doc-src/IsarOverview/Isar/Logic.thy	Tue Nov 13 13:51:12 2007 +0100
@@ -579,11 +579,11 @@
conclusion of some pending goal but some independent claim.

The general idea demonstrated in this subsection is very
-important in Isar and distinguishes it from tactic-style proofs:
+important in Isar and distinguishes it from \isa{apply}-style proofs:
\begin{quote}\em
Do not manipulate the proof state into a particular form by applying
-tactics but state the desired form explicitly and let the tactic verify
-that from this form the original goal follows.
+proof methods but state the desired form explicitly and let the proof
+methods verify that from this form the original goal follows.
\end{quote}
This yields more readable and also more robust proofs.

@@ -692,9 +692,8 @@

subsubsection{*Combining proof styles*}

-text{* Finally, whole scripts'' (tactic-based proofs in the style of
-\cite{LNCS2283}) may appear in the leaves of the proof tree, although this is
-best avoided.  Here is a contrived example: *}
+text{* Finally, whole \isa{apply}-scripts may appear in the leaves of the
+proof tree, although this is best avoided.  Here is a contrived example: *}

lemma "A \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B"
proof
@@ -710,7 +709,7 @@
text{*\noindent You may need to resort to this technique if an
automatic step fails to prove the desired proposition.

-When converting a proof from tactic-style into Isar you can proceed
+When converting a proof from \isa{apply}-style into Isar you can proceed
in a top-down manner: parts of the proof can be left in script form
while the outer structure is already expressed in Isar. *}

--- a/doc-src/IsarOverview/Isar/document/Induction.tex	Tue Nov 13 11:04:30 2007 +0100
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Tue Nov 13 13:51:12 2007 +0100
@@ -180,7 +180,7 @@
%
\isatagproof
\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
+\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all%
\endisatagproof
{\isafoldproof}%
%
@@ -191,6 +191,8 @@
\begin{isamarkuptext}%
\noindent The constraint \isa{{\isacharcolon}{\isacharcolon}nat} is needed because all of
+This proof also demonstrates that \isakeyword{by} can take two arguments,
+one to start and one to finish the proof --- the latter is optional.

If we want to expose more of the structure of the
proof, we can use pattern matching to avoid having to repeat the goal
@@ -327,7 +329,7 @@
%
\isatagproof
\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs\ arbitrary{\isacharcolon}\ ys{\isacharparenright}\ auto%
+\ {\isacharparenleft}induct\ xs\ arbitrary{\isacharcolon}\ ys{\isacharparenright}\ simp{\isacharunderscore}all%
\endisatagproof
{\isafoldproof}%
%
@@ -339,8 +341,6 @@
\noindent The annotation \isa{arbitrary{\isacharcolon}}~\emph{vars}
universally quantifies all \emph{vars} before the induction.  Hence
they can be replaced by \emph{arbitrary} values in the proof.
-This proof also demonstrates that \isakeyword{by} can take two arguments,
-one to start and one to finish the proof --- the latter is optional.

The nice thing about generalization via \isa{arbitrary{\isacharcolon}} is that in
the induction step the claim is available in unquantified form but
@@ -366,7 +366,7 @@
%
\isatagproof
\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs{\isacharparenright}\ auto%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
\endisatagproof
{\isafoldproof}%
%
@@ -419,7 +419,7 @@
\ \ \ \ \isacommand{with}\isamarkupfalse%
\ {\isachardoublequoteopen}map\ f\ xs{\isacharprime}\ {\isacharequal}\ map\ f\ ys{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ auto\isanewline
+\ simp\isanewline
\ \ \ \ \isacommand{from}\isamarkupfalse%
\ Asm{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}OF\ this{\isacharbrackright}\ {\isacharbackquoteopen}xs\ {\isacharequal}\ x{\isacharhash}xs{\isacharprime}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
--- a/doc-src/IsarOverview/Isar/document/Logic.tex	Tue Nov 13 11:04:30 2007 +0100
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex	Tue Nov 13 13:51:12 2007 +0100
@@ -1363,11 +1363,11 @@
conclusion of some pending goal but some independent claim.

The general idea demonstrated in this subsection is very
-important in Isar and distinguishes it from tactic-style proofs:
+important in Isar and distinguishes it from \isa{apply}-style proofs:
\begin{quote}\em
Do not manipulate the proof state into a particular form by applying
-tactics but state the desired form explicitly and let the tactic verify
-that from this form the original goal follows.
+proof methods but state the desired form explicitly and let the proof
+methods verify that from this form the original goal follows.
\end{quote}
This yields more readable and also more robust proofs.

@@ -1627,9 +1627,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Finally, whole scripts'' (tactic-based proofs in the style of
-\cite{LNCS2283}) may appear in the leaves of the proof tree, although this is
-best avoided.  Here is a contrived example:%
+Finally, whole \isa{apply}-scripts may appear in the leaves of the
+proof tree, although this is best avoided.  Here is a contrived example:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
@@ -1669,7 +1668,7 @@
\noindent You may need to resort to this technique if an
automatic step fails to prove the desired proposition.

-When converting a proof from tactic-style into Isar you can proceed
+When converting a proof from \isa{apply}-style into Isar you can proceed
in a top-down manner: parts of the proof can be left in script form
while the outer structure is already expressed in Isar.%
\end{isamarkuptext}%
--- a/doc-src/IsarOverview/Isar/document/intro.tex	Tue Nov 13 11:04:30 2007 +0100
+++ b/doc-src/IsarOverview/Isar/document/intro.tex	Tue Nov 13 13:51:12 2007 +0100
@@ -1,57 +1,11 @@
\section{Introduction}

-Isabelle is a generic proof assistant.  Isar is an extension of
-Isabelle with structured proofs in a stylised language of mathematics.
-These proofs are readable for both a human and a machine.
-Isabelle/HOL~\cite{LNCS2283} is a specialisation of Isabelle with
-higher-order logic (HOL). This paper is a compact introduction to
-structured proofs in Isar/HOL, an extension of Isabelle/HOL. We
-intentionally do not present the full language but concentrate on the
-essentials. Neither do we give a formal semantics of Isar. Instead we
-introduce Isar by example. We believe that the language speaks for
-itself'' in the same way that traditional mathematical proofs do,
-which are also introduced by example rather than by teaching students
-logic first. A detailed exposition of Isar can be found in Markus
-Wenzel's PhD thesis~\cite{Wenzel-PhD} (which also discusses related
-work) and the Isar reference manual~\cite{Isar-Ref-Man}.
-
-\subsection{Background}
-
-Interactive theorem proving has been dominated by a model of proof
-that goes back to the LCF system~\cite{LCF}: a proof is a more or less
-structured sequence of commands that manipulate an implicit proof
-state. Thus the proof text is only suitable for the machine; for a
-human, the proof only comes alive when he can see the state changes
-caused by the stepwise execution of the commands. Such proofs are like
-uncommented assembly language programs. We call them
-\emph{tactic-style} proofs because LCF proof commands were called
-tactics.
-
-A radically different approach was taken by the Mizar
-system~\cite{Rudnicki92} where proofs are written in a stylised language akin
-to that used in ordinary mathematics texts. The most important argument in
-favour of a mathematics-like proof language is communication: as soon as not
-just the theorem but also the proof becomes an object of interest, it should
-be readable.  From a system development point of view there is a second
-important argument against tactic-style proofs: they are much harder to
-maintain when the system is modified.
-%The reason is as follows. Since it is
-%usually quite unclear what exactly is proved at some point in the middle of a
-%command sequence, updating a failed proof often requires executing the proof
-%up to the point of failure using the old version of the system.  In contrast,
-%mathematics-like proofs contain enough information to tell you what is proved
-%at any point.
-
-For these reasons the Isabelle system, originally firmly in the
-LCF-tradition, was extended with a language for writing structured
-proofs in a mathematics-like style. As the name already indicates,
-Isar was certainly inspired by Mizar. However, there are many
-differences. For a start, Isar is generic: only a few of the language
-constructs described below are specific to HOL; many are generic and
-thus available for any logic defined in Isabelle, e.g.\ ZF.
-Furthermore, we have Isabelle's powerful automatic proof procedures at
-our disposal.  A closer comparison of Isar and Mizar can be found
-elsewhere~\cite{WenzelW-JAR}.
+This is a tutorial introduction to structured proofs in Isabelle/HOL.
+It introduces the core of the proof language Isar by example. Isar is
+an extension of the \isa{apply}-style proofs introduced in the
+Isabelle/HOL tutorial~\cite{LNCS2283} with structured proofs in a
+stylised language of mathematics.  These proofs are readable for both
+human and machine.

\subsection{A first glimpse of Isar}
Below you find a simplified grammar for Isar proofs.
@@ -64,7 +18,7 @@
&$\mid$& \isakeyword{by} \emph{method}\\[1ex]
\emph{statement} &::= & \isakeyword{fix} \emph{variables} \\
&$\mid$& \isakeyword{assume} \emph{propositions} \\
-             &$\mid$& (\isakeyword{from} \emph{facts})$^?$
+             &$\mid$& (\isakeyword{from} \emph{fact}*)$^?$
(\isakeyword{show} $\mid$ \isakeyword{have})
\emph{propositions} \emph{proof} \\[1ex]
\emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string} \\[1ex]
@@ -73,8 +27,7 @@
\end{center}
A proof can be either compound (\isakeyword{proof} --
\isakeyword{qed}) or atomic (\isakeyword{by}). A \emph{method} is a
-proof method (tactic) offered by the underlying theorem prover.
-Thus this grammar is generic both w.r.t.\ the logic and the theorem prover.
+proof method.

This is a typical proof skeleton:
\begin{center}
@@ -94,11 +47,33 @@
do not contribute to the theorem being proved. In contrast,
\isakeyword{show} establishes the conclusion of the theorem.

-\subsection{Bits of Isabelle}
+\subsection{Background}
+
+Interactive theorem proving has been dominated by a model of proof
+that goes back to the LCF system~\cite{LCF}: a proof is a more or less
+structured sequence of commands that manipulate an implicit proof
+state. Thus the proof text is only suitable for the machine; for a
+human, the proof only comes alive when he can see the state changes
+caused by the stepwise execution of the commands. Such proofs are like
+uncommented assembly language programs. Their Isabelle incarnation are
+sequences of \isa{apply}-commands.

-We recall some basic notions and notation from Isabelle. For more
-details and for instructions how to run examples see
-elsewhere~\cite{LNCS2283}.
+In contrast there is the model of a mathematics-like proof language
+pioneered in the Mizar system~\cite{Rudnicki92} and followed by
+Isar~\cite{WenzelW-JAR}.
+The most important arguments in favour of this style are
+\emph{communication} and \emph{maintainance}: structured proofs are
+immensly more readable and maintainable than \isa{apply}-scripts.
+
+For reading this tutorial you should be familiar with natural
+deduction and the basics of Isabelle/HOL~\cite{LNCS2283} although we
+summarize the most important aspects of Isabelle below.  The
+definitive Isar reference is its manual~\cite{Isar-Ref-Man}. For an
+example-based account of Isar's support for reasoning by chains of
+(in)equations see~\cite{BauerW-TPHOLs01}.
+
+
+\subsection{Bits of Isabelle}

Isabelle's meta-logic comes with a type of \emph{propositions} with
implication $\Longrightarrow$ and a universal quantifier $\bigwedge$ for expressing
@@ -128,33 +103,25 @@
rule), \isa{simp} (for simplification) and \isa{blast} (for predicate
calculus reasoning).

-\subsection{Overview of the paper}
-
-The rest of the paper is divided into two parts.
-Section~\ref{sec:Logic} introduces proofs in pure logic based on
-natural deduction. Section~\ref{sec:Induct} is dedicated to induction,
-the key reasoning principle for computer science applications.
-
-There are two further areas where Isar provides specific support, but
-which we do not document here. Reasoning by chains of (in)equations is
-axiomatically defined structures by means of so called locales'' was
-first described in \cite{KWP-TPHOLs99} but has evolved much since
-then.

-Finally, a word of warning for potential writers of Isar proofs.  It
-has always been easier to write obscure rather than readable texts.
-Similarly, tactic-style proofs are often (though by no means always!)
-easier to write than readable ones: structure does not emerge
-automatically but needs to be understood and imposed. If the precise
-structure of the proof is unclear at beginning, it can be useful to
-start in a tactic-based style for exploratory purposes until one has
-found a proof which can be converted into a structured text in a
-second step.
-% Top down conversion is possible because Isar
-%allows tactic-style proofs as components of structured ones.
+A word of warning for potential writers of Isar proofs.  It
+is easier to write obscure rather than readable texts.  Similarly,
+\isa{apply}-style proofs are sometimes easier to write than readable
+ones: structure does not emerge automatically but needs to be
+understood and imposed. If the precise structure of the proof is
+unclear at beginning, it can be useful to start with \isa{apply} for
+exploratory purposes until one has found a proof which can be
+converted into a structured text in a second step. Top down conversion
+is possible because Isar allows \isa{apply}-style proofs as components
+of structured ones.

-%Do not be mislead by the simplicity of the formulae being proved,
-%especially in the beginning. Isar has been used very successfully in
-%large applications, for example the formalisation of Java, in
-%particular the verification of the bytecode verifier~\cite{KleinN-TCS}.
+Finally, do not be mislead by the simplicity of the formulae being proved,
+especially in the beginning. Isar has been used very successfully in
+large applications, for example the formalisation of Java
+dialects~\cite{KleinN-TOPLAS}.
+\medskip
+
+The rest of this tutorial is divided into two parts.
+Section~\ref{sec:Logic} introduces proofs in pure logic based on
+natural deduction. Section~\ref{sec:Induct} is dedicated to induction.
--- a/doc-src/IsarOverview/Isar/document/root.bib	Tue Nov 13 11:04:30 2007 +0100
+++ b/doc-src/IsarOverview/Isar/document/root.bib	Tue Nov 13 13:51:12 2007 +0100
@@ -13,22 +13,15 @@
title="Edinburgh {LCF}: a Mechanised Logic of Computation",
publisher=Springer,series=LNCS,volume=78,year=1979}

-@InProceedings{KWP-TPHOLs99,
-author={Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson},
-title={Locales: A Sectioning Concept for {Isabelle}},
-booktitle={Theorem Proving in Higher Order Logics, TPHOLs'99},
-editor={Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Thery},
-year=1999,publisher=Springer,series=LNCS,volume=1690,pages="149--165"}
-
@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
publisher=Springer,series=LNCS,volume=2283,year=2002,
note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}

-@article{KleinN-TCS,author={Gerwin Klein and Tobias Nipkow},
-title={Verified Bytecode Verifiers},
-journal=TCS,year=2002,note={To appear.
-\url{http://www.in.tum.de/~nipkow/pubs/tcs03.html}}}
+@article{KleinN-TOPLAS,author={Gerwin Klein and Tobias Nipkow},
+title={A Machine-Checked Model for a {Java}-Like Language, Virtual Machine and Compiler},
+journal=TOPLAS,volume = {28}, number = {4}, year = {2006}, pages = {619--695},
+doi = {http://doi.acm.org/10.1145/1146809.1146811}}

@InProceedings{Rudnicki92,author={P. Rudnicki},
title={An Overview of the {Mizar} Project},
@@ -40,12 +33,6 @@
organization={Technische Universit{\"a}t M{\"u}nchen},year=2002,
note={\url{http://isabelle.in.tum.de/dist/Isabelle2002/doc/isar-ref.pdf}}}

-@phdthesis{Wenzel-PhD,author={Markus Wenzel},title={Isabelle/Isar --- A
-Versatile Environment for Human-Readable Formal Proof Documents},
-school={Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
-year=2002,
-note={\url{http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html}}}
-
@article{WenzelW-JAR,author={Markus Wenzel and Freek Wiedijk},
title={A comparison of the mathematical proof languages {Mizar} and {Isar}},
journal=JAR,year=2002,pages={389--411}}
--- a/doc-src/IsarOverview/Isar/document/root.tex	Tue Nov 13 11:04:30 2007 +0100
+++ b/doc-src/IsarOverview/Isar/document/root.tex	Tue Nov 13 13:51:12 2007 +0100
@@ -12,23 +12,13 @@

\begin{document}

-\title{%A Compact Introduction to
-Structured Proofs in Isar/HOL\thanks{Published in TYPES 2002, LNCS 2646.}}
+\title{A Tutorial Introduction to Structured Isar Proofs}
\author{Tobias Nipkow}
\institute{Institut f{\"u}r Informatik, TU M{\"u}nchen\\
{\small\url{http://www.in.tum.de/~nipkow/}}}
\date{}
\maketitle

-\begin{abstract}
-  Isar is an extension of the theorem prover Isabelle with a language
-  for writing human-readable structured proofs. This paper is an
-  introduction to the basic constructs of this language.
-% It is aimed at potential users of Isar
-% but also discusses the design rationals
-% behind the language and its constructs.
-\end{abstract}
-
\input{intro.tex}
\input{Logic.tex}
\input{Induction.tex}