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