author | wenzelm |

Mon Mar 04 19:06:52 2002 +0100 (2002-03-04) | |

changeset 13012 | f8bfc61ee1b5 |

parent 13011 | a474097a4c65 |

child 13013 | 4db07fc3d96f |

hide SVC stuff (outdated);

moved records to isar-ref;

moved records to isar-ref;

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|(}