# HG changeset patch # User nipkow # Date 1194958272 -3600 # Node ID 8ba39d2d9d0b817e6efe0fe2d24ad6b0ad2ae38c # Parent 7ab693b8ee87ab8162e9863cc45840368fb8f6e1 updated diff -r 7ab693b8ee87 -r 8ba39d2d9d0b doc-src/IsarOverview/Isar/Induction.thy --- 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 * (\i::nat\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 the operations involved are overloaded. +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 \ [] \ hd(rev xs) = last xs" -by (induct xs) auto +by (induct xs) simp_all text{*\noindent This is an improvement over that style the tutorial~\cite{LNCS2283} advises, which requires @{text"\"}. @@ -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 diff -r 7ab693b8ee87 -r 8ba39d2d9d0b doc-src/IsarOverview/Isar/Logic.thy --- 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 \ (A \ B) \ 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. *} diff -r 7ab693b8ee87 -r 8ba39d2d9d0b doc-src/IsarOverview/Isar/document/Induction.tex --- 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 the operations involved are overloaded. +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% \ Asm{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ \isacommand{have}\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% diff -r 7ab693b8ee87 -r 8ba39d2d9d0b doc-src/IsarOverview/Isar/document/Logic.tex --- 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}% diff -r 7ab693b8ee87 -r 8ba39d2d9d0b doc-src/IsarOverview/Isar/document/intro.tex --- 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 -described elsewhere~\cite{BauerW-TPHOLs01}. Reasoning about -axiomatically defined structures by means of so called ``locales'' was -first described in \cite{KWP-TPHOLs99} but has evolved much since -then. +\subsection{Advice} -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. diff -r 7ab693b8ee87 -r 8ba39d2d9d0b doc-src/IsarOverview/Isar/document/root.bib --- 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}} diff -r 7ab693b8ee87 -r 8ba39d2d9d0b doc-src/IsarOverview/Isar/document/root.tex --- 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}