doc-src/IsarRef/intro.tex
changeset 7981 5120a2a15d06
parent 7895 7c492d8bc8e3
child 7987 d9aef93c0e32
     1.1 --- a/doc-src/IsarRef/intro.tex	Sat Oct 30 20:12:23 1999 +0200
     1.2 +++ b/doc-src/IsarRef/intro.tex	Sat Oct 30 20:13:16 1999 +0200
     1.3 @@ -16,19 +16,18 @@
     1.4  end
     1.5  \end{ttbox}
     1.6  Note that any Isabelle/Isar command may be retracted by \texttt{undo}; the
     1.7 -\texttt{help} command prints the list of available language elements.
     1.8 +\texttt{help} command prints a list of available language elements.
     1.9  
    1.10  Plain TTY-based interaction like this used to be quite feasible with
    1.11  traditional tactic based theorem proving, but developing Isar documents
    1.12  demands some better user-interface support.  \emph{Proof~General}\index{Proof
    1.13    General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based
    1.14  environment for interactive theorem provers that does all the cut-and-paste
    1.15 -and forward-backward walk through the document in a very neat way.  Note that
    1.16 -in Isabelle/Isar, the current position within a partial proof document is
    1.17 -equally important than the actual proof state.  Thus Proof~General provides
    1.18 -the canonical working environment for Isabelle/Isar, both for getting
    1.19 -acquainted (e.g.\ by replaying existing Isar documents) and real production
    1.20 -work.
    1.21 +and forward-backward walk through the text in a very neat way.  Note that in
    1.22 +Isabelle/Isar, the current position within a partial proof document is equally
    1.23 +important than the actual proof state.  Thus Proof~General provides the
    1.24 +canonical working environment for Isabelle/Isar, both for getting acquainted
    1.25 +(e.g.\ by replaying existing Isar documents) and real production work.
    1.26  
    1.27  \medskip
    1.28  
    1.29 @@ -42,7 +41,8 @@
    1.30  You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
    1.31  actual installation directory of Proof~General.  From now on, the capital
    1.32  \texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
    1.33 -interface.  Its usage is as follows:
    1.34 +interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for
    1.35 +  classic Isabelle tactic scripts.}  Its usage is as follows:
    1.36  \begin{ttbox}
    1.37  Usage: interface [OPTIONS] [FILES ...]
    1.38  
    1.39 @@ -61,9 +61,19 @@
    1.40  via the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For example, plain GNU
    1.41  Emacs may be configured as follows:
    1.42  \begin{ttbox}
    1.43 -PROOFGENERAL_OPTIONS="-p emacs"
    1.44 +PROOFGENERAL_OPTIONS="-u false -p emacs"
    1.45  \end{ttbox}
    1.46  
    1.47 +Occasionally, a user's \texttt{.emacs} file contains material that is
    1.48 +incompatible with the version of (X)Emacs that Proof~General prefers.  Then
    1.49 +proper startup may be still achieved by using the \texttt{-u false}
    1.50 +option.\footnote{Any Emacs lisp file \texttt{proofgeneral-settings.el}
    1.51 +  occurring in \texttt{\$ISABELLE_HOME/etc} or
    1.52 +  \texttt{\$ISABELLE_HOME_USER/etc} is automatically loaded by the
    1.53 +  Proof~General interface script as well.}
    1.54 +
    1.55 +\medskip
    1.56 +
    1.57  With the proper Isabelle interface setup, Isar documents may now be edited by
    1.58  visiting appropriate theory files, e.g.\ 
    1.59  \begin{ttbox}
    1.60 @@ -71,18 +81,49 @@
    1.61  \end{ttbox}
    1.62  Users of XEmacs may note the tool bar for navigating forward and backward
    1.63  through the text.  Consult the Proof~General documentation \cite{proofgeneral}
    1.64 -for further basic command sequences, like ``\texttt{c-c return}'' or
    1.65 +for further basic command sequences, such as ``\texttt{c-c return}'' or
    1.66  ``\texttt{c-c u}''.
    1.67  
    1.68 -\medskip
    1.69 +
    1.70 +\section{Isabelle/Isar theories}
    1.71 +
    1.72 +Isabelle/Isar offers two main improvements over classic Isabelle:
    1.73 +\begin{enumerate}
    1.74 +\item A new \emph{theory format}, occasionally referred to as ``new-style
    1.75 +  theories'', supporting interactive development and unlimited undo operation.
    1.76 +\item A \emph{formal proof document language} designed to support intelligible
    1.77 +  semi-automated reasoning.  Instead of putting together unreadable tactic
    1.78 +  scripts, the author is enabled to express the reasoning in way that is close
    1.79 +  to mathematical practice.
    1.80 +\end{enumerate}
    1.81 +
    1.82 +The Isar proof language is embedded into the new theory format as a proper
    1.83 +sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
    1.84 +$\LEMMANAME$ at the theory level, and left again with the final conclusion
    1.85 +(e.g.\ via $\QEDNAME$).  A few theory extension mechanisms require proof as
    1.86 +well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
    1.87 +the representing sets.
    1.88  
    1.89 -Occasionally, a user's \texttt{.emacs} file contains material that is
    1.90 -incompatible with the version of (X)Emacs that Proof~General prefers.  Then
    1.91 -proper startup may be still achieved by using the \texttt{-u false}
    1.92 -option.\footnote{Any Emacs lisp file \texttt{proofgeneral-settings.el}
    1.93 -  occurring in \texttt{\$ISABELLE_HOME/etc} or
    1.94 -  \texttt{\$ISABELLE_HOME_USER/etc} is automatically loaded by the
    1.95 -  Proof~General interface script as well.}
    1.96 +New-style theory files may still be associated with separate ML files
    1.97 +consisting of plain old tactic scripts.  There is no longer any ML binding
    1.98 +generated for the theory and theorems, though.  ML functions \texttt{theory},
    1.99 +\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
   1.100 +Nevertheless, migration between classic Isabelle and Isabelle/Isar is
   1.101 +relatively easy.  Thus users may start to benefit from interactive theory
   1.102 +development even before they have any idea of the Isar proof language at all.
   1.103 +
   1.104 +\begin{warn}
   1.105 +  Currently Proof~General does \emph{not} support mixed interactive
   1.106 +  development of classic Isabelle theory files or tactic scripts, together
   1.107 +  with Isar documents.  The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
   1.108 +  Proof~General are handled as two different theorem proving systems, only one
   1.109 +  of these may be active at the same time.
   1.110 +\end{warn}
   1.111 +
   1.112 +Porting of existing tactic scripts is best done by running two separate
   1.113 +Proof~General sessions, one for replaying the old script and the other for the
   1.114 +emerging Isabelle/Isar document.
   1.115 +
   1.116  
   1.117  \section{How to write Isar proofs anyway?}
   1.118  
   1.119 @@ -93,17 +134,14 @@
   1.120  other hand, Isabelle/Isar comes much closer to existing mathematical practice
   1.121  of formal proof, so users with less experience in old-style tactical proving,
   1.122  but a good understanding of mathematical proof, might cope with Isar even
   1.123 -better.
   1.124 +better.  See also \cite{Wenzel:1999:TPHOL} for further background information
   1.125 +on Isar.
   1.126  
   1.127 -This document really is a \emph{reference manual}.  Nevertheless, we will give
   1.128 -some discussions of the general principles underlying Isar in
   1.129 -chapter~\ref{ch:basics}, and provide some clues of how these may be put into
   1.130 -practice.  Some more background information on Isar is given in
   1.131 -\cite{Wenzel:1999:TPHOL}.  While there is no proper tutorial on Isabelle/Isar
   1.132 -available yet, there are several examples distributed with Isabelle.  See
   1.133 -\texttt{HOL/Isar_examples} and \texttt{HOL/HOL-Real/HahnBanach} in the
   1.134 -Isabelle library:
   1.135 -
   1.136 +\medskip This really is a \emph{reference manual}.  Nevertheless, we will also
   1.137 +give some clues of how the concepts introduced here may be put into practice.
   1.138 +Appendix~\ref{ap:refcard} provides a quick reference card of the most common
   1.139 +Isabelle/Isar language elements.  There are several examples distributed with
   1.140 +Isabelle, and available via the Isabelle WWW library:
   1.141  \begin{center}\small
   1.142    \begin{tabular}{l}
   1.143      \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
   1.144 @@ -111,8 +149,9 @@
   1.145    \end{tabular}
   1.146  \end{center}
   1.147  
   1.148 -Apart from browsable HTML sources, both Isabelle/Isar sessions also provide
   1.149 -actual documents (in PDF).
   1.150 +See \texttt{HOL/Isar_examples} for a collection of introductory examples.
   1.151 +\texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application.  Apart from
   1.152 +browsable HTML sources, both sessions provide actual documents (in PDF).
   1.153  
   1.154  %%% Local Variables: 
   1.155  %%% mode: latex