1.1 --- a/doc-src/IsarRef/Thy/Introduction.thy Sun Feb 15 18:50:51 2009 +0100
1.2 +++ b/doc-src/IsarRef/Thy/Introduction.thy Sun Feb 15 18:53:41 2009 +0100
1.3 @@ -10,27 +10,27 @@
1.4 The \emph{Isabelle} system essentially provides a generic
1.5 infrastructure for building deductive systems (programmed in
1.6 Standard ML), with a special focus on interactive theorem proving in
1.7 - higher-order logics. In the olden days even end-users would refer
1.8 - to certain ML functions (goal commands, tactics, tacticals etc.) to
1.9 - pursue their everyday theorem proving tasks
1.10 - \cite{isabelle-intro,isabelle-ref}.
1.11 + higher-order logics. Many years ago, even end-users would refer to
1.12 + certain ML functions (goal commands, tactics, tacticals etc.) to
1.13 + pursue their everyday theorem proving tasks.
1.14
1.15 In contrast \emph{Isar} provides an interpreted language environment
1.16 of its own, which has been specifically tailored for the needs of
1.17 theory and proof development. Compared to raw ML, the Isabelle/Isar
1.18 top-level provides a more robust and comfortable development
1.19 - platform, with proper support for theory development graphs,
1.20 - single-step transactions with unlimited undo, etc. The
1.21 - Isabelle/Isar version of the \emph{Proof~General} user interface
1.22 - \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
1.23 - front-end for interactive theory and proof development in this
1.24 - advanced theorem proving environment.
1.25 + platform, with proper support for theory development graphs, managed
1.26 + transactions with unlimited undo etc. The Isabelle/Isar version of
1.27 + the \emph{Proof~General} user interface
1.28 + \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
1.29 + for interactive theory and proof development in this advanced
1.30 + theorem proving environment, even though it is somewhat biased
1.31 + towards old-style proof scripts.
1.32
1.33 \medskip Apart from the technical advances over bare-bones ML
1.34 programming, the main purpose of the Isar language is to provide a
1.35 conceptually different view on machine-checked proofs
1.36 - \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
1.37 - ``Intelligible semi-automated reasoning''. Drawing from both the
1.38 + \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. \emph{Isar} stands for
1.39 + \emph{Intelligible semi-automated reasoning}. Drawing from both the
1.40 traditions of informal mathematical proof texts and high-level
1.41 programming languages, Isar offers a versatile environment for
1.42 structured formal proof documents. Thus properly written Isar
1.43 @@ -45,15 +45,15 @@
1.44 Despite its grand design of structured proof texts, Isar is able to
1.45 assimilate the old tactical style as an ``improper'' sub-language.
1.46 This provides an easy upgrade path for existing tactic scripts, as
1.47 - well as additional means for interactive experimentation and
1.48 - debugging of structured proofs. Isabelle/Isar supports a broad
1.49 - range of proof styles, both readable and unreadable ones.
1.50 + well as some means for interactive experimentation and debugging of
1.51 + structured proofs. Isabelle/Isar supports a broad range of proof
1.52 + styles, both readable and unreadable ones.
1.53
1.54 \medskip The generic Isabelle/Isar framework (see
1.55 - \chref{ch:isar-framework}) should work reasonably well for any
1.56 - Isabelle object-logic that conforms to the natural deduction view of
1.57 - the Isabelle/Pure framework. Specific language elements introduced
1.58 - by the major object-logics are described in \chref{ch:hol}
1.59 + \chref{ch:isar-framework}) works reasonably well for any Isabelle
1.60 + object-logic that conforms to the natural deduction view of the
1.61 + Isabelle/Pure framework. Specific language elements introduced by
1.62 + the major object-logics are described in \chref{ch:hol}
1.63 (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
1.64 (Isabelle/ZF). The main language elements are already provided by
1.65 the Isabelle/Pure framework. Nevertheless, examples given in the
1.66 @@ -70,194 +70,4 @@
1.67 context; other commands emulate old-style tactical theorem proving.
1.68 *}
1.69
1.70 -
1.71 -section {* User interfaces *}
1.72 -
1.73 -subsection {* Terminal sessions *}
1.74 -
1.75 -text {*
1.76 - The Isabelle \texttt{tty} tool provides a very interface for running
1.77 - the Isar interaction loop, with some support for command line
1.78 - editing. For example:
1.79 -\begin{ttbox}
1.80 -isabelle tty\medskip
1.81 -{\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
1.82 -theory Foo imports Main begin;
1.83 -definition foo :: nat where "foo == 1";
1.84 -lemma "0 < foo" by (simp add: foo_def);
1.85 -end;
1.86 -\end{ttbox}
1.87 -
1.88 - Any Isabelle/Isar command may be retracted by @{command undo}.
1.89 - See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
1.90 - comprehensive overview of available commands and other language
1.91 - elements.
1.92 -*}
1.93 -
1.94 -
1.95 -subsection {* Emacs Proof General *}
1.96 -
1.97 -text {*
1.98 - Plain TTY-based interaction as above used to be quite feasible with
1.99 - traditional tactic based theorem proving, but developing Isar
1.100 - documents really demands some better user-interface support. The
1.101 - Proof~General environment by David Aspinall
1.102 - \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
1.103 - interface for interactive theorem provers that organizes all the
1.104 - cut-and-paste and forward-backward walk through the text in a very
1.105 - neat way. In Isabelle/Isar, the current position within a partial
1.106 - proof document is equally important than the actual proof state.
1.107 - Thus Proof~General provides the canonical working environment for
1.108 - Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
1.109 - existing Isar documents) and for production work.
1.110 -*}
1.111 -
1.112 -
1.113 -subsubsection{* Proof~General as default Isabelle interface *}
1.114 -
1.115 -text {*
1.116 - The Isabelle interface wrapper script provides an easy way to invoke
1.117 - Proof~General (including XEmacs or GNU Emacs). The default
1.118 - configuration of Isabelle is smart enough to detect the
1.119 - Proof~General distribution in several canonical places (e.g.\
1.120 - @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}). Thus the
1.121 - capital @{verbatim Isabelle} executable would already refer to the
1.122 - @{verbatim "ProofGeneral/isar"} interface without further ado. The
1.123 - Isabelle interface script provides several options; pass @{verbatim
1.124 - "-?"} to see its usage.
1.125 -
1.126 - With the proper Isabelle interface setup, Isar documents may now be edited by
1.127 - visiting appropriate theory files, e.g.\
1.128 -\begin{ttbox}
1.129 -Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
1.130 -\end{ttbox}
1.131 - Beginners may note the tool bar for navigating forward and backward
1.132 - through the text (this depends on the local Emacs installation).
1.133 - Consult the Proof~General documentation \cite{proofgeneral} for
1.134 - further basic command sequences, in particular ``@{verbatim "C-c C-return"}''
1.135 - and ``@{verbatim "C-c u"}''.
1.136 -
1.137 - \medskip Proof~General may be also configured manually by giving
1.138 - Isabelle settings like this (see also \cite{isabelle-sys}):
1.139 -
1.140 -\begin{ttbox}
1.141 -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
1.142 -PROOFGENERAL_OPTIONS=""
1.143 -\end{ttbox}
1.144 - You may have to change @{verbatim
1.145 - "$ISABELLE_HOME/contrib/ProofGeneral"} to the actual installation
1.146 - directory of Proof~General.
1.147 -
1.148 - \medskip Apart from the Isabelle command line, defaults for
1.149 - interface options may be given by the @{verbatim PROOFGENERAL_OPTIONS}
1.150 - setting. For example, the Emacs executable to be used may be
1.151 - configured in Isabelle's settings like this:
1.152 -\begin{ttbox}
1.153 -PROOFGENERAL_OPTIONS="-p xemacs-mule"
1.154 -\end{ttbox}
1.155 -
1.156 - Occasionally, a user's @{verbatim "~/.emacs"} file contains code
1.157 - that is incompatible with the (X)Emacs version used by
1.158 - Proof~General, causing the interface startup to fail prematurely.
1.159 - Here the @{verbatim "-u false"} option helps to get the interface
1.160 - process up and running. Note that additional Lisp customization
1.161 - code may reside in @{verbatim "proofgeneral-settings.el"} of
1.162 - @{verbatim "$ISABELLE_HOME/etc"} or @{verbatim
1.163 - "$ISABELLE_HOME_USER/etc"}.
1.164 -*}
1.165 -
1.166 -
1.167 -subsubsection {* The X-Symbol package *}
1.168 -
1.169 -text {*
1.170 - Proof~General incorporates a version of the Emacs X-Symbol package
1.171 - \cite{x-symbol}, which handles proper mathematical symbols displayed
1.172 - on screen. Pass option @{verbatim "-x true"} to the Isabelle
1.173 - interface script, or check the appropriate Proof~General menu
1.174 - setting by hand. The main challenge of getting X-Symbol to work
1.175 - properly is the underlying (semi-automated) X11 font setup.
1.176 -
1.177 - \medskip Using proper mathematical symbols in Isabelle theories can
1.178 - be very convenient for readability of large formulas. On the other
1.179 - hand, the plain ASCII sources easily become somewhat unintelligible.
1.180 - For example, @{text "\<Longrightarrow>"} would appear as @{verbatim "\<Longrightarrow>"} according
1.181 - the default set of Isabelle symbols. Nevertheless, the Isabelle
1.182 - document preparation system (see \chref{ch:document-prep}) will be
1.183 - happy to print non-ASCII symbols properly. It is even possible to
1.184 - invent additional notation beyond the display capabilities of Emacs
1.185 - and X-Symbol.
1.186 -*}
1.187 -
1.188 -
1.189 -section {* Isabelle/Isar theories *}
1.190 -
1.191 -text {*
1.192 - Isabelle/Isar offers the following main improvements over classic
1.193 - Isabelle.
1.194 -
1.195 - \begin{enumerate}
1.196 -
1.197 - \item A \emph{theory format} that integrates specifications and
1.198 - proofs, supporting interactive development and unlimited undo
1.199 - operation.
1.200 -
1.201 - \item A \emph{formal proof document language} designed to support
1.202 - intelligible semi-automated reasoning. Instead of putting together
1.203 - unreadable tactic scripts, the author is enabled to express the
1.204 - reasoning in way that is close to usual mathematical practice. The
1.205 - old tactical style has been assimilated as ``improper'' language
1.206 - elements.
1.207 -
1.208 - \item A simple document preparation system, for typesetting formal
1.209 - developments together with informal text. The resulting
1.210 - hyper-linked PDF documents are equally well suited for WWW
1.211 - presentation and as printed copies.
1.212 -
1.213 - \end{enumerate}
1.214 -
1.215 - The Isar proof language is embedded into the new theory format as a
1.216 - proper sub-language. Proof mode is entered by stating some
1.217 - @{command theorem} or @{command lemma} at the theory level, and
1.218 - left again with the final conclusion (e.g.\ via @{command qed}).
1.219 - A few theory specification mechanisms also require some proof, such
1.220 - as HOL's @{command typedef} which demands non-emptiness of the
1.221 - representing sets.
1.222 -*}
1.223 -
1.224 -
1.225 -section {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
1.226 -
1.227 -text {*
1.228 - This is one of the key questions, of course. First of all, the
1.229 - tactic script emulation of Isabelle/Isar essentially provides a
1.230 - clarified version of the very same unstructured proof style of
1.231 - classic Isabelle. Old-time users should quickly become acquainted
1.232 - with that (slightly degenerative) view of Isar.
1.233 -
1.234 - Writing \emph{proper} Isar proof texts targeted at human readers is
1.235 - quite different, though. Experienced users of the unstructured
1.236 - style may even have to unlearn some of their habits to master proof
1.237 - composition in Isar. In contrast, new users with less experience in
1.238 - old-style tactical proving, but a good understanding of mathematical
1.239 - proof in general, often get started easier.
1.240 -
1.241 - \medskip The present text really is only a reference manual on
1.242 - Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
1.243 - give some clues of how the concepts introduced here may be put into
1.244 - practice. Especially note that \appref{ap:refcard} provides a quick
1.245 - reference card of the most common Isabelle/Isar language elements.
1.246 -
1.247 - Further issues concerning the Isar concepts are covered in the
1.248 - literature
1.249 - \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
1.250 - The author's PhD thesis \cite{Wenzel-PhD} presently provides the
1.251 - most complete exposition of Isar foundations, techniques, and
1.252 - applications. A number of example applications are distributed with
1.253 - Isabelle, and available via the Isabelle WWW library (e.g.\
1.254 - \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
1.255 - Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
1.256 - examples, both in proper Isar proof style and unstructured tactic
1.257 - scripts.
1.258 -*}
1.259 -
1.260 end