wenzelm@7046

1 

wenzelm@7046

2 
\chapter{Introduction}

wenzelm@7046

3 

wenzelm@7167

4 
\section{Quick start}

wenzelm@7167

5 

wenzelm@8508

6 
\subsection{Terminal sessions}

wenzelm@8508

7 

wenzelm@7175

8 
Isar is already part of Isabelle (as of version Isabelle99, or later). The

wenzelm@7175

9 
\texttt{isabelle} binary provides option \texttt{I} to run the Isar

wenzelm@7175

10 
interaction loop at startup, rather than the plain ML toplevel. Thus the

wenzelm@8547

11 
quickest way to do \emph{anything} with Isabelle/Isar is as follows:

wenzelm@7175

12 
\begin{ttbox}

wenzelm@7175

13 
isabelle I HOL\medskip

wenzelm@7175

14 
\out{> Welcome to Isabelle/HOL (Isabelle99)}\medskip

wenzelm@7175

15 
theory Foo = Main:

wenzelm@7297

16 
constdefs foo :: nat "foo == 1";

wenzelm@7297

17 
lemma "0 < foo" by (simp add: foo_def);

wenzelm@7175

18 
end

wenzelm@7175

19 
\end{ttbox}

wenzelm@8547

20 
Note that any Isabelle/Isar command may be retracted by \texttt{undo}. The

wenzelm@7981

21 
\texttt{help} command prints a list of available language elements.

wenzelm@7175

22 

wenzelm@8508

23 

wenzelm@8508

24 
\subsection{The Proof~General interface}

wenzelm@8508

25 

wenzelm@8508

26 
Plain TTYbased interaction as above used to be quite feasible with

wenzelm@8547

27 
traditional tactic based theorem proving, but developing Isar documents really

wenzelm@8508

28 
demands some better userinterface support. David Aspinall's

wenzelm@8508

29 
\emph{Proof~General}\index{Proof General} environment

wenzelm@8547

30 
\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs interface for

wenzelm@8547

31 
interactive theorem provers that does all the cutandpaste and

wenzelm@8508

32 
forwardbackward walk through the text in a very neat way. In Isabelle/Isar,

wenzelm@8508

33 
the current position within a partial proof document is equally important than

wenzelm@8508

34 
the actual proof state. Thus Proof~General provides the canonical working

wenzelm@8508

35 
environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying

wenzelm@8547

36 
existing Isar documents) and for production work.

wenzelm@7175

37 

wenzelm@7175

38 
\medskip

wenzelm@7167

39 

wenzelm@7315

40 
The easiest way to use Proof~General is to make it the default Isabelle user

wenzelm@8508

41 
interface (see also \cite{isabellesys}). Just put something like this into

wenzelm@8508

42 
your Isabelle settings file:

wenzelm@7175

43 
\begin{ttbox}

wenzelm@7175

44 
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface

wenzelm@8508

45 
PROOFGENERAL_OPTIONS=""

wenzelm@7175

46 
\end{ttbox}

wenzelm@7175

47 
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the

wenzelm@7335

48 
actual installation directory of Proof~General. From now on, the capital

wenzelm@7315

49 
\texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}

wenzelm@7981

50 
interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for

wenzelm@8508

51 
classic Isabelle tactic scripts.}

wenzelm@7175

52 

wenzelm@8547

53 
The interface script provides several options, just pass \verb,?, to see its

wenzelm@8547

54 
usage. Apart from the command line, the defaults for these options may be

wenzelm@8547

55 
overridden via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For

wenzelm@8516

56 
example, plain FSF Emacs (instead of the default XEmacs) may be configured in

wenzelm@8516

57 
Isabelle's settings via \texttt{PROOFGENERAL_OPTIONS="p emacs"}.

wenzelm@7460

58 

wenzelm@8516

59 
Occasionally, the user's \verb,~/.emacs, file contains material that is

wenzelm@8516

60 
incompatible with the version of Emacs that Proof~General prefers. Then

wenzelm@8508

61 
proper startup may be still achieved by using the \texttt{u false} option.

wenzelm@8547

62 
Also note that any Emacs lisp file called \texttt{proofgeneralsettings.el}

wenzelm@8547

63 
occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}

wenzelm@8547

64 
is automatically loaded by the Proof~General interface script as well.

wenzelm@7981

65 

wenzelm@7981

66 
\medskip

wenzelm@7981

67 

wenzelm@7175

68 
With the proper Isabelle interface setup, Isar documents may now be edited by

wenzelm@7175

69 
visiting appropriate theory files, e.g.\

wenzelm@7175

70 
\begin{ttbox}

wenzelm@7175

71 
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy

wenzelm@7175

72 
\end{ttbox}

wenzelm@7315

73 
Users of XEmacs may note the tool bar for navigating forward and backward

wenzelm@8516

74 
through the text. Consult the Proof~General documentation \cite{proofgeneral}

wenzelm@8547

75 
for further basic command sequences, such as ``\texttt{Cc Creturn}'' or

wenzelm@8547

76 
``\texttt{Cc u}''.

wenzelm@8508

77 

wenzelm@8508

78 
\medskip

wenzelm@8508

79 

wenzelm@8508

80 
Proof~General also supports the Emacs XSymbol package \cite{xsymbol}, which

wenzelm@8508

81 
provides a nice way to get proper mathematical symbols displayed on screen.

wenzelm@8508

82 
Just pass option \texttt{x true} to the Isabelle interface script, or check

wenzelm@8516

83 
the appropriate menu setting by hand. In any case, the XSymbol package must

wenzelm@8516

84 
have been properly installed already.

wenzelm@8516

85 

wenzelm@8516

86 
Note that using actual mathematical symbols in the text easily makes the ASCII

wenzelm@8516

87 
sources hard to read. For example, $\forall$ will appear as \verb,\\<forall>,

wenzelm@8516

88 
according the default set of Isabelle symbols. On the other hand, the

wenzelm@8516

89 
Isabelle document preparation system \cite{isabellesys} will be happy to

wenzelm@8516

90 
print nonASCII symbols properly. It is even possible to invent additional

wenzelm@8547

91 
notation beyond the display capabilities of XEmacs and XSymbol.

wenzelm@7175

92 

wenzelm@7981

93 

wenzelm@7981

94 
\section{Isabelle/Isar theories}

wenzelm@7981

95 

wenzelm@8547

96 
Isabelle/Isar offers the following main improvements over classic Isabelle.

wenzelm@7981

97 
\begin{enumerate}

wenzelm@7981

98 
\item A new \emph{theory format}, occasionally referred to as ``newstyle

wenzelm@7981

99 
theories'', supporting interactive development and unlimited undo operation.

wenzelm@7981

100 
\item A \emph{formal proof document language} designed to support intelligible

wenzelm@7981

101 
semiautomated reasoning. Instead of putting together unreadable tactic

wenzelm@7981

102 
scripts, the author is enabled to express the reasoning in way that is close

wenzelm@8508

103 
to usual mathematical practice.

wenzelm@8547

104 
\item A simple document preparation system, for typesetting formal

wenzelm@8547

105 
developments together with informal text. The resulting hyperlinked PDF

wenzelm@8547

106 
documents are equally well suited for WWW presentation and as printed

wenzelm@8547

107 
copies.

wenzelm@7981

108 
\end{enumerate}

wenzelm@7981

109 

wenzelm@7981

110 
The Isar proof language is embedded into the new theory format as a proper

wenzelm@7981

111 
sublanguage. Proof mode is entered by stating some $\THEOREMNAME$ or

wenzelm@7981

112 
$\LEMMANAME$ at the theory level, and left again with the final conclusion

wenzelm@7981

113 
(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as

wenzelm@8547

114 
well, such as HOL's $\isarkeyword{typedef}$ which demands nonemptiness of the

wenzelm@8547

115 
representing sets.

wenzelm@7460

116 

wenzelm@7981

117 
Newstyle theory files may still be associated with separate ML files

wenzelm@7981

118 
consisting of plain old tactic scripts. There is no longer any ML binding

wenzelm@7981

119 
generated for the theory and theorems, though. ML functions \texttt{theory},

wenzelm@7981

120 
\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelleref}.

