doc-src/IsarRef/logics.tex
changeset 13014 3c1c493e6d93
parent 12879 8e1cae1de136
child 13016 c039b8ede204
     1.1 --- a/doc-src/IsarRef/logics.tex	Mon Mar 04 19:07:22 2002 +0100
     1.2 +++ b/doc-src/IsarRef/logics.tex	Mon Mar 04 19:07:58 2002 +0100
     1.3 @@ -40,12 +40,14 @@
     1.4  \begin{rail}
     1.5    'judgment' constdecl
     1.6    ;
     1.7 -  ruleformat ('(' noasm ')')?
     1.8 +  atomize ('(' 'full' ')')?
     1.9 +  ;
    1.10 +  ruleformat ('(' 'noasm' ')')?
    1.11    ;
    1.12  \end{rail}
    1.13  
    1.14  \begin{descr}
    1.15 -  
    1.16 +
    1.17  \item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
    1.18    truth judgment of the current object-logic.  Its type $\sigma$ should
    1.19    specify a coercion of the category of object-level propositions to $prop$ of
    1.20 @@ -53,25 +55,27 @@
    1.21    the object language (internally of syntactic category $logic$) with that of
    1.22    $prop$.  Only one $\isarkeyword{judgment}$ declaration may be given in any
    1.23    theory development.
    1.24 -  
    1.25 +
    1.26  \item [$atomize$] (as a method) rewrites any non-atomic premises of a
    1.27    sub-goal, using the meta-level equations declared via $atomize$ (as an
    1.28    attribute) beforehand.  As a result, heavily nested goals become amenable to
    1.29    fundamental operations such as resolution (cf.\ the $rule$ method) and
    1.30 -  proof-by-assumption (cf.\ $assumption$).
    1.31 -  
    1.32 +  proof-by-assumption (cf.\ $assumption$).  Giving the ``$(full)$'' option
    1.33 +  here means to turn the subgoal into an object-statement (if possible),
    1.34 +  including the outermost parameters and assumptions as well.
    1.35 +
    1.36    A typical collection of $atomize$ rules for a particular object-logic would
    1.37    provide an internalization for each of the connectives of $\Forall$, $\Imp$,
    1.38    and $\equiv$.  Meta-level conjunction expressed in the manner of minimal
    1.39    higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$
    1.40    should be covered as well (this is particularly important for locales, see
    1.41    \S\ref{sec:locale}).
    1.42 -  
    1.43 +
    1.44  \item [$rule_format$] rewrites a theorem by the equalities declared as
    1.45    $rulify$ rules in the current object-logic.  By default, the result is fully
    1.46    normalized, including assumptions and conclusions at any depth.  The
    1.47    $no_asm$ option restricts the transformation to the conclusion of a rule.
    1.48 -  
    1.49 +
    1.50    In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to
    1.51    replace (bounded) universal quantification ($\forall$) and implication
    1.52    ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
    1.53 @@ -97,21 +101,36 @@
    1.54  \end{rail}
    1.55  
    1.56  \begin{descr}
    1.57 +  
    1.58  \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
    1.59    $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
    1.60    also declares type arity $t :: (term, \dots, term) term$, making $t$ an
    1.61    actual HOL type constructor.
    1.62 +  
    1.63  \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
    1.64    non-emptiness of the set $A$.  After finishing the proof, the theory will be
    1.65 -  augmented by a Gordon/HOL-style type definition.  See \cite{isabelle-HOL}
    1.66 -  for more information.  Note that user-level theories usually do not directly
    1.67 -  refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
    1.68 -  packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and
    1.69 -  $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
    1.70 +  augmented by a Gordon/HOL-style type definition, which establishes a
    1.71 +  bijection between the representing set $A$ and the new type $t$.
    1.72 +  
    1.73 +  Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term
    1.74 +  constant) of the same name.  The injection from type to set is called
    1.75 +  $Rep_t$, its inverse $Abs_t$.  Theorems $Rep_t$, $Rep_inverse$, and
    1.76 +  $Abs_inverse$ provide the most basic characterization as a corresponding
    1.77 +  injection/surjection pair (in both directions).  Rules $Rep_t_inject$ and
    1.78 +  $Abs_t_inject$ provide a slightly more comfortable view on the injectivity
    1.79 +  part; likewise do $Rep_t_cases$, $Rep_t_induct$, and $Abs_t_cases$,
    1.80 +  $Abs_t_induct$ for surjectivity.  The latter rules are already declare as
    1.81 +  type or set rules for the generic $cases$ and $induct$ methods.
    1.82  \end{descr}
    1.83  
    1.84 +Raw type declarations are rarely useful in practice.  The main application is
    1.85 +with experimental (or even axiomatic!) theory fragments.  Instead of primitive
    1.86 +HOL type definitions, user-level theories usually refer to higher-level
    1.87 +packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or
    1.88 +$\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
    1.89  
    1.90 -\subsection{Low-level tuples}
    1.91 +
    1.92 +\subsection{Adhoc tuples}
    1.93  
    1.94  \indexisarattof{HOL}{split-format}
    1.95  \begin{matharray}{rcl}
    1.96 @@ -128,25 +147,89 @@
    1.97  \end{rail}
    1.98  
    1.99  \begin{descr}
   1.100 -  
   1.101 +
   1.102  \item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
   1.103    tuple types into canonical form as specified by the arguments given; $\vec
   1.104    p@i$ refers to occurrences in premise $i$ of the rule.  The
   1.105    $split_format~(complete)$ form causes \emph{all} arguments in function
   1.106    applications to be represented canonically according to their tuple type
   1.107    structure.
   1.108 -  
   1.109 +
   1.110    Note that these operations tend to invent funny names for new local
   1.111    parameters to be introduced.
   1.112  
   1.113  \end{descr}
   1.114  
   1.115  
   1.116 -\subsection{Records}\label{sec:hol-record}
   1.117 +\section{Records}\label{sec:hol-record}
   1.118 +
   1.119 +In principle, records merely generalize the concept of tuples where components
   1.120 +may be addressed by labels instead of just position.  The logical
   1.121 +infrastructure of records in Isabelle/HOL is slightly more advanced, though,
   1.122 +supporting truly extensible record schemes.  This admits operations that are
   1.123 +polymorphic with respect to record extension, yielding ``object-oriented''
   1.124 +effects like (single) inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for
   1.125 +more details on object-oriented verification and record subtyping in HOL.
   1.126 +
   1.127 +
   1.128 +\subsection{Basic concepts}
   1.129 +
   1.130 +Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the
   1.131 +level of terms and types.  The notation is as follows:
   1.132 +
   1.133 +\begin{center}
   1.134 +\begin{tabular}{l|l|l}
   1.135 +  & record terms & record types \\ \hline
   1.136 +  fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
   1.137 +  schematic & $\record{x = a\fs y = b\fs \more = m}$ &
   1.138 +    $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
   1.139 +\end{tabular}
   1.140 +\end{center}
   1.141 +
   1.142 +\noindent The ASCII representation of $\record{x = a}$ is \texttt{(| x = a |)}.
   1.143 +
   1.144 +A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
   1.145 +$y$ of value $b$.  The corresponding type is $\record{x \ty A\fs y \ty B}$,
   1.146 +assuming that $a \ty A$ and $b \ty B$.
   1.147  
   1.148 -FIXME proof tools (simp, cases/induct; no split!?);
   1.149 +A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
   1.150 +$x$ and $y$ as before, but also possibly further fields as indicated by the
   1.151 +``$\more$'' notation (which is actually part of the syntax).  The improper
   1.152 +field ``$\more$'' of a record scheme is called the \emph{more part}.
   1.153 +Logically it is just a free variable, which is occasionally referred to as
   1.154 +\emph{row variable} in the literature.  The more part of a record scheme may
   1.155 +be instantiated by zero or more further components.  For example, the above
   1.156 +scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more =
   1.157 +  m'}$, where $m'$ refers to a different more part.  Fixed records are special
   1.158 +instances of record schemes, where ``$\more$'' is properly terminated by the
   1.159 +$() :: unit$ element.  Actually, $\record{x = a\fs y = b}$ is just an
   1.160 +abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
   1.161 +
   1.162 +\medskip
   1.163  
   1.164 -FIXME mixfix syntax;
   1.165 +Two key observations make extensible records in a simply typed language like
   1.166 +HOL feasible:
   1.167 +\begin{enumerate}
   1.168 +\item the more part is internalized, as a free term or type variable,
   1.169 +\item field names are externalized, they cannot be accessed within the logic
   1.170 +  as first-class values.
   1.171 +\end{enumerate}
   1.172 +
   1.173 +\medskip
   1.174 +
   1.175 +In Isabelle/HOL record types have to be defined explicitly, fixing their field
   1.176 +names and types, and their (optional) parent record (see
   1.177 +{\S}\ref{sec:hol-record-def}).  Afterwards, records may be formed using above
   1.178 +syntax, while obeying the canonical order of fields as given by their
   1.179 +declaration.  The record package provides several standard operations like
   1.180 +selectors and updates (see {\S}\ref{sec:hol-record-ops}).  The common setup
   1.181 +for various generic proof tools enable succinct reasoning patterns (see
   1.182 +{\S}\ref{sec:hol-record-thms}).  See also the Isabelle/HOL tutorial
   1.183 +\cite{isabelle-hol-book} for further instructions on using records in
   1.184 +practice.
   1.185 +
   1.186 +
   1.187 +\subsection{Record specifications}\label{sec:hol-record-def}
   1.188  
   1.189  \indexisarcmdof{HOL}{record}
   1.190  \begin{matharray}{rcl}
   1.191 @@ -162,10 +245,135 @@
   1.192  \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
   1.193    defines extensible record type $(\vec\alpha)t$, derived from the optional
   1.194    parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
   1.195 -  See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on
   1.196 -  simply-typed extensible records.
   1.197 +
   1.198 +  The type variables of $\tau$ and $\vec\sigma$ need to be covered by the
   1.199 +  (distinct) parameters $\vec\alpha$.  Type constructor $t$ has to be new,
   1.200 +  while $\tau$ needs to specify an instance of an existing record type.  At
   1.201 +  least one new field $\vec c$ has to be specified.  Basically, field names
   1.202 +  need to belong to a unique record.  This is not a real restriction in
   1.203 +  practice, since fields are qualified by the record name internally.
   1.204 +
   1.205 +  The parent record specification $\tau$ is optional; if omitted $t$ becomes a
   1.206 +  root record.  The hierarchy of all records declared within a theory context
   1.207 +  forms a forest structure, i.e.\ a set of trees starting with a root record
   1.208 +  each.  There is no way to merge multiple parent records!
   1.209 +
   1.210 +  For convenience, $(\vec\alpha) \, t$ is made a type abbreviation for the
   1.211 +  fixed record type $\record{\vec c \ty \vec\sigma}$, likewise is
   1.212 +  $(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c
   1.213 +    \ty \vec\sigma\fs \more \ty \zeta}$.
   1.214 +
   1.215  \end{descr}
   1.216  
   1.217 +\subsection{Record operations}\label{sec:hol-record-ops}
   1.218 +
   1.219 +Any record definition of the form presented above produces certain standard
   1.220 +operations.  Selectors and updates are provided for any field, including the
   1.221 +improper one ``$more$''.  There are also cumulative record constructor
   1.222 +functions.  To simplify the presentation below, we assume for now that
   1.223 +$(\vec\alpha) \, t$ is a root record with fields $\vec c \ty \vec\sigma$.
   1.224 +
   1.225 +\medskip \textbf{Selectors} and \textbf{updates} are available for any field
   1.226 +(including ``$more$''):
   1.227 +\begin{matharray}{lll}
   1.228 +  c@i & \ty & \record{\vec c \ty \vec \sigma, \more \ty \zeta} \To \sigma@i \\
   1.229 +  c@i_update & \ty & \sigma@i \To \record{\vec c \ty \vec\sigma, \more \ty \zeta} \To
   1.230 +    \record{\vec c \ty \vec\sigma, \more \ty \zeta}
   1.231 +\end{matharray}
   1.232 +
   1.233 +There is special syntax for application of updates: $r \, \record{x \asn a}$
   1.234 +abbreviates term $x_update \, a \, r$.  Further notation for repeated updates
   1.235 +is also available: $r \, \record{x \asn a} \, \record{y \asn b} \, \record{z
   1.236 +  \asn c}$ may be written $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$.
   1.237 +Note that because of postfix notation the order of fields shown here is
   1.238 +reverse than in the actual term.  Since repeated updates are just function
   1.239 +applications, fields may be freely permuted in $\record{x \asn a\fs y \asn
   1.240 +  b\fs z \asn c}$, as far as logical equality is concerned.  Thus
   1.241 +commutativity of updates can be proven within the logic for any two fields,
   1.242 +but not as a general theorem: fields are not first-class values.
   1.243 +
   1.244 +\medskip The \textbf{make} operation provides a cumulative record constructor
   1.245 +functions:
   1.246 +\begin{matharray}{lll}
   1.247 +  t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
   1.248 +\end{matharray}
   1.249 +
   1.250 +\medskip We now reconsider the case of non-root records, which are derived of
   1.251 +some parent.  In general, the latter may depend on another parent as well,
   1.252 +resulting in a list of \emph{ancestor records}.  Appending the lists of fields
   1.253 +of all ancestors results in a certain field prefix.  The record package
   1.254 +automatically takes care of this by lifting operations over this context of
   1.255 +ancestor fields.  Assuming that $(\vec\alpha) \, t$ has ancestor fields $\vec
   1.256 +b \ty \vec\rho$, the above record operations will get the following types:
   1.257 +\begin{matharray}{lll}
   1.258 +  c@i & \ty & \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty
   1.259 +    \zeta} \To \sigma@i \\
   1.260 +  c@i_update & \ty & \sigma@i \To
   1.261 +    \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To
   1.262 +    \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\
   1.263 +  t{\dtt}make & \ty & \vec\rho \To \vec\sigma \To
   1.264 +    \record{\vec b \ty \vec\rho, \vec c \ty \vec \sigma} \\
   1.265 +\end{matharray}
   1.266 +\noindent
   1.267 +
   1.268 +\medskip Some further operations address the extension aspect of a derived
   1.269 +record scheme specifically: $fields$ produces a record fragment consisting of
   1.270 +exactly the new fields introduced here (the result may serve as a more part
   1.271 +elsewhere); $extend$ takes a fixed record and adds a given more part;
   1.272 +$truncate$ restricts a record scheme to a fixed record.
   1.273 +
   1.274 +\begin{matharray}{lll}
   1.275 +  t{\dtt}fields & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
   1.276 +  t{\dtt}extend & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \To
   1.277 +    \zeta \To \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\
   1.278 +  t{\dtt}truncate & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To
   1.279 +    \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\
   1.280 +\end{matharray}
   1.281 +
   1.282 +\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ are actually coincide for root records.
   1.283 +
   1.284 +
   1.285 +\subsection{Derived rules and proof tools}\label{sec:hol-record-thms}
   1.286 +
   1.287 +The record package proves several results internally, declaring these facts to
   1.288 +appropriate proof tools.  This enables users to reason about record structures
   1.289 +quite comfortably.  Assume that $t$ is a record type as specified above.
   1.290 +
   1.291 +\begin{enumerate}
   1.292 +
   1.293 +\item Standard conversions for selectors or updates applied to record
   1.294 +  constructor terms are made part of the default Simplifier context; thus
   1.295 +  proofs by reduction of basic operations merely require the $simp$ method
   1.296 +  without further arguments.  These rules are available as $t{\dtt}simps$.
   1.297 +
   1.298 +\item Selectors applied to updated records are automatically reduced by an
   1.299 +  internal simplification procedure, which is also part of the default
   1.300 +  Simplifier context.
   1.301 +
   1.302 +\item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
   1.303 +  \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$
   1.304 +  rules.  These rules are available as $t{\dtt}iffs$.
   1.305 +
   1.306 +\item The introduction rule for record equality analogous to $x~r = x~r' \Imp
   1.307 +  y~r = y~r' \Imp \dots \Imp r = r'$ is declared to the Simplifier, and as the
   1.308 +  basic rule context as ``$intro?$''.  The rule is called $t{\dtt}equality$.
   1.309 +
   1.310 +\item Representations of arbitrary record expressions as canonical constructor
   1.311 +  terms are provided both in $cases$ and $induct$ format (cf.\ the generic
   1.312 +  proof methods of the same name, \S\ref{sec:cases-induct}).  Several
   1.313 +  variations are available, for fixed records, record schemes, more parts etc.
   1.314 +
   1.315 +  The generic proof methods are sufficiently smart to pick the most sensible
   1.316 +  rule according to the type of the indicated record expression: users just
   1.317 +  need to apply something like ``$(cases r)$'' to a certain proof problem.
   1.318 +
   1.319 +\item The derived record operations $t{\dtt}make$, $t{\dtt}fields$,
   1.320 +  $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but
   1.321 +  usually need to be expanded by hand, using the collective fact
   1.322 +  $t{\dtt}defs$.
   1.323 +
   1.324 +\end{enumerate}
   1.325 +
   1.326  
   1.327  \subsection{Datatypes}\label{sec:hol-datatype}
   1.328  
   1.329 @@ -202,12 +410,12 @@
   1.330  to the constructors involved, while parameters are named after the types (see
   1.331  also \S\ref{sec:cases-induct}).
   1.332  
   1.333 -See \cite{isabelle-HOL} for more details on datatypes.  Note that the theory
   1.334 -syntax above has been slightly simplified over the old version, usually
   1.335 -requiring more quotes and less parentheses.  Apart from proper proof methods
   1.336 -for case-analysis and induction, there are also emulations of ML tactics
   1.337 +See \cite{isabelle-HOL} for more details on datatypes, but beware of the
   1.338 +old-style theory syntax being used there!  Apart from proper proof methods for
   1.339 +case-analysis and induction, there are also emulations of ML tactics
   1.340  \texttt{case_tac} and \texttt{induct_tac} available, see
   1.341 -\S\ref{sec:induct_tac}.
   1.342 +\S\ref{sec:induct_tac}; these admit to refer directly to the internal
   1.343 +structure of subgoals (including internally bound parameters).
   1.344  
   1.345  
   1.346  \subsection{Recursive functions}\label{sec:recursion}
   1.347 @@ -253,25 +461,25 @@
   1.348  
   1.349  \begin{descr}
   1.350  \item [$\isarkeyword{primrec}$] defines primitive recursive functions over
   1.351 -  datatypes, see also \cite{isabelle-HOL}.
   1.352 +  datatypes, see also \cite{isabelle-HOL} FIXME.
   1.353  \item [$\isarkeyword{recdef}$] defines general well-founded recursive
   1.354 -  functions (using the TFL package), see also \cite{isabelle-HOL}.  The
   1.355 +  functions (using the TFL package), see also \cite{isabelle-HOL} FIXME.  The
   1.356    $(permissive)$ option tells TFL to recover from failed proof attempts,
   1.357    returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
   1.358    $recdef_wf$ hints refer to auxiliary rules to be used in the internal
   1.359 -  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\ 
   1.360 +  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\
   1.361    \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
   1.362 -  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ 
   1.363 +  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
   1.364    \S\ref{sec:classical}).
   1.365  \item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
   1.366    termination condition number $i$ (default $1$) as generated by a
   1.367    $\isarkeyword{recdef}$ definition of constant $c$.
   1.368 -  
   1.369 +
   1.370    Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
   1.371    internal proofs without manual intervention.
   1.372  \end{descr}
   1.373  
   1.374 -Both kinds of recursive definitions accommodate reasoning by induction (cf.\ 
   1.375 +Both kinds of recursive definitions accommodate reasoning by induction (cf.\
   1.376  \S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
   1.377  the function definition) refers to a specific induction rule, with parameters
   1.378  named according to the user-specified equations.  Case names of
   1.379 @@ -342,8 +550,8 @@
   1.380    automated monotonicity proof of $\isarkeyword{inductive}$.
   1.381  \end{descr}
   1.382  
   1.383 -See \cite{isabelle-HOL} for further information on inductive definitions in
   1.384 -HOL.
   1.385 +See \cite{isabelle-HOL} FIXME for further information on inductive definitions
   1.386 +in HOL.
   1.387  
   1.388  
   1.389  \subsection{Arithmetic proof support}
   1.390 @@ -402,7 +610,7 @@
   1.391    ;
   1.392    indcases (prop +)
   1.393    ;
   1.394 -  inductivecases thmdecl? (prop +)
   1.395 +  inductivecases (thmdecl? (prop +) + 'and')
   1.396    ;
   1.397  
   1.398    rule: ('rule' ':' thmref)
   1.399 @@ -417,11 +625,11 @@
   1.400    both goal addressing and dynamic instantiation.  Note that named rule cases
   1.401    are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
   1.402    methods (see \S\ref{sec:cases-induct}).
   1.403 -  
   1.404 +
   1.405  \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
   1.406    to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
   1.407    forward manner.
   1.408 -  
   1.409 +
   1.410    While $ind_cases$ is a proof method to apply the result immediately as
   1.411    elimination rules, $\isarkeyword{inductive_cases}$ provides case split
   1.412    theorems at the theory level for later use,
   1.413 @@ -471,14 +679,12 @@
   1.414    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
   1.415  \end{rail}
   1.416  
   1.417 -Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ 
   1.418 +Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\
   1.419  \S\ref{sec:hol-datatype}).  Mutual recursive is supported, but no nesting nor
   1.420  arbitrary branching.  Domain constructors may be strict (default) or lazy, the
   1.421 -latter admits to introduce infinitary objects in the typical LCF manner (lazy
   1.422 -lists etc.).
   1.423 -
   1.424 -See also \cite{MuellerNvOS99} for further information HOLCF domains in
   1.425 -general.
   1.426 +latter admits to introduce infinitary objects in the typical LCF manner (e.g.\
   1.427 +lazy lists).  See also \cite{MuellerNvOS99} for a general discussion of HOLCF
   1.428 +domains.
   1.429  
   1.430  
   1.431  \section{ZF}
   1.432 @@ -492,7 +698,7 @@
   1.433  FIXME
   1.434  
   1.435  
   1.436 -%%% Local Variables: 
   1.437 +%%% Local Variables:
   1.438  %%% mode: latex
   1.439  %%% TeX-master: "isar-ref"
   1.440 -%%% End: 
   1.441 +%%% End: