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@7315

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

wenzelm@7175

19 

wenzelm@7175

20 
Plain TTYbased interaction like this used to be quite feasible with

wenzelm@7175

21 
traditional tactic based theorem proving, but developing Isar documents

wenzelm@7297

22 
demands some better userinterface support. \emph{Proof~General}\index{Proof

wenzelm@7297

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

wenzelm@7297

24 
environment for interactive theorem provers that does all the cutandpaste

wenzelm@7297

25 
and forwardbackward walk through the document in a very neat way. Note that

wenzelm@7297

26 
in Isabelle/Isar, the current position within a partial proof document is more

wenzelm@7297

27 
informative than the actual proof state. Thus Proof~General provides the

wenzelm@7297

28 
canonical working environment for Isabelle/Isar, both for getting acquainted

wenzelm@7297

29 
(e.g.\ by replaying existing Isar documents) and serious production work.

wenzelm@7175

30 

wenzelm@7175

31 
\medskip

wenzelm@7167

32 

wenzelm@7315

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

wenzelm@7297

34 
interface. Just say something like this in your Isabelle settings file (cf.\

wenzelm@7297

35 
\cite{isabellesys}):

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@7335

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

wenzelm@7315

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

wenzelm@7335

43 
interface. Its usage is as follows:

wenzelm@7175

44 
\begin{ttbox}

wenzelm@7175

45 
Usage: interface [OPTIONS] [FILES ...]

wenzelm@7175

46 

wenzelm@7460

47 
Options are:

wenzelm@7460

48 
l NAME logic image name (default $ISABELLE_LOGIC=HOL)

wenzelm@7460

49 
p NAME Emacs program name (default xemacs)

wenzelm@7460

50 
u BOOL use .emacs file (default true)

wenzelm@7460

51 
w BOOL use window system (default true)

wenzelm@7175

52 

wenzelm@7460

53 
Starts Proof General for Isabelle/Isar with proof documents FILES

wenzelm@7460

54 
(default Scratch.thy).

wenzelm@7460

55 

wenzelm@7460

56 
PROOFGENERAL_OPTIONS=

wenzelm@7175

57 
\end{ttbox}

wenzelm@7335

58 
Apart from the command line, the defaults for these options may be overridden

wenzelm@7335

59 
via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For example, plain GNU

wenzelm@7460

60 
Emacs may be configured as follows:

wenzelm@7175

61 
\begin{ttbox}

wenzelm@7460

62 
PROOFGENERAL_OPTIONS="p emacs"

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@7315

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

wenzelm@7297

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

wenzelm@7297

72 
for further basic commands, such as \texttt{cc return} or \texttt{cc u}.

wenzelm@7175

73 

wenzelm@7460

74 
\medskip

wenzelm@7460

75 

wenzelm@7460

76 
Occasionally, a user's \texttt{.emacs} contains material that is incompatible

wenzelm@7460

77 
with the version of (X)Emacs that Proof~General prefers. Then proper startup

wenzelm@7460

78 
may be still achieved by using the \texttt{u false} option.\footnote{Also

wenzelm@7460

79 
note that the Emacs lisp files

wenzelm@7460

80 
\texttt{\$ISABELLE_HOME/etc/proofgeneralsettings.el} and

wenzelm@7460

81 
\texttt{\$ISABELLE_HOME_USER/etc/proofgeneralsettings.el} are automatically

wenzelm@7460

82 
loaded by Proof~General if invoked via the interface wrapper script.}

wenzelm@7460

83 

wenzelm@7167

84 

wenzelm@7167

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

wenzelm@7167

86 

wenzelm@7297

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

wenzelm@7297

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

wenzelm@7297

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

wenzelm@7297

90 
thinking different in order to make effective use of Isabelle/Isar. On the

wenzelm@7297

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

wenzelm@7297

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

wenzelm@7297

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

wenzelm@7297

94 
better.

wenzelm@7297

95 

wenzelm@7297

96 
Unfortunately, there is no tutorial on Isabelle/Isar available yet. This

wenzelm@7297

97 
document really is a \emph{reference manual}. Nevertheless, we will give some

wenzelm@7297

98 
discussions of the general principles underlying Isar in

wenzelm@7297

99 
chapter~\ref{ch:basics}, and provide some clues of how these may be put into

wenzelm@7297

100 
practice. Some more background information on Isar is given in

wenzelm@7297

101 
\cite{Wenzel:1999:TPHOL}. Furthermore, there are several examples distributed

wenzelm@7297

102 
with Isabelle (see directory \texttt{HOL/Isar_examples}).

wenzelm@7175

103 

wenzelm@7167

104 

wenzelm@7046

105 
%%% Local Variables:

wenzelm@7046

106 
%%% mode: latex

wenzelm@7046

107 
%%% TeXmaster: "isarref"

wenzelm@7046

108 
%%% End:
