doc-src/IsarRef/intro.tex
author wenzelm
Sat Oct 16 18:56:09 1999 +0200 (1999-10-16)
changeset 7875 1baf422ec16a
parent 7836 7a9270282fd3
child 7895 7c492d8bc8e3
permissions -rw-r--r--
PROOFGENERAL_OPTIONS="-u false";
wenzelm@7046
     1
wenzelm@7046
     2
\chapter{Introduction}
wenzelm@7046
     3
wenzelm@7167
     4
\section{Quick start}
wenzelm@7167
     5
wenzelm@7175
     6
Isar is already part of Isabelle (as of version Isabelle99, or later).  The
wenzelm@7175
     7
\texttt{isabelle} binary provides option \texttt{-I} to run the Isar
wenzelm@7175
     8
interaction loop at startup, rather than the plain ML top-level.  Thus the
wenzelm@7175
     9
quickest way to do anything with Isabelle/Isar is as follows:
wenzelm@7175
    10
\begin{ttbox}
wenzelm@7175
    11
isabelle -I HOL\medskip
wenzelm@7175
    12
\out{> Welcome to Isabelle/HOL (Isabelle99)}\medskip
wenzelm@7175
    13
theory Foo = Main:
wenzelm@7297
    14
constdefs foo :: nat  "foo == 1";
wenzelm@7297
    15
lemma "0 < foo" by (simp add: foo_def);
wenzelm@7175
    16
end
wenzelm@7175
    17
\end{ttbox}
wenzelm@7315
    18
Note that any Isabelle/Isar command may be retracted by \texttt{undo}.
wenzelm@7175
    19
wenzelm@7175
    20
Plain TTY-based interaction like this used to be quite feasible with
wenzelm@7175
    21
traditional tactic based theorem proving, but developing Isar documents
wenzelm@7297
    22
demands some better user-interface support.  \emph{Proof~General}\index{Proof
wenzelm@7297
    23
  General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based
wenzelm@7297
    24
environment for interactive theorem provers that does all the cut-and-paste
wenzelm@7297
    25
and forward-backward walk through the document in a very neat way.  Note that
wenzelm@7297
    26
in Isabelle/Isar, the current position within a partial proof document is more
wenzelm@7297
    27
informative than the actual proof state.  Thus Proof~General provides the
wenzelm@7297
    28
canonical working environment for Isabelle/Isar, both for getting acquainted
wenzelm@7297
    29
(e.g.\ by replaying existing Isar documents) and serious production work.
wenzelm@7175
    30
wenzelm@7175
    31
\medskip
wenzelm@7167
    32
wenzelm@7315
    33
The easiest way to use Proof~General is to make it the default Isabelle user
wenzelm@7297
    34
interface.  Just say something like this in your Isabelle settings file (cf.\ 
wenzelm@7297
    35
\cite{isabelle-sys}):
wenzelm@7175
    36
\begin{ttbox}
wenzelm@7175
    37
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
wenzelm@7875
    38
PROOFGENERAL_OPTIONS="-u false"
wenzelm@7175
    39
\end{ttbox}
wenzelm@7175
    40
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
wenzelm@7335
    41
actual installation directory of Proof~General.  From now on, the capital
wenzelm@7315
    42
\texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
wenzelm@7335
    43
interface.  Its usage is as follows:
wenzelm@7175
    44
\begin{ttbox}
wenzelm@7175
    45
Usage: interface [OPTIONS] [FILES ...]
wenzelm@7175
    46
wenzelm@7460
    47
  Options are:
wenzelm@7460
    48
    -l NAME      logic image name (default $ISABELLE_LOGIC=HOL)
wenzelm@7460
    49
    -p NAME      Emacs program name (default xemacs)
wenzelm@7460
    50
    -u BOOL      use .emacs file (default true)
wenzelm@7460
    51
    -w BOOL      use window system (default true)
wenzelm@7175
    52
wenzelm@7460
    53
  Starts Proof General for Isabelle/Isar with proof documents FILES
wenzelm@7460
    54
  (default Scratch.thy).
wenzelm@7460
    55
wenzelm@7460
    56
  PROOFGENERAL_OPTIONS=
wenzelm@7508
    57
\end{ttbox} %$
wenzelm@7335
    58
Apart from the command line, the defaults for these options may be overridden
wenzelm@7335
    59
via the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For example, plain GNU
wenzelm@7460
    60
Emacs may be configured as follows:
wenzelm@7175
    61
\begin{ttbox}
wenzelm@7460
    62
PROOFGENERAL_OPTIONS="-p emacs"
wenzelm@7175
    63
\end{ttbox}
wenzelm@7175
    64
wenzelm@7175
    65
With the proper Isabelle interface setup, Isar documents may now be edited by
wenzelm@7175
    66
visiting appropriate theory files, e.g.\ 
wenzelm@7175
    67
\begin{ttbox}
wenzelm@7175
    68
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
wenzelm@7175
    69
\end{ttbox}
wenzelm@7315
    70
Users of XEmacs may note the tool bar for navigating forward and backward
wenzelm@7297
    71
through the text.  Consult the Proof~General documentation \cite{proofgeneral}
wenzelm@7466
    72
for further basic commands, like \texttt{c-c return} or \texttt{c-c u}.
wenzelm@7175
    73
wenzelm@7460
    74
\medskip
wenzelm@7460
    75
wenzelm@7460
    76
Occasionally, a user's \texttt{.emacs} contains material that is incompatible
wenzelm@7460
    77
with the version of (X)Emacs that Proof~General prefers.  Then proper startup
wenzelm@7466
    78
may be still achieved by using the \texttt{-u false} option.\footnote{Any
wenzelm@7532
    79
  Emacs lisp file \texttt{proofgeneral-settings.el} occurring in
wenzelm@7532
    80
  \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc} is
wenzelm@7532
    81
  automatically loaded by the Proof~General interface script as well.}
wenzelm@7167
    82
wenzelm@7167
    83
\section{How to write Isar proofs anyway?}
wenzelm@7167
    84
wenzelm@7297
    85
This is one of the key questions, of course.  Isar offers a rather different
wenzelm@7297
    86
approach to formal proof documents than plain old tactic scripts.  Experienced
wenzelm@7297
    87
users of existing interactive theorem proving systems may have to learn
wenzelm@7297
    88
thinking different in order to make effective use of Isabelle/Isar.  On the
wenzelm@7297
    89
other hand, Isabelle/Isar comes much closer to existing mathematical practice
wenzelm@7297
    90
of formal proof, so users with less experience in old-style tactical proving,
wenzelm@7297
    91
but a good understanding of mathematical proof might cope with Isar even
wenzelm@7297
    92
better.
wenzelm@7297
    93
wenzelm@7836
    94
This document really is a \emph{reference manual}.  Nevertheless, we will give
wenzelm@7836
    95
some discussions of the general principles underlying Isar in
wenzelm@7297
    96
chapter~\ref{ch:basics}, and provide some clues of how these may be put into
wenzelm@7297
    97
practice.  Some more background information on Isar is given in
wenzelm@7836
    98
\cite{Wenzel:1999:TPHOL}.  While there is no proper tutorial on Isabelle/Isar
wenzelm@7836
    99
available yet, there are several examples distributed with Isabelle.  See
wenzelm@7836
   100
\texttt{HOL/Isar_examples} and \texttt{HOL/HOL-Real/HahnBanach} in the
wenzelm@7836
   101
Isabelle library:
wenzelm@7175
   102
wenzelm@7836
   103
\begin{center}\small
wenzelm@7836
   104
  \begin{tabular}{l}
wenzelm@7836
   105
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
wenzelm@7836
   106
    \url{http://isabelle.in.tum.de/library/} \\
wenzelm@7836
   107
  \end{tabular}
wenzelm@7836
   108
\end{center}
wenzelm@7836
   109
wenzelm@7836
   110
Apart from browsable HTML sources, both example sessions also provide actual
wenzelm@7836
   111
documents.
wenzelm@7167
   112
wenzelm@7046
   113
%%% Local Variables: 
wenzelm@7046
   114
%%% mode: latex
wenzelm@7046
   115
%%% TeX-master: "isar-ref"
wenzelm@7046
   116
%%% End: