--- a/doc-src/IsarRef/generic.tex Mon Aug 23 09:36:05 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Mon Aug 23 11:43:21 1999 +0200
@@ -154,6 +154,7 @@
\begin{matharray}{rcl}
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
+ expand_classes & : & \isarmeth \\
\end{matharray}
Axiomatic type classes are provided by Isabelle/Pure as a purely
@@ -178,8 +179,12 @@
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 $expand_classes$] iteratively expands the class introduction
+ rules
\end{descr}
+See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
+axiomatic type classes, including instantiation proofs.
\section{The Simplifier}
@@ -194,13 +199,15 @@
\end{matharray}
\begin{rail}
- 'simp' (simpmod+)?
+ 'simp' (simpmod * )
;
simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
;
\end{rail}
+FIXME
+
\subsection{Forward simplification}
--- a/doc-src/IsarRef/hol.tex Mon Aug 23 09:36:05 1999 +0200
+++ b/doc-src/IsarRef/hol.tex Mon Aug 23 11:43:21 1999 +0200
@@ -51,10 +51,11 @@
\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 extensible records.
\end{descr}
+See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
+simply-typed extensible records.
+
\section{Datatypes}\label{sec:datatype}
@@ -78,10 +79,15 @@
\end{rail}
\begin{descr}
-\item [$\isarkeyword{datatype}$] FIXME
-\item [$\isarkeyword{rep_datatype}$] FIXME
+\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
+\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
+ ones, generating the standard infrastructure of derived concepts (primitive
+ recursion etc.).
\end{descr}
+See \cite{isabelle-HOL} for more details on datatypes. Note that the theory
+syntax above has been slightly simplified over the old version.
+
\section{Recursive functions}
@@ -101,10 +107,14 @@
\end{rail}
\begin{descr}
-\item [$\isarkeyword{primrec}$] FIXME
-\item [$\isarkeyword{recdef}$] FIXME
+\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
+ datatypes.
+\item [$\isarkeyword{recdef}$] defines general well-founded recursive
+ functions (using the TFL package).
\end{descr}
+See \cite{isabelle-HOL} for more information.
+
\section{(Co)Inductive sets}
@@ -129,14 +139,47 @@
\end{rail}
\begin{descr}
-\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] FIXME
-\item [$\isarkeyword{inductive_cases}$] FIXME
+\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
+ (co)inductive sets from the given introduction rules.
+\item [$\isarkeyword{inductive_cases}$] creates simplified instances of
+ elimination rules of (co)inductive sets.
\end{descr}
+See \cite{isabelle-HOL} for more information. Note that
+$\isarkeyword{inductive_cases}$ corresponds to the ML function
+\texttt{mk_cases}.
+
\section{Proof by induction}
-FIXME induct proof method
+\indexisarmeth{induct}
+\begin{matharray}{rcl}
+ induct & : & \isarmeth \\
+\end{matharray}
+
+The $induct$ method provides a uniform interface to induction over datatypes,
+inductive sets, and recursive functions. Basically, it is just an interface
+to the $rule$ method applied to appropriate instances of the corresponding
+induction rules.
+
+\begin{rail}
+ 'induct' (inst * 'and') kind?
+ ;
+
+ inst: term term?
+ ;
+ kind: ('type' | 'set' | 'function') ':' nameref
+ ;
+\end{rail}
+
+\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 (at least one has to be given in that case).
+\end{descr}
%%% Local Variables:
--- a/doc-src/IsarRef/pure.tex Mon Aug 23 09:36:05 1999 +0200
+++ b/doc-src/IsarRef/pure.tex Mon Aug 23 11:43:21 1999 +0200
@@ -117,8 +117,9 @@
mark chapter and section headings.
\item [$\TEXT~text$] specifies an actual body of prose text, including
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.}
+ exploited. Nevertheless, any text of the form
+ \texttt{\at\ttlbrace\dots\ttrbrace} should be considered as reserved for
+ future use.}
\end{descr}
@@ -444,7 +445,7 @@
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
+a local object 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).
@@ -459,8 +460,8 @@
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
+Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
+combining $\FIX x$ with another kind of assumption that causes any
hypothetical equation $x = t$ to be eliminated by reflexivity. Thus,
exporting some result $\phi[x]$ simply yields $\phi[t]$.
@@ -481,20 +482,20 @@
\begin{descr}
\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
+ $\Phi$. Subsequent results applied to 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.
+ (separated by $\isarkeyword{and}$); the resulting list of facts consists of
+ all of these concatenated.
\item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
In results exported from the context, $x$ is replaced by $t$. Basically,
$\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\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.
+The internal register $prems$\indexisarreg{prems} refers to the current list
+of assumptions.
\subsection{Facts and forward chaining}
@@ -507,10 +508,12 @@
\isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
\end{matharray}
-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).
+New facts are established either by assumption or proof of local statements.
+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). Note that the internal register of
+\emph{current facts} may be referred as theorem list
+$facts$.\indexisarreg{facts}
\begin{rail}
'note' thmdef? thmrefs comment?
@@ -536,9 +539,6 @@
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}
@@ -666,7 +666,7 @@
\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 (this is indicated
- as $[!]$ in the printed result. The main application of
+ as $[!]$ in the printed result). The main application of
$\isarkeyword{sorry}$ is to support top-down proof development.
\end{descr}
@@ -725,8 +725,8 @@
$\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
+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.
@@ -746,10 +746,11 @@
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.
+A few \emph{automatic} term abbreviations\index{automatic abbreviation} for
+goals and facts are available as well. For any open goal, $\VVar{thesis}$
+refers to its object-logical 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
--- a/doc-src/IsarRef/syntax.tex Mon Aug 23 09:36:05 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex Mon Aug 23 11:43:21 1999 +0200
@@ -13,9 +13,8 @@
\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.
+within outer syntax. Thus, 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
@@ -42,15 +41,16 @@
typefree & = & \verb,',ident \\
typevar & = & \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
string & = & \verb,", ~\dots~ \verb,", \\
- verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[2ex]
-
+ verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\
+\end{matharray}
+\begin{matharray}{rcl}
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,~, \\
+ \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;