doc-src/IsarRef/Thy/Introduction.thy

Replaced group_ and ring_simps by algebra_simps;
removed compare_rls - use algebra_simps now

(* $Id$ *)

theory Introduction
imports Main
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 \cite{Wenzel:2006:Festschrift}
  is generic and should work 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
  the Isabelle/Pure framework. Nevertheless, examples given in the
  generic parts will usually refer to Isabelle/HOL as well.

  \medskip Isar commands may be either \emph{proper} document
  constructors, or \emph{improper commands}.  Some proof methods and
  attributes introduced later are classified as improper as well.
  Improper Isar language elements, which are marked by ``@{text
  "\<^sup>*"}'' 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.
*}


section {* User interfaces *}

subsection {* Terminal sessions *}

text {*
  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 @{command undo}.
  See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
  comprehensive overview of available commands and other language
  elements.
*}


subsection {* Emacs 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 \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.
*}


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


section {* 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