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
 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 \<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
 tutorial~\cite{LNCS2283} advises, which requires @{text"\<longrightarrow>"}.
@@ -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
 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%

--- 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
-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.

--- 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}