wenzelm@7981

121 
Nevertheless, migration between classic Isabelle and Isabelle/Isar is

wenzelm@7981

122 
relatively easy. Thus users may start to benefit from interactive theory

wenzelm@8547

123 
development and document preparation, even before they have any idea of the

wenzelm@8547

124 
Isar proof language at all.

wenzelm@7981

125 

wenzelm@7981

126 
\begin{warn}

wenzelm@8547

127 
Currently, Proof~General does \emph{not} support mixed interactive

wenzelm@7981

128 
development of classic Isabelle theory files or tactic scripts, together

wenzelm@7981

129 
with Isar documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of

wenzelm@7981

130 
Proof~General are handled as two different theorem proving systems, only one

wenzelm@7981

131 
of these may be active at the same time.

wenzelm@7981

132 
\end{warn}

wenzelm@7981

133 

wenzelm@7981

134 
Porting of existing tactic scripts is best done by running two separate

wenzelm@7981

135 
Proof~General sessions, one for replaying the old script and the other for the

wenzelm@7981

136 
emerging Isabelle/Isar document.

wenzelm@7981

137 

wenzelm@7167

138 

wenzelm@7167

139 
\section{How to write Isar proofs anyway?}

wenzelm@7167

140 

wenzelm@7297

141 
This is one of the key questions, of course. Isar offers a rather different

wenzelm@7297

142 
approach to formal proof documents than plain old tactic scripts. Experienced

wenzelm@7297

143 
users of existing interactive theorem proving systems may have to learn

wenzelm@7895

144 
thinking differently in order to make effective use of Isabelle/Isar. On the

wenzelm@7297

145 
other hand, Isabelle/Isar comes much closer to existing mathematical practice

wenzelm@7297

146 
of formal proof, so users with less experience in oldstyle tactical proving,

wenzelm@7895

147 
but a good understanding of mathematical proof, might cope with Isar even

wenzelm@7981

148 
better. See also \cite{Wenzel:1999:TPHOL} for further background information

wenzelm@7981

149 
on Isar.

wenzelm@8547

150 
%FIXME cite [HahnBanachinIsar]

wenzelm@7297

151 

wenzelm@7981

152 
\medskip This really is a \emph{reference manual}. Nevertheless, we will also

wenzelm@7981

153 
give some clues of how the concepts introduced here may be put into practice.

wenzelm@7981

154 
Appendix~\ref{ap:refcard} provides a quick reference card of the most common

wenzelm@7981

155 
Isabelle/Isar language elements. There are several examples distributed with

wenzelm@8516

156 
Isabelle, and available via the Isabelle WWW library as well as the

wenzelm@8516

157 
Isabelle/Isar page:

wenzelm@7836

158 
\begin{center}\small

wenzelm@7836

159 
\begin{tabular}{l}

wenzelm@7836

160 
\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\

wenzelm@8516

161 
\url{http://isabelle.in.tum.de/library/} \\[1ex]

wenzelm@8508

162 
\url{http://isabelle.in.tum.de/Isar/} \\

wenzelm@7836

163 
\end{tabular}

wenzelm@7836

164 
\end{center}

wenzelm@7836

165 

wenzelm@7987

166 
See \texttt{HOL/Isar_examples} for a collection of introductory examples, and

wenzelm@8547

167 
\texttt{HOL/HOLReal/HahnBanach} for a big mathematics application. Apart

wenzelm@8547

168 
from plain HTML sources, these sessions also provide actual documents (in

wenzelm@8547

169 
PDF).

wenzelm@8547

170 

wenzelm@7167

171 

wenzelm@7046

172 
%%% Local Variables:

wenzelm@7046

173 
%%% mode: latex

wenzelm@7046

174 
%%% TeXmaster: "isarref"

wenzelm@7046

175 
%%% End:
