doc-src/IsarRef/Thy/document/Introduction.tex
author wenzelm
Sat Oct 04 17:40:58 2008 +0200 (2008-10-04)
changeset 28505 f98751bd715f
parent 27057 ecbe1afe800b
child 29717 51ed69c9422b
child 30240 5b25fee0362c
permissions -rw-r--r--
updated generated file;
wenzelm@27035
     1
%
wenzelm@27035
     2
\begin{isabellebody}%
wenzelm@27035
     3
\def\isabellecontext{Introduction}%
wenzelm@27035
     4
%
wenzelm@27035
     5
\isadelimtheory
wenzelm@27035
     6
\isanewline
wenzelm@27035
     7
\isanewline
wenzelm@27035
     8
%
wenzelm@27035
     9
\endisadelimtheory
wenzelm@27035
    10
%
wenzelm@27035
    11
\isatagtheory
wenzelm@27035
    12
\isacommand{theory}\isamarkupfalse%
wenzelm@27035
    13
\ Introduction\isanewline
wenzelm@27052
    14
\isakeyword{imports}\ Main\isanewline
wenzelm@27035
    15
\isakeyword{begin}%
wenzelm@27035
    16
\endisatagtheory
wenzelm@27035
    17
{\isafoldtheory}%
wenzelm@27035
    18
%
wenzelm@27035
    19
\isadelimtheory
wenzelm@27035
    20
%
wenzelm@27035
    21
\endisadelimtheory
wenzelm@27035
    22
%
wenzelm@27035
    23
\isamarkupchapter{Introduction%
wenzelm@27035
    24
}
wenzelm@27035
    25
\isamarkuptrue%
wenzelm@27035
    26
%
wenzelm@27035
    27
\isamarkupsection{Overview%
wenzelm@27035
    28
}
wenzelm@27035
    29
\isamarkuptrue%
wenzelm@27035
    30
%
wenzelm@27035
    31
\begin{isamarkuptext}%
wenzelm@27035
    32
The \emph{Isabelle} system essentially provides a generic
wenzelm@27035
    33
  infrastructure for building deductive systems (programmed in
wenzelm@27035
    34
  Standard ML), with a special focus on interactive theorem proving in
wenzelm@27035
    35
  higher-order logics.  In the olden days even end-users would refer
wenzelm@27035
    36
  to certain ML functions (goal commands, tactics, tacticals etc.) to
wenzelm@27035
    37
  pursue their everyday theorem proving tasks
wenzelm@27035
    38
  \cite{isabelle-intro,isabelle-ref}.
wenzelm@27035
    39
  
wenzelm@27035
    40
  In contrast \emph{Isar} provides an interpreted language environment
wenzelm@27035
    41
  of its own, which has been specifically tailored for the needs of
wenzelm@27035
    42
  theory and proof development.  Compared to raw ML, the Isabelle/Isar
wenzelm@27035
    43
  top-level provides a more robust and comfortable development
wenzelm@27035
    44
  platform, with proper support for theory development graphs,
wenzelm@27035
    45
  single-step transactions with unlimited undo, etc.  The
wenzelm@27035
    46
  Isabelle/Isar version of the \emph{Proof~General} user interface
wenzelm@27035
    47
  \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
wenzelm@27035
    48
  front-end for interactive theory and proof development in this
wenzelm@27035
    49
  advanced theorem proving environment.
wenzelm@27035
    50
wenzelm@27035
    51
  \medskip Apart from the technical advances over bare-bones ML
wenzelm@27035
    52
  programming, the main purpose of the Isar language is to provide a
wenzelm@27035
    53
  conceptually different view on machine-checked proofs
wenzelm@27035
    54
  \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  ``Isar'' stands for
wenzelm@27035
    55
  ``Intelligible semi-automated reasoning''.  Drawing from both the
wenzelm@27035
    56
  traditions of informal mathematical proof texts and high-level
wenzelm@27035
    57
  programming languages, Isar offers a versatile environment for
wenzelm@27035
    58
  structured formal proof documents.  Thus properly written Isar
wenzelm@27035
    59
  proofs become accessible to a broader audience than unstructured
wenzelm@27035
    60
  tactic scripts (which typically only provide operational information
wenzelm@27035
    61
  for the machine).  Writing human-readable proof texts certainly
wenzelm@27035
    62
  requires some additional efforts by the writer to achieve a good
wenzelm@27035
    63
  presentation, both of formal and informal parts of the text.  On the
wenzelm@27035
    64
  other hand, human-readable formal texts gain some value in their own
wenzelm@27035
    65
  right, independently of the mechanic proof-checking process.
wenzelm@27035
    66
wenzelm@27035
    67
  Despite its grand design of structured proof texts, Isar is able to
wenzelm@27035
    68
  assimilate the old tactical style as an ``improper'' sub-language.
wenzelm@27035
    69
  This provides an easy upgrade path for existing tactic scripts, as
wenzelm@27035
    70
  well as additional means for interactive experimentation and
wenzelm@27035
    71
  debugging of structured proofs.  Isabelle/Isar supports a broad
wenzelm@27035
    72
  range of proof styles, both readable and unreadable ones.
wenzelm@27035
    73
wenzelm@27057
    74
  \medskip The Isabelle/Isar framework \cite{Wenzel:2006:Festschrift}
wenzelm@27057
    75
  is generic and should work reasonably well for any Isabelle
wenzelm@27057
    76
  object-logic that conforms to the natural deduction view of the
wenzelm@27057
    77
  Isabelle/Pure framework.  Specific language elements introduced by
wenzelm@27057
    78
  the major object-logics are described in \chref{ch:hol}
wenzelm@27057
    79
  (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
wenzelm@27057
    80
  (Isabelle/ZF).  The main language elements are already provided by
wenzelm@27057
    81
  the Isabelle/Pure framework. Nevertheless, examples given in the
wenzelm@27057
    82
  generic parts will usually refer to Isabelle/HOL as well.
wenzelm@27042
    83
wenzelm@27042
    84
  \medskip Isar commands may be either \emph{proper} document
wenzelm@27042
    85
  constructors, or \emph{improper commands}.  Some proof methods and
wenzelm@27042
    86
  attributes introduced later are classified as improper as well.
wenzelm@27042
    87
  Improper Isar language elements, which are marked by ``\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}'' in the subsequent chapters; they are often helpful
wenzelm@27042
    88
  when developing proof documents, but their use is discouraged for
wenzelm@27042
    89
  the final human-readable outcome.  Typical examples are diagnostic
wenzelm@27042
    90
  commands that print terms or theorems according to the current
wenzelm@27042
    91
  context; other commands emulate old-style tactical theorem proving.%
wenzelm@27035
    92
\end{isamarkuptext}%
wenzelm@27035
    93
\isamarkuptrue%
wenzelm@27035
    94
%
wenzelm@27052
    95
\isamarkupsection{User interfaces%
wenzelm@27035
    96
}
wenzelm@27035
    97
\isamarkuptrue%
wenzelm@27035
    98
%
wenzelm@27035
    99
\isamarkupsubsection{Terminal sessions%
wenzelm@27035
   100
}
wenzelm@27035
   101
\isamarkuptrue%
wenzelm@27035
   102
%
wenzelm@27035
   103
\begin{isamarkuptext}%
wenzelm@27036
   104
The Isabelle \texttt{tty} tool provides a very interface for running
wenzelm@27036
   105
  the Isar interaction loop, with some support for command line
wenzelm@27036
   106
  editing.  For example:
wenzelm@27035
   107
\begin{ttbox}
wenzelm@28505
   108
isabelle tty\medskip
wenzelm@27036
   109
{\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
wenzelm@27035
   110
theory Foo imports Main begin;
wenzelm@27035
   111
definition foo :: nat where "foo == 1";
wenzelm@27035
   112
lemma "0 < foo" by (simp add: foo_def);
wenzelm@27035
   113
end;
wenzelm@27035
   114
\end{ttbox}
wenzelm@27035
   115
wenzelm@27036
   116
  Any Isabelle/Isar command may be retracted by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}.
wenzelm@27036
   117
  See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
wenzelm@27036
   118
  comprehensive overview of available commands and other language
wenzelm@27036
   119
  elements.%
wenzelm@27035
   120
\end{isamarkuptext}%
wenzelm@27035
   121
\isamarkuptrue%
wenzelm@27035
   122
%
wenzelm@27042
   123
\isamarkupsubsection{Emacs Proof General%
wenzelm@27035
   124
}
wenzelm@27035
   125
