--- a/doc-src/IsarRef/basics.tex Sun Aug 22 18:21:36 1999 +0200
+++ b/doc-src/IsarRef/basics.tex Sun Aug 22 21:13:20 1999 +0200
@@ -4,23 +4,36 @@
Isabelle/Isar offers two main improvements over classic Isabelle:
\begin{enumerate}
\item A new \emph{theory format}, often referred to as ``new-style theories'',
- supporting interactive development with unlimited undo operation.
-\item A formal \emph{proof language} language designed to support
- \emph{intelligible} semi-automated reasoning. Rather than putting together
- tactic scripts, the author is enabled to express the reasoning in way that
- is close to mathematical practice.
+ supporting interactive development and unlimited undo operation.
+\item A \emph{formal proof language} designed to support intelligible
+ semi-automated reasoning. Rather than putting together tactic scripts, the
+ author is enabled to express the reasoning in way that is close to
+ mathematical practice.
\end{enumerate}
The Isar proof language is embedded into the new theory format as a proper
sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or
-$\LEMMANAME$ at the theory levels, and left with the final end of proof. Some
-theory extension mechanisms require proof as well, such as the HOL
-$\isarkeyword{typedef}$.
+$\LEMMANAME$ at the theory levels, and left with the final end of proof (e.g.\
+via $\QEDNAME$). Some theory extension mechanisms require proof as well, such
+as the HOL $\isarkeyword{typedef}$ mechanism that only works for non-empty
+representing sets.
New-style theory files may still be associated with an ML file consisting of
-plain old tactic scripts. Generally, migration between the two formats is
-made relatively easy, and users may start to benefit from interactive theory
-development even before they have any idea of the Isar proof language.
+plain old tactic scripts. There is no longer any ML binding generated for the
+theory and theorems, though. Functions \texttt{theory}, \texttt{thm}, and
+\texttt{thms} may be used to retrieve this information from ML (see also
+\cite{isabelle-ref}). Nevertheless, migration between classic Isabelle and
+Isabelle/Isar is relatively easy. Thus users may start to benefit from
+interactive theory development even before they have any idea of the Isar
+proof language.
+
+\begin{warn}
+ Proof~General does \emph{not} support mixed interactive development of
+ classic Isabelle theory files and tactic scripts together with Isar
+ documents at the same time. The \texttt{isa} and \texttt{isar} versions of
+ Proof~General appear as two different theorem proving systems; only one
+ prover may be active at any time.
+\end{warn}
\section{The Isar proof language}
--- a/doc-src/IsarRef/generic.tex Sun Aug 22 18:21:36 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Sun Aug 22 21:13:20 1999 +0200
@@ -1,7 +1,7 @@
\chapter{Generic Tools and Packages}\label{ch:gen-tools}
-\section{Basic proof methods and attributes}\label{sec:pure-meth}
+\section{Basic proof methods}\label{sec:pure-meth}
\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
\indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
@@ -33,6 +33,9 @@
%FIXME thmref (single)
%FIXME var vs. term
+
+\section{Miscellaneous attributes}
+
\indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
\indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
@@ -78,6 +81,73 @@
FIXME
+
+\section{Calculational proof}\label{sec:calculation}
+
+\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
+\begin{matharray}{rcl}
+ \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
+ \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
+ trans & : & \isaratt \\
+\end{matharray}
+
+Calculational proof is forward reasoning with implicit application of
+transitivity rules (such those of $=$, $\le$, $<$). Isabelle/Isar maintains
+an auxiliary register $calculation$\indexisarreg{calculation} for accumulating
+results obtained by transitivity obtained together with the current facts.
+Command $\ALSO$ updates $calculation$ from the most recent result, while
+$\FINALLY$ exhibits the final result by forward chaining towards the next goal
+statement. Both commands require valid current facts, i.e.\ may occur only
+after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or
+some finished $\HAVENAME$ or $\SHOWNAME$.
+
+Also note that the automatic term abbreviation ``$\dots$'' has its canonical
+application with calculational proofs. It automatically refers to the
+argument\footnote{The argument of a curried infix expression is its right-hand
+ side.} of the preceding statement.
+
+Isabelle/Isar calculations are implicitly subject to block structure in the
+sense that new threads of calculational reasoning are commenced for any new
+block (as opened by a local goal, for example). This means that, apart from
+being able to nest calculations, there is no separate \emph{begin-calculation}
+command required.
+
+\begin{rail}
+ ('also' | 'finally') transrules? comment?
+ ;
+ 'trans' (() | 'add' ':' | 'del' ':') thmrefs
+ ;
+
+ transrules: '(' thmrefs ')' interest?
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
+ follows. The first occurrence of $\ALSO$ in some calculational thread
+ initialises $calculation$ by $facts$. Any subsequent $\ALSO$ on the
+ \emph{same} level of block-structure updates $calculation$ by some
+ transitivity rule applied to $calculation$ and $facts$ (in that order).
+ Transitivity rules are picked from the current context plus those given as
+ $thms$ (the latter have precedence).
+
+\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
+ $\ALSO$, and concludes the current calculational thread. The final result
+ is exhibited as fact for forward chaining towards the next goal. Basically,
+ $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. A typical proof
+ idiom is $\FINALLY~\SHOW~\VVar{thesis}~\DOT$.
+
+\item [Attribute $trans$] maintains the set of transitivity rules of the
+ theory or proof context, by adding or deleting the theorems provided as
+ arguments. The default is adding of rules.
+\end{descr}
+
+See theory \texttt{HOL/Isar_examples/Group} for a simple applications of
+calculations for basic equational reasoning.
+\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
+calculational steps in combination with natural deduction.
+
+
\section{Axiomatic Type Classes}\label{sec:axclass}
\indexisarcmd{axclass}\indexisarcmd{instance}
@@ -114,8 +184,48 @@
\section{The Simplifier}
+\subsection{Simplification methods}
+
+\indexisarmeth{simp}\indexisarmeth{asm_simp}\indexisaratt{simp}
+\begin{matharray}{rcl}
+ simp & : & \isarmeth \\
+ asm_simp & : & \isarmeth \\
+ simp & : & \isaratt \\
+\end{matharray}
+
+\begin{rail}
+ 'simp' (simpmod+)?
+ ;
+
+ simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
+ ;
+\end{rail}
+
+
+\subsection{Forward simplification}
+
+\indexisaratt{simplify}\indexisaratt{asm_simplify}\indexisaratt{full_simplify}\indexisaratt{asm_full_simplify}
+\begin{matharray}{rcl}
+ simplify & : & \isaratt \\
+ asm_simplify & : & \isaratt \\
+ full_simplify & : & \isaratt \\
+ asm_full_simplify & : & \isaratt \\
+\end{matharray}
+
+FIXME
+
+
\section{The Classical Reasoner}
+\subsection{Single step methods}
+
+\subsection{Automatic methods}
+
+\subsection{Combined automatic methods}
+
+\subsection{Modifying the context}
+
+
%\indexisarcmd{}
%\begin{matharray}{rcl}
--- a/doc-src/IsarRef/intro.tex Sun Aug 22 18:21:36 1999 +0200
+++ b/doc-src/IsarRef/intro.tex Sun Aug 22 21:13:20 1999 +0200
@@ -15,7 +15,7 @@
lemma "0 < foo" by (simp add: foo_def);
end
\end{ttbox}
-Note that \emph{any} Isabelle/Isar command may be retracted by \texttt{undo}.
+Note that any Isabelle/Isar command may be retracted by \texttt{undo}.
Plain TTY-based interaction like this used to be quite feasible with
traditional tactic based theorem proving, but developing Isar documents
@@ -30,7 +30,7 @@
\medskip
-The easiest way to use ProofGeneral is to make it the default Isabelle user
+The easiest way to use Proof~General is to make it the default Isabelle user
interface. Just say something like this in your Isabelle settings file (cf.\
\cite{isabelle-sys}):
\begin{ttbox}
@@ -39,8 +39,8 @@
\end{ttbox}
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
actual installation directory of Proof~General. Now the capital
-\texttt{Isabelle} binary refers to the \texttt{ProofGeneral/isar} interface.
-It's usage is as follows:
+\texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
+interface. It's usage is as follows:
\begin{ttbox}
Usage: interface [OPTIONS] [FILES ...]
@@ -53,12 +53,12 @@
Starts Proof General for Isabelle/Isar with proof documents FILES
(default Scratch.thy).
\end{ttbox}
-The defaults for these options may be changed via the
-\texttt{PROOFGENERAL_OPTIONS} setting. For example, GNU Emacs\footnote{GNU
- Emacs version 20.x required.} with loading of the startup file enabled may
-be configured as follows:\footnote{The interface disables \texttt{.emacs} by
- default to ensure successful startup despite any strange commands that tend
- to occur there.}
+Note that the defaults for these options may be overridden via the
+\texttt{PROOFGENERAL_OPTIONS} setting. For example, GNU
+Emacs\footnote{Version 20.x required.} with loading of the startup file
+enabled may be configured as follows:\footnote{The interface disables
+ \texttt{.emacs} by default to ensure successful startup despite any strange
+ commands that tend to occur there.}
\begin{ttbox}
PROOFGENERAL_OPTIONS="-p emacs -u true"
\end{ttbox}
@@ -68,7 +68,7 @@
\begin{ttbox}
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
\end{ttbox}
-Users of XEmacs may note the toolbar for navigating forward and backward
+Users of XEmacs may note the tool bar for navigating forward and backward
through the text. Consult the Proof~General documentation \cite{proofgeneral}
for further basic commands, such as \texttt{c-c return} or \texttt{c-c u}.
--- a/doc-src/IsarRef/pure.tex Sun Aug 22 18:21:36 1999 +0200
+++ b/doc-src/IsarRef/pure.tex Sun Aug 22 21:13:20 1999 +0200
@@ -1,12 +1,12 @@
-\chapter{Basic Isar elements}
+\chapter{Basic Isar elements}\label{ch:pure-syntax}
-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).
+Subsequently, we introduce the main part 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 pre-loaded by most object logics (such as the
+Simplifier). See chapter~\ref{ch:hol-tools} for actual object-logic specific
+elements (for Isabelle/HOL).
\medskip
@@ -114,10 +114,11 @@
just as in typical {\LaTeX} documents.
\item [$\isarkeyword{chapter}~text$, $\isarkeyword{section}~text$,
$\isarkeyword{subsection}~text$, and $\isarkeyword{subsubsection}~text$]
- specify chapter and section headings.
+ mark chapter and section headings.
\item [$\TEXT~text$] specifies an actual body of prose text, including
- references to formal entities (the latter feature is not yet exploited in
- any way).
+ references to formal entities.\footnote{The latter feature is not yet
+ exploited. Nevertheless, any text of the form \texttt{\at\{\dots\}}
+ should be considered as reserved for future use.}
\end{descr}
@@ -153,7 +154,7 @@
\end{descr}
-\subsection{Types}\label{sec:types-pure}
+\subsection{Primitive types and type abbreviations}\label{sec:types-pure}
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
\begin{matharray}{rcl}
@@ -300,9 +301,9 @@
\isarcmd{local} & : & \isartrans{theory}{theory} \\
\end{matharray}
-Isabelle organizes any kind of names (of types, constants, theorems etc.) by
+Isabelle organises 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
+the behaviour of name space entry by hand, yet the following commands provide
some way to do so.
\begin{descr}
@@ -343,7 +344,7 @@
\item [$\isarkeyword{setup}~text$] changes the current theory context by
applying setup functions $text$, which has to be an ML expression of type
$(theory \to theory)~list$. The $\isarkeyword{setup}$ command is the usual
- way to initialize object-logic specific tools and packages written in ML.
+ way to initialise object-logic specific tools and packages written in ML.
\end{descr}
@@ -386,15 +387,18 @@
\begin{descr}
\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
- function $text$, which has to be of type $Sign\mathord.sg \times object \to
- term)$.
+ function $text$, which has to be of type $Sign\mathord.sg \times
+ Object\mathord.T \to term)$.
\end{descr}
\section{Proof commands}
-Proof commands provide transitions of Isar/VM machine configurations. There
-are three different modes of operation.
+Proof commands provide transitions of Isar/VM machine configurations, which
+are block-structured, consisting of a stack of nodes with three main
+components: logical \emph{proof context}, local \emph{facts}, and open
+\emph{goals}. Isar/VM transitions are \emph{typed} according to the following
+three three different modes 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
@@ -402,8 +406,8 @@
\item [$proof(state)$] is like an internal theory mode: the context may be
augmented by \emph{stating} additional assumptions, intermediate result etc.
\item [$proof(chain)$] is an intermediate mode between $proof(state)$ and
- $proof(prove)$: some existing facts have been just picked up in order to use
- them when refining the goal to be claimed next.
+ $proof(prove)$: existing facts have been just picked up in order to use them
+ when refining the goal to be claimed next.
\end{descr}
@@ -426,40 +430,72 @@
\end{rail}
-\subsection{Proof context}
+\subsection{Proof context}\label{sec:proof-context}
-\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}\indexisarcmd{let}
+\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
\begin{matharray}{rcl}
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
\isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
\isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
\isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
- \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
\end{matharray}
-FIXME
+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 entity that may be used in the subsequent proof as any other variable
+or constant. Furthermore, any result $\phi[x]$ exported from the current
+context will be universally closed wrt.\ $x$ at the outermost level (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
+proof steps. On the other hand, any result $\phi$ exported from the context
+becomes conditional wrt.\ the assumption. Thus, solving an enclosing goal
+using this result would basically introduce a new subgoal stemming from the
+assumption. How this situation is handled depends on the actual version of
+assumption command used: while $\ASSUMENAME$ solves the subgoal by unifying
+with some premise of the goal, $\PRESUMENAME$ leaves the subgoal unchanged to
+be proved later by the user.
+
+Local definitions, introduced by $\DEF{a}{x \equiv t}$, are achieved by
+combining $\FIX x$ with another version of assumption that causes any
+hypothetical equation $x = t$ to be eliminated by reflexivity. Thus,
+exporting some result $\phi[x]$ simply yields $\phi[t]$.
\begin{rail}
'fix' (var +) comment?
;
- ('assume' | 'presume') thmdecl? \\ (prop proppat? +) comment?
+ ('assume' | 'presume') (assm comment? + 'and')
;
'def' thmdecl? \\ var '==' term termpat? comment?
;
- 'let' ((term + 'as') '=' term comment? + 'and')
- ;
var: name ('::' type)?
;
+ assm: thmdecl? (prop proppat? +)
+ ;
\end{rail}
\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
+\item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$.
+\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems
+ $\Phi$. Subsequent results used to solve some enclosing goal (e.g.\ via
+ $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be able to
+ unify with existing premises in the goal, while $\PRESUMENAME$ leaves $\Phi$
+ as new subgoals. Note that several lists of assumptions may be given
+ (separated by \railterm{and}); the resulting list of current facts consists
+ of all of these.
+\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}~\PRESUME{}{x \equiv t}$ (the
+ resulting hypothetical equation is solved by reflexivity, though).
\end{descr}
+The internal register $prems$\indexisarreg{prems} refers to all current
+assumptions as a list of theorems.
+
\subsection{Facts and forward chaining}
@@ -471,7 +507,10 @@
\isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
\end{matharray}
-FIXME
+New facts are established either by assumption or proof of local statements
+(via $\HAVENAME$ or $\SHOWNAME$). Any facts will usually be involved in
+proofs of further results: either as explicit arguments of proof methods or
+when forward chaining towards the next goal via $\THEN$ (and variants).
\begin{rail}
'note' thmdef? thmrefs comment?
@@ -497,6 +536,9 @@
chaining is from earlier facts together with the current ones.
\end{descr}
+Note that the internal register of \emph{current facts} may be referred as
+theorem list $facts$.\indexisarreg{facts}
+
\subsection{Goal statements}
@@ -629,6 +671,92 @@
\end{descr}
+\subsection{Improper proof steps}
+
+The following commands emulate unstructured 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} \\
+ \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
+\end{matharray}
+
+\railalias{thenapply}{then\_apply}
+\railterm{thenapply}
+
+\begin{rail}
+ 'apply' method
+ ;
+ thenapply method
+ ;
+ 'back'
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{apply}~m$] applies proof method $m$ in the
+ plain-old-tactic sense. Facts for forward chaining are ignored.
+\item [$\isarkeyword{then_apply}~m$] is similar to $\isarkeyword{apply}$, but
+ observes the goal's facts.
+\item [$\isarkeyword{back}$] does back-tracking over the result sequence of
+ the last proof command. Basically, any proof command may return multiple
+ results.
+\end{descr}
+
+
+\subsection{Term abbreviations}\label{sec:term-abbrev}
+
+\indexisarcmd{let}
+\begin{matharray}{rcl}
+ \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
+ \isarkeyword{is} & : & syntax \\
+\end{matharray}
+
+Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
+or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$
+etc.) with a list of patterns $\IS{p@1 \dots p@n}$. In both cases,
+higher-order matching is applied to bind extra-logical text
+variables\index{text variables}, which may be either of the form $\VVar{x}$
+(token class \railtoken{textvar}, see \S\ref{sec:lex-syntax}) or nameless
+dummies ``\verb,_,'' (underscore).\index{dummy variables} Note that in the
+$\LETNAME$ form the patterns occur on the left-hand side, while the $\ISNAME$
+patterns are in postfix position.
+
+Note that 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.
+
+\begin{rail}
+ 'let' ((term + 'as') '=' term comment? + 'and')
+ ;
+\end{rail}
+
+The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
+\railnonterm{proppat} (see \S\ref{sec:term-pats}).
+
+\begin{descr}
+\item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
+ by simultaneous higher-order matching against terms $\vec t$.
+\item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the
+ preceding statement. Also note that $\ISNAME$ is not a separate command,
+ but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
+\end{descr}
+
+Furthermore, a few automatic term abbreviations\index{automatic abbreviation}
+for goals and facts are available. For any open goal, $\VVar{thesis}$ refers
+to its object-logic statement, $\VVar{thesis_prop}$ to the full proposition
+(which may be a rule), and $\VVar{thesis_concl}$ to its (atomic) conclusion.
+
+Facts (i.e.\ assumptions and finished goals) that have an application $f(x)$
+as object-logic statement get $x$ bound to the special text variable
+``$\dots$'' (three dots). The canonical application of this feature are
+calculational proofs, see \S\ref{sec:calculation}.
+
+
\subsection{Block structure}
While Isar is inherently block-structured, opening and closing blocks is
@@ -657,67 +785,18 @@
\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
+ the enclosing context. Thus fixed variables are generalised, assumptions
discharged, and local definitions eliminated.
\end{descr}
-\subsection{Calculational proof}
-
-\indexisarcmd{also}\indexisarcmd{finally}
-\begin{matharray}{rcl}
- \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
- \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
-\end{matharray}
-
-FIXME
-
-\begin{rail}
- ('also' | 'finally') transrules? comment?
- ;
-
- transrules: '(' thmrefs ')' interest?
- ;
-\end{rail}
-
-\begin{descr}
-\item [$\ALSO~(thms)$] FIXME
-\item [$\FINALLY~(thms)$] FIXME
-\end{descr}
-
-
-
-\subsection{Improper proof steps}
-
-The following commands emulate unstructured 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} \\
- \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
-\end{matharray}
-
-\railalias{thenapply}{then\_apply}
-\railterm{thenapply}
-
-\begin{rail}
- 'apply' method
- ;
- thenapply method
- ;
- 'back'
- ;
-\end{rail}
-
-\begin{descr}
-\item [$ $] FIXME
-\end{descr}
-
\section{Other commands}
+The following commands are not part of the actual proper or improper
+Isabelle/Isar syntax, but assist interactive development, for example. Also
+note that $undo$ does not apply here, since the theory or proof configuration
+is not changed.
+
\subsection{Diagnostics}
\indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm}
--- a/doc-src/IsarRef/syntax.tex Sun Aug 22 18:21:36 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex Sun Aug 22 21:13:20 1999 +0200
@@ -1,15 +1,69 @@
-
-%FIXME
-% - examples (!?)
-
\chapter{Isar document syntax}
-FIXME shortcut
+We give a complete reference of all basic syntactic entities underlying the
+the Isabelle/Isar document syntax. This chapter will not introduce any actual
+theory and proof commands, though (cf.\ chapter~\ref{ch:pure-syntax} and
+later).
+
+\medskip
+
+In order to get started with writing well-formed Isabelle/Isar documents, the
+most important aspect to be noted is the difference of \emph{inner} versus
+\emph{outer} syntax. Inner syntax is that of Isabelle types and terms of the
+logic, while outer syntax is that of Isabelle/Isar theories (and proofs). As
+a general rule, inner syntax entities may occur only as \emph{atomic entities}
+within outer syntax. For example, quoted string \texttt{"x + y"} and
+identifier \texttt{z} are legal term specifications, while \texttt{x + y} is
+not.
+
+\begin{warn}
+ Note that old-style Isabelle theories used to fake parts of the inner type
+ syntax, with complicated rules when quotes may be omitted. Despite the
+ minor drawback of requiring quotes more often, Isabelle/Isar is simpler and
+ more robust in that respect.
+\end{warn}
+
+
+\section{Lexical matters}\label{sec:lex-syntax}
+
+The Isabelle/Isar outer syntax provides token classes as presented below.
+Note that some of these coincide (by full intention) with inner lexical syntax
+as given in \cite{isabelle-ref}. These different levels of syntax should not
+be confused, though.
-FIXME important note: inner versus outer syntax
+\begin{matharray}{rcl}
+ ident & = & letter~quasiletter^* \\
+ longident & = & ident\verb,.,ident~\dots~ident \\
+ symident & = & sym^+ \\
+ nat & = & digit^+ \\
+ var & = & \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
+ textvar & = & \verb,??,ident \\
+ typefree & = & \verb,',ident \\
+ typevar & = & \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
+ string & = & \verb,", ~\dots~ \verb,", \\
+ verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[2ex]
-\section{Lexical matters}
+ letter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
+ digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
+ quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
+ sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ %$
+ \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \verb,<, ~|~
+ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \mathtt{\at} ~|~ \verb,^, ~|~ \verb,_, ~|~
+ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
+\end{matharray}
+
+The syntax of \texttt{string} admits any characters, including newlines;
+\verb|"| and \verb|\| have to be escaped by a backslash, though. Note that
+ML-style control character notation is not supported. The body of
+\texttt{verbatim} may consist of any text not containing \verb|*}|.
+
+Comments take the form \texttt{(*~\dots~*)} and may be nested, just as in ML.
+Note that these are \emph{source} comments only, which are stripped after
+lexical analysis of the input. The Isar document syntax also provides several
+elements of \emph{formal comments} that are actually part of the text (see
+\S\ref{sec:comments}, \S\ref{sec:formal-cmt-thy}, \S\ref{sec:formal-cmt-prf}).
+
\section{Common syntax entities}
@@ -46,7 +100,7 @@
\end{rail}
-\subsection{Comments}
+\subsection{Comments}\label{sec:comments}
Large chunks of plain \railqtoken{text} are usually given
\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|\dots\verb|*}|. For
@@ -58,8 +112,8 @@
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.
+more obscure; \texttt{\%\%} means that interest drops by $\infty$ ---
+\emph{abandon every hope, who enter here}.
\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
\begin{rail}
@@ -94,7 +148,7 @@
\subsection{Types and terms}\label{sec:types-terms}
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.
+too flexible in order to be modelled 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 (the parsing and type-checking is performed later). For
convenience, a slightly more liberal convention is adopted: quotes may be
@@ -123,7 +177,7 @@
\end{rail}
-\subsection{Term patterns}
+\subsection{Term patterns}\label{sec:term-pats}
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}$.
@@ -161,8 +215,8 @@
\subsection{Attributes and theorems}\label{sec:syn-att}
Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own
-``semi-inner'' syntax, which does not have to be atomic at the outer level
-unlike that of types and terms. Instead, the attribute argument
+``semi-inner'' syntax, in the sense that input conforming \railnonterm{args}
+below are parsed by the attribute a second time. 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, including \railtoken{keyword}s conforming to
@@ -180,7 +234,7 @@
;
\end{rail}
-Theorem specifications come in several flavors: \railnonterm{axmdecl} and
+Theorem specifications come in several flavours: \railnonterm{axmdecl} and
\railnonterm{thmdecl} usually refer to axioms, assumptions or results of goal
statements, \railnonterm{thmdef} collects lists of existing theorems.
Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs}