hide SVC stuff (outdated);
authorwenzelm
Mon Mar 04 19:06:52 2002 +0100 (2002-03-04)
changeset 13012f8bfc61ee1b5
parent 13011 a474097a4c65
child 13013 4db07fc3d96f
hide SVC stuff (outdated);
moved records to isar-ref;
doc-src/HOL/HOL.tex
     1.1 --- a/doc-src/HOL/HOL.tex	Mon Mar 04 19:06:01 2002 +0100
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon Mar 04 19:06:52 2002 +0100
     1.3 @@ -1038,95 +1038,96 @@
     1.4  {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
     1.5  
     1.6  
     1.7 -\section{Calling the decision procedure SVC}\label{sec:HOL:SVC}
     1.8 -
     1.9 -\index{SVC decision procedure|(}
    1.10 -
    1.11 -The Stanford Validity Checker (SVC) is a tool that can check the validity of
    1.12 -certain types of formulae.  If it is installed on your machine, then
    1.13 -Isabelle/HOL can be configured to call it through the tactic
    1.14 -\ttindex{svc_tac}.  It is ideal for large tautologies and complex problems in
    1.15 -linear arithmetic.  Subexpressions that SVC cannot handle are automatically
    1.16 -replaced by variables, so you can call the tactic on any subgoal.  See the
    1.17 -file \texttt{HOL/ex/svc_test.ML} for examples.
    1.18 -\begin{ttbox} 
    1.19 -svc_tac   : int -> tactic
    1.20 -Svc.trace : bool ref      \hfill{\bf initially false}
    1.21 -\end{ttbox}
    1.22 -
    1.23 -\begin{ttdescription}
    1.24 -\item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating
    1.25 -  it into a formula recognized by~SVC\@.  If it succeeds then the subgoal is
    1.26 -  removed.  It fails if SVC is unable to prove the subgoal.  It crashes with
    1.27 -  an error message if SVC appears not to be installed.  Numeric variables may
    1.28 -  have types \texttt{nat}, \texttt{int} or \texttt{real}.
    1.29 -
    1.30 -\item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac}
    1.31 -  to trace its operations: abstraction of the subgoal, translation to SVC
    1.32 -  syntax, SVC's response.
    1.33 -\end{ttdescription}
    1.34 -
    1.35 -Here is an example, with tracing turned on:
    1.36 -\begin{ttbox}
    1.37 -set Svc.trace;
    1.38 -{\out val it : bool = true}
    1.39 -Goal "(#3::nat)*a <= #2 + #4*b + #6*c  & #11 <= #2*a + b + #2*c & \ttback
    1.40 -\ttback     a + #3*b <= #5 + #2*c  --> #2 + #3*b <= #2*a + #6*c";
    1.41 -
    1.42 -by (svc_tac 1);
    1.43 -{\out Subgoal abstracted to}
    1.44 -{\out #3 * a <= #2 + #4 * b + #6 * c &}
    1.45 -{\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
    1.46 -{\out #2 + #3 * b <= #2 * a + #6 * c}
    1.47 -{\out Calling SVC:}
    1.48 -{\out (=> (<= 0  (F_c) )  (=> (<= 0  (F_b) )  (=> (<= 0  (F_a) )}
    1.49 -{\out   (=> (AND (<= {* 3  (F_a) }  {+ {+ 2  {* 4  (F_b) } }  }
    1.50 -{\out {* 6  (F_c) } } )  (AND (<= 11  {+ {+ {* 2  (F_a) }  (F_b) }}
    1.51 -{\out   {* 2  (F_c) } } )  (<= {+ (F_a)  {* 3  (F_b) } }  {+ 5  }
    1.52 -{\out {* 2  (F_c) } } ) ) )  (< {+ 2  {* 3  (F_b) } }  {+ 1  {+ }
    1.53 -{\out {* 2  (F_a) }  {* 6  (F_c) } } } ) ) ) ) ) }
    1.54 -{\out SVC Returns:}
    1.55 -{\out VALID}
    1.56 -{\out Level 1}
    1.57 -{\out #3 * a <= #2 + #4 * b + #6 * c &}
    1.58 -{\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
    1.59 -{\out #2 + #3 * b <= #2 * a + #6 * c}
    1.60 -{\out No subgoals!}
    1.61 -\end{ttbox}
    1.62 -
    1.63 -
    1.64 -\begin{warn}
    1.65 -Calling \ttindex{svc_tac} entails an above-average risk of
    1.66 -unsoundness.  Isabelle does not check SVC's result independently.  Moreover,
    1.67 -the tactic translates the submitted formula using code that lies outside
    1.68 -Isabelle's inference core.  Theorems that depend upon results proved using SVC
    1.69 -(and other oracles) are displayed with the annotation \texttt{[!]} attached.
    1.70 -You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of
    1.71 -theorem~$th$, as described in the \emph{Reference Manual}.  
    1.72 -\end{warn}
    1.73 -
    1.74 -To start, first download SVC from the Internet at URL
    1.75 -\begin{ttbox}
    1.76 -http://agamemnon.stanford.edu/~levitt/vc/index.html
    1.77 -\end{ttbox}
    1.78 -and install it using the instructions supplied.  SVC requires two environment
    1.79 -variables:
    1.80 -\begin{ttdescription}
    1.81 -\item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC
    1.82 -    distribution directory. 
    1.83 +%FIXME outdated, both from the Isabelle and SVC perspective
    1.84 +% \section{Calling the decision procedure SVC}\label{sec:HOL:SVC}
    1.85 +
    1.86 +% \index{SVC decision procedure|(}
    1.87 +
    1.88 +% The Stanford Validity Checker (SVC) is a tool that can check the validity of
    1.89 +% certain types of formulae.  If it is installed on your machine, then
    1.90 +% Isabelle/HOL can be configured to call it through the tactic
    1.91 +% \ttindex{svc_tac}.  It is ideal for large tautologies and complex problems in
    1.92 +% linear arithmetic.  Subexpressions that SVC cannot handle are automatically
    1.93 +% replaced by variables, so you can call the tactic on any subgoal.  See the
    1.94 +% file \texttt{HOL/ex/svc_test.ML} for examples.
    1.95 +% \begin{ttbox} 
    1.96 +% svc_tac   : int -> tactic
    1.97 +% Svc.trace : bool ref      \hfill{\bf initially false}
    1.98 +% \end{ttbox}
    1.99 +
   1.100 +% \begin{ttdescription}
   1.101 +% \item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating
   1.102 +%   it into a formula recognized by~SVC\@.  If it succeeds then the subgoal is
   1.103 +%   removed.  It fails if SVC is unable to prove the subgoal.  It crashes with
   1.104 +%   an error message if SVC appears not to be installed.  Numeric variables may
   1.105 +%   have types \texttt{nat}, \texttt{int} or \texttt{real}.
   1.106 +
   1.107 +% \item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac}
   1.108 +%   to trace its operations: abstraction of the subgoal, translation to SVC
   1.109 +%   syntax, SVC's response.
   1.110 +% \end{ttdescription}
   1.111 +
   1.112 +% Here is an example, with tracing turned on:
   1.113 +% \begin{ttbox}
   1.114 +% set Svc.trace;
   1.115 +% {\out val it : bool = true}
   1.116 +% Goal "(#3::nat)*a <= #2 + #4*b + #6*c  & #11 <= #2*a + b + #2*c & \ttback
   1.117 +% \ttback     a + #3*b <= #5 + #2*c  --> #2 + #3*b <= #2*a + #6*c";
   1.118 +
   1.119 +% by (svc_tac 1);
   1.120 +% {\out Subgoal abstracted to}
   1.121 +% {\out #3 * a <= #2 + #4 * b + #6 * c &}
   1.122 +% {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
   1.123 +% {\out #2 + #3 * b <= #2 * a + #6 * c}
   1.124 +% {\out Calling SVC:}
   1.125 +% {\out (=> (<= 0  (F_c) )  (=> (<= 0  (F_b) )  (=> (<= 0  (F_a) )}
   1.126 +% {\out   (=> (AND (<= {* 3  (F_a) }  {+ {+ 2  {* 4  (F_b) } }  }
   1.127 +% {\out {* 6  (F_c) } } )  (AND (<= 11  {+ {+ {* 2  (F_a) }  (F_b) }}
   1.128 +% {\out   {* 2  (F_c) } } )  (<= {+ (F_a)  {* 3  (F_b) } }  {+ 5  }
   1.129 +% {\out {* 2  (F_c) } } ) ) )  (< {+ 2  {* 3  (F_b) } }  {+ 1  {+ }
   1.130 +% {\out {* 2  (F_a) }  {* 6  (F_c) } } } ) ) ) ) ) }
   1.131 +% {\out SVC Returns:}
   1.132 +% {\out VALID}
   1.133 +% {\out Level 1}
   1.134 +% {\out #3 * a <= #2 + #4 * b + #6 * c &}
   1.135 +% {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
   1.136 +% {\out #2 + #3 * b <= #2 * a + #6 * c}
   1.137 +% {\out No subgoals!}
   1.138 +% \end{ttbox}
   1.139 +
   1.140 +
   1.141 +% \begin{warn}
   1.142 +% Calling \ttindex{svc_tac} entails an above-average risk of
   1.143 +% unsoundness.  Isabelle does not check SVC's result independently.  Moreover,
   1.144 +% the tactic translates the submitted formula using code that lies outside
   1.145 +% Isabelle's inference core.  Theorems that depend upon results proved using SVC
   1.146 +% (and other oracles) are displayed with the annotation \texttt{[!]} attached.
   1.147 +% You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of
   1.148 +% theorem~$th$, as described in the \emph{Reference Manual}.  
   1.149 +% \end{warn}
   1.150 +
   1.151 +% To start, first download SVC from the Internet at URL
   1.152 +% \begin{ttbox}
   1.153 +% http://agamemnon.stanford.edu/~levitt/vc/index.html
   1.154 +% \end{ttbox}
   1.155 +% and install it using the instructions supplied.  SVC requires two environment
   1.156 +% variables:
   1.157 +% \begin{ttdescription}
   1.158 +% \item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC
   1.159 +%     distribution directory. 
   1.160      
   1.161 -  \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and
   1.162 -    operating system.  
   1.163 -\end{ttdescription}
   1.164 -You can set these environment variables either using the Unix shell or through
   1.165 -an Isabelle \texttt{settings} file.  Isabelle assumes SVC to be installed if
   1.166 -\texttt{SVC_HOME} is defined.
   1.167 -
   1.168 -\paragraph*{Acknowledgement.}  This interface uses code supplied by S{\o}ren
   1.169 -Heilmann.
   1.170 -
   1.171 -
   1.172 -\index{SVC decision procedure|)}
   1.173 +%   \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and
   1.174 +%     operating system.  
   1.175 +% \end{ttdescription}
   1.176 +% You can set these environment variables either using the Unix shell or through
   1.177 +% an Isabelle \texttt{settings} file.  Isabelle assumes SVC to be installed if
   1.178 +% \texttt{SVC_HOME} is defined.
   1.179 +
   1.180 +% \paragraph*{Acknowledgement.}  This interface uses code supplied by S{\o}ren
   1.181 +% Heilmann.
   1.182 +
   1.183 +
   1.184 +% \index{SVC decision procedure|)}
   1.185  
   1.186  
   1.187  
   1.188 @@ -1405,20 +1406,20 @@
   1.189  orderings.  For full details, please survey the theories in subdirectories
   1.190  \texttt{Integ} and \texttt{Real}.
   1.191  
   1.192 -All three numeric types admit numerals of the form \texttt{\#$sd\ldots d$},
   1.193 +All three numeric types admit numerals of the form \texttt{$sd\ldots d$},
   1.194  where $s$ is an optional minus sign and $d\ldots d$ is a string of digits.
   1.195  Numerals are represented internally by a datatype for binary notation, which
   1.196  allows numerical calculations to be performed by rewriting.  For example, the
   1.197 -integer division of \texttt{\#54342339} by \texttt{\#3452} takes about five
   1.198 +integer division of \texttt{54342339} by \texttt{3452} takes about five
   1.199  seconds.  By default, the simplifier cancels like terms on the opposite sites
   1.200  of relational operators (reducing \texttt{z+x<x+y} to \texttt{z<y}, for
   1.201 -instance.  The simplifier also collects like terms, replacing
   1.202 -\texttt{x+y+x*\#3} by \texttt{\#4*x+y}.
   1.203 -
   1.204 -Sometimes numerals are not wanted, because for example \texttt{n+\#3} does not
   1.205 +instance.  The simplifier also collects like terms, replacing \texttt{x+y+x*3}
   1.206 +by \texttt{4*x+y}.
   1.207 +
   1.208 +Sometimes numerals are not wanted, because for example \texttt{n+3} does not
   1.209  match a pattern of the form \texttt{Suc $k$}.  You can re-arrange the form of
   1.210 -an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such
   1.211 -as \texttt{n+\#3 = Suc (Suc (Suc n))}.  As an alternative, you can disable the
   1.212 +an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such as
   1.213 +\texttt{n+3 = Suc (Suc (Suc n))}.  As an alternative, you can disable the
   1.214  fancier simplifications by using a basic simpset such as \texttt{HOL_ss}
   1.215  rather than the default one, \texttt{simpset()}.
   1.216  
   1.217 @@ -1701,253 +1702,6 @@
   1.218  \end{warn}
   1.219  
   1.220  
   1.221 -\section{Records}
   1.222 -
   1.223 -At a first approximation, records are just a minor generalisation of tuples,
   1.224 -where components may be addressed by labels instead of just position (think of
   1.225 -{\ML}, for example).  The version of records offered by Isabelle/HOL is
   1.226 -slightly more advanced, though, supporting \emph{extensible record schemes}.
   1.227 -This admits operations that are polymorphic with respect to record extension,
   1.228 -yielding ``object-oriented'' effects like (single) inheritance.  See also
   1.229 -\cite{NaraschewskiW-TPHOLs98} for more details on object-oriented
   1.230 -verification and record subtyping in HOL.
   1.231 -
   1.232 -
   1.233 -\subsection{Basics}
   1.234 -
   1.235 -Isabelle/HOL supports fixed and schematic records both at the level of terms
   1.236 -and types.  The concrete syntax is as follows:
   1.237 -
   1.238 -\begin{center}
   1.239 -\begin{tabular}{l|l|l}
   1.240 -  & record terms & record types \\ \hline
   1.241 -  fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
   1.242 -  schematic & $\record{x = a\fs y = b\fs \more = m}$ &
   1.243 -    $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
   1.244 -\end{tabular}
   1.245 -\end{center}
   1.246 -
   1.247 -\noindent The \textsc{ascii} representation of $\record{x = a}$ is \texttt{(| x = a |)}.
   1.248 -
   1.249 -A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
   1.250 -$y$ of value $b$.  The corresponding type is $\record{x \ty A\fs y \ty B}$,
   1.251 -assuming that $a \ty A$ and $b \ty B$.
   1.252 -
   1.253 -A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
   1.254 -$x$ and $y$ as before, but also possibly further fields as indicated by the
   1.255 -``$\more$'' notation (which is actually part of the syntax).  The improper
   1.256 -field ``$\more$'' of a record scheme is called the \emph{more part}.
   1.257 -Logically it is just a free variable, which is occasionally referred to as
   1.258 -\emph{row variable} in the literature.  The more part of a record scheme may
   1.259 -be instantiated by zero or more further components.  For example, above scheme
   1.260 -might get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = m'}$,
   1.261 -where $m'$ refers to a different more part.  Fixed records are special
   1.262 -instances of record schemes, where ``$\more$'' is properly terminated by the
   1.263 -$() :: unit$ element.  Actually, $\record{x = a\fs y = b}$ is just an
   1.264 -abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
   1.265 -
   1.266 -\medskip
   1.267 -
   1.268 -There are two key features that make extensible records in a simply typed
   1.269 -language like HOL feasible:
   1.270 -\begin{enumerate}
   1.271 -\item the more part is internalised, as a free term or type variable,
   1.272 -\item field names are externalised, they cannot be accessed within the logic
   1.273 -  as first-class values.
   1.274 -\end{enumerate}
   1.275 -
   1.276 -\medskip
   1.277 -
   1.278 -In Isabelle/HOL record types have to be defined explicitly, fixing their field
   1.279 -names and types, and their (optional) parent record (see
   1.280 -{\S}\ref{sec:HOL:record-def}).  Afterwards, records may be formed using above
   1.281 -syntax, while obeying the canonical order of fields as given by their
   1.282 -declaration.  The record package also provides several operations like
   1.283 -selectors and updates (see {\S}\ref{sec:HOL:record-ops}), together with
   1.284 -characteristic properties (see {\S}\ref{sec:HOL:record-thms}).
   1.285 -
   1.286 -There is an example theory demonstrating most basic aspects of extensible
   1.287 -records (see theory \texttt{HOL/ex/Records} in the Isabelle sources).
   1.288 -
   1.289 -
   1.290 -\subsection{Defining records}\label{sec:HOL:record-def}
   1.291 -
   1.292 -The theory syntax for record type definitions is shown in
   1.293 -Fig.~\ref{fig:HOL:record}.  For the definition of `typevarlist' and `type' see
   1.294 -\iflabelundefined{chap:classical}
   1.295 -{the appendix of the {\em Reference Manual\/}}%
   1.296 -{Appendix~\ref{app:TheorySyntax}}.
   1.297 -
   1.298 -\begin{figure}[htbp]
   1.299 -\begin{rail}
   1.300 -record  : 'record' typevarlist name '=' parent (field +);
   1.301 -
   1.302 -parent  : ( () | type '+');
   1.303 -field   : name '::' type;
   1.304 -\end{rail}
   1.305 -\caption{Syntax of record type definitions}
   1.306 -\label{fig:HOL:record}
   1.307 -\end{figure}
   1.308 -
   1.309 -A general \ttindex{record} specification is of the following form:
   1.310 -\[
   1.311 -\mathtt{record}~(\alpha@1, \dots, \alpha@n) \, t ~=~
   1.312 -  (\tau@1, \dots, \tau@m) \, s ~+~ c@1 :: \sigma@1 ~ \dots ~ c@l :: \sigma@l
   1.313 -\]
   1.314 -where $\vec\alpha@n$ are distinct type variables, and $\vec\tau@m$,
   1.315 -$\vec\sigma@l$ are types containing at most variables from $\vec\alpha@n$.
   1.316 -Type constructor $t$ has to be new, while $s$ has to specify an existing
   1.317 -record type.  Furthermore, the $\vec c@l$ have to be distinct field names.
   1.318 -There has to be at least one field.
   1.319 -
   1.320 -In principle, field names may never be shared with other records.  This is no
   1.321 -actual restriction in practice, since $\vec c@l$ are internally declared
   1.322 -within a separate name space qualified by the name $t$ of the record.
   1.323 -
   1.324 -\medskip
   1.325 -
   1.326 -Above definition introduces a new record type $(\vec\alpha@n) \, t$ by
   1.327 -extending an existing one $(\vec\tau@m) \, s$ by new fields $\vec c@l \ty
   1.328 -\vec\sigma@l$.  The parent record specification is optional, by omitting it
   1.329 -$t$ becomes a \emph{root record}.  The hierarchy of all records declared
   1.330 -within a theory forms a forest structure, i.e.\ a set of trees, where any of
   1.331 -these is rooted by some root record.
   1.332 -
   1.333 -For convenience, $(\vec\alpha@n) \, t$ is made a type abbreviation for the
   1.334 -fixed record type $\record{\vec c@l \ty \vec\sigma@l}$, and $(\vec\alpha@n,
   1.335 -\zeta) \, t_scheme$ is made an abbreviation for $\record{\vec c@l \ty
   1.336 -  \vec\sigma@l\fs \more \ty \zeta}$.
   1.337 -
   1.338 -\medskip
   1.339 -
   1.340 -The following simple example defines a root record type $point$ with fields $x
   1.341 -\ty nat$ and $y \ty nat$, and record type $cpoint$ by extending $point$ with
   1.342 -an additional $colour$ component.
   1.343 -
   1.344 -\begin{ttbox}
   1.345 -  record point =
   1.346 -    x :: nat
   1.347 -    y :: nat
   1.348 -
   1.349 -  record cpoint = point +
   1.350 -    colour :: string
   1.351 -\end{ttbox}
   1.352 -
   1.353 -
   1.354 -\subsection{Record operations}\label{sec:HOL:record-ops}
   1.355 -
   1.356 -Any record definition of the form presented above produces certain standard
   1.357 -operations.  Selectors and updates are provided for any field, including the
   1.358 -improper one ``$more$''.  There are also cumulative record constructor
   1.359 -functions.
   1.360 -
   1.361 -To simplify the presentation below, we first assume that $(\vec\alpha@n) \, t$
   1.362 -is a root record with fields $\vec c@l \ty \vec\sigma@l$.
   1.363 -
   1.364 -\medskip
   1.365 -
   1.366 -\textbf{Selectors} and \textbf{updates} are available for any field (including
   1.367 -``$more$'') as follows:
   1.368 -\begin{matharray}{lll}
   1.369 -  c@i & \ty & \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To \sigma@i \\
   1.370 -  c@i_update & \ty & \sigma@i \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To
   1.371 -    \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta}
   1.372 -\end{matharray}
   1.373 -
   1.374 -There is some special syntax for updates: $r \, \record{x \asn a}$ abbreviates
   1.375 -term $x_update \, a \, r$.  Repeated updates are supported as well: $r \,
   1.376 -\record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as
   1.377 -$r \, \record{x \asn a\fs y \asn b\fs z \asn c}$.  Note that because of
   1.378 -postfix notation the order of fields shown here is reverse than in the actual
   1.379 -term.  This might lead to confusion in conjunction with special proof tools
   1.380 -such as ordered rewriting.
   1.381 -
   1.382 -Since repeated updates are just function applications, fields may be freely
   1.383 -permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as the logic
   1.384 -is concerned.  Thus commutativity of updates can be proven within the logic
   1.385 -for any two fields, but not as a general theorem: fields are not first-class
   1.386 -values.
   1.387 -
   1.388 -\medskip
   1.389 -
   1.390 -\textbf{Make} operations provide cumulative record constructor functions:
   1.391 -\begin{matharray}{lll}
   1.392 -  make & \ty & \vec\sigma@l \To \record{\vec c@l \ty \vec \sigma@l} \\
   1.393 -  make_scheme & \ty & \vec\sigma@l \To
   1.394 -    \zeta \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \\
   1.395 -\end{matharray}
   1.396 -\noindent
   1.397 -These functions are curried.  The corresponding definitions in terms of actual
   1.398 -record terms are part of the standard simpset.  Thus $point\dtt make\,a\,b$
   1.399 -rewrites to $\record{x = a\fs y = b}$.
   1.400 -
   1.401 -\medskip
   1.402 -
   1.403 -Any of above selector, update and make operations are declared within a local
   1.404 -name space prefixed by the name $t$ of the record.  In case that different
   1.405 -records share base names of fields, one has to qualify names explicitly (e.g.\ 
   1.406 -$t\dtt c@i_update$).  This is recommended especially for operations like
   1.407 -$make$ or $update_more$ that always have the same base name.  Just use $t\dtt
   1.408 -make$ etc.\ to avoid confusion.
   1.409 -
   1.410 -\bigskip
   1.411 -
   1.412 -We reconsider the case of non-root records, which are derived of some parent
   1.413 -record.  In general, the latter may depend on another parent as well,
   1.414 -resulting in a list of \emph{ancestor records}.  Appending the lists of fields
   1.415 -of all ancestors results in a certain field prefix.  The record package
   1.416 -automatically takes care of this by lifting operations over this context of
   1.417 -ancestor fields.  Assuming that $(\vec\alpha@n) \, t$ has ancestor fields
   1.418 -$\vec d@k \ty \vec\rho@k$, selectors will get the following types:
   1.419 -\begin{matharray}{lll}
   1.420 -  c@i & \ty & \record{\vec d@k \ty \vec\rho@k, \vec c@l \ty \vec \sigma@l, \more \ty \zeta}
   1.421 -    \To \sigma@i
   1.422 -\end{matharray}
   1.423 -\noindent
   1.424 -Update and make operations are analogous.
   1.425 -
   1.426 -
   1.427 -\subsection{Record proof tools}\label{sec:HOL:record-thms}
   1.428 -
   1.429 -The record package declares the following proof rules for any record type $t$.
   1.430 -\begin{enumerate}
   1.431 -  
   1.432 -\item Standard conversions (selectors or updates applied to record constructor
   1.433 -  terms, make function definitions) are part of the standard simpset (via
   1.434 -  \texttt{addsimps}).
   1.435 -  
   1.436 -\item Selectors applied to updated records are automatically reduced by
   1.437 -  simplification procedure \ttindex{record_simproc}, which is part of the
   1.438 -  default simpset.
   1.439 -  
   1.440 -\item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
   1.441 -  \conj y=y'$ are made part of the standard simpset and claset (via
   1.442 -  \texttt{addIffs}).
   1.443 -  
   1.444 -\item The introduction rule for record equality analogous to $x~r = x~r' \Imp
   1.445 -  y~r = y~r' \Imp \dots \Imp r = r'$ is added to the simpset and to the claset
   1.446 -  (as an ``extra introduction'').
   1.447 -  
   1.448 -\item A tactic for record field splitting (\ttindex{record_split_tac}) may be
   1.449 -  made part of the claset (via \texttt{addSWrapper}).  This tactic is based on
   1.450 -  rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, b))$ for
   1.451 -  any field.
   1.452 -\end{enumerate}
   1.453 -
   1.454 -The first two kinds of rules are stored within the theory as $t\dtt simps$ and
   1.455 -$t\dtt iffs$, respectively; record equality introduction is available as
   1.456 -$t\dtt equality$.  In some situations it might be appropriate to expand the
   1.457 -definitions of updates: $t\dtt update_defs$.  Note that these names are
   1.458 -\emph{not} bound at the {\ML} level.
   1.459 -
   1.460 -\medskip
   1.461 -
   1.462 -Most of the time, plain Simplification should be sufficient to solve goals
   1.463 -involving records.  Combinations of the Simplifier and Classical Reasoner
   1.464 -(\texttt{Auto_tac} or \texttt{Force_tac}) are very useful, too.  The example
   1.465 -theory \texttt{HOL/ex/Records} demonstrates typical proofs concerning records.
   1.466 -
   1.467 -
   1.468  \section{Datatype definitions}
   1.469  \label{sec:HOL:datatype}
   1.470  \index{*datatype|(}