# HG changeset patch
# User wenzelm
# Date 970145355 -7200
# Node ID dcb72400bc321235c947114bf7da94b562d2b3de
# Parent  72a719e997b9872443c3603c12072937cc7c1e85
record proof tools: t.equality;
inductibe: split_asm, splits, cases;
tuned;

diff -r 72a719e997b9 -r dcb72400bc32 doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Thu Sep 28 14:48:05 2000 +0200
+++ b/doc-src/HOL/HOL.tex	Thu Sep 28 14:49:15 2000 +0200
@@ -1216,10 +1216,10 @@
 $\lambda$-abstraction.  Some important examples are
 \begin{description}
 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$}
-\item[Quantifiers:] \texttt{!~{\it pattern}:$A$.~$P$}
-\item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$}
+\item[Quantifiers:] \texttt{ALL~{\it pattern}:$A$.~$P$}
+\item[Choice:] {\underscoreon \tt SOME~{\it pattern}.~$P$}
 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}
-\item[Sets:] \texttt{{\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}}
+\item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}}
 \end{description}
 
 There is a simple tactic which supports reasoning about patterns:
@@ -1855,12 +1855,12 @@
 \end{matharray}
 
 There is some special syntax for updates: $r \, \record{x \asn a}$ abbreviates
-term $x_update \, a \, r$.  Repeated updates are also supported: $r \,
+term $x_update \, a \, r$.  Repeated updates are supported as well: $r \,
 \record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as
 $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$.  Note that because of
 postfix notation the order of fields shown here is reverse than in the actual
-term.  This might lead to confusion in conjunction with proof tools like
-ordered rewriting.
+term.  This might lead to confusion in conjunction with special proof tools
+such as ordered rewriting.
 
 Since repeated updates are just function applications, fields may be freely
 permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as the logic
@@ -1907,9 +1907,9 @@
 Update and make operations are analogous.
 
 
-\subsection{Proof tools}\label{sec:HOL:record-thms}
-
-The record package provides the following proof rules for any record type $t$.
+\subsection{Record proof tools}\label{sec:HOL:record-thms}
+
+The record package declares the following proof rules for any record type $t$.
 \begin{enumerate}
   
 \item Standard conversions (selectors or updates applied to record constructor
@@ -1924,6 +1924,10 @@
   \conj y=y'$ are made part of the standard simpset and claset (via
   \texttt{addIffs}).
   
+\item The introduction rule for record equality analogous to $x~r = x~r' \Imp
+  y~r = y~r' \Imp \dots \Imp r = r'$ is added to the simpset and to the claset
+  (as an ``extra introduction'').
+  
 \item A tactic for record field splitting (\ttindex{record_split_tac}) may be
   made part of the claset (via \texttt{addSWrapper}).  This tactic is based on
   rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, b))$ for
@@ -1931,19 +1935,17 @@
 \end{enumerate}
 
 The first two kinds of rules are stored within the theory as $t\dtt simps$ and
-$t\dtt iffs$, respectively.  In some situations it might be appropriate to
-expand the definitions of updates: $t\dtt update_defs$.  Note that these names
-are \emph{not} bound at the {\ML} level.
+$t\dtt iffs$, respectively; record equality introduction is available as
+$t\dtt equality$.  In some situations it might be appropriate to expand the
+definitions of updates: $t\dtt update_defs$.  Note that these names are
+\emph{not} bound at the {\ML} level.
 
 \medskip
 
-The example theory \texttt{HOL/ex/Records} demonstrates typical proofs
-concerning records.  The basic idea is to make \ttindex{record_split_tac}
-expand quantified record variables and then simplify by the conversion rules.
-By using a combination of the simplifier and classical prover together with
-the default simpset and claset, record problems should be solved with a single
-stroke of \texttt{Auto_tac} or \texttt{Force_tac}.  Most of the time, plain
-\texttt{Simp_tac} should be sufficient, though.
+Most of the time, plain Simplification should be sufficient to solve goals
+involving records.  Combinations of the Simplifier and Classical Reasoner
+(\texttt{Auto_tac} or \texttt{Force_tac}) are very useful, too.  The example
+theory \texttt{HOL/ex/Records} demonstrates typical proofs concerning records.
 
 
 \section{Datatype definitions}
@@ -2190,6 +2192,10 @@
 This theorem can be added to a simpset via \ttindex{addsplits}
 (see~{\S}\ref{subsec:HOL:case:splitting}).
 
+Case splitting on assumption works as well, by using the rule
+$t@j.$\texttt{split_asm} in the same manner.  Both rules are available under
+$t@j.$\texttt{splits} (this name is \emph{not} bound in ML, though).
+
 \begin{warn}\index{simplification!of \texttt{case}}%
   By default only the selector expression ($e$ above) in a
   \texttt{case}-construct is simplified, in analogy with \texttt{if} (see
@@ -2865,9 +2871,11 @@
 the recursive sets.  The rules are also available individually, using the
 names given them in the theory file. 
 
-\item[\tt elims] is the list of elimination rule.
-
-\item[\tt elim] is the head of the list \texttt{elims}.
+\item[\tt elims] is the list of elimination rule.  This is for compatibility
+  with ML scripts; within the theory the name is \texttt{cases}.
+  
+\item[\tt elim] is the head of the list \texttt{elims}.  This is for
+  compatibility only.
   
 \item[\tt mk_cases] is a function to create simplified instances of {\tt
 elim} using freeness reasoning on underlying datatypes.
@@ -3215,5 +3223,5 @@
 
 %%% Local Variables: 
 %%% mode: latex
-%%% TeX-master: "logics"
+%%% TeX-master: "logics-HOL"
 %%% End: