summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/IsarRef/intro.tex

changeset 7981 | 5120a2a15d06 |

parent 7895 | 7c492d8bc8e3 |

child 7987 | d9aef93c0e32 |

1.1 --- a/doc-src/IsarRef/intro.tex Sat Oct 30 20:12:23 1999 +0200 1.2 +++ b/doc-src/IsarRef/intro.tex Sat Oct 30 20:13:16 1999 +0200 1.3 @@ -16,19 +16,18 @@ 1.4 end 1.5 \end{ttbox} 1.6 Note that any Isabelle/Isar command may be retracted by \texttt{undo}; the 1.7 -\texttt{help} command prints the list of available language elements. 1.8 +\texttt{help} command prints a list of available language elements. 1.9 1.10 Plain TTY-based interaction like this used to be quite feasible with 1.11 traditional tactic based theorem proving, but developing Isar documents 1.12 demands some better user-interface support. \emph{Proof~General}\index{Proof 1.13 General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based 1.14 environment for interactive theorem provers that does all the cut-and-paste 1.15 -and forward-backward walk through the document in a very neat way. Note that 1.16 -in Isabelle/Isar, the current position within a partial proof document is 1.17 -equally important than the actual proof state. Thus Proof~General provides 1.18 -the canonical working environment for Isabelle/Isar, both for getting 1.19 -acquainted (e.g.\ by replaying existing Isar documents) and real production 1.20 -work. 1.21 +and forward-backward walk through the text in a very neat way. Note that in 1.22 +Isabelle/Isar, the current position within a partial proof document is equally 1.23 +important than the actual proof state. Thus Proof~General provides the 1.24 +canonical working environment for Isabelle/Isar, both for getting acquainted 1.25 +(e.g.\ by replaying existing Isar documents) and real production work. 1.26 1.27 \medskip 1.28 1.29 @@ -42,7 +41,8 @@ 1.30 You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the 1.31 actual installation directory of Proof~General. From now on, the capital 1.32 \texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar} 1.33 -interface. Its usage is as follows: 1.34 +interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for 1.35 + classic Isabelle tactic scripts.} Its usage is as follows: 1.36 \begin{ttbox} 1.37 Usage: interface [OPTIONS] [FILES ...] 1.38 1.39 @@ -61,9 +61,19 @@ 1.40 via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For example, plain GNU 1.41 Emacs may be configured as follows: 1.42 \begin{ttbox} 1.43 -PROOFGENERAL_OPTIONS="-p emacs" 1.44 +PROOFGENERAL_OPTIONS="-u false -p emacs" 1.45 \end{ttbox} 1.46 1.47 +Occasionally, a user's \texttt{.emacs} file contains material that is 1.48 +incompatible with the version of (X)Emacs that Proof~General prefers. Then 1.49 +proper startup may be still achieved by using the \texttt{-u false} 1.50 +option.\footnote{Any Emacs lisp file \texttt{proofgeneral-settings.el} 1.51 + occurring in \texttt{\$ISABELLE_HOME/etc} or 1.52 + \texttt{\$ISABELLE_HOME_USER/etc} is automatically loaded by the 1.53 + Proof~General interface script as well.} 1.54 + 1.55 +\medskip 1.56 + 1.57 With the proper Isabelle interface setup, Isar documents may now be edited by 1.58 visiting appropriate theory files, e.g.\ 1.59 \begin{ttbox} 1.60 @@ -71,18 +81,49 @@ 1.61 \end{ttbox} 1.62 Users of XEmacs may note the tool bar for navigating forward and backward 1.63 through the text. Consult the Proof~General documentation \cite{proofgeneral} 1.64 -for further basic command sequences, like ``\texttt{c-c return}'' or 1.65 +for further basic command sequences, such as ``\texttt{c-c return}'' or 1.66 ``\texttt{c-c u}''. 1.67 1.68 -\medskip 1.69 + 1.70 +\section{Isabelle/Isar theories} 1.71 + 1.72 +Isabelle/Isar offers two main improvements over classic Isabelle: 1.73 +\begin{enumerate} 1.74 +\item A new \emph{theory format}, occasionally referred to as ``new-style 1.75 + theories'', supporting interactive development and unlimited undo operation. 1.76 +\item A \emph{formal proof document language} designed to support intelligible 1.77 + semi-automated reasoning. Instead of putting together unreadable tactic 1.78 + scripts, the author is enabled to express the reasoning in way that is close 1.79 + to mathematical practice. 1.80 +\end{enumerate} 1.81 + 1.82 +The Isar proof language is embedded into the new theory format as a proper 1.83 +sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or 1.84 +$\LEMMANAME$ at the theory level, and left again with the final conclusion 1.85 +(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as 1.86 +well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of 1.87 +the representing sets. 1.88 1.89 -Occasionally, a user's \texttt{.emacs} file contains material that is 1.90 -incompatible with the version of (X)Emacs that Proof~General prefers. Then 1.91 -proper startup may be still achieved by using the \texttt{-u false} 1.92 -option.\footnote{Any Emacs lisp file \texttt{proofgeneral-settings.el} 1.93 - occurring in \texttt{\$ISABELLE_HOME/etc} or 1.94 - \texttt{\$ISABELLE_HOME_USER/etc} is automatically loaded by the 1.95 - Proof~General interface script as well.} 1.96 +New-style theory files may still be associated with separate ML files 1.97 +consisting of plain old tactic scripts. There is no longer any ML binding 1.98 +generated for the theory and theorems, though. ML functions \texttt{theory}, 1.99 +\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}. 1.100 +Nevertheless, migration between classic Isabelle and Isabelle/Isar is 1.101 +relatively easy. Thus users may start to benefit from interactive theory 1.102 +development even before they have any idea of the Isar proof language at all. 1.103 + 1.104 +\begin{warn} 1.105 + Currently Proof~General does \emph{not} support mixed interactive 1.106 + development of classic Isabelle theory files or tactic scripts, together 1.107 + with Isar documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of 1.108 + Proof~General are handled as two different theorem proving systems, only one 1.109 + of these may be active at the same time. 1.110 +\end{warn} 1.111 + 1.112 +Porting of existing tactic scripts is best done by running two separate 1.113 +Proof~General sessions, one for replaying the old script and the other for the 1.114 +emerging Isabelle/Isar document. 1.115 + 1.116 1.117 \section{How to write Isar proofs anyway?} 1.118 1.119 @@ -93,17 +134,14 @@ 1.120 other hand, Isabelle/Isar comes much closer to existing mathematical practice 1.121 of formal proof, so users with less experience in old-style tactical proving, 1.122 but a good understanding of mathematical proof, might cope with Isar even 1.123 -better. 1.124 +better. See also \cite{Wenzel:1999:TPHOL} for further background information 1.125 +on Isar. 1.126 1.127 -This document really is a \emph{reference manual}. Nevertheless, we will give 1.128 -some discussions of the general principles underlying Isar in 1.129 -chapter~\ref{ch:basics}, and provide some clues of how these may be put into 1.130 -practice. Some more background information on Isar is given in 1.131 -\cite{Wenzel:1999:TPHOL}. While there is no proper tutorial on Isabelle/Isar 1.132 -available yet, there are several examples distributed with Isabelle. See 1.133 -\texttt{HOL/Isar_examples} and \texttt{HOL/HOL-Real/HahnBanach} in the 1.134 -Isabelle library: 1.135 - 1.136 +\medskip This really is a \emph{reference manual}. Nevertheless, we will also 1.137 +give some clues of how the concepts introduced here may be put into practice. 1.138 +Appendix~\ref{ap:refcard} provides a quick reference card of the most common 1.139 +Isabelle/Isar language elements. There are several examples distributed with 1.140 +Isabelle, and available via the Isabelle WWW library: 1.141 \begin{center}\small 1.142 \begin{tabular}{l} 1.143 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ 1.144 @@ -111,8 +149,9 @@ 1.145 \end{tabular} 1.146 \end{center} 1.147 1.148 -Apart from browsable HTML sources, both Isabelle/Isar sessions also provide 1.149 -actual documents (in PDF). 1.150 +See \texttt{HOL/Isar_examples} for a collection of introductory examples. 1.151 +\texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from 1.152 +browsable HTML sources, both sessions provide actual documents (in PDF). 1.153 1.154 %%% Local Variables: 1.155 %%% mode: latex