--- a/doc-src/IsarRef/generic.tex Tue Aug 03 13:16:29 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Tue Aug 03 18:56:51 1999 +0200
@@ -1,5 +1,76 @@
-\chapter{Generic Tools and Packages}
+\chapter{Generic Tools and Packages}\label{ch:gen-tools}
+
+\section{Basic proof methods and attributes}\label{sec:pure-meth}
+
+\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
+\indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
+\indexisarmeth{rule}\indexisarmeth{erule}
+\begin{matharray}{rcl}
+ fail & : & \isarmeth \\
+ succeed & : & \isarmeth \\
+ - & : & \isarmeth \\
+ assumption & : & \isarmeth \\
+ finish & : & \isarmeth \\
+ fold & : & \isarmeth \\
+ unfold & : & \isarmeth \\
+ rule & : & \isarmeth \\
+ erule^* & : & \isarmeth \\
+\end{matharray}
+
+\begin{rail}
+ ('fold' | 'unfold' | 'rule' | 'erule') thmrefs
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$ $]
+\end{descr}
+
+FIXME
+
+%FIXME sort
+%FIXME thmref (single)
+%FIXME var vs. term
+
+\indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
+\indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
+\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
+\begin{matharray}{rcl}
+ tag & : & \isaratt \\
+ untag & : & \isaratt \\
+ COMP & : & \isaratt \\
+ RS & : & \isaratt \\
+ OF & : & \isaratt \\
+ where & : & \isaratt \\
+ of & : & \isaratt \\
+ standard & : & \isaratt \\
+ elimify & : & \isaratt \\
+ transfer & : & \isaratt \\
+ export & : & \isaratt \\
+\end{matharray}
+
+\begin{rail}
+ ('tag' | 'untag') (nameref+)
+ ;
+ ('COMP' | 'RS') nat? thmref
+ ;
+ 'OF' thmrefs
+ ;
+ 'where' (term '=' term * 'and')
+ ;
+ 'of' (inst * ) ('concl:' (inst * ))?
+ ;
+
+ inst: underscore | term
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$ $]
+\end{descr}
+
+FIXME
\section{Axiomatic Type Classes}\label{sec:axclass}
@@ -23,7 +94,7 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{axclass}~$] FIXME
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
c@2$] setup up a goal stating the class relation or type arity. The proof
@@ -31,7 +102,7 @@
characteristic theorems of the type classes involved. After finishing the
proof the theory will be augmented by a type signature declaration
corresponding to the resulting theorem.
-\end{description}
+\end{descr}
@@ -49,9 +120,9 @@
%\end{rail}
-%\begin{description}
+%\begin{descr}
%\item [$ $]
-%\end{description}
+%\end{descr}
%%% Local Variables:
--- a/doc-src/IsarRef/hol.tex Tue Aug 03 13:16:29 1999 +0200
+++ b/doc-src/IsarRef/hol.tex Tue Aug 03 18:56:51 1999 +0200
@@ -1,5 +1,5 @@
-\chapter{Isabelle/HOL Tools and Packages}
+\chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools}
\section{Primitive types}
@@ -16,7 +16,7 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
$\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
also declares type arity $t :: (term, \dots, term) term$, making $t$ an
@@ -28,7 +28,7 @@
refer to the HOL $\isarkeyword{typedef}$ primitive, but uses more advanced
packages such as $\isarkeyword{record}$ (\S\ref{sec:record}) or
$\isarkeyword{datatype}$ (\S\ref{sec:datatype}).
-\end{description}
+\end{descr}
\section{Records}\label{sec:record}
@@ -47,18 +47,18 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
defines extensible record type $(\vec\alpha)t$, derived from the optional
parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
simply-typed records.
-\end{description}
+\end{descr}
\section{Datatypes}\label{sec:datatype}
-\indexisarcmd{datatype}\indexisarcmd{rep_datatype}
+\indexisarcmd{datatype}\indexisarcmd{rep-datatype}
\begin{matharray}{rcl}
\isarcmd{datatype} & : & \isartrans{theory}{theory} \\
\isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
@@ -77,10 +77,10 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{datatype}$] FIXME
\item [$\isarkeyword{rep_datatype}$] FIXME
-\end{description}
+\end{descr}
\section{Recursive functions}
@@ -100,15 +100,15 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{primrec}$] FIXME
\item [$\isarkeyword{recdef}$] FIXME
-\end{description}
+\end{descr}
\section{(Co)Inductive sets}
-\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive\_cases}
+\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive-cases}
\begin{matharray}{rcl}
\isarcmd{inductive} & : & \isartrans{theory}{theory} \\
\isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
@@ -128,10 +128,10 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] FIXME
\item [$\isarkeyword{inductive_cases}$] FIXME
-\end{description}
+\end{descr}
\section{Proof by induction}
--- a/doc-src/IsarRef/intro.tex Tue Aug 03 13:16:29 1999 +0200
+++ b/doc-src/IsarRef/intro.tex Tue Aug 03 18:56:51 1999 +0200
@@ -1,6 +1,15 @@
\chapter{Introduction}
+\section{Quick start}
+
+FIXME examples, ProofGeneral setup
+
+\section{Examples}
+
+\section{How to write Isar proofs anyway?}
+
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"
--- a/doc-src/IsarRef/isar-ref.tex Tue Aug 03 13:16:29 1999 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Tue Aug 03 18:56:51 1999 +0200
@@ -9,8 +9,8 @@
\makeindex
-\railterm{lbrace,rbrace,llbrace,rrbrace}
-\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim}
+\railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
+\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
\railalias{name}{\railqtoken{name}}
\railalias{nameref}{\railqtoken{nameref}}
@@ -37,7 +37,38 @@
\maketitle
\begin{abstract}
- FIXME
+ \emph{Intelligible semi-automated reasoning} (\emph{Isar}) is a generic
+ approach to readable formal proof documents. It sets out to bridge the
+ semantic gap between any internal notions of proof based on primitive
+ inferences and tactics, and an appropriate level of abstraction for
+ user-level work. The Isar formal proof language has been designed to
+ satisfy quite contradictory requirements, being both ``declarative'' and
+ immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.
+
+ The current version of Isabelle offers Isar as an alternative proof language
+ interface layer, beyond traditional tactic scripts. The Isabelle/Isar
+ system provides an interpreter for the Isar formal proof document language.
+ Isabelle/Isar input may consist either of \emph{proper document
+ constructors}, or \emph{improper auxiliary commands} (for diagnostics,
+ exploration etc.). Proof texts consisting of proper document constructors
+ only admit a purely static reading, thus being intelligible later without
+ requiring dynamic replay that is so typical for traditional proof scripts.
+ 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
+ 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,
+ including forward and backward tracing of partial documents; intermediate
+ states may be inspected by diagnostic commands.
+
+ The Isar subsystem of Isabelle is tightly integrated into the Isabelle/Pure
+ meta-logic implementation. Theories, theorems, proof procedures etc.\ may
+ be used interchangeably between Isabelle-classic proof scripts and
+ Isabelle/Isar documents. Isar is as generic as Isabelle, able to support a
+ wide range of object-logics. The current end-user setup is mainly for
+ Isabelle/HOL.
\end{abstract}
\pagenumbering{roman} \tableofcontents \clearfirst
--- a/doc-src/IsarRef/pure.tex Tue Aug 03 13:16:29 1999 +0200
+++ b/doc-src/IsarRef/pure.tex Tue Aug 03 18:56:51 1999 +0200
@@ -1,11 +1,27 @@
-\chapter{Common Isar elements}
+\chapter{Basic Isar elements}
+
+Subsequently, we introduce most of the basic Isar theory and proof commands as
+provided by Isabelle/Pure. Chapter~\ref{ch:gen-tools} describes further Isar
+elements as provided by generic tools and packages that are either part of
+Pure Isabelle, or preloaded by most object logics (such as the simplifier).
+See chapter~\ref{ch:hol-tools} for actual object-logic specific elements (for
+Isabelle/HOL).
-FIXME $*$ indicates \emph{improper commands}
+\medskip
+
+Isar commands may be either \emph{proper} document constructors, or
+\emph{improper commands} (indicated by $^*$). Improper commands might be
+helpful when developing proof documents, while their use is strongly
+discouraged for the final outcome. Typical examples are diagnostic commands
+that print terms or theorems according to the current context; other commands
+even emulate old-style tactical theorem proving, which facilitates porting of
+legacy proof scripts.
+
\section{Theory commands}
-\subsection{Defining theories}
+\subsection{Defining theories}\label{sec:begin-thy}
\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
\begin{matharray}{rcl}
@@ -15,15 +31,16 @@
\end{matharray}
Isabelle/Isar ``new-style'' theories are either defined via theory files or
-interactively.\footnote{In contrast, ``old-style'' Isabelle theories support
- batch processing only, with only the ML proof script part suitable for
- interaction.}
+interactively. Both actual theory specifications and proofs are handled
+uniformly --- occasionally definitional mechanisms even require some proof.
+In contrast, ``old-style'' Isabelle theories support batch processing only,
+with the proof scripts collected in separate ML files.
The first command of any theory has to be $\THEORY$, starting a new theory
-based on the merge of existing ones. In interactive experiments, the theory
-context may be changed by $\CONTEXT$ without creating a new theory. In both
-cases the concluding command is $\END$, which has to be the very last one of
-any proper theory file.
+based on the merge of existing ones. The theory context may be changed by
+$\CONTEXT$ without creating a new theory. In both cases $\END$ concludes the
+theory development; it has to be the very last command of any proper theory
+file.
\begin{rail}
'theory' name '=' (name + '+') filespecs? ':'
@@ -33,38 +50,42 @@
'end'
;;
- filespecs : 'files' ((name | '(' name ')') +);
+ filespecs: 'files' ((name | parname) +);
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\THEORY~A = B@1 + \cdots + B@n$] commences a new theory $A$ based on
existing ones $B@1 + \cdots + B@n$. Note that Isabelle's theory loader
system ensures that any of the base theories are properly loaded (and fully
- up-to-date when $\THEORY$ is executed interactively).
+ up-to-date when $\THEORY$ is executed interactively). The optional
+ $\isarkeyword{files}$ specification declares additional dependencies on ML
+ files. Unless put in in parentheses, any file will be loaded immediately
+ via $\isarcmd{use}$ (see also \S\ref{sec:ML}).
-\item [$\CONTEXT~B$] enters existing theory context $B$, basically in
+\item [$\CONTEXT~B$] enters an existing theory context $B$, basically in
read-only mode, so only a limited set of commands may be performed. Just as
for $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.
-\item [$\END$] concludes the current theory definition of context switch.
-\end{description}
+\item [$\END$] concludes the current theory definition or context switch.
+\end{descr}
-\subsection{Formal comments}
+\subsection{Formal comments}\label{sec:formal-cmt-thy}
-\indexisarcmd{title}\indexisarcmd{chapter}\indexisarcmd{subsection}\indexisarcmd{subsubsection}
-\indexisarcmd{text}\indexisarcmd{txt}
+\indexisarcmd{title}\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
+\indexisarcmd{subsubsection}\indexisarcmd{text}
\begin{matharray}{rcl}
\isarcmd{title} & : & \isartrans{theory}{theory} \\
\isarcmd{chapter} & : & \isartrans{theory}{theory} \\
+ \isarcmd{section} & : & \isartrans{theory}{theory} \\
\isarcmd{subsection} & : & \isartrans{theory}{theory} \\
\isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
\isarcmd{text} & : & \isartrans{theory}{theory} \\
- \isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\
\end{matharray}
-There are several commands to include \emph{formal comments} in theory and
-proof specification. In contrast to source-level comments
+There are several commands to include \emph{formal comments} in theory
+specification (a few more are available for proofs, see
+\S\ref{sec:formal-cmt-prf}). In contrast to source-level comments
\verb|(*|\dots\verb|*)|, which are stripped at the lexical level, any text
given as formal comment is meant to be part of the actual document.
Consequently, it would be included in the final printed version.
@@ -81,28 +102,20 @@
\begin{rail}
'title' text text? text?
;
- 'chapter' text
- ;
- 'subsection' text
- ;
- 'subsubsection' text
- ;
- 'text' text
- ;
- 'txt' text
+ ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') text
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{title}~title~author~date$] specifies the document title
just as in typical LaTeX documents.
-\item [$\isarkeyword{chapter}~text$, $\isarkeyword{subsection}~text$,
- $\isarkeyword{subsubsection}~text$] specify chapter and subsection headings.
+\item [$\isarkeyword{chapter}~text$, $\isarkeyword{section}~text$,
+ $\isarkeyword{subsection}~text$, $\isarkeyword{subsubsection}~text$] specify
+ chapter and subsection headings.
\item [$\TEXT~text$] specifies an actual body of prose text, including
references to formal entities.\footnote{The latter feature is not yet
exploited in any way.}
-\item [$\TXT~text$] is similar to $\TEXT$, but may appear within proofs.
-\end{description}
+\end{descr}
\subsection{Type classes and sorts}\label{sec:classes}
@@ -115,7 +128,7 @@
\end{matharray}
\begin{rail}
- 'classes' (classdecl +)
+ 'classes' (classdecl comment? +)
;
'classrel' nameref '<' nameref comment?
;
@@ -123,7 +136,7 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{classes}~c<cs ~\dots$] declares class $c$ to be a
subclass of existing classes $cs$. Cyclic class structures are ruled out.
\item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
@@ -133,7 +146,7 @@
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
any type variables input without sort constraints. Typically, the default
sort would be only changed when defining new logics.
-\end{description}
+\end{descr}
\subsection{Types}\label{sec:types-pure}
@@ -157,7 +170,7 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\TYPES~(\vec\alpha)t = \tau~\dots$] 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
@@ -174,7 +187,7 @@
order-sorted signature of types by new type constructor arities. This is
done axiomatically! The $\isarkeyword{instance}$ command provides a way
introduce proven type arities (see \S\ref{sec:axclass}).
-\end{description}
+\end{descr}
\subsection{Constants and simple definitions}
@@ -198,7 +211,7 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\CONSTS~c::\tau~\dots$] declares constant $c$ to have any instance of
type scheme $\tau$. The optional mixfix annotations may attach concrete
syntax to the constant.
@@ -208,10 +221,10 @@
\item [$\isarkeyword{constdefs}~c::\tau~eqn~\dots$] combines constant
declarations and definitions, using canonical name $c_def$ for the
definitional axiom.
-\end{description}
+\end{descr}
-\subsection{Concrete syntax}
+\subsection{Syntax and translations}
\indexisarcmd{syntax}\indexisarcmd{translations}
\begin{matharray}{rcl}
@@ -228,7 +241,7 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{syntax}~mode~decls$] is similar to $\CONSTS~decls$,
except the actual logical signature extension. Thus the context free
grammar of Isabelle's inner syntax may be augmented in arbitrary ways. The
@@ -240,7 +253,7 @@
(\texttt{=>}), print rules (\texttt{<=}). Translation patterns may be
prefixed by the syntactic category to be used for parsing; the default is
\texttt{logic}.
-\end{description}
+\end{descr}
\subsection{Axioms and theorems}
@@ -259,7 +272,7 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{axioms}~name: \phi~\dots$] introduces arbitrary
statements as logical axioms. In fact, axioms are ``axiomatic theorems'',
and may be referred as any other theorems later.
@@ -272,35 +285,32 @@
the default simpset, for example.
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
tags the results as ``lemma''.
-\end{description}
+\end{descr}
-\subsection{Manipulating name spaces}
+\subsection{Name spaces}
-\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{path}
+Isabelle organizes any kind of names (of types, constants, theorems etc.) by
+hierarchically structured name spaces. Normally the user never has to control
+the behavior of name space entry by hand, yet the following commands provide
+some way to do so.
+
+\indexisarcmd{global}\indexisarcmd{local}
\begin{matharray}{rcl}
\isarcmd{global} & : & \isartrans{theory}{theory} \\
\isarcmd{local} & : & \isartrans{theory}{theory} \\
- \isarcmd{path} & : & \isartrans{theory}{theory} \\
\end{matharray}
-\begin{rail}
- 'global'
- ;
- 'local'
- ;
- 'path' nameref
- ;
-\end{rail}
-
-\begin{description}
-\item [$\isarkeyword{global}$] FIXME
-\item [$\isarkeyword{local}$] FIXME
-\item [$\isarkeyword{path}~name$] FIXME
-\end{description}
+\begin{descr}
+\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
+ name declaration mode. Initially, theories start in $\isarkeyword{local}$
+ mode, causing all names to be automatically qualified by the theory name.
+ Changing this to $\isarkeyword{global}$ causes all names to be declared as
+ base names only.
+\end{descr}
-\subsection{Incorporating ML code}
+\subsection{Incorporating ML code}\label{sec:ML}
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{setup}
\begin{matharray}{rcl}
@@ -318,18 +328,25 @@
;
\end{rail}
-\begin{description}
-\item [$\isarkeyword{use}~file$] FIXME
-\item [$\isarkeyword{ML}~text$] FIXME
-\item [$\isarkeyword{setup}~text$] FIXME
-\end{description}
+\begin{descr}
+\item [$\isarkeyword{use}~file$] reads and execute ML commands from $file$.
+ The current theory context as passed down to the ML session. Furthermore,
+ the file name is checked with the dependency declarations given in the
+ theory header (see also \S\ref{sec:begin-thy}).
+ \item [$\isarkeyword{ML}~text$] reads and executes ML commands from $text$.
+ The theory context is passed just as in $\isarkeyword{use}$.
+\item [$\isarkeyword{setup}~text$] changes the current theory context by
+ applying setup functions $text$ (which has to be an ML expression of type
+ $(theory -> theory)~list$. The $\isarkeyword{setup}$ is the usual way to
+ initialize object-logic specific tools and packages written in ML.
+\end{descr}
-\subsection{ML translation functions}
+\subsection{Syntax translation functions}
-\indexisarcmd{parse\_ast\_translation}\indexisarcmd{parse\_translation}
-\indexisarcmd{print\_translation}\indexisarcmd{typed\_print\_translation}
-\indexisarcmd{print\_ast\_translation}\indexisarcmd{token\_translation}
+\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
+\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
+\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
\begin{matharray}{rcl}
\isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
\isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
@@ -358,107 +375,50 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{oracle}~name=text$] FIXME
-\end{description}
+\end{descr}
\section{Proof commands}
-\subsection{Goal statements}
+Proof commands provide transitions of Isar/VM machine configurations. There
+are three different kinds of operation:
+\begin{descr}
+\item [$proof(prove)$] means that a new goal has just been stated that is now
+ to be \emph{proven}; the next command may refine it by some proof method
+ ($\approx$ tactic) and enter a sub-proof to establish the final result.
+\item [$proof(state)$] is like an internal theory mode: the context may be
+ augmented by \emph{stating} additional assumptions, intermediate result;
+\item [$proof(chain)$] indicates an intermediate mode between $proof(state)$
+ and $proof(state)$: some already established facts have been just picked up
+ in order to use them when refining the subsequent goal.
+\end{descr}
-\indexisarcmd{theorem}\indexisarcmd{lemma}
-\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
+
+\subsection{Formal comments}\label{sec:formal-cmt-prf}
+
+The following formal comments in proof mode closely correspond to the ones of
+theory mode (see \S\ref{sec:formal-cmt-thy} for more information).
+
+\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}\indexisarcmd{txt}
\begin{matharray}{rcl}
- \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
- \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
- \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
- \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
- \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
- \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
+ \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
+ \isarcmd{subsect} & : & \isartrans{proof(state)}{proof(state)} \\
+ \isarcmd{subsubsect} & : & \isartrans{proof(state)}{proof(state)} \\
+ \isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\
\end{matharray}
\begin{rail}
- ('theorem' | 'lemma') goal
- ;
- ('have' | 'show' | 'hence' | 'thus') goal
- ;
-
- goal: thmdecl? proppat comment?
+ ('sect' | 'subsect' | 'subsubsect' | 'txt') text
;
\end{rail}
-\begin{description}
-\item [$\THEOREM{name}{\phi}$] enters proof mode with $\phi$ as main goal,
- eventually resulting in some theorem $\turn \phi$, which stored in the
- theory.
-\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
- ``lemma''.
-\item [$\HAVE{name}{\phi}$] FIXME
-\item [$\SHOW{name}{\phi}$] FIXME
-\item [$\HENCE{name}{\phi}$] FIXME
-\item [$\THUS{name}{\phi}$] FIXME
-\end{description}
-
-
-\subsection{Initial and terminal proof steps}
-
-\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
-\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
-\begin{matharray}{rcl}
- \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
- \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
- \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
- \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
- \isarcmd{..} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
- \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
-\end{matharray}
-
-\begin{rail}
- 'proof' interest? meth? comment?
- ;
- 'qed' meth? comment?
- ;
- 'by' meth meth? comment?
- ;
- ('.' | '..' | 'sorry') comment?
- ;
-
- meth: method interest?
- ;
-\end{rail}
-
-\begin{description}
-\item [$ $] FIXME
-\end{description}
-
-
-\subsection{Facts and forward chaining}
-
-\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
-\begin{matharray}{rcl}
- \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
- \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
- \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
- \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
-\end{matharray}
-
-\begin{rail}
- 'note' thmdef? thmrefs comment?
- ;
- 'then' comment?
- ;
- ('from' | 'with') thmrefs comment?
- ;
-\end{rail}
-
-\begin{description}
-\item [$ $] FIXME
-\end{description}
-
\subsection{Proof context}
+FIXME
+
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}\indexisarcmd{let}
\begin{matharray}{rcl}
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
@@ -482,13 +442,195 @@
;
\end{rail}
-\begin{description}
-\item [$ $] FIXME
-\end{description}
+\begin{descr}
+\item [$\FIX{x}$] FIXME
+\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] FIXME
+\item [$\DEF{a}{x \equiv t}$] FIXME
+\item [$\LET{\vec p = \vec t}$] FIXME
+\end{descr}
+
+
+\subsection{Facts and forward chaining}
+
+FIXME
+
+\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
+\begin{matharray}{rcl}
+ \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
+ \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
+ \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
+ \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
+\end{matharray}
+
+\begin{rail}
+ 'note' thmdef? thmrefs comment?
+ ;
+ 'then' comment?
+ ;
+ ('from' | 'with') thmrefs comment?
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\NOTE{a}{bs}$] recalls existing facts $bs$, binding the result as $a$
+ (and $facts$). Note that attributes may be involved as well, both on the
+ left and right hand side.
+\item [$\THEN$] indicates forward chaining by the current facts in order to
+ establish the subsequent goal. The initial proof method invoked to solve
+ that will be offered these facts to do anything ``appropriate'' (see also
+ \S\ref{sec:proof-steps}). For example, method $rule$ (see
+ \S\ref{sec:pure-meth}) would do an elimination rather than an introduction.
+\item [$\FROM{bs}$] abbreviates $\NOTE{facts}{bs}~\THEN$; also note that
+ $\THEN$ is equivalent to $\FROM{facts}$.
+\item [$\WITH{bs}$] abbreviates $\FROM{bs~facts}$; thus the forward chaining
+ is from earlier facts together with the current ones.
+\end{descr}
+
+
+\subsection{Goal statements}
+
+Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
+and $\LEMMANAME$. New local goals may be claimed within proof mode: four
+variants indicate whether the result is meant to solve some pending goal and
+whether forward chaining is employed.
+
+\indexisarcmd{theorem}\indexisarcmd{lemma}
+\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
+\begin{matharray}{rcl}
+ \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
+ \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
+ \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
+ \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
+ \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
+ \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
+\end{matharray}
+
+\begin{rail}
+ ('theorem' | 'lemma') goal
+ ;
+ ('have' | 'show' | 'hence' | 'thus') goal
+ ;
+
+ goal: thmdecl? proppat comment?
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\THEOREM{name}{\phi}$] enters proof mode with $\phi$ as main goal,
+ eventually resulting in some theorem $\turn \phi$, which stored in the
+ theory.
+\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
+ ``lemma''.
+\item [$\HAVE{name}{\phi}$] claims a local goal, eventually resulting in a
+ theorem with the current assumption context as hypotheses.
+\item [$\SHOW{name}{\phi}$] same as $\HAVE{name}{\phi}$, but solves some
+ pending goal with the result exported to the enclosing assumption context.
+\item [$\HENCE{name}{\phi}$] abbreviates $\THEN~\HAVE{name}{\phi}$, i.e.\
+ claims a local goal to be proven by forward chaining the current facts.
+\item [$\THUS{name}{\phi}$] abbreviates $\THEN~\SHOW{name}{\phi}$.
+\end{descr}
+
+
+\subsection{Initial and terminal proof steps}\label{sec:proof-steps}
+
+Arbitrary goal refinements via tactics is considered harmful. Consequently
+the Isar framework admits proof methods to be invoked in two places only.
+\begin{enumerate}
+\item An \emph{initial} refinement step (via $\PROOF{m@1}$) reduces a newly
+ stated intermediate goal to a number of sub-goals that are to be solved
+ subsequently. Facts are passed to $m@1$ for forward chaining if so
+ indicated by $proof(chain)$ mode.
+
+\item A \emph{terminal} conclusion step (via $\QED{m@2}$)) solves any remaining
+ pending goals completely. No facts are passed to $m@2$.
+\end{enumerate}
+
+The only other proper way to affect pending goals is by $\SHOWNAME$, which
+involves an explicit statement of what is solved.
+
+Also note that initial proof methods should either solve the goal completely,
+or constitute some well-understood deterministic 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. A much better technique is to $\SHOWNAME$ some non-trivial
+reduction as an explicit rule, which is solved completely by some automated
+method, and then applied to some pending goal.
+
+\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
+\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
+\begin{matharray}{rcl}
+ \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
+ \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
+ \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ \isarcmd{..} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+ \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
+\end{matharray}
+
+\begin{rail}
+ 'proof' interest? meth? comment?
+ ;
+ 'qed' meth? comment?
+ ;
+ 'by' meth meth? comment?
+ ;
+ ('.' | '..' | 'sorry') comment?
+ ;
+
+ meth: method interest?
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\PROOF{m}$] refines the pending goal by proof method $m$ (facts for
+ forward chaining are passed if indicated by $proof(chain)$).
+\item [$\QED{m}$] refines any remaining goals by proof method $m$ and
+ concludes the sub-proof. If the goal had been $\SHOWNAME$, some pending
+ sub-goal is solved as well by the rule resulting from the result exported to
+ the enclosing goal context.
+
+ Thus $\QEDNAME$ may fail for two reasons: either $m$ fails to solve all
+ remaining goals completely, or the resulting rule does not resolve with any
+ enclosing goal. Debugging such a situation might involve temporarily
+ changing $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by
+ replacing $\ASSUMENAME$ by $\PRESUMENAME$.
+\item [$\BY{m@1}{m@2}$] is a \emph{terminal proof}; it abbreviates
+ $\PROOF{m@1}~\QED{m@2}$, automatically backtracking across both methods.
+
+ Debugging an unsuccessful $\BY{m@1}{m@2}$ commands might be done by simply
+ expanding the abbreviation by hand; usually $\PROOF{m@1}$ is already
+ sufficient to see what goes wrong.
+\item [$\isarkeyword{..}$] is a \emph{default proof}; it abbreviates
+ $\BY{default}{finish}$, where method $default$ usually applies a single
+ elimination or introduction rule according to the topmost symbol, and
+ $finish$ solves all goals by assumption.
+\item [$\isarkeyword{.}$] is a \emph{trivial proof}, it abbreviates
+ $\BY{-}{finish}$, where method $-$ does nothing except inserting any facts
+ into the proof state.
+\item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that
+ \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve
+ the goal without much ado. Of course, the result is a fake theorem only,
+ involving some oracle in its internal derivation object. Note that this is
+ indicated as \texttt{[!]} in the printed result. The main application of
+ $\isarkeyword{sorry}$ is to support top-down proof development.
+\end{descr}
\subsection{Block structure}
+While Isar is inherently block-structured, opening and closing blocks is
+mostly handled rather casually, with little explicit user-intervention. Any
+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 are typically switched via
+$\isarkeyword{next}$, which is just a single block-close followed by
+block-open again. Thus the effect of $\isarkeyword{next}$ is to reset the
+proof context to that of the head of the sub-proof. Note that there is no
+goal focus involved!
+
+There are explicit block parentheses as well. These typically achieve a
+strong forward style of reasoning.
+
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
\begin{matharray}{rcl}
\isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
@@ -496,10 +638,15 @@
\isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
\end{matharray}
-\begin{description}
-\item [$ $] FIXME
-\end{description}
-
+\begin{descr}
+\item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,
+ resetting the context to the initial one.
+\item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
+ close blocks. Any current facts pass through $\isarkeyword{\{\{}$
+ unchanged, while $\isarkeyword{\}\}}$ causes them to be \emph{exported} into
+ the enclosing context. Thus fixed variables are generalized, assumptions
+ discharged, and local definitions eliminated.
+\end{descr}
\subsection{Calculational proof}
@@ -517,15 +664,19 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$ $] FIXME
-\end{description}
+\end{descr}
\subsection{Improper proof steps}
-\indexisarcmd{apply}\indexisarcmd{then\_apply}\indexisarcmd{back}
+The following commands emulate tactic scripts to some extent. While these are
+anathema for writing proper Isar proof documents, they might come in handy for
+exploring and debugging.
+
+\indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back}
\begin{matharray}{rcl}
\isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
\isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
@@ -544,9 +695,9 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$ $] FIXME
-\end{description}
+\end{descr}
\section{Other commands}
@@ -572,7 +723,7 @@
;
\end{rail}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{typ}~\tau$, $\isarkeyword{term}~t$,
$\isarkeyword{prop}~\phi$] read and print types / terms / propositions
according to the current theory or proof context.
@@ -580,13 +731,13 @@
theory or proof context. Note that any attributes included in the theorem
specifications are applied to a temporary proof context derived from the
current theory or proof; the resulting context is discarded.
-\end{description}
+\end{descr}
\subsection{System operations}
-\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use\_thy}\indexisarcmd{use\_thy\_only}
-\indexisarcmd{update\_thy}\indexisarcmd{update\_thy\_only}
+\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
+\indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
\begin{matharray}{rcl}
\isarcmd{cd} & : & \isarkeep{\cdot} \\
\isarcmd{pwd} & : & \isarkeep{\cdot} \\
@@ -596,7 +747,7 @@
\isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\
\end{matharray}
-\begin{description}
+\begin{descr}
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
process.
\item [$\isarkeyword{pwd}~$] prints the current working directory.
@@ -604,7 +755,7 @@
$\isarkeyword{update_thy}~name$, $\isarkeyword{update_thy_only}~name$] load
theory files. These commands are exactly the same as the corresponding ML
functions (see also \cite[\S1 and \S6]{isabelle-ref}).
-\end{description}
+\end{descr}
%%% Local Variables:
--- a/doc-src/IsarRef/syntax.tex Tue Aug 03 13:16:29 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex Tue Aug 03 18:56:51 1999 +0200
@@ -18,18 +18,18 @@
entities, such as names, terms, theorem specifications, which have been
factored out of the actual Isar language elements described later.
-Some of the basic syntactic entities introduced below act much like tokens
-rather than nonterminals, in particular for error messages are concerned.
+Note that some of the basic syntactic entities introduced below act much like
+tokens rather than nonterminals, in particular for the sake of error messages.
E.g.\ syntax elements such as $\CONSTS$ referring to \railqtoken{name} or
-\railqtoken{type} would really report a missing \railqtoken{name} or
-\railqtoken{type} rather than any of its constituent primitive tokens
-(\railtoken{ident}, \railtoken{string} etc.).
+\railqtoken{type} would really report a missing name or type rather than any
+of the constituent primitive tokens such as \railtoken{ident} or
+\railtoken{string}.
\subsection{Names}
Entity \railqtoken{name} usually refers to any name of types, constants,
-theorems, etc.\ to be \emph{declared} or \emph{defined} (so qualified
+theorems etc.\ that are to be \emph{declared} or \emph{defined} (so qualified
identifiers are excluded). Quoted strings provide an escape for
non-identifier names or those ruled out by outer syntax keywords (e.g.\
\verb|"let"|). Already existing objects are usually referenced by
@@ -37,34 +37,37 @@
\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
\begin{rail}
- name : ident | symident | string
+ name: ident | symident | string
;
- parname : '(' name ')'
+ parname: '(' name ')'
;
- nameref : name | longident
+ nameref: name | longident
;
\end{rail}
\subsection{Comments}
-Large chunks of plain \railqtoken{text} are usually given \railtoken{verbatim},
-i.e.\ enclosed in \verb|{*|\dots\verb|*}|. For convenience, any of the
-smaller text entities (\railtoken{ident}, \railtoken{string} etc.) are
-admitted as well. Almost any of the Isar commands may be annotated by a
-marginal \railnonterm{comment}: \texttt{--} \railqtoken{text}. Note that this
-kind of comment is actually part of the language, while source level comments
-\verb|(*|\dots\verb|*)| are already stripped at the lexical level. A few
-commands such as $\PROOFNAME$ admit additional markup with a ``level of
-interest'', currently only \texttt{\%} for ``boring, don't read this''.
+Large chunks of plain \railqtoken{text} are usually given
+\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|\dots\verb|*}|. For
+convenience, any of the smaller text conforming to \railqtoken{nameref} are
+admitted as well. Almost any of the Isar commands may be annotated by some
+marginal \railnonterm{comment} of the form \texttt{--} \railqtoken{text}.
+Note that this kind of comment is actually part of the language, while source
+level comments \verb|(*|\dots\verb|*)| are already stripped at the lexical
+level. A few commands such as $\PROOFNAME$ admit additional markup with a
+``level of interest'': \texttt{\%} followed by an optional number $n$ (default
+$n = 1$) indicates that the respective part of the document becomes $n$ levels
+more boring or obscure; \texttt{\%\%} means that the interest drops by
+$\infty$ --- abandon every hope, who enter here.
\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
\begin{rail}
- text : verbatim | nameref
+ text: verbatim | nameref
;
- comment : '--' text
+ comment: '--' text
;
- interest : '\%'
+ interest: percent nat? | ppercent
;
\end{rail}
@@ -72,68 +75,67 @@
\subsection{Sorts and arities}
The syntax of sorts and arities is given directly at the outer level. Note
-that this in contrast to that types and terms (see below). Only few commands
-ever refer to sorts or arities explicitly.
+that this is in contrast to that types and terms (see \ref{sec:types-terms}).
\indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
\indexouternonterm{classdecl}
\begin{rail}
- sort : nameref | lbrace (nameref * ',') rbrace
+ classdecl: name ('<' (nameref ',' +))?
;
- arity : ( () | '(' (sort + ',') ')' ) sort
+ sort: nameref | lbrace (nameref * ',') rbrace
;
- simplearity : ( () | '(' (sort + ',') ')' ) nameref
+ arity: ('(' (sort + ',') ')')? sort
;
- classdecl: name ('<' (nameref ',' +))? comment?
+ simplearity: ('(' (sort + ',') ')')? nameref
+ ;
\end{rail}
-\subsection{Types and terms}
+\subsection{Types and terms}\label{sec:types-terms}
-The actual inner Isabelle syntax, i.e.\ that of types and terms, is far too
-flexible in order to be modeled explicitly at the outer theory level.
-Basically, any such entity would have to be quoted at the outer level to turn
-it into a single token, with the actual parsing deferred to some functions
-that read and type-check terms etc.\ (note that \railqtoken{prop}s will be
-handled differently from plain \railqtoken{term}s here). For convenience, the
-quotes may be omitted for any \emph{atomic} term or type (e.g.\ a single
-variable).
+The actual inner Isabelle syntax, that of types and terms of the logic, is far
+too flexible in order to be modeled explicitly at the outer theory level.
+Basically, any such entity has to be quoted at the outer level to turn it into
+a single token, with the actual parsing deferred to some functions for reading
+and type-checking. For convenience, a more liberal convention is adopted:
+quotes may be omitted for any type or term that is already \emph{atomic} at
+the outer level. E.g.\ one may write \texttt{x} instead of \texttt{"x"}.
\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
\begin{rail}
- type : nameref | typefree | typevar
+ type: nameref | typefree | typevar
;
- term : nameref | var | textvar | nat
+ term: nameref | var | textvar | nat
;
- prop : term
+ prop: term
;
\end{rail}
-Type definitions etc.\ usually refer to \railnonterm{typespec} on the
-left-hand side. This models basic type constructor application at the outer
-syntax level. Note that only plain postfix notation is available here, but no
-infixes.
+Type declarations and definitions usually refer to \railnonterm{typespec} on
+the left-hand side. This models basic type constructor application at the
+outer syntax level. Note that only plain postfix notation is available here,
+but no infixes.
\indexouternonterm{typespec}
\begin{rail}
- typespec : (() | typefree | '(' ( typefree + ',' ) ')') name
+ typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
;
\end{rail}
\subsection{Term patterns}
-Statements like $\SHOWNAME$ involve propositions, some others like $\DEFNAME$
-plain terms. Any of these usually admit automatic binding of schematic text
-variables by giving (optional) patterns $\IS{p@1 \dots p@n}$. For
-\railqtoken{prop}s the $\CONCLNAME$ part refers to the conclusion only, in case
-actual rules are involved, rather than atomic propositions.
+Assumptions and goal statements usually admit automatic binding of schematic
+text variables by giving (optional) patterns of the form $\IS{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}
- termpat : '(' (term + 'is' ) ')'
+ termpat: '(' ('is' term +) ')'
;
- proppat : '(' (() | (prop + 'is' )) (() | 'concl' (prop + 'is' )) ')'
+ proppat: '(' (('is' prop +) | 'concl' ('is' prop +) | ('is' prop +) 'concl' ('is' prop +)) ')'
;
\end{rail}
@@ -141,16 +143,17 @@
\subsection{Mixfix annotations}
Mixfix annotations specify concrete \emph{inner} syntax of Isabelle types and
-terms. Some commands such as $\TYPES$ admit infixes only, while $\CONSTS$
-etc.\ support the full range of general mixfixes and binders.
+terms. Some commands such as $\TYPES$ admit infixes only, while $\CONSTS$ and
+$\isarkeyword{syntax}$ support the full range of general mixfixes and binders.
\indexouternonterm{infix}\indexouternonterm{mixfix}
\begin{rail}
- infix : '(' ('infixl' | 'infixr') (() | string) nat ')'
+ infix: '(' ('infixl' | 'infixr') string? nat ')'
+ ;
+ mixfix: infix | '(' string pris? nat? ')' | '(' 'binder' string pris? nat ')'
;
- mixfix : infix | string (() | '[' (nat + ',') ']') (() | nat) |
- 'binder' string (() | '[' (nat + ',') ']') nat
+ pris: '[' (nat + ',') ']'
;
\end{rail}
@@ -161,42 +164,41 @@
``semi-inner'' syntax, which does not have to be atomic at the outer level
unlike that of types and terms. Instead, the attribute argument
specifications may be any sequence of atomic entities (identifiers, strings
-etc.), or properly bracketed argument lists. Below \railqtoken{atom} refers to
-any atomic entity (\railtoken{ident}, \railtoken{longident},
-\railtoken{symident} etc.), including keywords that conform to
-\railtoken{symident}, but do not coincide with actual command names.
+etc.), or properly bracketed argument lists. Below \railqtoken{atom} refers
+to any atomic entity, including keywords that conform to \railtoken{symident}.
\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
\begin{rail}
- atom : nameref | typefree | typevar | var | textvar | nat
+ atom: nameref | typefree | typevar | var | textvar | nat | keyword
;
- arg : atom | '(' args ')' | '[' args ']' | lbrace args rbrace
+ arg: atom | '(' args ')' | '[' args ']' | lbrace args rbrace
;
- args : arg *
+ args: arg *
;
- attributes : '[' (nameref args * ',') ']'
+ attributes: '[' (nameref args * ',') ']'
;
\end{rail}
-Theorem specifications come in three flavors: \railnonterm{thmdecl} usually
-refers to the result of an assumption or goal statement (e.g.\ $\SHOWNAME$),
-\railnonterm{thmdef} collects lists of existing theorems (as in $\NOTENAME$),
-\railnonterm{thmrefs} refers to any list of existing theorems (e.g.\ occurring
-as proof method arguments). Any of these may include lists of attributes,
-which are applied to the preceding theorem or list of theorems.
+Theorem specifications come in several flavors: \railnonterm{axmdecl} and
+\railnonterm{thmdecl} usually refer to assumptions or results of goal
+statements, \railnonterm{thmdef} collects lists of existing theorems,
+\railnonterm{thmrefs} refers to any lists of existing theorems. Any of these
+may include lists of attributes, which are applied to the preceding theorem or
+list of theorems.
\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
\begin{rail}
- thmname : name attributes | name | attributes
+ axmdecl: name attributes? ':'
;
- axmdecl : name attributes? ':'
+ thmdecl: thmname ':'
;
- thmdecl : thmname ':'
+ thmdef: thmname '='
;
- thmdef : thmname '='
+ thmrefs: nameref attributes? +
;
- thmrefs : nameref (() | attributes) +
+
+ thmname: name attributes | name | attributes
;
\end{rail}
@@ -205,19 +207,18 @@
Proof methods are either basic ones, or expressions composed of methods via
``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternatives),
-``\texttt{?}'' (try), ``\texttt{*}'' (repeat, ${} \ge 0$ times),
-``\texttt{+}'' (repeat, ${} > 0$ times). In practice, proof methods are very
-often just a comma separated list of \railqtoken{nameref}~\railnonterm{args}
-specifications. Thus the syntax is similar to that of attributes, with plain
-parentheses instead of square brackets (see also \S\ref{sec:syn-att}). Note
-that parentheses may be dropped for single method specifications without
-arguments.
+``\texttt{?}'' (try), ``\texttt{*}'' (repeat ${} \ge 0$ times), ``\texttt{+}''
+(repeat ${} > 0$ times). In practice, proof methods are usually just a comma
+separated list of \railqtoken{nameref}~\railnonterm{args} specifications.
+Thus the syntax is similar to that of attributes, with plain parentheses
+instead of square brackets (see also \S\ref{sec:syn-att}). Note that
+parentheses may be dropped for single method specifications without arguments.
\indexouternonterm{method}
\begin{rail}
- method : (nameref | '(' methods ')') (() | '?' | '*' | '+')
+ method: (nameref | '(' methods ')') (() | '?' | '*' | '+')
;
- methods : (nameref args | method) + (',' | '|')
+ methods: (nameref args | method) + (',' | '|')
;
\end{rail}