doc-src/IsarRef/Thy/Introduction.thy

+(* $Id$ *)
+
+theory Introduction
+imports Pure
+begin
+
+chapter {* Introduction *}
+
+section {* Overview *}
+
+text {*
+  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}.
+  
+  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.
+
+  \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
+  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
+  for the machine).  Writing human-readable proof texts certainly
+  requires some additional efforts by the writer to achieve a good
+  presentation, both of formal and informal parts of the text.  On the
+  other hand, human-readable formal texts gain some value in their own
+  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.
+
+  \medskip The Isabelle/Isar framework is generic and should work
+  reasonably well for any Isabelle object-logic that conforms to the
+  natural deduction view of the Isabelle/Pure framework.  Major
+  Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF
+  \cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF
+  \cite{isabelle-ZF} have already been set up for end-users.
+*}
+
+
+section {* Quick start *}
+
+subsection {* Terminal sessions *}
+
+text {*
+  Isar is already part of Isabelle.  The low-level @{verbatim
+  isabelle} binary provides option @{verbatim "-I"} to run the
+  Isabelle/Isar interaction loop at startup, rather than the raw ML
+  top-level.  So the most basic way to do anything with Isabelle/Isar
+  is as follows:   % FIXME update
+\begin{ttbox}
+isabelle -I HOL\medskip
+\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
+theory Foo imports Main begin;
+definition foo :: nat where "foo == 1";
+lemma "0 < foo" by (simp add: foo_def);
+end;
+\end{ttbox}
+
+  Note that any Isabelle/Isar command may be retracted by @{command
+  "undo"}.  See the Isabelle/Isar Quick Reference
+  (\appref{ap:refcard}) for a comprehensive overview of available
+  commands and other language elements.
+*}
+
+
+subsection {* Proof General *}
+
+text {*
+  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.
+*}
+
+
+subsubsection{* Proof~General as default Isabelle interface *}
+
+text {*
+  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.\
+  @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}).  Thus the
+  capital @{verbatim Isabelle} executable would already refer to the
+  @{verbatim "ProofGeneral/isar"} interface without further ado.  The
+  Isabelle interface script provides several options; pass @{verbatim
+  "-?"}  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 ``@{verbatim "C-c C-return"}''
+  and ``@{verbatim "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 @{verbatim
+  "$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 @{verbatim 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 @{verbatim "~/.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 @{verbatim "-u false"} option helps to get the interface
+  process up and running.  Note that additional Lisp customization
+  code may reside in @{verbatim "proofgeneral-settings.el"} of
+  @{verbatim "$ISABELLE_HOME/etc"} or @{verbatim
+  "$ISABELLE_HOME_USER/etc"}.
+*}
+
+
+subsubsection {* The X-Symbol package *}
+
+text {*
+  Proof~General incorporates a version of the Emacs X-Symbol package
+  \cite{x-symbol}, which handles proper mathematical symbols displayed
+  on screen.  Pass option @{verbatim "-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, @{text "\<Longrightarrow>"} would appear as @{verbatim "\<Longrightarrow>"} according
+  the default set of Isabelle symbols.  Nevertheless, the Isabelle
+  document preparation system (see \secref{sec: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.
+*}
+
+
+section {* Isabelle/Isar theories *}
+
+text {*
+  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
+  @{command "theorem"} or @{command "lemma"} at the theory level, and
+  left again with the final conclusion (e.g.\ via @{command "qed"}).
+  A few theory specification mechanisms also require some proof, such
+  as HOL's @{command "typedef"} which demands non-emptiness of the
+  representing sets.
+*}
+
+
+subsection {* Document preparation \label{sec:document-prep} *}
+
+text {*
+  Isabelle/Isar provides a simple document preparation system based on
+  existing {PDF-\LaTeX} technology, with full support of hyper-links
+  (both local references and URLs) and bookmarks.  Thus the results
+  are equally well suited for WWW browsing and as printed copies.
+
+  \medskip Isabelle generates {\LaTeX} output as part of the run of a
+  \emph{logic session} (see also \cite{isabelle-sys}).  Getting
+  started with a working configuration for common situations is quite
+  easy by using the Isabelle @{verbatim mkdir} and @{verbatim make}
+  tools.  First invoke
+\begin{ttbox}
+  isatool mkdir Foo
+\end{ttbox}
+  to initialize a separate directory for session @{verbatim Foo} ---
+  it is safe to experiment, since @{verbatim "isatool mkdir"} never
+  overwrites existing files.  Ensure that @{verbatim "Foo/ROOT.ML"}
+  holds ML commands to load all theories required for this session;
+  furthermore @{verbatim "Foo/document/root.tex"} should include any
+  special {\LaTeX} macro packages required for your document (the
+  default is usually sufficient as a start).
+
+  The session is controlled by a separate @{verbatim IsaMakefile}
+  (with crude source dependencies by default).  This file is located
+  one level up from the @{verbatim Foo} directory location.  Now
+  invoke
+\begin{ttbox}
+  isatool make Foo
+\end{ttbox}
+  to run the @{verbatim Foo} session, with browser information and
+  document preparation enabled.  Unless any errors are reported by
+  Isabelle or {\LaTeX}, the output will appear inside the directory
+  @{verbatim ISABELLE_BROWSER_INFO}, as reported by the batch job in
+  verbose mode.
+
+  \medskip You may also consider to tune the @{verbatim usedir}
+  options in @{verbatim IsaMakefile}, for example to change the output
+  format from @{verbatim pdf} to @{verbatim dvi}, or activate the
+  @{verbatim "-D"} option to retain a second copy of the generated
+  {\LaTeX} sources.
+
+  \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
+  for further details on Isabelle logic sessions and theory
+  presentation.  The Isabelle/HOL tutorial \cite{isabelle-hol-book}
+  also covers theory presentation issues.
+*}
+
+
+subsection {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
+
+text {*
+  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