summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 28 Sep 2000 14:49:15 +0200 | |

changeset 10109 | dcb72400bc32 |

parent 10108 | 72a719e997b9 |

child 10110 | 7d6e03a1f11e |

record proof tools: t.equality;
inductibe: split_asm, splits, cases;
tuned;

--- 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: