doc-src/IsarRef/intro.tex
author kleing
Mon, 29 Dec 2003 06:49:26 +0100
changeset 14333 14f29eb097a3
parent 13039 cfcc1f6f21df
child 16016 9e57d19cb21c
permissions -rw-r--r--
\<^bsub> .. \<^esub>
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     1
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     2
\chapter{Introduction}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     3
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
     4
\section{Overview}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
     5
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
     6
The \emph{Isabelle} system essentially provides a generic infrastructure for
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
     7
building deductive systems (programmed in Standard ML), with a special focus
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
     8
on interactive theorem proving in higher-order logics.  In the olden days even
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
     9
end-users would refer to certain ML functions (goal commands, tactics,
12879
wenzelm
parents: 12621
diff changeset
    10
tacticals etc.) to pursue their everyday theorem proving tasks
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    11
\cite{isabelle-intro,isabelle-ref}.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    12
  
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    13
In contrast \emph{Isar} provides an interpreted language environment of its
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    14
own, which has been specifically tailored for the needs of theory and proof
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    15
development.  Compared to raw ML, the Isabelle/Isar top-level provides a more
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    16
robust and comfortable development platform, with proper support for theory
13039
wenzelm
parents: 12879
diff changeset
    17
development graphs, single-step transactions with unlimited undo, etc.  The
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    18
Isabelle/Isar version of the \emph{Proof~General} user interface
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    19
\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for
13039
wenzelm
parents: 12879
diff changeset
    20
interactive theory and proof development in this advanced theorem proving
wenzelm
parents: 12879
diff changeset
    21
environment.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    22
13039
wenzelm
parents: 12879
diff changeset
    23
\medskip Apart from the technical advances over bare-bones ML programming, the
wenzelm
parents: 12879
diff changeset
    24
main purpose of the Isar language is to provide a conceptually different view
wenzelm
parents: 12879
diff changeset
    25
on machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  ``Isar''
wenzelm
parents: 12879
diff changeset
    26
stands for ``Intelligible semi-automated reasoning''.  Drawing from both the
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    27
traditions of informal mathematical proof texts and high-level programming
13039
wenzelm
parents: 12879
diff changeset
    28
languages, Isar offers a versatile environment for structured formal proof
wenzelm
parents: 12879
diff changeset
    29
documents.  Thus properly written Isar proofs become accessible to a broader
wenzelm
parents: 12879
diff changeset
    30
audience than unstructured tactic scripts (which typically only provide
wenzelm
parents: 12879
diff changeset
    31
operational information for the machine).  Writing human-readable proof texts
wenzelm
parents: 12879
diff changeset
    32
certainly requires some additional efforts by the writer to achieve a good
wenzelm
parents: 12879
diff changeset
    33
presentation, both of formal and informal parts of the text.  On the other
wenzelm
parents: 12879
diff changeset
    34
hand, human-readable formal texts gain some value in their own right,
wenzelm
parents: 12879
diff changeset
    35
independently of the mechanic proof-checking process.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    36
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    37
Despite its grand design of structured proof texts, Isar is able to assimilate
12879
wenzelm
parents: 12621
diff changeset
    38
the old tactical style as an ``improper'' sub-language.  This provides an easy
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    39
upgrade path for existing tactic scripts, as well as additional means for
12879
wenzelm
parents: 12621
diff changeset
    40
interactive experimentation and debugging of structured proofs.  Isabelle/Isar
wenzelm
parents: 12621
diff changeset
    41
supports a broad range of proof styles, both readable and unreadable ones.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    42
12879
wenzelm
parents: 12621
diff changeset
    43
\medskip The Isabelle/Isar framework is generic and should work reasonably
wenzelm
parents: 12621
diff changeset
    44
well for any Isabelle object-logic that conforms to the natural deduction view
wenzelm
parents: 12621
diff changeset
    45
of the Isabelle/Pure framework.  Major Isabelle logics like HOL
wenzelm
parents: 12621
diff changeset
    46
\cite{isabelle-HOL}, HOLCF \cite{MuellerNvOS99}, FOL \cite{isabelle-logics},
wenzelm
parents: 12621
diff changeset
    47
and ZF \cite{isabelle-ZF} have already been set up for end-users.
wenzelm
parents: 12621
diff changeset
    48
Nonetheless, much of the existing body of theories still consist of old-style
wenzelm
parents: 12621
diff changeset
    49
theory files with accompanied ML code for proof scripts; this legacy will be
wenzelm
parents: 12621
diff changeset
    50
gradually converted in due time.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    51
43a97a2155d0 first stage of major update;
wenzelm
parents: 11041
diff changeset
    52
7167
wenzelm
parents: 7046
diff changeset
    53
\section{Quick start}
wenzelm
parents: 7046
diff changeset
    54
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    55
\subsection{Terminal sessions}
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    56
12879
wenzelm
parents: 12621
diff changeset
    57
Isar is already part of Isabelle.  The low-level \texttt{isabelle} binary
wenzelm
parents: 12621
diff changeset
    58
provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
wenzelm
parents: 12621
diff changeset
    59
startup, rather than the raw ML top-level.  So the most basic way to do
wenzelm
parents: 12621
diff changeset
    60
anything with Isabelle/Isar is as follows:
7175
wenzelm
parents: 7167
diff changeset
    61
\begin{ttbox}
wenzelm
parents: 7167
diff changeset
    62
isabelle -I HOL\medskip
12879
wenzelm
parents: 12621
diff changeset
    63
\out{> Welcome to Isabelle/HOL (Isabelle2002)}\medskip
7175
wenzelm
parents: 7167
diff changeset
    64
theory Foo = Main:
7297
wenzelm
parents: 7175
diff changeset
    65
constdefs foo :: nat  "foo == 1";
wenzelm
parents: 7175
diff changeset
    66
lemma "0 < foo" by (simp add: foo_def);
7175
wenzelm
parents: 7167
diff changeset
    67
end
wenzelm
parents: 7167
diff changeset
    68
\end{ttbox}
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 8843
diff changeset
    69
Note that any Isabelle/Isar command may be retracted by \texttt{undo}.  See
10160
wenzelm
parents: 10110
diff changeset
    70
the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
10110
7d6e03a1f11e fixed ref;
wenzelm
parents: 9849
diff changeset
    71
comprehensive overview of available commands and other language elements.
7175
wenzelm
parents: 7167
diff changeset
    72
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    73
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
    74
\subsection{Proof~General}
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    75
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    76
Plain TTY-based interaction as above used to be quite feasible with
8547
wenzelm
parents: 8516
diff changeset
    77
traditional tactic based theorem proving, but developing Isar documents really
12879
wenzelm
parents: 12621
diff changeset
    78
demands some better user-interface support.  The Proof~General environment by
wenzelm
parents: 12621
diff changeset
    79
David Aspinall \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
wenzelm
parents: 12621
diff changeset
    80
interface for interactive theorem provers that organizes all the cut-and-paste
wenzelm
parents: 12621
diff changeset
    81
and forward-backward walk through the text in a very neat way.  In
wenzelm
parents: 12621
diff changeset
    82
Isabelle/Isar, the current position within a partial proof document is equally
wenzelm
parents: 12621
diff changeset
    83
important than the actual proof state.  Thus Proof~General provides the
wenzelm
parents: 12621
diff changeset
    84
canonical working environment for Isabelle/Isar, both for getting acquainted
wenzelm
parents: 12621
diff changeset
    85
(e.g.\ by replaying existing Isar documents) and for production work.
7175
wenzelm
parents: 7167
diff changeset
    86
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
    87
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
    88
\subsubsection{Proof~General as default Isabelle interface}
7167
wenzelm
parents: 7046
diff changeset
    89
12879
wenzelm
parents: 12621
diff changeset
    90
The Isabelle interface wrapper script provides an easy way to invoke
13039
wenzelm
parents: 12879
diff changeset
    91
Proof~General (including XEmacs or GNU Emacs).  The default configuration of
12879
wenzelm
parents: 12621
diff changeset
    92
Isabelle is smart enough to detect the Proof~General distribution in several
wenzelm
parents: 12621
diff changeset
    93
