--- a/doc-src/IsarRef/basics.tex Sat Sep 04 20:55:52 1999 +0200
+++ b/doc-src/IsarRef/basics.tex Sat Sep 04 20:57:32 1999 +0200
@@ -3,8 +3,9 @@
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 and unlimited undo operation.
+\item A new \emph{theory format}, occasionally referred to as ``new-style
+ theories'', supporting interactive development with 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
@@ -13,32 +14,35 @@
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 level, 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}$ which only works for non-empty representing
-sets.
+$\LEMMANAME$ at the theory level, and left with the conclusion of the proof
+(via $\QEDNAME$ etc.). Some theory extension mechanisms require proof as
+well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
+the representing sets.
New-style theory files may still be associated with an ML file consisting of
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
-\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.
+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 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 are handled as two different theorem proving
- systems, only one may be active at the same time.
+ Currently 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 are handled as two different
+ theorem proving systems, only one may be active at the same time.
\end{warn}
+Porting of existing tactic scripts is best done by running two separate
+Proof~General sessions, one for replaying the old script and the other for the
+emerging Isabelle/Isar document.
+
\section{The Isar proof language}
-Sorry, this rather important section has not been written yet! Refer to
+Sorry, this important section has not been written yet! Refer to
\cite{Wenzel:1999:TPHOL} for the time being.
\subsection{Commands}
--- a/doc-src/IsarRef/generic.tex Sat Sep 04 20:55:52 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Sat Sep 04 20:57:32 1999 +0200
@@ -28,8 +28,8 @@
performs a single reduction step using the $rule$ method (see below); thus a
plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
$\PROOFNAME$ alone.
-\item [$assumption$] solves some goal by assumption. The facts (if any) are
- guaranteed to participate.
+\item [$assumption$] solves some goal by assumption. Any facts given are
+ guaranteed to participate in the refinement.
\item [$rule~thms$] 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
@@ -104,7 +104,7 @@
intended (see also \texttt{RS} and \texttt{COMP} in
\cite[\S5]{isabelle-ref}).
-\item [$of~ts$ and $where~\vec x = \vec t$] perform positional and named
+\item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
instantiation, respectively. The terms given in $of$ are substituted for
any schematic variables occurring in a theorem from left to right;
``\texttt{_}'' (underscore) indicates to skip a position.
@@ -179,7 +179,7 @@
$\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$''.
+ idiom is ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$''.
\item [$trans$] maintains the set of transitivity rules of the theory or proof
context, by adding or deleting theorems (the default is to add).
@@ -230,8 +230,8 @@
establish the 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.
-\item [Method $intro_classes$] iteratively expands the class introduction
- rules
+\item [$intro_classes$] iteratively expands the class introduction rules of
+ this theory.
\end{descr}
See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
@@ -260,17 +260,20 @@
\end{rail}
\begin{descr}
-\item [Methods $simp$ and $asm_simp$] invoke Isabelle's simplifier, after
- modifying the context by adding or deleting given rules. The
- \railtoken{only} modifier first removes all other rewrite rules and
- congruences, and then is like \railtoken{add}. In contrast,
- \railtoken{other} ignores its arguments; nevertheless there may be
- side-effects on the context via attributes. This provides a back door for
- arbitrary context manipulation.
+\item [$simp$ and $asm_simp$] invoke Isabelle's simplifier, after modifying
+ the context by adding or deleting given rules. The \railtoken{only}
+ modifier first removes all other rewrite rules and congruences, and then is
+ like \railtoken{add}. In contrast, \railtoken{other} ignores its arguments;
+ nevertheless there may be side-effects on the context via attributes. This
+ provides a back door for arbitrary context manipulation.
Both of these methods are based on \texttt{asm_full_simp_tac}, see
- \cite[\S10]{isabelle-ref}; $simp$ removes any exisiting premises of the
- goal, before inserting the goal facts; $asm_simp$ leaves the premises.
+ \cite[\S10]{isabelle-ref}; $simp$ removes any premises of the goal, before
+ inserting the goal facts; $asm_simp$ leaves the premises. Thus $asm_simp$
+ may refer to premises that are not explicitly spelled out, potentially
+ obscuring the reasoning. The plain $simp$ method is more faithful in the
+ sense that, apart from the rewrite rules of the current context, \emph{at
+ most} the explicitly provided facts may participate in the simplification.
\end{descr}
\subsection{Modifying the context}
@@ -286,8 +289,8 @@
\end{rail}
\begin{descr}
-\item [Attribute $simp$] adds or deletes rules from the theory or proof
- context (the default is to add).
+\item [$simp$] adds or deletes rules from the theory or proof context (the
+ default is to add).
\end{descr}
@@ -325,14 +328,14 @@
\end{rail}
\begin{descr}
-\item [Method $rule$] as offered by the classical reasoner is a refinement
- over the primitive one (see \S\ref{sec:pure-meth}). In the case that no
- rules are provided as arguments, it automatically determines elimination and
+\item [$rule$] as offered by the classical reasoner is a refinement over the
+ primitive one (see \S\ref{sec:pure-meth}). In the case that no rules are
+ provided as arguments, it automatically determines elimination and
introduction rules from the context (see also \S\ref{sec:classical-mod}).
In that form it is the default method for basic proof steps, such as
$\PROOFNAME$ and ``$\DDOT$'' (two dots).
-\item [Methods $intro$ and $elim$] repeatedly refine some goal by intro- or
+\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
elim-resolution, after having inserted the facts. Omitting the arguments
refers to any suitable rules from the context, otherwise only the explicitly
given ones may be applied. The latter form admits better control of what
@@ -340,9 +343,9 @@
$\PROOFNAME$ that splits up certain connectives of the goal, before entering
the sub-proof.
-\item [Method $contradiction$] solves some goal by contradiction, deriving any
- result from both $\neg A$ and $A$. Facts, which are guaranteed to
- participate, may appear in either order.
+\item [$contradiction$] solves some goal by contradiction, deriving any result
+ from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may
+ appear in either order.
\end{descr}
@@ -430,7 +433,7 @@
\item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
respectively. By default, rules are considered as \emph{safe}, while a
single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\
- not applied in the search-oriented automatic methods).
+ not applied in the search-oriented automatic methods, but only $rule$).
\item [$iff$] declares equations both as rewrite rules for the simplifier and
classical reasoning rules.
--- a/doc-src/IsarRef/hol.tex Sat Sep 04 20:55:52 1999 +0200
+++ b/doc-src/IsarRef/hol.tex Sat Sep 04 20:57:32 1999 +0200
@@ -174,11 +174,11 @@
\begin{descr}
\item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the
- induction rule of the type/set/function specified by $kind$ and instantiated
- by $insts$. The latter either consists of pairs $P$ $x$ (induction
- predicate and variable), where $P$ is optional. If $kind$ is omitted, the
- default is to pick a datatype induction rule according to the type of some
- induction variable, which may not be omitted that case.
+ induction rule of the type~/ set~/ function specified by $kind$ and
+ instantiated by $insts$. The latter either consists of pairs $P$ $x$
+ (induction predicate and variable), where $P$ is optional. If $kind$ is
+ omitted, the default is to pick a datatype induction rule according to the
+ type of some induction variable, which may not be omitted that case.
\end{descr}
--- a/doc-src/IsarRef/intro.tex Sat Sep 04 20:55:52 1999 +0200
+++ b/doc-src/IsarRef/intro.tex Sat Sep 04 20:57:32 1999 +0200
@@ -69,18 +69,16 @@
\end{ttbox}
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}.
+for further basic commands, like \texttt{c-c return} or \texttt{c-c u}.
\medskip
Occasionally, a user's \texttt{.emacs} contains material that is incompatible
with the version of (X)Emacs that Proof~General prefers. Then proper startup
-may be still achieved by using the \texttt{-u false} option.\footnote{Also
- note that the Emacs lisp files
- \texttt{\$ISABELLE_HOME/etc/proofgeneral-settings.el} and
- \texttt{\$ISABELLE_HOME_USER/etc/proofgeneral-settings.el} are automatically
- loaded by Proof~General if invoked via the interface wrapper script.}
-
+may be still achieved by using the \texttt{-u false} option.\footnote{Any
+ \texttt{proofgeneral-settings.el} file occurring in
+ \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc} is
+ automatically loaded by the Proof~General interface script as well.}
\section{How to write Isar proofs anyway?}
--- a/doc-src/IsarRef/isar-ref.tex Sat Sep 04 20:55:52 1999 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Sat Sep 04 20:57:32 1999 +0200
@@ -67,7 +67,8 @@
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.
+ object-logics. The current working environment for end-users is setup
+ mainly for Isabelle/HOL.
\end{abstract}
\pagenumbering{roman} \tableofcontents \clearfirst
@@ -80,7 +81,6 @@
\nocite{Syme:1997:DECLARE}
\nocite{Syme:1998:thesis}
\nocite{Syme:1999:TPHOL}
-\nocite{Wenzel:1999:TPHOL}
\include{intro}
\include{basics}
--- a/doc-src/IsarRef/pure.tex Sat Sep 04 20:55:52 1999 +0200
+++ b/doc-src/IsarRef/pure.tex Sat Sep 04 20:57:32 1999 +0200
@@ -11,13 +11,13 @@
\medskip
Isar commands may be either \emph{proper} document constructors, or
-\emph{improper commands} (indicated by $^*$). Some proof methods and
-attributes introduced later are classified as improper as well. Improper Isar
-language elements might be helpful when developing proof documents, while
-their use is strongly discouraged for the final version. 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.
+\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 usually 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}
@@ -337,13 +337,13 @@
\begin{descr}
\item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
- The current theory context (if present) is passed down to the ML session.
- Furthermore, the file name is checked with the $\isarkeyword{files}$
- dependency declaration given in the theory header (see also
- \S\ref{sec:begin-thy}).
-
+ The current theory context (if present) is passed down to the ML session,
+ but must not be modified. Furthermore, the file name is checked with the
+ $\isarkeyword{files}$ dependency declaration 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 for $\isarkeyword{use}$.
+ The theory context is passed in the same way as for $\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
@@ -584,8 +584,8 @@
\begin{descr}
\item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
- eventually resulting in some theorem $\turn \phi$, which will be stored in
- the theory.
+ eventually resulting in some theorem $\turn \phi$, and put back into the
+ theory.
\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
``lemma''.
\item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
@@ -735,12 +735,11 @@
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 ``\texttt{_}'' (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.
+higher-order matching is applied to bind extra-logical text 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 postfix position.
Term abbreviations are quite different from actual local definitions as
introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are
@@ -765,15 +764,20 @@
A few \emph{automatic} term abbreviations\index{automatic abbreviation} for
goals and facts are available as well. For any open goal,
-$\VVar{thesis_prop}$ refers to the full proposition (which may be a rule),
-$\VVar{thesis_concl}$ to its (atomic) conclusion, and $\VVar{thesis}$ to its
+$\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
+(which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
+(atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
object-logical statement. The latter two abstract over any meta-level
-parameters.
+parameters bound by $\Forall$.
-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}).
+Fact statements resulting from assumptions or finished goals are bound as
+$\Var{this_prop}$\indexisarvar{this-prop},
+$\Var{this_concl}$\indexisarvar{this-concl}, and
+$\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case
+$\Var{this}$ refers to an object-logic statement that is an application
+$f(x)$, then $x$ is bound to the special text variable
+``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of
+this feature are calculational proofs (see \S\ref{sec:calculation}).
\subsection{Block structure}
--- a/doc-src/IsarRef/syntax.tex Sat Sep 04 20:55:52 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex Sat Sep 04 20:57:32 1999 +0200
@@ -22,6 +22,14 @@
robust in that respect.
\end{warn}
+\medskip
+
+Another notable point is proper input termination. Proof~General demands any
+command to be terminated by ``\texttt{;}''
+(semicolon)\index{semicolon}\index{*;}. As far as plain Isabelle/Isar is
+concerned, commands may be directly run together. Thus for better
+readability, we usually omit semicolons when discussion Isar proof text here.
+
\section{Lexical matters}\label{sec:lex-syntax}
@@ -37,7 +45,6 @@
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,", \\
@@ -105,15 +112,15 @@
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 units 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 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
-obscure; \texttt{\%\%} means that interest drops by $\infty$ --- abandon every
-hope, who enter here.
+are admitted as well. Almost any of the Isar commands may be annotated by a
+marginal \railnonterm{comment} of the form \texttt{--} \railqtoken{text}.
+Note that the latter kind of comment is actually part of the language, while
+source level comments \verb|(*|\dots\verb|*)| are 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 obscure; \texttt{\%\%} means that interest drops by $\infty$ --- abandon
+every hope, who enter here.
\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
\begin{rail}
@@ -153,13 +160,15 @@
token (the parsing and type-checking is performed 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. E.g.\ one may
-write just \texttt{x} instead of \texttt{"x"}.
+write just \texttt{x} instead of \texttt{"x"}. Note that symbolic identifiers
+such as \texttt{++} are available as well, provided these are not superceded
+by commands or keywords (like \texttt{+}).
\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
\begin{rail}
type: nameref | typefree | typevar
;
- term: nameref | var | textvar | nat
+ term: nameref | var | nat
;
prop: term
;
@@ -224,7 +233,7 @@
\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
\begin{rail}
- atom: nameref | typefree | typevar | var | textvar | nat | keyword
+ atom: nameref | typefree | typevar | var | nat | keyword
;
arg: atom | '(' args ')' | '[' args ']' | lbrace args rbrace
;
@@ -240,7 +249,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.
+sides; attributes are applied to any immediately preceding theorem. If names
+are omitted, the theorems are not stored within the theory's theorem database;
+any given attributes are still applied, though.
\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
@@ -265,8 +276,8 @@
Proof methods are either basic ones, or expressions composed of methods via
``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
-``\texttt{?}'' (try), ``\texttt{+}'' (at least once). In practice, proof
-methods are usually just a comma separated list of
+``\texttt{?}'' (try once), ``\texttt{+}'' (repeat at least once). 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. Note that parentheses may be dropped for single method