\isamarkuptrue%
wenzelm@27035
   126
%
wenzelm@27035
   127
\begin{isamarkuptext}%
wenzelm@27035
   128
Plain TTY-based interaction as above used to be quite feasible with
wenzelm@27035
   129
  traditional tactic based theorem proving, but developing Isar
wenzelm@27035
   130
  documents really demands some better user-interface support.  The
wenzelm@27035
   131
  Proof~General environment by David Aspinall
wenzelm@27035
   132
  \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
wenzelm@27035
   133
  interface for interactive theorem provers that organizes all the
wenzelm@27035
   134
  cut-and-paste and forward-backward walk through the text in a very
wenzelm@27035
   135
  neat way.  In Isabelle/Isar, the current position within a partial
wenzelm@27035
   136
  proof document is equally important than the actual proof state.
wenzelm@27035
   137
  Thus Proof~General provides the canonical working environment for
wenzelm@27035
   138
  Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
wenzelm@27035
   139
  existing Isar documents) and for production work.%
wenzelm@27035
   140
\end{isamarkuptext}%
wenzelm@27035
   141
\isamarkuptrue%
wenzelm@27035
   142
%
wenzelm@27035
   143
\isamarkupsubsubsection{Proof~General as default Isabelle interface%
wenzelm@27035
   144
}
wenzelm@27035
   145
\isamarkuptrue%
wenzelm@27035
   146
%
wenzelm@27035
   147
\begin{isamarkuptext}%
wenzelm@27035
   148
The Isabelle interface wrapper script provides an easy way to invoke
wenzelm@27035
   149
  Proof~General (including XEmacs or GNU Emacs).  The default
wenzelm@27035
   150
  configuration of Isabelle is smart enough to detect the
wenzelm@27035
   151
  Proof~General distribution in several canonical places (e.g.\
wenzelm@27035
   152
  \verb|$ISABELLE_HOME/contrib/ProofGeneral|).  Thus the
wenzelm@27035
   153
  capital \verb|Isabelle| executable would already refer to the
wenzelm@27035
   154
  \verb|ProofGeneral/isar| interface without further ado.  The
wenzelm@27035
   155
  Isabelle interface script provides several options; pass \verb|-?|  to see its usage.
wenzelm@27035
   156
wenzelm@27035
   157
  With the proper Isabelle interface setup, Isar documents may now be edited by
wenzelm@27035
   158
  visiting appropriate theory files, e.g.\ 
wenzelm@27035
   159
\begin{ttbox}
wenzelm@27035
   160
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
wenzelm@27035
   161
\end{ttbox}
wenzelm@27035
   162
  Beginners may note the tool bar for navigating forward and backward
wenzelm@27035
   163
  through the text (this depends on the local Emacs installation).
wenzelm@27035
   164
  Consult the Proof~General documentation \cite{proofgeneral} for
wenzelm@27035
   165
  further basic command sequences, in particular ``\verb|C-c C-return|''
wenzelm@27035
   166
  and ``\verb|C-c u|''.
wenzelm@27035
   167
wenzelm@27035
   168
  \medskip Proof~General may be also configured manually by giving
wenzelm@27035
   169
  Isabelle settings like this (see also \cite{isabelle-sys}):
wenzelm@27035
   170
wenzelm@27035
   171
\begin{ttbox}
wenzelm@27035
   172
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
wenzelm@27035
   173
PROOFGENERAL_OPTIONS=""
wenzelm@27035
   174
\end{ttbox}
wenzelm@27035
   175
  You may have to change \verb|$ISABELLE_HOME/contrib/ProofGeneral| to the actual installation
wenzelm@27035
   176
  directory of Proof~General.
wenzelm@27035
   177
wenzelm@27035
   178
  \medskip Apart from the Isabelle command line, defaults for
wenzelm@27035
   179
  interface options may be given by the \verb|PROOFGENERAL_OPTIONS|
wenzelm@27035
   180
  setting.  For example, the Emacs executable to be used may be
wenzelm@27035
   181
  configured in Isabelle's settings like this:
wenzelm@27035
   182
\begin{ttbox}
wenzelm@27035
   183
PROOFGENERAL_OPTIONS="-p xemacs-mule"  
wenzelm@27035
   184
\end{ttbox}
wenzelm@27035
   185
wenzelm@27035
   186
  Occasionally, a user's \verb|~/.emacs| file contains code
wenzelm@27035
   187
  that is incompatible with the (X)Emacs version used by
wenzelm@27035
   188
  Proof~General, causing the interface startup to fail prematurely.
wenzelm@27035
   189
  Here the \verb|-u false| option helps to get the interface
wenzelm@27035
   190
  process up and running.  Note that additional Lisp customization
wenzelm@27035
   191
  code may reside in \verb|proofgeneral-settings.el| of
wenzelm@27035
   192
  \verb|$ISABELLE_HOME/etc| or \verb|$ISABELLE_HOME_USER/etc|.%
wenzelm@27035
   193
\end{isamarkuptext}%
wenzelm@27035
   194
\isamarkuptrue%
wenzelm@27035
   195
%
wenzelm@27035
   196
\isamarkupsubsubsection{The X-Symbol package%
wenzelm@27035
   197
}
wenzelm@27035
   198
\isamarkuptrue%
wenzelm@27035
   199
%
wenzelm@27035
   200
\begin{isamarkuptext}%
wenzelm@27035
   201
Proof~General incorporates a version of the Emacs X-Symbol package
wenzelm@27035
   202
  \cite{x-symbol}, which handles proper mathematical symbols displayed
wenzelm@27035
   203
  on screen.  Pass option \verb|-x true| to the Isabelle
wenzelm@27035
   204
  interface script, or check the appropriate Proof~General menu
wenzelm@27035
   205
  setting by hand.  The main challenge of getting X-Symbol to work
wenzelm@27035
   206
  properly is the underlying (semi-automated) X11 font setup.
wenzelm@27035
   207
wenzelm@27035
   208
  \medskip Using proper mathematical symbols in Isabelle theories can
wenzelm@27035
   209
  be very convenient for readability of large formulas.  On the other
wenzelm@27035
   210
  hand, the plain ASCII sources easily become somewhat unintelligible.
wenzelm@27035
   211
  For example, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} would appear as \verb|\<Longrightarrow>| according
wenzelm@27035
   212
  the default set of Isabelle symbols.  Nevertheless, the Isabelle
wenzelm@27042
   213
  document preparation system (see \chref{ch:document-prep}) will be
wenzelm@27035
   214
  happy to print non-ASCII symbols properly.  It is even possible to
wenzelm@27035
   215
  invent additional notation beyond the display capabilities of Emacs
wenzelm@27035
   216
  and X-Symbol.%
wenzelm@27035
   217
\end{isamarkuptext}%
wenzelm@27035
   218
\isamarkuptrue%
wenzelm@27035
   219
%
wenzelm@27035
   220
\isamarkupsection{Isabelle/Isar theories%
wenzelm@27035
   221
}
wenzelm@27035
   222
\isamarkuptrue%
wenzelm@27035
   223
%
wenzelm@27035
   224
\begin{isamarkuptext}%
wenzelm@27035
   225
Isabelle/Isar offers the following main improvements over classic
wenzelm@27035
   226
  Isabelle.
wenzelm@27035
   227
wenzelm@27035
   228
  \begin{enumerate}
wenzelm@27035
   229
  
wenzelm@27035
   230
  \item A \emph{theory format} that integrates specifications and
wenzelm@27035
   231
  proofs, supporting interactive development and unlimited undo
wenzelm@27035
   232
  operation.
wenzelm@27035
   233
  
wenzelm@27035
   234
  \item A \emph{formal proof document language} designed to support
wenzelm@27035
   235
  intelligible semi-automated reasoning.  Instead of putting together
wenzelm@27035
   236
  unreadable tactic scripts, the author is enabled to express the
wenzelm@27035
   237
  reasoning in way that is close to usual mathematical practice.  The
wenzelm@27035
   238
  old tactical style has been assimilated as ``improper'' language
wenzelm@27035
   239
  elements.
wenzelm@27035
   240
  
wenzelm@27035
   241
  \item A simple document preparation system, for typesetting formal
wenzelm@27035
   242
  developments together with informal text.  The resulting
wenzelm@27035
   243
  hyper-linked PDF documents are equally well suited for WWW
wenzelm@27035
   244
  presentation and as printed copies.
wenzelm@27035
   245
wenzelm@27035
   246
  \end{enumerate}
wenzelm@27035
   247
wenzelm@27035
   248
  The Isar proof language is embedded into the new theory format as a
wenzelm@27035
   249
  proper sub-language.  Proof mode is entered by stating some
wenzelm@27035
   250
  \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory level, and
wenzelm@27035
   251
  left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).
wenzelm@27035
   252
  A few theory specification mechanisms also require some proof, such
wenzelm@27035
   253
  as HOL's \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} which demands non-emptiness of the
wenzelm@27035
   254
  representing sets.%
wenzelm@27035
   255
\end{isamarkuptext}%
wenzelm@27035
   256
\isamarkuptrue%
wenzelm@27035
   257
%
wenzelm@27052
   258
\isamarkupsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
wenzelm@27035
   259
}
wenzelm@27035
   260
\isamarkuptrue%
wenzelm@27035
   261
%
wenzelm@27035
   262
\begin{isamarkuptext}%
wenzelm@27035
   263
This is one of the key questions, of course.  First of all, the
wenzelm@27035
   264
  tactic script emulation of Isabelle/Isar essentially provides a
wenzelm@27035
   265
  clarified version of the very same unstructured proof style of
wenzelm@27035
   266
  classic Isabelle.  Old-time users should quickly become acquainted
wenzelm@27035
   267
  with that (slightly degenerative) view of Isar.
wenzelm@27035
   268
wenzelm@27035
   269
  Writing \emph{proper} Isar proof texts targeted at human readers is
wenzelm@27035
   270
  quite different, though.  Experienced users of the unstructured
wenzelm@27035
   271
  style may even have to unlearn some of their habits to master proof
wenzelm@27035
   272
  composition in Isar.  In contrast, new users with less experience in
wenzelm@27035
   273
  old-style tactical proving, but a good understanding of mathematical
wenzelm@27035
   274
  proof in general, often get started easier.
wenzelm@27035
   275
wenzelm@27035
   276
  \medskip The present text really is only a reference manual on
wenzelm@27035
   277
  Isabelle/Isar, not a tutorial.  Nevertheless, we will attempt to
wenzelm@27035
   278
  give some clues of how the concepts introduced here may be put into
wenzelm@27035
   279
  practice.  Especially note that \appref{ap:refcard} provides a quick
wenzelm@27035
   280
  reference card of the most common Isabelle/Isar language elements.
wenzelm@27035
   281
wenzelm@27035
   282
  Further issues concerning the Isar concepts are covered in the
wenzelm@27035
   283
  literature
wenzelm@27035
   284
  \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
wenzelm@27035
   285
  The author's PhD thesis \cite{Wenzel-PhD} presently provides the
wenzelm@27035
   286
  most complete exposition of Isar foundations, techniques, and
wenzelm@27035
   287
  applications.  A number of example applications are distributed with
wenzelm@27035
   288
  Isabelle, and available via the Isabelle WWW library (e.g.\
wenzelm@27035
   289
  \url{http://isabelle.in.tum.de/library/}).  The ``Archive of Formal
wenzelm@27035
   290
  Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
wenzelm@27035
   291
  examples, both in proper Isar proof style and unstructured tactic
wenzelm@27035
   292
  scripts.%
wenzelm@27035
   293
\end{isamarkuptext}%
wenzelm@27035
   294
\isamarkuptrue%
wenzelm@27035
   295
%
wenzelm@27035
   296
\isadelimtheory
wenzelm@27035
   297
%
wenzelm@27035
   298
\endisadelimtheory
wenzelm@27035
   299
%
wenzelm@27035
   300
\isatagtheory
wenzelm@27035
   301
\isacommand{end}\isamarkupfalse%
wenzelm@27035
   302
%
wenzelm@27035
   303
\endisatagtheory
wenzelm@27035
   304
{\isafoldtheory}%
wenzelm@27035
   305
%
wenzelm@27035
   306
\isadelimtheory
wenzelm@27035
   307
%
wenzelm@27035
   308
\endisadelimtheory
wenzelm@27035
   309
\isanewline
wenzelm@27035
   310
\end{isabellebody}%
wenzelm@27035
   311
%%% Local Variables:
wenzelm@27035
   312
%%% mode: latex
wenzelm@27035
   313
%%% TeX-master: "root"
wenzelm@27035
   314
%%% End: