# HG changeset patch # User wenzelm # Date 935401401 -7200 # Node ID 3907d597cae617f6c8a68897e2ad7c13c125810a # Parent 768fab6dae742c7edf21d8745ed6676e8f011997 tuned; diff -r 768fab6dae74 -r 3907d597cae6 doc-src/IsarRef/generic.tex --- 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} diff -r 768fab6dae74 -r 3907d597cae6 doc-src/IsarRef/hol.tex --- 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: diff -r 768fab6dae74 -r 3907d597cae6 doc-src/IsarRef/pure.tex --- 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 diff -r 768fab6dae74 -r 3907d597cae6 doc-src/IsarRef/syntax.tex --- 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;