# HG changeset patch # User wenzelm # Date 935085913 -7200 # Node ID c1eeeadbe80ac73b25568d66e046ea8b551fb039 # Parent 81286f228b2d5f1e821fceb8696edfe93d902b5b more; diff -r 81286f228b2d -r c1eeeadbe80a doc-src/IsarRef/basics.tex --- a/doc-src/IsarRef/basics.tex Thu Aug 19 19:56:17 1999 +0200 +++ b/doc-src/IsarRef/basics.tex Thu Aug 19 20:05:13 1999 +0200 @@ -1,11 +1,39 @@ -\chapter{Basic Concepts} +\chapter{Basic Concepts}\label{ch:basics} + +Isabelle/Isar offers two main improvements over classic Isabelle: +\begin{enumerate} +\item A new \emph{theory format}, often referred to as ``new-style theories'', + supporting interactive development with unlimited undo operation. +\item A formal \emph{proof language} language designed to support + \emph{intelligible} semi-automated reasoning. Rather than putting together + tactic scripts, the author is enabled to express the reasoning in way that + is close to mathematical practice. +\end{enumerate} -\section{Isabelle/Isar Theories} +The Isar proof language is embedded into the new theory format as a proper +sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or +$\LEMMANAME$ at the theory levels, and left with the final end of proof. Some +theory extension mechanisms require proof as well, such as the HOL +$\isarkeyword{typedef}$. + +New-style theory files may still be associated with an ML file consisting of +plain old tactic scripts. Generally, migration between the two formats is +made relatively easy, and users may start to benefit from interactive theory +development even before they have any idea of the Isar proof language. + \section{The Isar proof language} -\subsection{Proof commands} +This rather important section has not been written yet! Refer to +\cite{Wenzel:1999:TPHOL} for the time being. + +\subsection{Commands} + +\subsubsection{Isar primitives} + +\subsubsection{Derived elements} + \subsection{Methods} diff -r 81286f228b2d -r c1eeeadbe80a doc-src/IsarRef/intro.tex --- a/doc-src/IsarRef/intro.tex Thu Aug 19 19:56:17 1999 +0200 +++ b/doc-src/IsarRef/intro.tex Thu Aug 19 20:05:13 1999 +0200 @@ -11,36 +11,36 @@ isabelle -I HOL\medskip \out{> Welcome to Isabelle/HOL (Isabelle99)}\medskip theory Foo = Main: -constdefs foo :: nat "foo == 1" -lemma "0 < foo" by (simp add: foo_def) +constdefs foo :: nat "foo == 1"; +lemma "0 < foo" by (simp add: foo_def); end \end{ttbox} +Note that \emph{any} Isabelle/Isar command may be retracted by \texttt{undo}. Plain TTY-based interaction like this used to be quite feasible with traditional tactic based theorem proving, but developing Isar documents -demands some better user-interface support. -\emph{ProofGeneral}\index{ProofGeneral} of LFCS Edinburgh \cite{proofgeneral} -offers a generic Emacs-based environment for interactive theorem provers that -does all the cut-and-paste and forward-backward walk through the document in a -very neat way. Note that in Isabelle/Isar, the current position within a -partial proof document is more informative than the actual proof state. Thus -the ProofGeneral/isar interface provides the canonical working environment for -Isabelle/Isar, both for getting acquainted (e.g.\ by replaying existing Isar -documents) and serious production work. +demands some better user-interface support. \emph{Proof~General}\index{Proof + General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based +environment for interactive theorem provers that does all the cut-and-paste +and forward-backward walk through the document in a very neat way. Note that +in Isabelle/Isar, the current position within a partial proof document is more +informative than the actual proof state. Thus Proof~General provides the +canonical working environment for Isabelle/Isar, both for getting acquainted +(e.g.\ by replaying existing Isar documents) and serious production work. \medskip -The easiest way to use ProofGeneral/isar is to make it the default Isabelle -user interface. Just say something like this in your Isabelle settings file -(cf.\ \cite{isabelle-sys}): +The easiest way to use ProofGeneral is to make it the default Isabelle user +interface. Just say something like this in your Isabelle settings file (cf.\ +\cite{isabelle-sys}): \begin{ttbox} ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface PROOFGENERAL_OPTIONS="" \end{ttbox} You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the -actual installation directory of ProofGeneral. Now the capital -\texttt{Isabelle} binary refers to the ProofGeneral/isar interface. It's -usage is as follows: +actual installation directory of Proof~General. Now the capital +\texttt{Isabelle} binary refers to the \texttt{ProofGeneral/isar} interface. +It's usage is as follows: \begin{ttbox} Usage: interface [OPTIONS] [FILES ...] @@ -50,14 +50,15 @@ -u BOOL use .emacs file (default false) -w BOOL use window system (default true) -Starts ProofGeneral for Isabelle/Isar with proof documents FILES +Starts Proof General for Isabelle/Isar with proof documents FILES (default Scratch.thy). \end{ttbox} The defaults for these options may be changed via the -\texttt{PROOFGENERAL_OPTIONS} setting. For example, GNU Emacs with loading of -the startup file enabled may be configured as follows:\footnote{The interface - disables \texttt{.emacs} by default to ensure successful startup despite any - strange commands that tend to occur there.} +\texttt{PROOFGENERAL_OPTIONS} setting. For example, GNU Emacs\footnote{GNU + Emacs version 20.x required.} with loading of the startup file enabled may +be configured as follows:\footnote{The interface disables \texttt{.emacs} by + default to ensure successful startup despite any strange commands that tend + to occur there.} \begin{ttbox} PROOFGENERAL_OPTIONS="-p emacs -u true" \end{ttbox} @@ -68,13 +69,28 @@ Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy \end{ttbox} Users of XEmacs may note the toolbar for navigating forward and backward -through the text. Consult the ProofGeneral documentation for further basic -commands, such as \texttt{c-c return} or \texttt{c-c u}. +through the text. Consult the Proof~General documentation \cite{proofgeneral} +for further basic commands, such as \texttt{c-c return} or \texttt{c-c u}. \section{How to write Isar proofs anyway?} -FIXME +This is one of the key questions, of course. Isar offers a rather different +approach to formal proof documents than plain old tactic scripts. Experienced +users of existing interactive theorem proving systems may have to learn +thinking different in order to make effective use of Isabelle/Isar. On the +other hand, Isabelle/Isar comes much closer to existing mathematical practice +of formal proof, so users with less experience in old-style tactical proving, +but a good understanding of mathematical proof might cope with Isar even +better. + +Unfortunately, there is no tutorial on Isabelle/Isar available yet. This +document really is a \emph{reference manual}. Nevertheless, we will give some +discussions of the general principles underlying Isar in +chapter~\ref{ch:basics}, and provide some clues of how these may be put into +practice. Some more background information on Isar is given in +\cite{Wenzel:1999:TPHOL}. Furthermore, there are several examples distributed +with Isabelle (see directory \texttt{HOL/Isar_examples}). %%% Local Variables: diff -r 81286f228b2d -r c1eeeadbe80a doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Thu Aug 19 19:56:17 1999 +0200 +++ b/doc-src/IsarRef/isar-ref.tex Thu Aug 19 20:05:13 1999 +0200 @@ -56,7 +56,7 @@ Any of the Isabelle/Isar commands may be executed in single-steps, so basically the interpreter has a proof text debugger already built-in. - Employing the \emph{ProofGeneral/isar} instantiation of the generic Emacs + Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs interface for interactive proof assistants of LFCS Edinburgh, we arrive at a reasonable environment for \emph{live document editing}. Thus proof texts may be developed incrementally by issuing proper document constructors,