doc-src/IsarRef/intro.tex
author wenzelm
Wed Aug 04 18:20:24 1999 +0200 (1999-08-04)
changeset 7175 8263d0b50e12
parent 7167 0b2e3ef1d8f4
child 7297 c1eeeadbe80a
permissions -rw-r--r--
tuned;
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@7175
    14
constdefs foo :: nat  "foo == 1"
wenzelm@7175
    15
lemma "0 < foo" by (simp add: foo_def)
wenzelm@7175
    16
end
wenzelm@7175
    17
\end{ttbox}
wenzelm@7175
    18
wenzelm@7175
    19
Plain TTY-based interaction like this used to be quite feasible with
wenzelm@7175
    20
traditional tactic based theorem proving, but developing Isar documents
wenzelm@7175
    21
demands some better user-interface support.
wenzelm@7175
    22
\emph{ProofGeneral}\index{ProofGeneral} of LFCS Edinburgh \cite{proofgeneral}
wenzelm@7175
    23
offers a generic Emacs-based environment for interactive theorem provers that
wenzelm@7175
    24
does all the cut-and-paste and forward-backward walk through the document in a
wenzelm@7175
    25
very neat way.  Note that in Isabelle/Isar, the current position within a
wenzelm@7175
    26
partial proof document is more informative than the actual proof state.  Thus
wenzelm@7175
    27
the ProofGeneral/isar interface provides the canonical working environment for
wenzelm@7175
    28
Isabelle/Isar, both for getting acquainted (e.g.\ by replaying existing Isar
wenzelm@7175
    29
documents) and serious production work.
wenzelm@7175
    30
wenzelm@7175
    31
\medskip
wenzelm@7167
    32
wenzelm@7175
    33
The easiest way to use ProofGeneral/isar is to make it the default Isabelle
wenzelm@7175
    34
user interface.  Just say something like this in your Isabelle settings file
wenzelm@7175
    35
(cf.\ \cite{isabelle-sys}):
wenzelm@7175
    36
\begin{ttbox}
wenzelm@7175
    37
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
wenzelm@7175
    38
PROOFGENERAL_OPTIONS=""
wenzelm@7175
    39
\end{ttbox}
wenzelm@7175
    40
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
wenzelm@7175
    41
actual installation directory of ProofGeneral.  Now the capital
wenzelm@7175
    42
\texttt{Isabelle} binary refers to the ProofGeneral/isar interface.  It's
wenzelm@7175
    43
usage is as follows:
wenzelm@7175
    44
\begin{ttbox}
wenzelm@7175
    45
Usage: interface [OPTIONS] [FILES ...]
wenzelm@7175
    46
wenzelm@7175
    47
Options are:
wenzelm@7175
    48
  -l NAME      logic image name (default $ISABELLE_LOGIC=HOL)
wenzelm@7175
    49
  -p NAME      Emacs program name (default xemacs)
wenzelm@7175
    50
  -u BOOL      use .emacs file (default false)
wenzelm@7175
    51
  -w BOOL      use window system (default true)
wenzelm@7175
    52
wenzelm@7175
    53
Starts ProofGeneral for Isabelle/Isar with proof documents FILES
wenzelm@7175
    54
(default Scratch.thy).
wenzelm@7175
    55
\end{ttbox}
wenzelm@7175
    56
The defaults for these options may be changed via the
wenzelm@7175
    57
\texttt{PROOFGENERAL_OPTIONS} setting.  For example, GNU Emacs with loading of
wenzelm@7175
    58
the startup file enabled may be configured as follows:\footnote{The interface
wenzelm@7175
    59
  disables \texttt{.emacs} by default to ensure successful startup despite any
wenzelm@7175
    60
  strange commands that tend to occur there.}
wenzelm@7175
    61
\begin{ttbox}
wenzelm@7175
    62
PROOFGENERAL_OPTIONS="-p emacs -u true"
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@7175
    70
Users of XEmacs may note the toolbar for navigating forward and backward
wenzelm@7175
    71
through the text.  Consult the ProofGeneral documentation for further basic
wenzelm@7175
    72
commands, such as \texttt{c-c return} or \texttt{c-c u}.
wenzelm@7175
    73
wenzelm@7167
    74
wenzelm@7167
    75
\section{How to write Isar proofs anyway?}
wenzelm@7167
    76
wenzelm@7175
    77
FIXME
wenzelm@7175
    78
wenzelm@7167
    79
wenzelm@7046
    80
%%% Local Variables: 
wenzelm@7046
    81
%%% mode: latex
wenzelm@7046
    82
%%% TeX-master: "isar-ref"
wenzelm@7046
    83
%%% End: