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 toplevel. 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 TTYbased 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 userinterface support. \emph{Proof~General}\index{Proof

wenzelm@7297

24 
General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacsbased

wenzelm@7297

25 
environment for interactive theorem provers that does all the cutandpaste

wenzelm@7981

26 
and forwardbackward 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{isabellesys}):

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{proofgeneralsettings.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{cc return}'' or

wenzelm@7895

85 
``\texttt{cc 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 ``newstyle

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 
semiautomated 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 
sublanguage. 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 nonemptiness of

wenzelm@7981

105 
the representing sets.

wenzelm@7460

106 

wenzelm@7981

107 
Newstyle 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{isabelleref}.

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 oldstyle 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/HOLReal/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 
%%% TeXmaster: "isarref"

wenzelm@7046

159 
%%% End:
