doc-src/IsarRef/intro.tex
author wenzelm
Fri, 10 Nov 2000 19:02:37 +0100
changeset 10432 3dfbc913d184
parent 10160 bb8f9412fec6
child 10993 883248dcf3f8
permissions -rw-r--r--
added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
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
7167
wenzelm
parents: 7046
diff changeset
     4
\section{Quick start}
wenzelm
parents: 7046
diff changeset
     5
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
     6
\subsection{Terminal sessions}
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
     7
7175
wenzelm
parents: 7167
diff changeset
     8
Isar is already part of Isabelle (as of version Isabelle99, or later).  The
9604
wenzelm
parents: 9272
diff changeset
     9
\texttt{isabelle} binary provides option \texttt{-I} to run the Isabelle/Isar
wenzelm
parents: 9272
diff changeset
    10
interaction loop at startup, rather than the raw ML top-level.  So the
wenzelm
parents: 9272
diff changeset
    11
quickest way to do anything with Isabelle/Isar is as follows:
7175
wenzelm
parents: 7167
diff changeset
    12
\begin{ttbox}
wenzelm
parents: 7167
diff changeset
    13
isabelle -I HOL\medskip
9272
19029b7de03c Isabelle99-1;
wenzelm
parents: 9233
diff changeset
    14
\out{> Welcome to Isabelle/HOL (Isabelle99-1)}\medskip
7175
wenzelm
parents: 7167
diff changeset
    15
theory Foo = Main:
7297
wenzelm
parents: 7175
diff changeset
    16
constdefs foo :: nat  "foo == 1";
wenzelm
parents: 7175
diff changeset
    17
lemma "0 < foo" by (simp add: foo_def);
7175
wenzelm
parents: 7167
diff changeset
    18
end
wenzelm
parents: 7167
diff changeset
    19
\end{ttbox}
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 8843
diff changeset
    20
Note that any Isabelle/Isar command may be retracted by \texttt{undo}.  See
10160
wenzelm
parents: 10110
diff changeset
    21
the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
10110
7d6e03a1f11e fixed ref;
wenzelm
parents: 9849
diff changeset
    22
comprehensive overview of available commands and other language elements.
7175
wenzelm
parents: 7167
diff changeset
    23
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    24
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
    25
\subsection{Proof~General}
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    26
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    27
Plain TTY-based interaction as above used to be quite feasible with
8547
wenzelm
parents: 8516
diff changeset
    28
traditional tactic based theorem proving, but developing Isar documents really
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    29
demands some better user-interface support.  David Aspinall's
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    30
\emph{Proof~General}\index{Proof General} environment
8547
wenzelm
parents: 8516
diff changeset
    31
\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs interface for
wenzelm
parents: 8516
diff changeset
    32
interactive theorem provers that does all the cut-and-paste and
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    33
forward-backward walk through the text in a very neat way.  In Isabelle/Isar,
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    34
the current position within a partial proof document is equally important than
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    35
the actual proof state.  Thus Proof~General provides the canonical working
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    36
environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
8547
wenzelm
parents: 8516
diff changeset
    37
existing Isar documents) and for production work.
7175
wenzelm
parents: 7167
diff changeset
    38
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
    39
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
    40
\subsubsection{Proof~General as default Isabelle interface}
7167
wenzelm
parents: 7046
diff changeset
    41
9849
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    42
The easiest way to invoke Proof~General is via the Isabelle interface wrapper
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    43
script.  The default configuration of Isabelle is smart enough to detect the
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    44
Proof~General distribution in several canonical places (e.g.\ 
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    45
\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}).  Thus the capital
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    46
\texttt{Isabelle} executable would already refer to the
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    47
\texttt{ProofGeneral/isar} interface without further ado.\footnote{There is
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    48
  also a \texttt{ProofGeneral/isa} interface for old tactic scripts written in
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    49
  ML.} The Isabelle interface script provides several options, just pass
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    50
\verb,-?, to see its usage.
7981
wenzelm
parents: 7895
diff changeset
    51
7175
wenzelm
parents: 7167
diff changeset
    52
With the proper Isabelle interface setup, Isar documents may now be edited by
wenzelm
parents: 7167
diff changeset
    53
visiting appropriate theory files, e.g.\ 
wenzelm
parents: 7167
diff changeset
    54
\begin{ttbox}
wenzelm
parents: 7167
diff changeset
    55
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
wenzelm
parents: 7167
diff changeset
    56
\end{ttbox}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7297
diff changeset
    57
Users of XEmacs may note the tool bar for navigating forward and backward
8516
f5f6a97ee43f simplified setup;
wenzelm
parents: 8508
diff changeset
    58
through the text.  Consult the Proof~General documentation \cite{proofgeneral}
8547
wenzelm
parents: 8516
diff changeset
    59
for further basic command sequences, such as ``\texttt{C-c C-return}'' or
wenzelm
parents: 8516
diff changeset
    60
``\texttt{C-c u}''.
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    61
9849
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    62
\medskip
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    63
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    64
Proof~General may be also configured manually by giving Isabelle settings like
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    65
this (see also \cite{isabelle-sys}):
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    66
\begin{ttbox}
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    67
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    68
PROOFGENERAL_OPTIONS=""
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    69
\end{ttbox}
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    70
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    71
actual installation directory of Proof~General.
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    72
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    73
\medskip
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    74
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    75
Apart from the Isabelle command line, defaults for interface options may be
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    76
given by the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For example, the
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    77
Emacs executable to be used may be configured in Isabelle's settings like this:
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    78
\begin{ttbox}
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    79
PROOFGENERAL_OPTIONS="-p xemacs-nomule"  
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    80
\end{ttbox}
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    81
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    82
Occasionally, the user's \verb,~/.emacs, file contains material that is
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    83
incompatible with the version of Emacs that Proof~General prefers.  Then
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    84
proper startup may be still achieved by using the \texttt{-u false} option.
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    85
Also note that any Emacs lisp file called \texttt{proofgeneral-settings.el}
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    86
occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    87
is automatically loaded by the Proof~General interface script as well.
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
    88
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
    89
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
    90
\subsubsection{The X-Symbol package}
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    91
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    92
Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    93
provides a nice way to get proper mathematical symbols displayed on screen.
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
    94
Just pass option \texttt{-x true} to the Isabelle interface script, or check
8516
f5f6a97ee43f simplified setup;
wenzelm
parents: 8508
diff changeset
    95
the appropriate menu setting by hand.  In any case, the X-Symbol package must
f5f6a97ee43f simplified setup;
wenzelm
parents: 8508
diff changeset
    96
have been properly installed already.
f5f6a97ee43f simplified setup;
wenzelm
parents: 8508
diff changeset
    97
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
    98
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
    99
package is very easy to install and configures itself automatically.  The
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   100
default configuration of Isabelle is smart enough to detect the X-Symbol
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   101
package in several canonical places (e.g.\ 
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   102
\texttt{\$ISABELLE_HOME/contrib/x-symbol}).
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   103
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   104
\medskip
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   105
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   106
Using proper mathematical symbols in Isabelle theories can be very convenient
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   107
for readability of large formulas.  On the other hand, the plain ASCII sources
10160
wenzelm
parents: 10110
diff changeset
   108
easily become somewhat unintelligible.  For example, $\Longrightarrow$ would
9849
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   109
appear as \verb,\<Longrightarrow>, according the default set of Isabelle
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   110
symbols.  Nevertheless, the Isabelle document preparation system (see
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   111
\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
   112
It is even possible to invent additional notation beyond the display
71ad08ad2cf0 simplified PG/X-Symbol intro;
wenzelm
parents: 9604
diff changeset
   113
capabilities of XEmacs and X-Symbol.
7175
wenzelm
parents: 7167
diff changeset
   114
7981
wenzelm
parents: 7895
diff changeset
   115
wenzelm
parents: 7895
diff changeset
   116
\section{Isabelle/Isar theories}
wenzelm
parents: 7895
diff changeset
   117
8547
wenzelm
parents: 8516
diff changeset
   118
Isabelle/Isar offers the following main improvements over classic Isabelle.
7981
wenzelm
parents: 7895
diff changeset
   119
\begin{enumerate}
wenzelm
parents: 7895
diff changeset
   120
\item A new \emph{theory format}, occasionally referred to as ``new-style
wenzelm
parents: 7895
diff changeset
   121
  theories'', supporting interactive development and unlimited undo operation.
wenzelm
parents: 7895
diff changeset
   122
\item A \emph{formal proof document language} designed to support intelligible
wenzelm
parents: 7895
diff changeset
   123
  semi-automated reasoning.  Instead of putting together unreadable tactic
wenzelm
parents: 7895
diff changeset
   124
  scripts, the author is enabled to express the reasoning in way that is close
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
   125
  to usual mathematical practice.
8547
wenzelm
parents: 8516
diff changeset
   126
\item A simple document preparation system, for typesetting formal
wenzelm
parents: 8516
diff changeset
   127
  developments together with informal text.  The resulting hyper-linked PDF
wenzelm
parents: 8516
diff changeset
   128
  documents are equally well suited for WWW presentation and as printed
wenzelm
parents: 8516
diff changeset
   129
  copies.
7981
wenzelm
parents: 7895
diff changeset
   130
\end{enumerate}
wenzelm
parents: 7895
diff changeset
   131
wenzelm
parents: 7895
diff changeset
   132
The Isar proof language is embedded into the new theory format as a proper
wenzelm
parents: 7895
diff changeset
   133
sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
wenzelm
parents: 7895
diff changeset
   134
$\LEMMANAME$ at the theory level, and left again with the final conclusion
wenzelm
parents: 7895
diff changeset
   135
(e.g.\ via $\QEDNAME$).  A few theory extension mechanisms require proof as
8547
wenzelm
parents: 8516
diff changeset
   136
well, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness of the
wenzelm
parents: 8516
diff changeset
   137
representing sets.
7460
wenzelm
parents: 7335
diff changeset
   138
7981
wenzelm
parents: 7895
diff changeset
   139
New-style theory files may still be associated with separate ML files
wenzelm
parents: 7895
diff changeset
   140
consisting of plain old tactic scripts.  There is no longer any ML binding
wenzelm
parents: 7895
diff changeset
   141
generated for the theory and theorems, though.  ML functions \texttt{theory},
wenzelm
parents: 7895
diff changeset
   142
\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
wenzelm
parents: 7895
diff changeset
   143
Nevertheless, migration between classic Isabelle and Isabelle/Isar is
wenzelm
parents: 7895
diff changeset
   144
relatively easy.  Thus users may start to benefit from interactive theory
8547
wenzelm
parents: 8516
diff changeset
   145
development and document preparation, even before they have any idea of the
wenzelm
parents: 8516
diff changeset
   146
Isar proof language at all.
7981
wenzelm
parents: 7895
diff changeset
   147
wenzelm
parents: 7895
diff changeset
   148
\begin{warn}
8547
wenzelm
parents: 8516
diff changeset
   149
  Currently, Proof~General does \emph{not} support mixed interactive
7981
wenzelm
parents: 7895
diff changeset
   150
  development of classic Isabelle theory files or tactic scripts, together
wenzelm
parents: 7895
diff changeset
   151
  with Isar documents.  The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
wenzelm
parents: 7895
diff changeset
   152
  Proof~General are handled as two different theorem proving systems, only one
wenzelm
parents: 7895
diff changeset
   153
  of these may be active at the same time.
wenzelm
parents: 7895
diff changeset
   154
\end{warn}
wenzelm
parents: 7895
diff changeset
   155
10160
wenzelm
parents: 10110
diff changeset
   156
Conversion of existing tactic scripts is best done by running two separate
7981
wenzelm
parents: 7895
diff changeset
   157
Proof~General sessions, one for replaying the old script and the other for the
10160
wenzelm
parents: 10110
diff changeset
   158
emerging Isabelle/Isar document.  Also note that Isar supports emulation
wenzelm
parents: 10110
diff changeset
   159
commands and methods that support traditional tactic scripts within new-style
wenzelm
parents: 10110
diff changeset
   160
theories, see appendix~\ref{ap:conv} for more information.
7981
wenzelm
parents: 7895
diff changeset
   161
7167
wenzelm
parents: 7046
diff changeset
   162
8843
5370a030dd47 improved X-Symbol stuff;
wenzelm
parents: 8684
diff changeset
   163
\subsection{Document preparation}\label{sec:document-prep}
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   164
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   165
Isabelle/Isar provides a simple document preparation system based on current
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   166
(PDF) {\LaTeX} technology, with full support of hyper-links (both local
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   167
references and URLs), bookmarks, thumbnails etc.  Thus the results are equally
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   168
well suited for WWW browsing and as printed copies.
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   169
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   170
\medskip
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   171
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   172
Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   173
  session} (see also \cite{isabelle-sys}).  Getting started with a working
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   174
configuration for common situations is quite easy by using the Isabelle
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   175
\texttt{mkdir} and \texttt{make} tools.  Just invoke
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   176
\begin{ttbox}
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   177
  isatool mkdir -d Foo
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   178
\end{ttbox}
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   179
to setup a separate directory for session \texttt{Foo}.\footnote{It is safe to
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   180
  experiment, since \texttt{isatool mkdir} never overwrites existing files.}
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   181
Ensure that \texttt{Foo/ROOT.ML} loads all theories required for this session.
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   182
Furthermore \texttt{Foo/document/root.tex} should include any special {\LaTeX}
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   183
macro packages required for your document (the default is usually sufficient
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   184
as a start).
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   185
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   186
The session is controlled by a separate \texttt{IsaMakefile} (with very crude
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   187
source dependencies only by default).  This file is located one level up from
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   188
the \texttt{Foo} directory location.  At that point just invoke
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   189
\begin{ttbox}
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   190
  isatool make Foo
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   191
\end{ttbox}
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   192
to run the \texttt{Foo} session, with browser information and document
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   193
preparation enabled.  Unless any errors are reported by Isabelle or {\LaTeX},
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   194
the output will appear inside the directory indicated by \texttt{isatool
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   195
  getenv ISABELLE_BROWSER_INFO}, with the logical session prefix added (e.g.\ 
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   196
\texttt{HOL/Foo}).  Note that the \texttt{index.html} located there provides a
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   197
link to the finished {\LaTeX} document, too.
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   198
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   199
Note that this really is batch processing --- better let Isabelle check your
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   200
theory and proof developments beforehand in interactive mode.
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   201
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   202
\medskip
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   203
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   204
You may also consider to tune the \texttt{usedir} options in
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   205
\texttt{IsaMakefile}, for example to change the output format from
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   206
\texttt{dvi} to \texttt{pdf}, or activate the \texttt{-D document} option in
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   207
order to preserve a copy of the generated {\LaTeX} sources.  The latter
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   208
feature is very useful for debugging {\LaTeX} errors, while avoiding repeated
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   209
runs of Isabelle.
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   210
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   211
\medskip
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   212
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   213
See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   214
on Isabelle logic sessions and theory presentation.
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   215
dfe444b748aa improved document preparation;
wenzelm
parents: 8547
diff changeset
   216
10160
wenzelm
parents: 10110
diff changeset
   217
\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
7167
wenzelm
parents: 7046
diff changeset
   218
7297
wenzelm
parents: 7175
diff changeset
   219
This is one of the key questions, of course.  Isar offers a rather different
wenzelm
parents: 7175
diff changeset
   220
approach to formal proof documents than plain old tactic scripts.  Experienced
wenzelm
parents: 7175
diff changeset
   221
users of existing interactive theorem proving systems may have to learn
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7875
diff changeset
   222
thinking differently in order to make effective use of Isabelle/Isar.  On the
7297
wenzelm
parents: 7175
diff changeset
   223
other hand, Isabelle/Isar comes much closer to existing mathematical practice
wenzelm
parents: 7175
diff changeset
   224
of formal proof, so users with less experience in old-style tactical proving,
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7875
diff changeset
   225
but a good understanding of mathematical proof, might cope with Isar even
10160
wenzelm
parents: 10110
diff changeset
   226
better.  See also \cite{Wenzel:1999:TPHOL,Bauer-Wenzel:2000:HB} for further
wenzelm
parents: 10110
diff changeset
   227
background information on Isar.
7297
wenzelm
parents: 7175
diff changeset
   228
10160
wenzelm
parents: 10110
diff changeset
   229
\medskip This really is a reference manual on Isabelle/Isar, not a tutorial.
wenzelm
parents: 10110
diff changeset
   230
Nevertheless, we will also give some clues of how the concepts introduced here
wenzelm
parents: 10110
diff changeset
   231
may be put into practice.  Appendix~\ref{ap:refcard} provides a quick
wenzelm
parents: 10110
diff changeset
   232
reference card of the most common Isabelle/Isar language elements.
wenzelm
parents: 10110
diff changeset
   233
Appendix~\ref{ap:conv} offers some practical hints on converting existing
wenzelm
parents: 10110
diff changeset
   234
Isabelle theories and proof scripts to the new format.
wenzelm
parents: 10110
diff changeset
   235
wenzelm
parents: 10110
diff changeset
   236
Several example applications are distributed with Isabelle, and available via
wenzelm
parents: 10110
diff changeset
   237
the Isabelle WWW library as well as the Isabelle/Isar page:
7836
7a9270282fd3 a4paper;
wenzelm
parents: 7532
diff changeset
   238
\begin{center}\small
7a9270282fd3 a4paper;
wenzelm
parents: 7532
diff changeset
   239
  \begin{tabular}{l}
7a9270282fd3 a4paper;
wenzelm
parents: 7532
diff changeset
   240
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
8516
f5f6a97ee43f simplified setup;
wenzelm
parents: 8508
diff changeset
   241
    \url{http://isabelle.in.tum.de/library/} \\[1ex]
8508
76d8d8aab881 simplified Proof General setup;
wenzelm
parents: 7987
diff changeset
   242
    \url{http://isabelle.in.tum.de/Isar/} \\
7836
7a9270282fd3 a4paper;
wenzelm
parents: 7532
diff changeset
   243
  \end{tabular}
7a9270282fd3 a4paper;
wenzelm
parents: 7532
diff changeset
   244
\end{center}
7a9270282fd3 a4paper;
wenzelm
parents: 7532
diff changeset
   245
10160
wenzelm
parents: 10110
diff changeset
   246
The following examples may be of particular interest.  Apart from the plain
wenzelm
parents: 10110
diff changeset
   247
sources represented in HTML, these Isabelle sessions also provide actual
wenzelm
parents: 10110
diff changeset
   248
documents (in PDF).
wenzelm
parents: 10110
diff changeset
   249
\begin{itemize}
wenzelm
parents: 10110
diff changeset
   250
\item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
wenzelm
parents: 10110
diff changeset
   251
  collection of introductory examples.
wenzelm
parents: 10110
diff changeset
   252
\item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
wenzelm
parents: 10110
diff changeset
   253
  typical mathematics-style reasoning in ``axiomatic'' structures.
wenzelm
parents: 10110
diff changeset
   254
\item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
wenzelm
parents: 10110
diff changeset
   255
  big mathematics application on infinitary vector spaces and functional
wenzelm
parents: 10110
diff changeset
   256
  analysis.
wenzelm
parents: 10110
diff changeset
   257
\item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
wenzelm
parents: 10110
diff changeset
   258
  properties of $\lambda$-calculus (Church-Rosser and termination).  This may
wenzelm
parents: 10110
diff changeset
   259
  serve as a realistic example of porting of legacy proof scripts into Isar
wenzelm
parents: 10110
diff changeset
   260
  tactic emulation scripts.
wenzelm
parents: 10110
diff changeset
   261
\item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
wenzelm
parents: 10110
diff changeset
   262
  formalization of a fragment of Java, together with a corresponding virtual
wenzelm
parents: 10110
diff changeset
   263
  machine and a specification of its bytecode verifier and a lightweight
wenzelm
parents: 10110
diff changeset
   264
  bytecode verifier, including proofs of type-safety.  This represents a very
wenzelm
parents: 10110
diff changeset
   265
  ``realistic'' example of large formalizations performed in either form of
wenzelm
parents: 10110
diff changeset
   266
  legacy scripts, tactic emulation scripts, and proper Isar proof texts.
wenzelm
parents: 10110
diff changeset
   267
\end{itemize}
8547
wenzelm
parents: 8516
diff changeset
   268
7167
wenzelm
parents: 7046
diff changeset
   269
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   270
%%% Local Variables: 
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   271
%%% mode: latex
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   272
%%% TeX-master: "isar-ref"
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   273
%%% End: