doc-src/IsarRef/intro.tex
author wenzelm
Sat Oct 30 20:13:16 1999 +0200 (1999-10-30)
changeset 7981 5120a2a15d06
parent 7895 7c492d8bc8e3
child 7987 d9aef93c0e32
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@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@7895
    18
Note that any Isabelle/Isar command may be retracted by \texttt{undo}; the
wenzelm@7981
    19
\texttt{help} command prints a list of available language elements.
wenzelm@7175
    20
wenzelm@7175
    21
Plain TTY-based interaction like this used to be quite feasible with
wenzelm@7175
    22
traditional tactic based theorem proving, but developing Isar documents
wenzelm@7297
    23
demands some better user-interface support.  \emph{Proof~General}\index{Proof
wenzelm@7297
    24
  General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based
wenzelm@7297
    25
environment for interactive theorem provers that does all the cut-and-paste
wenzelm@7981
    26
and forward-backward walk through the text in a very neat way.  Note that in
wenzelm@7981
    27
Isabelle/Isar, the current position within a partial proof document is equally
wenzelm@7981
    28
important than the actual proof state.  Thus Proof~General provides the
wenzelm@7981
    29
canonical working environment for Isabelle/Isar, both for getting acquainted
wenzelm@7981
    30
(e.g.\ by replaying existing Isar documents) and real production work.
wenzelm@7175
    31
wenzelm@7175
    32
\medskip
wenzelm@7167
    33
wenzelm@7315
    34
The easiest way to use Proof~General is to make it the default Isabelle user
wenzelm@7895
    35
interface.  Just put something like this into your Isabelle settings file (see
wenzelm@7895
    36
also \cite{isabelle-sys}):
wenzelm@7175
    37
\begin{ttbox}
wenzelm@7175
    38
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
wenzelm@7875
    39
PROOFGENERAL_OPTIONS="-u false"
wenzelm@7175
    40
\end{ttbox}
wenzelm@7175
    41
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
wenzelm@7335
    42
actual installation directory of Proof~General.  From now on, the capital
wenzelm@7315
    43
\texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
wenzelm@7981
    44
interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for
wenzelm@7981
    45
  classic Isabelle tactic scripts.}  Its usage is as follows:
wenzelm@7175
    46
\begin{ttbox}
wenzelm@7175
    47
Usage: interface [OPTIONS] [FILES ...]
wenzelm@7175
    48
wenzelm@7460
    49
  Options are:
wenzelm@7460
    50
    -l NAME      logic image name (default $ISABELLE_LOGIC=HOL)
wenzelm@7460
    51
    -p NAME      Emacs program name (default xemacs)
wenzelm@7460
    52
    -u BOOL      use .emacs file (default true)
wenzelm@7460
    53
    -w BOOL      use window system (default true)
wenzelm@7175
    54
wenzelm@7460
    55
  Starts Proof General for Isabelle/Isar with proof documents FILES
wenzelm@7460
    56
  (default Scratch.thy).
wenzelm@7460
    57
wenzelm@7460
    58
  PROOFGENERAL_OPTIONS=
wenzelm@7508
    59
\end{ttbox} %$
wenzelm@7335
    60
Apart from the command line, the defaults for these options may be overridden
wenzelm@7335
    61
via the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For example, plain GNU
wenzelm@7460
    62
Emacs may be configured as follows:
wenzelm@7175
    63
\begin{ttbox}
wenzelm@7981
    64
PROOFGENERAL_OPTIONS="-u false -p emacs"
wenzelm@7175
    65
\end{ttbox}
wenzelm@7175
    66
wenzelm@7981
    67
Occasionally, a user's \texttt{.emacs} file contains material that is
wenzelm@7981
    68
incompatible with the version of (X)Emacs that Proof~General prefers.  Then
wenzelm@7981
    69
proper startup may be still achieved by using the \texttt{-u false}
wenzelm@7981
    70
option.\footnote{Any Emacs lisp file \texttt{proofgeneral-settings.el}
wenzelm@7981
    71
  occurring in \texttt{\$ISABELLE_HOME/etc} or
wenzelm@7981
    72
  \texttt{\$ISABELLE_HOME_USER/etc} is automatically loaded by the
wenzelm@7981
    73
  Proof~General interface script as well.}
wenzelm@7981
    74
wenzelm@7981
    75
\medskip
wenzelm@7981
    76
wenzelm@7175
    77
With the proper Isabelle interface setup, Isar documents may now be edited by
wenzelm@7175
    78
visiting appropriate theory files, e.g.\ 
wenzelm@7175
    79
\begin{ttbox}
wenzelm@7175
    80
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
wenzelm@7175
    81
\end{ttbox}
wenzelm@7315
    82
Users of XEmacs may note the tool bar for navigating forward and backward
wenzelm@7297
    83
through the text.  Consult the Proof~General documentation \cite{proofgeneral}
wenzelm@7981
    84
for further basic command sequences, such as ``\texttt{c-c return}'' or
wenzelm@7895
    85
``\texttt{c-c u}''.
wenzelm@7175
    86
wenzelm@7981
    87
wenzelm@7981
    88
\section{Isabelle/Isar theories}
wenzelm@7981
    89
wenzelm@7981
    90
Isabelle/Isar offers two main improvements over classic Isabelle:
wenzelm@7981
    91
\begin{enumerate}
wenzelm@7981
    92
\item A new \emph{theory format}, occasionally referred to as ``new-style
wenzelm@7981
    93
  theories'', supporting interactive development and unlimited undo operation.
wenzelm@7981
    94
\item A \emph{formal proof document language} designed to support intelligible
wenzelm@7981
    95
  semi-automated reasoning.  Instead of putting together unreadable tactic
wenzelm@7981
    96
  scripts, the author is enabled to express the reasoning in way that is close
wenzelm@7981
    97
  to mathematical practice.
wenzelm@7981
    98
\end{enumerate}
wenzelm@7981
    99
wenzelm@7981
   100
The Isar proof language is embedded into the new theory format as a proper
wenzelm@7981
   101
sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
wenzelm@7981
   102
$\LEMMANAME$ at the theory level, and left again with the final conclusion
wenzelm@7981
   103
(e.g.\ via $\QEDNAME$).  A few theory extension mechanisms require proof as
wenzelm@7981
   104
well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
wenzelm@7981
   105
the representing sets.
wenzelm@7460
   106
wenzelm@7981
   107
New-style theory files may still be associated with separate ML files
wenzelm@7981
   108
consisting of plain old tactic scripts.  There is no longer any ML binding
wenzelm@7981
   109
generated for the theory and theorems, though.  ML functions \texttt{theory},
wenzelm@7981
   110
\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
wenzelm@7981
   111
Nevertheless, migration between classic Isabelle and Isabelle/Isar is
wenzelm@7981
   112
relatively easy.  Thus users may start to benefit from interactive theory
wenzelm@7981
   113
development even before they have any idea of the Isar proof language at all.
wenzelm@7981
   114
wenzelm@7981
   115
\begin{warn}
wenzelm@7981
   116
  Currently Proof~General does \emph{not} support mixed interactive
wenzelm@7981
   117
  development of classic Isabelle theory files or tactic scripts, together
wenzelm@7981
   118
  with Isar documents.  The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
wenzelm@7981
   119
  Proof~General are handled as two different theorem proving systems, only one
wenzelm@7981
   120
  of these may be active at the same time.
wenzelm@7981
   121
\end{warn}
wenzelm@7981
   122
wenzelm@7981
   123
Porting of existing tactic scripts is best done by running two separate
wenzelm@7981
   124
Proof~General sessions, one for replaying the old script and the other for the
wenzelm@7981
   125
emerging Isabelle/Isar document.
wenzelm@7981
   126
wenzelm@7167
   127
wenzelm@7167
   128
\section{How to write Isar proofs anyway?}
wenzelm@7167
   129
wenzelm@7297
   130
This is one of the key questions, of course.  Isar offers a rather different
wenzelm@7297
   131
approach to formal proof documents than plain old tactic scripts.  Experienced
wenzelm@7297
   132
users of existing interactive theorem proving systems may have to learn
wenzelm@7895
   133
thinking differently in order to make effective use of Isabelle/Isar.  On the
wenzelm@7297
   134
other hand, Isabelle/Isar comes much closer to existing mathematical practice
wenzelm@7297
   135
of formal proof, so users with less experience in old-style tactical proving,
wenzelm@7895
   136
but a good understanding of mathematical proof, might cope with Isar even
wenzelm@7981
   137
better.  See also \cite{Wenzel:1999:TPHOL} for further background information
wenzelm@7981
   138
on Isar.
wenzelm@7297
   139
wenzelm@7981
   140
\medskip This really is a \emph{reference manual}.  Nevertheless, we will also
wenzelm@7981
   141
give some clues of how the concepts introduced here may be put into practice.
wenzelm@7981
   142
Appendix~\ref{ap:refcard} provides a quick reference card of the most common
wenzelm@7981
   143
Isabelle/Isar language elements.  There are several examples distributed with
wenzelm@7981
   144
Isabelle, and available via the Isabelle WWW library:
wenzelm@7836
   145
\begin{center}\small
wenzelm@7836
   146
  \begin{tabular}{l}
wenzelm@7836
   147
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
wenzelm@7836
   148
    \url{http://isabelle.in.tum.de/library/} \\
wenzelm@7836
   149
  \end{tabular}
wenzelm@7836
   150
\end{center}
wenzelm@7836
   151
wenzelm@7981
   152
See \texttt{HOL/Isar_examples} for a collection of introductory examples.
wenzelm@7981
   153
\texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application.  Apart from
wenzelm@7981
   154
browsable HTML sources, both sessions provide actual documents (in PDF).
wenzelm@7167
   155
wenzelm@7046
   156
%%% Local Variables: 
wenzelm@7046
   157
%%% mode: latex
wenzelm@7046
   158
%%% TeX-master: "isar-ref"
wenzelm@7046
   159
%%% End: