doc-src/IsarRef/Thy/document/Introduction.tex

 %
 \begin{isabellebody}%
 \def\isabellecontext{Introduction}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%

 %
 \begin{isamarkuptext}%
 The \emph{Isabelle} system essentially provides a generic
   infrastructure for building deductive systems (programmed in
   Standard ML), with a special focus on interactive theorem proving in
-  higher-order logics.  In the olden days even end-users would refer
-  to certain ML functions (goal commands, tactics, tacticals etc.) to
-  pursue their everyday theorem proving tasks
-  \cite{isabelle-intro,isabelle-ref}.
+  higher-order logics.  Many years ago, even end-users would refer to
+  certain ML functions (goal commands, tactics, tacticals etc.) to
+  pursue their everyday theorem proving tasks.
   
   In contrast \emph{Isar} provides an interpreted language environment
   of its own, which has been specifically tailored for the needs of
   theory and proof development.  Compared to raw ML, the Isabelle/Isar
   top-level provides a more robust and comfortable development
-  platform, with proper support for theory development graphs,
-  single-step transactions with unlimited undo, etc.  The
-  Isabelle/Isar version of the \emph{Proof~General} user interface
-  \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
-  front-end for interactive theory and proof development in this
-  advanced theorem proving environment.
+  platform, with proper support for theory development graphs, managed
+  transactions with unlimited undo etc.  The Isabelle/Isar version of
+  the \emph{Proof~General} user interface
+  \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
+  for interactive theory and proof development in this advanced
+  theorem proving environment, even though it is somewhat biased
+  towards old-style proof scripts.
 
   \medskip Apart from the technical advances over bare-bones ML
   programming, the main purpose of the Isar language is to provide a
   conceptually different view on machine-checked proofs
-  \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  ``Isar'' stands for
-  ``Intelligible semi-automated reasoning''.  Drawing from both the
+  \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  \emph{Isar} stands for
+  \emph{Intelligible semi-automated reasoning}.  Drawing from both the
   traditions of informal mathematical proof texts and high-level
   programming languages, Isar offers a versatile environment for
   structured formal proof documents.  Thus properly written Isar
   proofs become accessible to a broader audience than unstructured
   tactic scripts (which typically only provide operational information

   right, independently of the mechanic proof-checking process.
 
   Despite its grand design of structured proof texts, Isar is able to
   assimilate the old tactical style as an ``improper'' sub-language.
   This provides an easy upgrade path for existing tactic scripts, as
-  well as additional means for interactive experimentation and
-  debugging of structured proofs.  Isabelle/Isar supports a broad
-  range of proof styles, both readable and unreadable ones.
+  well as some means for interactive experimentation and debugging of
+  structured proofs.  Isabelle/Isar supports a broad range of proof
+  styles, both readable and unreadable ones.
 
-  \medskip The Isabelle/Isar framework \cite{Wenzel:2006:Festschrift}
-  is generic and should work reasonably well for any Isabelle
+  \medskip The generic Isabelle/Isar framework (see
+  \chref{ch:isar-framework}) works reasonably well for any Isabelle
   object-logic that conforms to the natural deduction view of the
   Isabelle/Pure framework.  Specific language elements introduced by
   the major object-logics are described in \chref{ch:hol}
   (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
   (Isabelle/ZF).  The main language elements are already provided by

   Improper Isar language elements, which are marked by ``\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}'' in the subsequent chapters; they are often helpful
   when developing proof documents, but their use is discouraged for
   the final human-readable outcome.  Typical examples are diagnostic
   commands that print terms or theorems according to the current
   context; other commands emulate old-style tactical theorem proving.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{User interfaces%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Terminal sessions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The Isabelle \texttt{tty} tool provides a very interface for running
-  the Isar interaction loop, with some support for command line
-  editing.  For example:
-\begin{ttbox}
-isabelle tty\medskip
-{\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
-theory Foo imports Main begin;
-definition foo :: nat where "foo == 1";
-lemma "0 < foo" by (simp add: foo_def);
-end;
-\end{ttbox}
-
-  Any Isabelle/Isar command may be retracted by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}.
-  See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
-  comprehensive overview of available commands and other language
-  elements.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Emacs Proof General%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Plain TTY-based interaction as above used to be quite feasible with
-  traditional tactic based theorem proving, but developing Isar
-  documents really demands some better user-interface support.  The
-  Proof~General environment by David Aspinall
-  \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
-  interface for interactive theorem provers that organizes all the
-  cut-and-paste and forward-backward walk through the text in a very
-  neat way.  In Isabelle/Isar, the current position within a partial
-  proof document is equally important than the actual proof state.
-  Thus Proof~General provides the canonical working environment for
-  Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
-  existing Isar documents) and for production work.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Proof~General as default Isabelle interface%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The Isabelle interface wrapper script provides an easy way to invoke
-  Proof~General (including XEmacs or GNU Emacs).  The default
-  configuration of Isabelle is smart enough to detect the
-  Proof~General distribution in several canonical places (e.g.\
-  \verb|$ISABELLE_HOME/contrib/ProofGeneral|).  Thus the
-  capital \verb|Isabelle| executable would already refer to the
-  \verb|ProofGeneral/isar| interface without further ado.  The
-  Isabelle interface script provides several options; pass \verb|-?|  to see its usage.
-
-  With the proper Isabelle interface setup, Isar documents may now be edited by
-  visiting appropriate theory files, e.g.\ 
-\begin{ttbox}
-Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
-\end{ttbox}
-  Beginners may note the tool bar for navigating forward and backward
-  through the text (this depends on the local Emacs installation).
-  Consult the Proof~General documentation \cite{proofgeneral} for
-  further basic command sequences, in particular ``\verb|C-c C-return|''
-  and ``\verb|C-c u|''.
-
-  \medskip Proof~General may be also configured manually by giving
-  Isabelle settings like this (see also \cite{isabelle-sys}):
-
-\begin{ttbox}
-ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
-PROOFGENERAL_OPTIONS=""
-\end{ttbox}
-  You may have to change \verb|$ISABELLE_HOME/contrib/ProofGeneral| to the actual installation
-  directory of Proof~General.
-
-  \medskip Apart from the Isabelle command line, defaults for
-  interface options may be given by the \verb|PROOFGENERAL_OPTIONS|
-  setting.  For example, the Emacs executable to be used may be
-  configured in Isabelle's settings like this:
-\begin{ttbox}
-PROOFGENERAL_OPTIONS="-p xemacs-mule"  
-\end{ttbox}
-
-  Occasionally, a user's \verb|~/.emacs| file contains code
-  that is incompatible with the (X)Emacs version used by
-  Proof~General, causing the interface startup to fail prematurely.
-  Here the \verb|-u false| option helps to get the interface
-  process up and running.  Note that additional Lisp customization
-  code may reside in \verb|proofgeneral-settings.el| of
-  \verb|$ISABELLE_HOME/etc| or \verb|$ISABELLE_HOME_USER/etc|.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{The X-Symbol package%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Proof~General incorporates a version of the Emacs X-Symbol package
-  \cite{x-symbol}, which handles proper mathematical symbols displayed
-  on screen.  Pass option \verb|-x true| to the Isabelle
-  interface script, or check the appropriate Proof~General menu
-  setting by hand.  The main challenge of getting X-Symbol to work
-  properly is the underlying (semi-automated) X11 font setup.
-
-  \medskip Using proper mathematical symbols in Isabelle theories can
-  be very convenient for readability of large formulas.  On the other
-  hand, the plain ASCII sources easily become somewhat unintelligible.
-  For example, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} would appear as \verb|\<Longrightarrow>| according
-  the default set of Isabelle symbols.  Nevertheless, the Isabelle
-  document preparation system (see \chref{ch:document-prep}) will be
-  happy to print non-ASCII symbols properly.  It is even possible to
-  invent additional notation beyond the display capabilities of Emacs
-  and X-Symbol.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Isabelle/Isar theories%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Isabelle/Isar offers the following main improvements over classic
-  Isabelle.
-
-  \begin{enumerate}
-  
-  \item A \emph{theory format} that integrates specifications and
-  proofs, supporting interactive development and unlimited undo
-  operation.
-  
-  \item A \emph{formal proof document language} designed to support
-  intelligible semi-automated reasoning.  Instead of putting together
-  unreadable tactic scripts, the author is enabled to express the
-  reasoning in way that is close to usual mathematical practice.  The
-  old tactical style has been assimilated as ``improper'' language
-  elements.
-  
-  \item A simple document preparation system, for typesetting formal
-  developments together with informal text.  The resulting
-  hyper-linked PDF documents are equally well suited for WWW
-  presentation and as printed copies.
-
-  \end{enumerate}
-
-  The Isar proof language is embedded into the new theory format as a
-  proper sub-language.  Proof mode is entered by stating some
-  \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory level, and
-  left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).
-  A few theory specification mechanisms also require some proof, such
-  as HOL's \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} which demands non-emptiness of the
-  representing sets.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-This is one of the key questions, of course.  First of all, the
-  tactic script emulation of Isabelle/Isar essentially provides a
-  clarified version of the very same unstructured proof style of
-  classic Isabelle.  Old-time users should quickly become acquainted
-  with that (slightly degenerative) view of Isar.
-
-  Writing \emph{proper} Isar proof texts targeted at human readers is
-  quite different, though.  Experienced users of the unstructured
-  style may even have to unlearn some of their habits to master proof
-  composition in Isar.  In contrast, new users with less experience in
-  old-style tactical proving, but a good understanding of mathematical
-  proof in general, often get started easier.
-
-  \medskip The present text really is only a reference manual on
-  Isabelle/Isar, not a tutorial.  Nevertheless, we will attempt to
-  give some clues of how the concepts introduced here may be put into
-  practice.  Especially note that \appref{ap:refcard} provides a quick
-  reference card of the most common Isabelle/Isar language elements.
-
-  Further issues concerning the Isar concepts are covered in the
-  literature
-  \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
-  The author's PhD thesis \cite{Wenzel-PhD} presently provides the
-  most complete exposition of Isar foundations, techniques, and
-  applications.  A number of example applications are distributed with
-  Isabelle, and available via the Isabelle WWW library (e.g.\
-  \url{http://isabelle.in.tum.de/library/}).  The ``Archive of Formal
-  Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
-  examples, both in proper Isar proof style and unstructured tactic
-  scripts.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadelimtheory
 %