canonical places (e.g.\ \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}).  Thus
wenzelm
parents: 12621
diff changeset
    94
the capital \texttt{Isabelle} executable would already refer to the
9849
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    95
\texttt{ProofGeneral/isar} interface without further ado.\footnote{There is
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    96
  also a \texttt{ProofGeneral/isa} interface for old tactic scripts written in
12879
wenzelm
parents: 12621
diff changeset
    97
  ML.} The Isabelle interface script provides several options; pass \verb,-?,
wenzelm
parents: 12621
diff changeset
    98
to see its usage.
7981
wenzelm
parents: 7895
diff changeset
    99
7175
wenzelm
parents: 7167
diff changeset
   100
With the proper Isabelle interface setup, Isar documents may now be edited by
wenzelm
parents: 7167
diff changeset
   101
visiting appropriate theory files, e.g.\ 
wenzelm
parents: 7167
diff changeset
   102
\begin{ttbox}
12879
wenzelm
parents: 12621
diff changeset
   103
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
7175
wenzelm
parents: 7167
diff changeset
   104
\end{ttbox}
13039
wenzelm
parents: 12879
diff changeset
   105
Beginners may note the tool bar for navigating forward and backward through
wenzelm
parents: 12879
diff changeset
   106
the text (this depends on the local Emacs installation).  Consult the
12879
wenzelm
parents: 12621
diff changeset
   107
Proof~General documentation \cite{proofgeneral} for further basic command
wenzelm
parents: 12621
diff changeset
   108
sequences, in particular ``\texttt{C-c C-return}'' and ``\texttt{C-c u}''.
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
   109
9849
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   110
\medskip
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   111
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   112
Proof~General may be also configured manually by giving Isabelle settings like
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   113
this (see also \cite{isabelle-sys}):
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   114
\begin{ttbox}
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   115
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   116
PROOFGENERAL_OPTIONS=""
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   117
\end{ttbox}
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   118
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   119
actual installation directory of Proof~General.
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   120
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   121
\medskip
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   122
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   123
Apart from the Isabelle command line, defaults for interface options may be
12879
wenzelm
parents: 12621
diff changeset
   124
given by the \texttt{PROOFGENERAL_OPTIONS} setting.  For example, the Emacs
wenzelm
parents: 12621
diff changeset
   125
executable to be used may be configured in Isabelle's settings like this:
9849
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   126
\begin{ttbox}
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   127
PROOFGENERAL_OPTIONS="-p xemacs-nomule"  
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   128
\end{ttbox}
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   129
12879
wenzelm
parents: 12621
diff changeset
   130
Occasionally, a user's \verb,~/.emacs, file contains code that is incompatible
wenzelm
parents: 12621
diff changeset
   131
with the (X)Emacs version used by Proof~General, causing the interface startup
wenzelm
parents: 12621
diff changeset
   132
to fail prematurely.  Here the \texttt{-u false} option helps to get the
wenzelm
parents: 12621
diff changeset
   133
interface process up and running.  Note that additional Lisp customization
wenzelm
parents: 12621
diff changeset
   134
code may reside in \texttt{proofgeneral-settings.el} of
wenzelm
parents: 12621
diff changeset
   135
\texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}.
9849
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   136
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   137
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   138
\subsubsection{The X-Symbol package}
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
   139
12879
wenzelm
parents: 12621
diff changeset
   140
Proof~General provides native support for the Emacs X-Symbol package
wenzelm
parents: 12621
diff changeset
   141
\cite{x-symbol}, which handles proper mathematical symbols displayed on
wenzelm
parents: 12621
diff changeset
   142
screen.  Pass option \texttt{-x true} to the Isabelle interface script, or
wenzelm
parents: 12621
diff changeset
   143
check the appropriate Proof~General menu setting by hand.  In any case, the
wenzelm
parents: 12621
diff changeset
   144
X-Symbol package must have been properly installed already.
8516
f5f6a97ee43f simplified setup;
wenzelm
parents: 8508
diff changeset
   145
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   146
Contrary to what you may expect from the documentation of X-Symbol, the
9849
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   147
package is very easy to install and configures itself automatically.  The
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   148
default configuration of Isabelle is smart enough to detect the X-Symbol
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   149
package in several canonical places (e.g.\ 
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   150
\texttt{\$ISABELLE_HOME/contrib/x-symbol}).
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   151
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   152
\medskip
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   153
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   154
Using proper mathematical symbols in Isabelle theories can be very convenient
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   155
for readability of large formulas.  On the other hand, the plain ASCII sources
10160
wenzelm
parents: 10110
diff changeset
   156
easily become somewhat unintelligible.  For example, $\Longrightarrow$ would
9849
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   157
appear as \verb,\<Longrightarrow>, according the default set of Isabelle
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   158
symbols.  Nevertheless, the Isabelle document preparation system (see
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   159
\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   160
It is even possible to invent additional notation beyond the display
12879
wenzelm
parents: 12621
diff changeset
   161
capabilities of Emacs and X-Symbol.
7175
wenzelm
parents: 7167
diff changeset
   162
7981
wenzelm
parents: 7895
diff changeset
   163
wenzelm
parents: 7895
diff changeset
   164
\section{Isabelle/Isar theories}
wenzelm
parents: 7895
diff changeset
   165
8547
wenzelm
parents: 8516
diff changeset
   166
Isabelle/Isar offers the following main improvements over classic Isabelle.
7981
wenzelm
parents: 7895
diff changeset
   167
\begin{enumerate}
13039
wenzelm
parents: 12879
diff changeset
   168
  
7981
wenzelm
parents: 7895
diff changeset
   169
\item A new \emph{theory format}, occasionally referred to as ``new-style
wenzelm
parents: 7895
diff changeset
   170
  theories'', supporting interactive development and unlimited undo operation.
13039
wenzelm
parents: 12879
diff changeset
   171
  
7981
wenzelm
parents: 7895
diff changeset
   172
\item A \emph{formal proof document language} designed to support intelligible
wenzelm
parents: 7895
diff changeset
   173
  semi-automated reasoning.  Instead of putting together unreadable tactic
wenzelm
parents: 7895
diff changeset
   174
  scripts, the author is enabled to express the reasoning in way that is close
13039
wenzelm
parents: 12879
diff changeset
   175
  to usual mathematical practice.  The old tactical style has been assimilated
wenzelm
parents: 12879
diff changeset
   176
  as ``improper'' language elements.
wenzelm
parents: 12879
diff changeset
   177
  
8547
wenzelm
parents: 8516
diff changeset
   178
\item A simple document preparation system, for typesetting formal
wenzelm
parents: 8516
diff changeset
   179
  developments together with informal text.  The resulting hyper-linked PDF
wenzelm
parents: 8516
diff changeset
   180
  documents are equally well suited for WWW presentation and as printed
wenzelm
parents: 8516
diff changeset
   181
  copies.
13039
wenzelm
parents: 12879
diff changeset
   182
7981
wenzelm
parents: 7895
diff changeset
   183
\end{enumerate}
wenzelm
parents: 7895
diff changeset
   184
wenzelm
parents: 7895
diff changeset
   185
The Isar proof language is embedded into the new theory format as a proper
wenzelm
parents: 7895
diff changeset
   186
sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
wenzelm
parents: 7895
diff changeset
   187
$\LEMMANAME$ at the theory level, and left again with the final conclusion
12879
wenzelm
parents: 12621
diff changeset
   188
(e.g.\ via $\QEDNAME$).  A few theory specification mechanisms also require
wenzelm
parents: 12621
diff changeset
   189
some proof, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness
wenzelm
parents: 12621
diff changeset
   190
of the representing sets.
7460
wenzelm
parents: 7335
diff changeset
   191
7981
wenzelm
parents: 7895
diff changeset
   192
New-style theory files may still be associated with separate ML files
wenzelm
parents: 7895
diff changeset
   193
consisting of plain old tactic scripts.  There is no longer any ML binding
wenzelm
parents: 7895
diff changeset
   194
generated for the theory and theorems, though.  ML functions \texttt{theory},
13039
wenzelm
parents: 12879
diff changeset
   195
\texttt{thm}, and \texttt{thms} retrieve this information from the context
wenzelm
parents: 12879
diff changeset
   196
\cite{isabelle-ref}.  Nevertheless, migration between classic Isabelle and
wenzelm
parents: 12879
diff changeset
   197
Isabelle/Isar is relatively easy.  Thus users may start to benefit from
wenzelm
parents: 12879
diff changeset
   198
interactive theory development and document preparation, even before they have
wenzelm
parents: 12879
diff changeset
   199
any idea of the Isar proof language at all.
7981
wenzelm
parents: 7895
diff changeset
   200
wenzelm
parents: 7895
diff changeset
   201
\begin{warn}
12879
wenzelm
parents: 12621
diff changeset
   202
  Proof~General does \emph{not} support mixed interactive development of
wenzelm
parents: 12621
diff changeset
   203
  classic Isabelle theory files or tactic scripts, together with Isar
wenzelm
parents: 12621
diff changeset
   204
  documents.  The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
7981
wenzelm
parents: 7895
diff changeset
   205
  Proof~General are handled as two different theorem proving systems, only one
wenzelm
parents: 7895
diff changeset
   206
  of these may be active at the same time.
wenzelm
parents: 7895
diff changeset
   207
\end{warn}
wenzelm
parents: 7895
diff changeset
   208
12879
wenzelm
parents: 12621
diff changeset
   209
Manual conversion of existing tactic scripts may be done by running two
wenzelm
parents: 12621
diff changeset
   210
separate Proof~General sessions, one for replaying the old script and the
wenzelm
parents: 12621
diff changeset
   211
other for the emerging Isabelle/Isar document.  Also note that Isar supports
wenzelm
parents: 12621
diff changeset
   212
emulation commands and methods that support traditional tactic scripts within
wenzelm
parents: 12621
diff changeset
   213
new-style theories, see appendix~\ref{ap:conv} for more information.
7981
wenzelm
parents: 7895
diff changeset
   214
7167
wenzelm
parents: 7046
diff changeset
   215
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   216
\subsection{Document preparation}\label{sec:document-prep}
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   217
12879
wenzelm
parents: 12621
diff changeset
   218
Isabelle/Isar provides a simple document preparation system based on existing
13039
wenzelm
parents: 12879
diff changeset
   219
{PDF-\LaTeX} technology, with full support of hyper-links (both local
wenzelm
parents: 12879
diff changeset
   220
references and URLs), bookmarks, and thumbnails.  Thus the results are equally
wenzelm
parents: 12879
diff changeset
   221
well suited for WWW browsing and as printed copies.
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   222
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   223
\medskip
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   224
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   225
Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   226
  session} (see also \cite{isabelle-sys}).  Getting started with a working
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   227
configuration for common situations is quite easy by using the Isabelle
12879
wenzelm
parents: 12621
diff changeset
   228
\texttt{mkdir} and \texttt{make} tools.  First invoke
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   229
\begin{ttbox}
12879
wenzelm
parents: 12621
diff changeset
   230
  isatool mkdir Foo
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   231
\end{ttbox}
12879
wenzelm
parents: 12621
diff changeset
   232
to initialize a separate directory for session \texttt{Foo} --- it is safe to
wenzelm
parents: 12621
diff changeset
   233
experiment, since \texttt{isatool mkdir} never overwrites existing files.
wenzelm
parents: 12621
diff changeset
   234
Ensure that \texttt{Foo/ROOT.ML} holds ML commands to load all theories
wenzelm
parents: 12621
diff changeset
   235
required for this session; furthermore \texttt{Foo/document/root.tex} should
wenzelm
parents: 12621
diff changeset
   236
include any special {\LaTeX} macro packages required for your document (the
wenzelm
parents: 12621
diff changeset
   237
default is usually sufficient as a start).
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   238
12879
wenzelm
parents: 12621
diff changeset
   239
The session is controlled by a separate \texttt{IsaMakefile} (with crude
wenzelm
parents: 12621
diff changeset
   240
source dependencies by default).  This file is located one level up from the
wenzelm
parents: 12621
diff changeset
   241
\texttt{Foo} directory location.  Now invoke
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   242
\begin{ttbox}
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   243
  isatool make Foo
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   244
\end{ttbox}
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   245
to run the \texttt{Foo} session, with browser information and document
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   246
preparation enabled.  Unless any errors are reported by Isabelle or {\LaTeX},
12879
wenzelm
parents: 12621
diff changeset
   247
the output will appear inside the directory \texttt{ISABELLE_BROWSER_INFO}, as
wenzelm
parents: 12621
diff changeset
   248
reported by the batch job in verbose mode.
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   249
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   250
\medskip
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   251
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   252
You may also consider to tune the \texttt{usedir} options in
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   253
\texttt{IsaMakefile}, for example to change the output format from
13039
wenzelm
parents: 12879
diff changeset
   254
\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D} option to retain a
wenzelm
parents: 12879
diff changeset
   255
second copy of the generated {\LaTeX} sources.
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   256
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   257
\medskip
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   258
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   259
See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
12879
wenzelm
parents: 12621
diff changeset
   260
on Isabelle logic sessions and theory presentation.  The Isabelle/HOL tutorial
wenzelm
parents: 12621
diff changeset
   261
\cite{isabelle-hol-book} also covers theory presentation issues.
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   262
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   263
10160
wenzelm
parents: 10110
diff changeset
   264
\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
7167
wenzelm
parents: 7046
diff changeset
   265
12879
wenzelm
parents: 12621
diff changeset
   266
This is one of the key questions, of course.  First of all, the tactic script
wenzelm
parents: 12621
diff changeset
   267
emulation of Isabelle/Isar essentially provides a clarified version of the
wenzelm
parents: 12621
diff changeset
   268
very same unstructured proof style of classic Isabelle.  Old-time users should
13039
wenzelm
parents: 12879
diff changeset
   269
quickly become acquainted with that (slightly degenerative) view of Isar.
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   270
12879
wenzelm
parents: 12621
diff changeset
   271
Writing \emph{proper} Isar proof texts targeted at human readers is quite
wenzelm
parents: 12621
diff changeset
   272
different, though.  Experienced users of the unstructured style may even have
wenzelm
parents: 12621
diff changeset
   273
to unlearn some of their habits to master proof composition in Isar.  In
wenzelm
parents: 12621
diff changeset
   274
contrast, new users with less experience in old-style tactical proving, but a
13039
wenzelm
parents: 12879
diff changeset
   275
good understanding of mathematical proof in general, often get started easier.
7297
wenzelm
parents: 7175
diff changeset
   276
12879
wenzelm
parents: 12621
diff changeset
   277
\medskip The present text really is only a reference manual on Isabelle/Isar,
wenzelm
parents: 12621
diff changeset
   278
not a tutorial.  Nevertheless, we will attempt to give some clues of how the
wenzelm
parents: 12621
diff changeset
   279
concepts introduced here may be put into practice.  Appendix~\ref{ap:refcard}
wenzelm
parents: 12621
diff changeset
   280
provides a quick reference card of the most common Isabelle/Isar language
wenzelm
parents: 12621
diff changeset
   281
elements.  Appendix~\ref{ap:conv} offers some practical hints on converting
wenzelm
parents: 12621
diff changeset
   282
existing Isabelle theories and proof scripts to the new format (without
wenzelm
parents: 12621
diff changeset
   283
restructuring proofs).
10160
wenzelm
parents: 10110
diff changeset
   284
12879
wenzelm
parents: 12621
diff changeset
   285
Further issues concerning the Isar concepts are covered in the literature
wenzelm
parents: 12621
diff changeset
   286
\cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
wenzelm
parents: 12621
diff changeset
   287
The author's PhD thesis \cite{Wenzel-PhD} presently provides the most complete
wenzelm
parents: 12621
diff changeset
   288
exposition of Isar foundations, techniques, and applications.  A number of
wenzelm
parents: 12621
diff changeset
   289
example applications are distributed with Isabelle, and available via the
wenzelm
parents: 12621
diff changeset
   290
Isabelle WWW library (e.g.\ \url{http://isabelle.in.tum.de/library/}).  As a
wenzelm
parents: 12621
diff changeset
   291
general rule of thumb, more recent Isabelle applications that also include a
wenzelm
parents: 12621
diff changeset
   292
separate ``document'' (in PDF) are more likely to consist of proper
wenzelm
parents: 12621
diff changeset
   293
Isabelle/Isar theories and proofs.
7836
7a9270282fd3 a4paper;
wenzelm
parents: 7532
diff changeset
   294
12879
wenzelm
parents: 12621
diff changeset
   295
%FIXME
wenzelm
parents: 12621
diff changeset
   296
% The following examples may be of particular interest.  Apart from the plain
wenzelm
parents: 12621
diff changeset
   297
% sources represented in HTML, these Isabelle sessions also provide actual
wenzelm
parents: 12621
diff changeset
   298
% documents (in PDF).
wenzelm
parents: 12621
diff changeset
   299
% \begin{itemize}
wenzelm
parents: 12621
diff changeset
   300
% \item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
wenzelm
parents: 12621
diff changeset
   301
%   collection of introductory examples.
wenzelm
parents: 12621
diff changeset
   302
% \item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
wenzelm
parents: 12621
diff changeset
   303
%   typical mathematics-style reasoning in ``axiomatic'' structures.
wenzelm
parents: 12621
diff changeset
   304
% \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
wenzelm
parents: 12621
diff changeset
   305
%   big mathematics application on infinitary vector spaces and functional
wenzelm
parents: 12621
diff changeset
   306
%   analysis.
wenzelm
parents: 12621
diff changeset
   307
% \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
wenzelm
parents: 12621
diff changeset
   308
%   properties of $\lambda$-calculus (Church-Rosser and termination).
10993
883248dcf3f8 added Unix example;
wenzelm
parents: 10160
diff changeset
   309
  
12879
wenzelm
parents: 12621
diff changeset
   310
%   This may serve as a realistic example of porting of legacy proof scripts
wenzelm
parents: 12621
diff changeset
   311
%   into Isar tactic emulation scripts.
wenzelm
parents: 12621
diff changeset
   312
% \item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
wenzelm
parents: 12621
diff changeset
   313
%   model of the main aspects of the Unix file-system including its security
wenzelm
parents: 12621
diff changeset
   314
%   model, but ignoring processes.  A few odd effects caused by the general
wenzelm
parents: 12621
diff changeset
   315
%   ``worse-is-better'' approach followed in Unix are discussed within the
wenzelm
parents: 12621
diff changeset
   316
%   formal model.
10993
883248dcf3f8 added Unix example;
wenzelm
parents: 10160
diff changeset
   317
  
12879
wenzelm
parents: 12621
diff changeset
   318
%   This example represents a non-trivial verification task, with all proofs
wenzelm
parents: 12621
diff changeset
   319
%   carefully worked out using the proper part of the Isar proof language;
wenzelm
parents: 12621
diff changeset
   320
%   unstructured scripts are only used for symbolic evaluation.
wenzelm
parents: 12621
diff changeset
   321
% \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
wenzelm
parents: 12621
diff changeset
   322
%   formalization of a fragment of Java, together with a corresponding virtual
wenzelm
parents: 12621
diff changeset
   323
%   machine and a specification of its bytecode verifier and a lightweight
wenzelm
parents: 12621
diff changeset
   324
%   bytecode verifier, including proofs of type-safety.
10993
883248dcf3f8 added Unix example;
wenzelm
parents: 10160
diff changeset
   325
  
12879
wenzelm
parents: 12621
diff changeset
   326
%   This represents a very ``realistic'' example of large formalizations
wenzelm
parents: 12621
diff changeset
   327
%   performed in form of tactic emulation scripts and proper Isar proof texts.
wenzelm
parents: 12621
diff changeset
   328
% \end{itemize}
8547
wenzelm
parents: 8516
diff changeset
   329
7167
wenzelm
parents: 7046
diff changeset
   330
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   331
%%% Local Variables: 
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   332
%%% mode: latex
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   333
%%% TeX-master: "isar-ref"
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   334
%%% End: