author wenzelm Thu, 07 Mar 2002 19:04:00 +0100 changeset 13039 cfcc1f6f21df parent 13038 e968745986f1 child 13040 02bfd6d622ca
tuned;
 doc-src/IsarRef/generic.tex file | annotate | diff | comparison | revisions doc-src/IsarRef/intro.tex file | annotate | diff | comparison | revisions doc-src/IsarRef/logics.tex file | annotate | diff | comparison | revisions doc-src/IsarRef/pure.tex file | annotate | diff | comparison | revisions doc-src/IsarRef/syntax.tex file | annotate | diff | comparison | revisions
--- a/doc-src/IsarRef/generic.tex	Thu Mar 07 12:03:43 2002 +0100
+++ b/doc-src/IsarRef/generic.tex	Thu Mar 07 19:04:00 2002 +0100
@@ -37,8 +37,8 @@
of this class.

The axioms'' are stored as theorems according to the given name
-  specifications, adding the class name $c$ as name space prefix; these facts
-  are stored collectively as $c{\dtt}axioms$, too.
+  specifications, adding the class name $c$ as name space prefix; the same
+  facts are also stored collectively as $c{\dtt}axioms$.

\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a
goal stating a class relation or type arity.  The proof would usually
--- a/doc-src/IsarRef/intro.tex	Thu Mar 07 12:03:43 2002 +0100
+++ b/doc-src/IsarRef/intro.tex	Thu Mar 07 19:04:00 2002 +0100
@@ -14,24 +14,25 @@
own, which has been specifically tailored for the needs of theory and proof
development.  Compared to raw ML, the Isabelle/Isar top-level provides a more
robust and comfortable development platform, with proper support for theory
-development graphs, single-step evaluation with unlimited undo, etc.  The
+development graphs, single-step transactions with unlimited undo, etc.  The
Isabelle/Isar version of the \emph{Proof~General} user interface
\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for
-interactive theory and proof development.
+interactive theory and proof development in this advanced theorem proving
+environment.

-\medskip Apart from these technical advances over bare-bones ML programming,
-the main intention of Isar is to provide a conceptually different view on
-machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD} --- Isar'' stands
-for Intelligible semi-automated reasoning''.  Drawing from both the
+\medskip Apart from the technical advances over bare-bones ML programming, the
+main purpose of the Isar language is to provide a conceptually different view
+on machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  Isar''
+stands for Intelligible semi-automated reasoning''.  Drawing from both the
traditions of informal mathematical proof texts and high-level programming
-languages, Isar provides a versatile environment for structured formal proof
-documents.  Thus properly written Isar proof texts become accessible to a
-broader audience than unstructured tactic scripts (which typically only
-provide operational information for the machine).  Writing human-readable
-proof texts certainly requires some additional efforts by the writer in order
-to achieve a good presentation --- both of formal and informal parts of the
-text.  On the other hand, human-readable formal texts gain some value in their
-own right, independently of the mechanic proof-checking process.
+languages, Isar offers a versatile environment for structured formal proof
+documents.  Thus properly written Isar proofs become accessible to a broader
+audience than unstructured tactic scripts (which typically only provide
+operational information for the machine).  Writing human-readable proof texts
+certainly requires some additional efforts by the writer to achieve a good
+presentation, both of formal and informal parts of the text.  On the other
+hand, human-readable formal texts gain some value in their own right,
+independently of the mechanic proof-checking process.

Despite its grand design of structured proof texts, Isar is able to assimilate
the old tactical style as an improper'' sub-language.  This provides an easy
@@ -87,7 +88,7 @@
\subsubsection{Proof~General as default Isabelle interface}

The Isabelle interface wrapper script provides an easy way to invoke
-Proof~General (and XEmacs or GNU Emacs).  The default configuration of
+Proof~General (including XEmacs or GNU Emacs).  The default configuration of
Isabelle is smart enough to detect the Proof~General distribution in several
canonical places (e.g.\ \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital \texttt{Isabelle} executable would already refer to the @@ -101,8 +102,8 @@ \begin{ttbox} Isabelle $${\langle}isabellehome{\rangle}$$/src/HOL/Isar_examples/Summation.thy \end{ttbox} -Users may note the tool bar for navigating forward and backward through the -text (this depends on the local Emacs installation). Consult the +Beginners may note the tool bar for navigating forward and backward through +the text (this depends on the local Emacs installation). Consult the Proof~General documentation \cite{proofgeneral} for further basic command sequences, in particular \texttt{C-c C-return}'' and \texttt{C-c u}''. @@ -164,16 +165,21 @@ Isabelle/Isar offers the following main improvements over classic Isabelle. \begin{enumerate} + \item A new \emph{theory format}, occasionally referred to as new-style theories'', supporting interactive development and unlimited undo operation. + \item A \emph{formal proof document language} designed to support intelligible semi-automated reasoning. Instead of putting together unreadable tactic scripts, the author is enabled to express the reasoning in way that is close - to usual mathematical practice. + to usual mathematical practice. The old tactical style has been assimilated + as improper'' language elements. + \item A simple document preparation system, for typesetting formal developments together with informal text. The resulting hyper-linked PDF documents are equally well suited for WWW presentation and as printed copies. + \end{enumerate} The Isar proof language is embedded into the new theory format as a proper @@ -186,11 +192,11 @@ New-style theory files may still be associated with separate ML files consisting of plain old tactic scripts. There is no longer any ML binding generated for the theory and theorems, though. ML functions \texttt{theory}, -\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}. -Nevertheless, migration between classic Isabelle and Isabelle/Isar is -relatively easy. Thus users may start to benefit from interactive theory -development and document preparation, even before they have any idea of the -Isar proof language at all. +\texttt{thm}, and \texttt{thms} retrieve this information from the context +\cite{isabelle-ref}. Nevertheless, migration between classic Isabelle and +Isabelle/Isar is relatively easy. Thus users may start to benefit from +interactive theory development and document preparation, even before they have +any idea of the Isar proof language at all. \begin{warn} Proof~General does \emph{not} support mixed interactive development of @@ -210,9 +216,9 @@ \subsection{Document preparation}\label{sec:document-prep} Isabelle/Isar provides a simple document preparation system based on existing -PDF-\LaTeX technology, with full support of hyper-links (both local references -and URLs), bookmarks, and thumbnails. Thus the results are equally well -suited for WWW browsing and as printed copies. +{PDF-\LaTeX} technology, with full support of hyper-links (both local +references and URLs), bookmarks, and thumbnails. Thus the results are equally +well suited for WWW browsing and as printed copies. \medskip @@ -245,8 +251,8 @@ You may also consider to tune the \texttt{usedir} options in \texttt{IsaMakefile}, for example to change the output format from -\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D generated} option in -order to keep a second copy of the generated {\LaTeX} sources. +\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D} option to retain a +second copy of the generated {\LaTeX} sources. \medskip @@ -260,13 +266,13 @@ This is one of the key questions, of course. First of all, the tactic script emulation of Isabelle/Isar essentially provides a clarified version of the very same unstructured proof style of classic Isabelle. Old-time users should -quickly become acquainted with that (degenerative) view of Isar at the least. +quickly become acquainted with that (slightly degenerative) view of Isar. Writing \emph{proper} Isar proof texts targeted at human readers is quite different, though. Experienced users of the unstructured style may even have to unlearn some of their habits to master proof composition in Isar. In contrast, new users with less experience in old-style tactical proving, but a -good understanding of mathematical proof in general often get started easier. +good understanding of mathematical proof in general, often get started easier. \medskip The present text really is only a reference manual on Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to give some clues of how the --- a/doc-src/IsarRef/logics.tex Thu Mar 07 12:03:43 2002 +0100 +++ b/doc-src/IsarRef/logics.tex Thu Mar 07 19:04:00 2002 +0100 @@ -1,5 +1,5 @@ -\chapter{Object-logic specific elements}\label{ch:logics} +\chapter{Object-logic Specific Elements}\label{ch:logics} \section{General logic setup}\label{sec:object-logic} @@ -82,7 +82,7 @@ \section{HOL} -\subsection{Primitive types}\label{sec:typedef} +\subsection{Primitive types}\label{sec:hol-typedef} \indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef} \begin{matharray}{rcl} @@ -167,7 +167,7 @@ \end{descr} -\section{Records}\label{sec:hol-record} +\subsection{Records}\label{sec:hol-record} In principle, records merely generalize the concept of tuples where components may be addressed by labels instead of just position. The logical @@ -178,7 +178,7 @@ more details on object-oriented verification and record subtyping in HOL. -\subsection{Basic concepts} +\subsubsection{Basic concepts} Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the level of terms and types. The notation is as follows: @@ -235,7 +235,7 @@ practice. -\subsection{Record specifications}\label{sec:hol-record-def} +\subsubsection{Record specifications}\label{sec:hol-record-def} \indexisarcmdof{HOL}{record} \begin{matharray}{rcl} @@ -271,7 +271,7 @@ \end{descr} -\subsection{Record operations}\label{sec:hol-record-ops} +\subsubsection{Record operations}\label{sec:hol-record-ops} Any record definition of the form presented above produces certain standard operations. Selectors and updates are provided for any field, including the @@ -339,7 +339,7 @@ \noindent Note that$t{\dtt}make$and$t{\dtt}fields$are actually coincide for root records. -\subsection{Derived rules and proof tools}\label{sec:hol-record-thms} +\subsubsection{Derived rules and proof tools}\label{sec:hol-record-thms} The record package proves several results internally, declaring these facts to appropriate proof tools. This enables users to reason about record structures @@ -642,7 +642,7 @@ \end{descr} -\subsection{Generating executable code} +\subsection{Executable code} Isabelle/Pure provides a generic infrastructure to support code generation from executable specifications, both functional and relational programs. --- a/doc-src/IsarRef/pure.tex Thu Mar 07 12:03:43 2002 +0100 +++ b/doc-src/IsarRef/pure.tex Thu Mar 07 19:04:00 2002 +0100 @@ -1,8 +1,8 @@ \chapter{Basic Language Elements}\label{ch:pure-syntax} -Subsequently, we introduce the main part of Pure Isar theory and proof -commands, together with fundamental proof methods and attributes. +Subsequently, we introduce the main part of Pure theory and proof commands, +together with fundamental proof methods and attributes. Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic tools and packages (such as the Simplifier) that are either part of Pure Isabelle or pre-installed in most object logics. Chapter~\ref{ch:logics} @@ -14,9 +14,10 @@ \emph{improper commands}. Some proof methods and attributes introduced later are classified as improper as well. Improper Isar language elements, which are subsequently marked by $^*$'', are often helpful when developing proof -documents, while their use is discouraged for the final outcome. Typical -examples are diagnostic commands that print terms or theorems according to the -current context; other commands emulate old-style tactical theorem proving. +documents, while their use is discouraged for the final human-readable +outcome. Typical examples are diagnostic commands that print terms or +theorems according to the current context; other commands emulate old-style +tactical theorem proving. \section{Theory commands} @@ -42,8 +43,8 @@ there may be an optional$\isarkeyword{header}$declaration, which is relevant to document preparation only; it acts very much like a special pre-theory markup command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The -$\END$commands concludes a theory development; it has to be the very last -command of any theory file to loaded in batch-mode. The theory context may be +$\END$command concludes a theory development; it has to be the very last +command of any theory file loaded in batch-mode. The theory context may be also changed interactively by$\CONTEXT$without creating a new theory. \begin{rail} @@ -206,21 +207,27 @@ \end{rail} \begin{descr} + \item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}$(\vec\alpha)t$for existing type$\tau$. Unlike actual type definitions, as are available in Isabelle/HOL for example, type synonyms are just purely syntactic abbreviations without any logical significance. Internally, type synonyms are fully expanded. + \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor -$t$, intended as an actual logical type. Note that object-logics such as - Isabelle/HOL override$\isarkeyword{typedecl}$by their own version. +$t$, intended as an actual logical type. Note that the Isabelle/HOL + object-logic overrides$\isarkeyword{typedecl}$by its own version + (\S\ref{sec:hol-typedef}). + \item [$\isarkeyword{nonterminals}~\vec c$] declares$0$-ary type constructors$\vec c$to act as purely syntactic types, i.e.\ nonterminal symbols of Isabelle's inner syntax of terms or types. + \item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted signature of types by new type constructor arities. This is done axiomatically! The$\INSTANCE$command (see \S\ref{sec:axclass}) provides a way to introduce proven type arities. + \end{descr} @@ -332,7 +339,7 @@ Axioms are usually only introduced when declaring new logical systems. Everyday work is typically done the hard way, with proper definitions and - actual proven theorems. + proven theorems. \item [$\isarkeyword{lemmas}~a = \vec b$] retrieves and stores existing facts in the theory context, or the specified locale (see also @@ -454,11 +461,11 @@ } Note that mere tactic emulations may ignore the \texttt{facts} parameter -above. Proper proof methods would do something appropriate'' with the list -of current facts, though. Single-rule methods usually do strict -forward-chaining (e.g.\ by using \texttt{Method.multi_resolves}), while -automatic ones just insert the facts using \texttt{Method.insert_tac} before -applying the main tactic. +above. Proper proof methods would do something appropriate with the list of +current facts, though. Single-rule methods usually do strict forward-chaining +(e.g.\ by using \texttt{Method.multi_resolves}), while automatic ones just +insert the facts using \texttt{Method.insert_tac} before applying the main +tactic. \end{descr} @@ -564,8 +571,8 @@ operation may be performed next. The corresponding typings of proof commands restricts the shape of well-formed proof texts to particular command sequences. So dynamic arrangements of commands eventually turn out as static -texts. Appendix~\ref{ap:refcard} gives a simplified grammar of the overall -(extensible) language emerging that way. +texts of a certain structure. Appendix~\ref{ap:refcard} gives a simplified +grammar of the overall (extensible) language emerging that way. \subsection{Markup commands}\label{sec:markup-prf} @@ -605,11 +612,11 @@ The logical proof context consists of fixed variables and assumptions. The former closely correspond to Skolem constants, or meta-level universal quantification as provided by the Isabelle/Pure logical framework. -Introducing some \emph{arbitrary, but fixed} variable via$\FIX x$results in -a local value that may be used in the subsequent proof as any other variable -or constant. Furthermore, any result$\edrv \phi[x]$exported from the -context will be universally closed wrt.\$x$at the outermost level:$\edrv
-\All x \phi$(this is expressed using Isabelle's meta-variables). +Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$'' results +in a local value that may be used in the subsequent proof as any other +variable or constant. Furthermore, any result$\edrv \phi[x]$exported from +the context will be universally closed wrt.\$x$at the outermost level: +$\edrv \All x \phi$(this is expressed using Isabelle's meta-variables). Similarly, introducing some assumption$\chi$has two effects. On the one hand, a local theorem is created that may be used as a fact in subsequent @@ -622,8 +629,8 @@$\PRESUMENAME$leaves the subgoal unchanged in order to be proved later by the user. -Local definitions, introduced by$\DEF{}{x \equiv t}$, are achieved by -combining$\FIX x$with another version of assumption that causes any +Local definitions, introduced by $\DEF{}{x \equiv t}$'', are achieved by +combining $\FIX x$'' with another version of assumption that causes any hypothetical equation$x \equiv t$to be eliminated by the reflexivity rule. Thus, exporting some result$x \equiv t \drv \phi[x]$yields$\edrv \phi[t]$. @@ -640,8 +647,10 @@ \end{rail} \begin{descr} + \item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables$\vec x$. + \item [$\ASSUME{a}{\vec\phi}$and$\PRESUME{a}{\vec\phi}$] introduce local theorems$\vec\phi$by assumption. Subsequent results applied to an enclosing goal (e.g.\ by$\SHOWNAME$) are handled as follows:$\ASSUMENAME$@@ -651,12 +660,14 @@ Several lists of assumptions may be given (separated by$\isarkeyword{and}$); the resulting list of current facts consists of all of these concatenated. + \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition. In results exported from the context,$x$is replaced by$t$. Basically, -$\DEF{}{x \equiv t}$abbreviates$\FIX{x}~\ASSUME{}{x \equiv t}$, with the - resulting hypothetical equation solved by reflexivity. + $\DEF{}{x \equiv t}$'' abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$'', + with the resulting hypothetical equation solved by reflexivity. The default name for the definitional equation is$x_def$. + \end{descr} The special name$prems$\indexisarthm{prems} refers to all assumptions of the @@ -679,10 +690,10 @@ Any fact will usually be involved in further proofs, either as explicit arguments of proof methods, or when forward chaining towards the next goal via$\THEN$(and variants);$\FROMNAME$and$\WITHNAME$are composite forms -involving$\NOTE$. The$\USINGNAME$elements allows to augment the collection -of used facts \emph{after} a goal has been stated. Note that the special -theorem name$this$\indexisarthm{this} refers to the most recently established -facts, but only \emph{before} issuing a follow-up claim. +involving$\NOTENAME$. The$\USINGNAME$elements augments the collection of +used facts \emph{after} a goal has been stated. Note that the special theorem +name$this$\indexisarthm{this} refers to the most recently established facts, +but only \emph{before} issuing a follow-up claim. \begin{rail} 'note' (thmdef? thmrefs + 'and') @@ -692,28 +703,35 @@ \end{rail} \begin{descr} + \item [$\NOTE{a}{\vec b}$] recalls existing facts$\vec b$, binding the result as$a$. Note that attributes may be involved as well, both on the left and right hand sides. + \item [$\THEN$] indicates forward chaining by the current facts in order to establish the goal to be claimed next. The initial proof method invoked to - refine that will be offered the facts to do anything appropriate'' (cf.\ + refine that will be offered the facts to do anything appropriate'' (see also \S\ref{sec:proof-steps}). For example, method$rule$(see \S\ref{sec:pure-meth-att}) would typically do an elimination rather than an introduction. Automatic methods usually insert the facts into the goal state before operation. This provides a simple scheme to control relevance of facts in automated proof search. -\item [$\FROM{\vec b}$] abbreviates$\NOTE{}{\vec b}~\THEN$; thus$\THEN$is - equivalent to$\FROM{this}$. -\item [$\WITH{\vec b}$] abbreviates$\FROM{\vec b~this}$; thus the forward - chaining is from earlier facts together with the current ones. + +\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$''; thus$\THEN$+ is equivalent to $\FROM{this}$''. + +\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~\AND~this}$''; thus the + forward chaining is from earlier facts together with the current ones. + \item [$\USING{\vec b}$] augments the facts being currently indicated for use - in a subsequent refinement step (such as$\APPLYNAME$or$\PROOFNAME$). + by a subsequent refinement step (such as$\APPLYNAME$or$\PROOFNAME$). + \end{descr} -Forward chaining with an empty list of theorems is the same as not chaining. -Thus$\FROM{nothing}$has no effect apart from entering$prove(chain)$mode, -since$nothing$\indexisarthm{nothing} is bound to the empty list of theorems. +Forward chaining with an empty list of theorems is the same as not chaining at +all. Thus $\FROM{nothing}$'' has no effect apart from entering +$prove(chain)$mode, since$nothing$\indexisarthm{nothing} is bound to the +empty list of theorems. Basic proof methods (such as$rule$) expect multiple facts to be given in their proper order, corresponding to a prefix of the premises of the rule @@ -742,18 +760,18 @@ \end{matharray} From a theory context, proof mode is entered by an initial goal command such -as$\LEMMANAME$,$\THEOREMNAME$,$\COROLLARYNAME$. Within a proof, new claims -may be introduced locally as well; four variants are available here to +as$\LEMMANAME$,$\THEOREMNAME$, or$\COROLLARYNAME$. Within a proof, new +claims may be introduced locally as well; four variants are available here to indicate whether forward chaining of facts should be performed initially (via -$\THEN$), and whether the emerging result is meant to solve some pending goal. +$\THEN$), and whether the final result is meant to solve some pending goal. Goals may consist of multiple statements, resulting in a list of facts eventually. A pending multi-goal is internally represented as a meta-level -conjunction (printed as \verb,&&,), which is automatically split into the -corresponding number of sub-goals prior to any initial method application, via +conjunction (printed as \verb,&&,), which is usually split into the +corresponding number of sub-goals prior to an initial method application, via$\PROOFNAME$(\S\ref{sec:proof-steps}) or$\APPLYNAME$-(\S\ref{sec:tactic-commands}).\footnote{The$induct$method covered in - \S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.} +(\S\ref{sec:tactic-commands}). The$induct$method covered in +\S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously. Claims at the theory level may be either in short or long form. A short goal merely consists of several simultaneous propositions (often just one). A long @@ -775,13 +793,13 @@ \end{rail} \begin{descr} + \item [$\LEMMA{a}{\vec\phi}$] enters proof mode with$\vec\phi$as main goal, eventually resulting in some fact$\turn \vec\phi$to be put back into the - theory context, and optionally into the specified locale, cf.\ - \S\ref{sec:locale}. An additional \railnonterm{context} specification may - build an initial proof context for the subsequent claim; this may include - local definitions and syntax as well, see the definition of$contextelem$in - \S\ref{sec:locale}. + theory context, or into the specified locale (cf.\ \S\ref{sec:locale}). An + additional \railnonterm{context} specification may build up an initial proof + context for the subsequent claim; this includes local definitions and syntax + as well, see the definition of$contextelem$in \S\ref{sec:locale}. \item [$\THEOREM{a}{\vec\phi}$and$\COROLLARY{a}{\vec\phi}$] are essentially the same as$\LEMMA{a}{\vec\phi}$, but the facts are internally marked as @@ -796,27 +814,29 @@ \item [$\SHOW{a}{\vec\phi}$] is like$\HAVE{a}{\vec\phi}$plus a second stage to refine some pending sub-goal for each one of the finished result, after having been exported into the corresponding context (at the head of the - sub-proof that the$\SHOWNAME$command belongs to). + sub-proof of this$\SHOWNAME$command). To accommodate interactive debugging, resulting rules are printed before being applied internally. Even more, interactive execution of$\SHOWNAME$- predicts potential failure after finishing its proof, and displays the - resulting error message as a warning beforehand, adding this header: + predicts potential failure and displays the resulting error as a warning + beforehand. Watch out for the following message: \begin{ttbox} Problem! Local statement will fail to solve any pending goal \end{ttbox} + +\item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$'', i.e.\ claims a local + goal to be proven by forward chaining the current facts. Note that +$\HENCENAME$is also equivalent to $\FROM{this}~\HAVENAME$''. + +\item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$''. Note that$\THUSNAME$+ is also equivalent to $\FROM{this}~\SHOWNAME$''. -\item [$\HENCENAME$] abbreviates$\THEN~\HAVENAME$, i.e.\ claims a local goal - to be proven by forward chaining the current facts. Note that$\HENCENAME$- is also equivalent to$\FROM{this}~\HAVENAME$. -\item [$\THUSNAME$] abbreviates$\THEN~\SHOWNAME$. Note that$\THUSNAME$is - also equivalent to$\FROM{this}~\SHOWNAME$. \end{descr} -Any goal statement causes some term abbreviations (such as$\Var{thesis}$, -$\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}. -Furthermore, the local context of a (non-atomic) goal is provided via the +Any goal statement causes some term abbreviations (such as$\Var{thesis}$) to +be bound automatically, see also \S\ref{sec:term-abbrev}. Furthermore, the +local context of a (non-atomic) goal is provided via the$rule_context$\indexisarcase{rule-context} case, see also \S\ref{sec:rule-cases}. @@ -827,7 +847,7 @@ schematic variables}, although this does not conform to the aim of human-readable proof documents! The main problem with schematic goals is that the actual outcome is usually hard to predict, depending on the - behavior of the actual proof methods applied during the reasoning. Note + behavior of the proof methods applied during the course of reasoning. Note that most semi-automated methods heavily depend on several kinds of implicit rule declarations within the current theory context. As this would also result in non-compositional checking of sub-proofs, \emph{local goals} are @@ -863,7 +883,7 @@ remaining goals. No facts are passed to$m@2$. \end{enumerate} -The only other proper way to affect pending goals in a proof body is by +The only other (proper) way to affect pending goals in a proof body is by$\SHOWNAME$, which involves an explicit statement of what is to be solved eventually. Thus we avoid the fundamental problem of unstructured tactic scripts that consist of numerous consecutive goal transformations, with @@ -875,7 +895,7 @@ either solve the goal completely, or constitute some well-understood reduction to new sub-goals. Arbitrary automatic proof tools that are prone leave a large number of badly structured sub-goals are no help in continuing the proof -document in any intelligible way. +document in an intelligible manner. Unless given explicitly by the user, the default initial method is $rule$'', which applies a single standard elimination or introduction rule according to @@ -894,8 +914,10 @@ \end{rail} \begin{descr} + \item [$\PROOF{m@1}$] refines the goal by proof method$m@1$; facts for forward chaining are passed if so indicated by$proof(chain)$mode. + \item [$\QED{m@2}$] refines any remaining goals by proof method$m@2$and concludes the sub-proof by assumption. If the goal had been$\SHOWNAME$(or$\THUSNAME$), some pending sub-goal is solved as well by the rule resulting @@ -905,25 +927,29 @@ strong'' assumptions as introduced by$\ASSUMENAME$.} of the enclosing context. Debugging such a situation might involve temporarily changing$\SHOWNAME$into$\HAVENAME$, or weakening the local context by replacing - some occurrences of$\ASSUMENAME$by$\PRESUMENAME$. + occurrences of$\ASSUMENAME$by$\PRESUMENAME$. + \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it - abbreviates$\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods, - though. Debugging an unsuccessful$\BYY{m@1}{m@2}$commands might be done - by expanding its definition; in many cases$\PROOF{m@1}$is already - sufficient to see what is going wrong. + abbreviates$\PROOF{m@1}~\QED{m@2}$, but with backtracking across both + methods. Debugging an unsuccessful$\BYY{m@1}{m@2}$commands might be done + by expanding its definition; in many cases$\PROOF{m@1}$(or even +$\APPLY{m@1}$) is already sufficient to see the problem. + \item [$\DDOT$''] is a \emph{default proof}\index{proof!default}; it abbreviates$\BY{rule}$. + \item [$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it abbreviates$\BY{this}$. + \item [$\SORRY$] is a \emph{fake proof}\index{proof!fake} pretending to solve the pending claim without further ado. This only works in interactive - development, or if the \texttt{quick_and_dirty} flag is enabled. Certainly, - any facts emerging from fake proofs are not the real thing. Internally, - each theorem container is tainted by an oracle invocation, which is - indicated as $[!]$'' in the printed result. + development, or if the \texttt{quick_and_dirty} flag is enabled. Facts + emerging from fake proofs are not the real thing. Internally, each theorem + container is tainted by an oracle invocation, which is indicated as + $[!]$'' in the printed result. The most important application of$\SORRY$is to support experimentation and - top-down proof development in a simple manner. + top-down proof development. \end{descr} @@ -975,22 +1001,23 @@ \item [$-$''] does nothing but insert the forward chaining facts as premises into the goal. Note that command$\PROOFNAME$without any method actually performs a single reduction step using the$rule$method; thus a plain - \emph{do-nothing} proof step would be$\PROOF{-}$rather than$\PROOFNAME$- alone. + \emph{do-nothing} proof step would be $\PROOF{-}$'' rather than +$\PROOFNAME$alone. -\item [$assumption$] solves some goal by a single assumption step. Any facts - given (${} \le 1$) are guaranteed to participate in the refinement. Recall - that$\QEDNAME$(see \S\ref{sec:proof-steps}) already concludes any - remaining sub-goals by assumption, so structured proofs usually need not - quote the$assumption$method at all. +\item [$assumption$] solves some goal by a single assumption step. All given + facts are guaranteed to participate in the refinement; this means there may + be only$0$or$1$in the first place. Recall that$\QEDNAME$(see + \S\ref{sec:proof-steps}) already concludes any remaining sub-goals by + assumption, so structured proofs usually need not quote the$assumption$+ method at all. \item [$this$] applies all of the current facts directly as rules. Recall - that $\DOT$'' (dot) abbreviates$\BY{this}$. + that $\DOT$'' (dot) abbreviates $\BY{this}$''. \item [$rule~\vec a$] applies some rule given as argument in backward manner; facts are used to reduce the rule before applying it to the goal. Thus -$rule$without facts is plain \emph{introduction}, while with facts it - becomes \emph{elimination}. +$rule$without facts is plain introduction, while with facts it becomes + elimination. When no arguments are given, the$rule$method tries to pick appropriate rules automatically, as declared in the current context using the$intro$, @@ -1001,18 +1028,18 @@ \item [$rules$] performs intuitionistic proof search, depending on specifically declared rules from the context, or given as explicit arguments. Chained facts are inserted into the goal before commencing proof - search;$rules!$means to include the current$prems$as well. + search; $rules!$'' means to include the current$prems$as well. Rules need to be classified as$intro$,$elim$, or$dest$; here the $!$'' indicator refers to safe'' rules, which may be applied aggressively (without considering back-tracking later). Rules declared with $?$'' are ignored in proof search (the single-step$rule$method still observes these). An explicit weight annotation may be given as well; otherwise the - number of rule premises will be taken into account. - + number of rule premises will be taken into account here. + \item [$intro$,$elim$, and$dest$] declare introduction, elimination, and destruct rules, to be used with the$rule$and$rules$methods. Note that - the latter will ignore rules declare with $?$'', while $!$'' are used + the latter will ignore rules declared with $?$'', while $!$'' are used most aggressively. The classical reasoner (see \S\ref{sec:classical-basic}) introduces its own @@ -1024,7 +1051,7 @@ \item [$OF~\vec a$] applies some theorem to given rules$\vec a$(in parallel). This corresponds to the \texttt{MRS} operator in ML \cite[\S5]{isabelle-ref}, but note the reversed order. Positions may be - skipped by including $\_$'' (underscore) as argument. + effectively skipped by including $\_$'' (underscore) as argument. \item [$of~\vec t$] performs positional instantiation. The terms$\vec t$are substituted for any schematic variables occurring in a theorem from left to @@ -1045,8 +1072,8 @@ Abbreviations may be either bound by explicit$\LET{p \equiv t}$statements, or by annotating assumptions or goal statements with a list of patterns -$\ISS{p@1\;\dots}{p@n}$. In both cases, higher-order matching is invoked to -bind extra-logical term variables, which may be either named schematic +$\ISS{p@1\;\dots}{p@n}$''. In both cases, higher-order matching is invoked +to bind extra-logical term variables, which may be either named schematic variables of the form$\Var{x}$, or nameless dummies \texttt{_}'' (underscore).\indexisarvar{_@\texttt{_}} Note that in the$\LETNAME$form the patterns occur on the left-hand side, while the$\ISNAME$patterns are in @@ -1058,15 +1085,15 @@ in \emph{arbitrary} instances later. Even though actual polymorphism should be rarely used in practice, this mechanism is essential to achieve proper incremental type-inference, as the user proceeds to build up the Isar proof -text. +text from left to right. \medskip -Term abbreviations are quite different from actual local definitions as -introduced via$\DEFNAME$(see \S\ref{sec:proof-context}). The latter are -visible within the logic as actual equations, while abbreviations disappear -during the input process just after type checking. Also note that$\DEFNAME$-does not support polymorphism. +Term abbreviations are quite different from local definitions as introduced +via$\DEFNAME$(see \S\ref{sec:proof-context}). The latter are visible within +the logic as actual equations, while abbreviations disappear during the input +process just after type checking. Also note that$\DEFNAME$does not support +polymorphism. \begin{rail} 'let' ((term + 'and') '=' term + 'and') @@ -1110,9 +1137,8 @@ local goal statement automatically opens \emph{two} blocks, which are closed again when concluding the sub-proof (by$\QEDNAME$etc.). Sections of different context within a sub-proof may be switched via$\NEXT$, which is -just a single block-close followed by block-open again. Thus the effect of -$\NEXT$to reset the local proof context. There is no goal focus involved -here! +just a single block-close followed by block-open again. The effect of$\NEXT$+is to reset the local proof context; there is no goal focus involved here! For slightly more advanced applications, there are explicit block parentheses as well. These typically achieve a stronger forward style of reasoning. @@ -1183,20 +1209,19 @@ No facts are passed to$m$. Furthermore, the static context is that of the enclosing goal (as for actual$\QEDNAME$). Thus the proof method may not refer to any assumptions introduced in the current body, for example. - + \item [$\isarkeyword{done}$] completes a proof script, provided that the - current goal state is already solved completely. Note that actual - structured proof commands (e.g.\ $\DOT$'' or$\SORRY$) may be used to - conclude proof scripts as well. + current goal state is solved completely. Note that actual structured proof + commands (e.g.\ $\DOT$'' or$\SORRY$) may be used to conclude proof + scripts as well. \item [$\isarkeyword{defer}~n$and$\isarkeyword{prefer}~n$] shuffle the list of pending goals:$defer$puts off goal$n$to the end of the list ($n = 1$by default), while$prefer$brings goal$n$to the top. - + \item [$\isarkeyword{back}$] does back-tracking over the result sequence of - the latest proof command.\footnote{Unlike the ML function \texttt{back} - \cite{isabelle-ref}, the Isar command does not search upwards for further - branch points.} Basically, any proof command may return multiple results. + the latest proof command. Basically, any proof command may return multiple + results. \item [$\isarkeyword{declare}~thms$] declares theorems to the current theory context (or the specified locale, see also \S\ref{sec:locale}). No theorem @@ -1223,8 +1248,8 @@ different from faking'' actual proofs via$\SORRY$(see \S\ref{sec:proof-steps}):$\OOPS$does not observe the proof structure at all, but goes back right to the theory level. Furthermore,$\OOPS$does not -produce any result theorem --- there is no claim to be able to complete the -proof anyhow. +produce any result theorem --- there is no intended claim to be able to +complete the proof anyhow. A typical application of$\OOPS$is to explain Isar proofs \emph{within} the system itself, in conjunction with the document preparation tools of Isabelle @@ -1234,8 +1259,8 @@ $\OOPS$'' keyword. \medskip The$\OOPS$command is undo-able, unlike$\isarkeyword{kill}$(see -\S\ref{sec:history}). The effect is to get back to the theory \emph{before} -the opening of the proof. +\S\ref{sec:history}). The effect is to get back to the theory just before the +opening of the proof. \section{Other commands} @@ -1340,30 +1365,42 @@ for simplifications. \begin{descr} + \item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax, including keywords and command. + \item [$\isarkeyword{print_syntax}$] prints the inner syntax of types and terms, depending on the current context. The output can be very verbose, including grammar tables and syntax translation rules. See \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's inner syntax. + \item [$\isarkeyword{print_methods}$] prints all proof methods available in the current theory context. + \item [$\isarkeyword{print_attributes}$] prints all attributes available in the current theory context. + \item [$\isarkeyword{print_theorems}$] prints theorems available in the - current theory context. In interactive mode this actually refers to the - theorems left by the last transaction; this allows to inspect the result of - advanced definitional packages, such as$\isarkeyword{datatype}$. + current theory context. + + In interactive mode this actually refers to the theorems left by the last + transaction; this allows to inspect the result of advanced definitional + packages, such as$\isarkeyword{datatype}$. + \item [$\isarkeyword{thms_containing}~\vec t$] retrieves theorems from the theory context containing all of the constants occurring in the terms$\vec
t$. Note that giving the empty list yields \emph{all} theorems of the current theory. + \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts, using Isabelle's graph browser tool (see also \cite{isabelle-sys}). + \item [$\isarkeyword{print_facts}$] prints any named facts of the current context, including assumptions and local results. + \item [$\isarkeyword{print_binds}$] prints all term abbreviations present in the context. + \end{descr} @@ -1421,8 +1458,7 @@ \end{descr} These system commands are scarcely used when working with the Proof~General -interface, since loading of theories is done fully transparently. - +interface, since loading of theories is done transparently. %%% Local Variables: %%% mode: latex --- a/doc-src/IsarRef/syntax.tex Thu Mar 07 12:03:43 2002 +0100 +++ b/doc-src/IsarRef/syntax.tex Thu Mar 07 19:04:00 2002 +0100 @@ -1,5 +1,5 @@ -\chapter{Syntax primitives} +\chapter{Syntax Primitives} The rather generic framework of Isabelle/Isar syntax emerges from three main syntactic categories: \emph{commands} of the top-level Isar engine (covering @@ -40,7 +40,7 @@ particularly useful in interactive shell sessions to make clear where the current command is intended to end. Otherwise, the interpreter loop will continue to issue a secondary prompt \verb,#,'' until an end-of-command is -clearly indicated from the input syntax, e.g.\ encounter of the next command +clearly recognized from the input syntax, e.g.\ encounter of the next command keyword. Advanced interfaces such as Proof~General \cite{proofgeneral} do not require @@ -92,12 +92,11 @@ symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots \end{matharray} -The syntax of \railtoken{string} admits any characters, including newlines; -\verb|"|'' (double-quote) and \verb|\|'' (backslash) need to be escaped by -a backslash. Note that ML-style control characters are \emph{not} supported. -The body of \railtoken{verbatim} may consist of any text not containing -\verb|*}|''; this allows handsome inclusion of quotes without further -escapes. +The syntax of$string$admits any characters, including newlines; \verb|"|'' +(double-quote) and \verb|\|'' (backslash) need to be escaped by a backslash. +Note that ML-style control characters are \emph{not} supported. The body of +$verbatim$may consist of any text not containing \verb|*}|''; this allows +convenient inclusion of quotes without further escapes. Comments take the form \texttt{(*~\dots~*)} and may in principle be nested, just as in ML. Note that these are \emph{source} comments only, which are @@ -109,7 +108,8 @@ Proof~General does not handle nested comments properly; it is also unable to keep \verb,(*,\,/\,\verb,{*, and \verb,*),\,/\,\verb,*}, apart, despite their rather different meaning. These are inherent problems of Emacs - legacy. + legacy. Users should not be overly aggressive about nesting or alternating + these delimiters. \end{warn} \medskip @@ -209,8 +209,8 @@ level. Basically, any such entity has to be quoted to turn it into a single token (the parsing and type-checking is performed internally later). For convenience, a slightly more liberal convention is adopted: quotes may be -omitted for any type or term that is already \emph{atomic} at the outer level. -For example, one may just write \texttt{x} instead of \texttt{"x"}. Note that +omitted for any type or term that is already atomic at the outer level. For +example, one may just write \texttt{x} instead of \texttt{"x"}. Note that symbolic identifiers (e.g.\ \texttt{++} or$\forall$) are available as well, provided these have not been superseded by commands or other keywords already (e.g.\ \texttt{=} or \texttt{+}). @@ -338,9 +338,9 @@ Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs}, the former requires an actual singleton result. Any of these theorem specifications may include lists of attributes both on the left and right hand -sides; attributes are applied to any immediately preceding theorem. If names -are omitted, the theorems are not stored within the theorem database of the -theory or proof context; any given attributes are still applied, though. +sides; attributes are applied to any immediately preceding fact. If names are +omitted, the theorems are not stored within the theorem database of the theory +or proof context; any given attributes are still applied, though. \indexouternonterm{thmdecl}\indexouternonterm{axmdecl} \indexouternonterm{thmdef}\indexouternonterm{thmrefs} @@ -365,9 +365,9 @@ Wherever explicit propositions (or term fragments) occur in a proof text, casual binding of schematic term variables may be given specified via patterns -of the form$\ISS{p@1\;\dots}{p@n}$. There are separate versions available -for \railqtoken{term}s and \railqtoken{prop}s. The latter provides a -$\CONCLNAME$part with patterns referring the (atomic) conclusion of a rule. +of the form $\ISS{p@1\;\dots}{p@n}$''. There are separate versions +available for \railqtoken{term}s and \railqtoken{prop}s. The latter provides +a$\CONCLNAME$part with patterns referring the (atomic) conclusion of a rule. \indexouternonterm{termpat}\indexouternonterm{proppat} \begin{rail} @@ -380,8 +380,8 @@ Declarations of local variables$x :: \tau$and logical propositions$a :
\phi$represent different views on the same principle of introducing a local scope. In practice, one may usually omit the typing of$vars$(due to -type-inference), and the naming of propositions (due to implicit chaining of -emerging facts). In any case, Isar proof elements usually admit to introduce +type-inference), and the naming of propositions (due to implicit references of +current facts). In any case, Isar proof elements usually admit to introduce multiple such items simultaneously. \indexouternonterm{vars}\indexouternonterm{props} @@ -419,8 +419,8 @@ preparation system (see also \S\ref{sec:document-prep}). Thus embedding of -\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within a -text block would cause +\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}}'' +within a text block would cause \isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x} to appear in the final {\LaTeX} document. Also note that theorem antiquotations may involve attributes as well. For example, @@ -453,25 +453,32 @@ \texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|. \begin{descr} + \item [$\at\{thm~\vec a\}$] prints theorems$\vec a$. Note that attribute specifications may be included as well (see also \S\ref{sec:syn-att}); the$no_vars$operation (see \S\ref{sec:misc-meth-att}) would be particularly useful to suppress printing of schematic variables. + \item [$\at\{prop~\phi\}$] prints a well-typed proposition$\phi$. + \item [$\at\{term~t\}$] prints a well-typed term$t$. + \item [$\at\{typ~\tau\}$] prints a well-formed type$\tau$. + \item [$\at\{text~s\}$] prints uninterpreted source text$s$. This is particularly useful to print portions of text according to the Isabelle {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces - of terms that cannot be parsed or type-checked yet). + of terms that should not be parsed or type-checked yet). + \item [$\at\{goals\}$] prints the current \emph{dynamic} goal state. This is - only for support of tactic-emulation scripts within Isar --- presentation of - goal states does not conform to actual human-readable proof documents. - + mainly for support of tactic-emulation scripts within Isar --- presentation + of goal states does not conform to actual human-readable proof documents. Please do not include goal states into document output unless you really know what you are doing! + \item [$\at\{subgoals\}$] behaves almost like$goals\$, except that it does not
print the main goal.
+
\end{descr}

\medskip
@@ -507,9 +514,10 @@
the above flags are disabled by default, unless changed from ML.

\medskip Note that antiquotations do not only spare the author from tedious
-typing, but also achieve some degree of consistency-checking of informal
-explanations with formal developments, since well-formedness of terms and
-types with respect to the current theory or proof context can be ensured.
+typing of logical entities, but also achieve some degree of
+consistency-checking of informal explanations with formal developments:
+well-formedness of terms and types with respect to the current theory or proof
+context is ensured here.

%%% Local Variables:
%%% mode: latex