hol88 (2.02.19940316-13.1) Library/finite_sets/Manual/entries.tex

Summary

 Library/finite_sets/Manual/entries.tex |  161 ++++++++++++++++-----------------
 1 file changed, 79 insertions(+), 82 deletions(-)

    
download this patch

Patch contents

--- hol88-2.02.19940316.orig/Library/finite_sets/Manual/entries.tex
+++ hol88-2.02.19940316/Library/finite_sets/Manual/entries.tex
@@ -1,7 +1,4 @@
-\chapter{ML Functions in the Library}
-\label{entries}
-\input{entries-intro}
-\DOC{DELETE\_CONV}
+\chapter{ML Functions in the Library}\label{entries}\input{entries-intro}\DOC{DELETE\_CONV}
 
 \TYPE {\small\verb%DELETE_CONV : conv -> conv%}\egroup
 
@@ -171,6 +168,84 @@
 
 \ENDDOC
 
+\DOC{IN\_CONV}
+
+\TYPE {\small\verb%IN_CONV : conv -> conv%}\egroup
+
+\SYNOPSIS
+Decision procedure for membership in finite sets.
+
+\DESCRIBE 
+The function {\small\verb%IN_CONV%} is a parameterized conversion for proving or disproving
+membership assertions of the general form:
+{\par\samepage\setseps\small
+\begin{verbatim}
+   "t IN {t1,...,tn}"
+\end{verbatim}
+}
+\noindent where {\small\verb%{t1,...,tn}%} is a set of type {\small\verb%(ty)set%} and {\small\verb%t%} is a value
+of the base type {\small\verb%ty%}.  The first argument to {\small\verb%IN_CONV%} is expected to be a
+conversion that decides equality between values of the base type {\small\verb%ty%}.  Given
+an equation {\small\verb%"e1 = e2"%}, where {\small\verb%e1%} and {\small\verb%e2%} are terms of type {\small\verb%ty%}, this
+conversion should return the theorem {\small\verb%|- (e1 = e2) = T%} or the theorem
+{\small\verb%|- (e1 = e2) = F%}, as appropriate.
+
+Given such a conversion, the function {\small\verb%IN_CONV%} returns a conversion that
+maps a term of the form {\small\verb%"t IN {t1,...,tn}"%} to the theorem
+{\par\samepage\setseps\small
+\begin{verbatim}
+   |- t IN {t1,...,tn} = T
+\end{verbatim}
+}
+
+\noindent if {\small\verb%t%} is alpha-equivalent to any {\small\verb%ti%}, or if the supplied conversion
+proves {\small\verb%|- (t = ti) = T%} for any {\small\verb%ti%}. If the supplied conversion proves
+{\small\verb%|- (t = ti) = F%} for every {\small\verb%ti%}, then the result is the theorem
+{\par\samepage\setseps\small
+\begin{verbatim}
+   |- t IN {t1,...,tn} = F 
+\end{verbatim}
+}
+\noindent In all other cases, {\small\verb%IN_CONV%} will fail.
+
+\EXAMPLE
+In the following example, the conversion {\small\verb%num_EQ_CONV%} is supplied as a
+parameter and used to test equality of the candidate element {\small\verb%1%} with the
+actual elements of the given set.
+{\par\samepage\setseps\small
+\begin{verbatim}
+   #IN_CONV num_EQ_CONV "2 IN {0,SUC 1,3}";;
+   |- 2 IN {0,SUC 1,3} = T
+\end{verbatim}
+}
+\noindent The result is {\small\verb%T%} because {\small\verb%num_EQ_CONV%} is able to prove that {\small\verb%2%} is
+equal to {\small\verb%SUC 1%}. An example of a negative result is:
+{\par\samepage\setseps\small
+\begin{verbatim}
+   #IN_CONV num_EQ_CONV "1 IN {0,2,3}";;
+   |- 1 IN {0,2,3} = F
+\end{verbatim}
+}
+\noindent Finally the behaviour of the supplied conversion is irrelevant when
+the value to be tested for membership is alpha-equivalent to an actual element:
+{\par\samepage\setseps\small
+\begin{verbatim}
+   #IN_CONV NO_CONV "1 IN {3,2,1}";;
+   |- 1 IN {3,2,1} = T
+\end{verbatim}
+}
+\noindent The conversion {\small\verb%NO_CONV%} always fails, but {\small\verb%IN_CONV%} is nontheless
+able in this case to prove the required result.
+
+\FAILURE
+{\small\verb%IN_CONV conv%} fails if applied to a term that is not of the form {\small\verb%"t IN
+{t1,...,tn}"%}.  A call {\small\verb%IN_CONV conv "t IN {t1,...,tn}"%} fails unless the
+term {\small\verb%t%} is alpha-equivalent to some {\small\verb%ti%}, or {\small\verb%conv "t = ti"%} returns
+{\small\verb%|- (t = ti) = T%} for some {\small\verb%ti%}, or {\small\verb%conv "t = ti"%} returns
+{\small\verb%|- (t = ti) = F%} for every {\small\verb%ti%}.
+
+\ENDDOC
+
 \DOC{INSERT\_CONV}
 
 \TYPE {\small\verb%INSERT_CONV : conv -> conv%}\egroup
@@ -257,84 +332,6 @@
 
 \ENDDOC
 
-\DOC{IN\_CONV}
-
-\TYPE {\small\verb%IN_CONV : conv -> conv%}\egroup
-
-\SYNOPSIS
-Decision procedure for membership in finite sets.
-
-\DESCRIBE 
-The function {\small\verb%IN_CONV%} is a parameterized conversion for proving or disproving
-membership assertions of the general form:
-{\par\samepage\setseps\small
-\begin{verbatim}
-   "t IN {t1,...,tn}"
-\end{verbatim}
-}
-\noindent where {\small\verb%{t1,...,tn}%} is a set of type {\small\verb%(ty)set%} and {\small\verb%t%} is a value
-of the base type {\small\verb%ty%}.  The first argument to {\small\verb%IN_CONV%} is expected to be a
-conversion that decides equality between values of the base type {\small\verb%ty%}.  Given
-an equation {\small\verb%"e1 = e2"%}, where {\small\verb%e1%} and {\small\verb%e2%} are terms of type {\small\verb%ty%}, this
-conversion should return the theorem {\small\verb%|- (e1 = e2) = T%} or the theorem
-{\small\verb%|- (e1 = e2) = F%}, as appropriate.
-
-Given such a conversion, the function {\small\verb%IN_CONV%} returns a conversion that
-maps a term of the form {\small\verb%"t IN {t1,...,tn}"%} to the theorem
-{\par\samepage\setseps\small
-\begin{verbatim}
-   |- t IN {t1,...,tn} = T
-\end{verbatim}
-}
-
-\noindent if {\small\verb%t%} is alpha-equivalent to any {\small\verb%ti%}, or if the supplied conversion
-proves {\small\verb%|- (t = ti) = T%} for any {\small\verb%ti%}. If the supplied conversion proves
-{\small\verb%|- (t = ti) = F%} for every {\small\verb%ti%}, then the result is the theorem
-{\par\samepage\setseps\small
-\begin{verbatim}
-   |- t IN {t1,...,tn} = F 
-\end{verbatim}
-}
-\noindent In all other cases, {\small\verb%IN_CONV%} will fail.
-
-\EXAMPLE
-In the following example, the conversion {\small\verb%num_EQ_CONV%} is supplied as a
-parameter and used to test equality of the candidate element {\small\verb%1%} with the
-actual elements of the given set.
-{\par\samepage\setseps\small
-\begin{verbatim}
-   #IN_CONV num_EQ_CONV "2 IN {0,SUC 1,3}";;
-   |- 2 IN {0,SUC 1,3} = T
-\end{verbatim}
-}
-\noindent The result is {\small\verb%T%} because {\small\verb%num_EQ_CONV%} is able to prove that {\small\verb%2%} is
-equal to {\small\verb%SUC 1%}. An example of a negative result is:
-{\par\samepage\setseps\small
-\begin{verbatim}
-   #IN_CONV num_EQ_CONV "1 IN {0,2,3}";;
-   |- 1 IN {0,2,3} = F
-\end{verbatim}
-}
-\noindent Finally the behaviour of the supplied conversion is irrelevant when
-the value to be tested for membership is alpha-equivalent to an actual element:
-{\par\samepage\setseps\small
-\begin{verbatim}
-   #IN_CONV NO_CONV "1 IN {3,2,1}";;
-   |- 1 IN {3,2,1} = T
-\end{verbatim}
-}
-\noindent The conversion {\small\verb%NO_CONV%} always fails, but {\small\verb%IN_CONV%} is nontheless
-able in this case to prove the required result.
-
-\FAILURE
-{\small\verb%IN_CONV conv%} fails if applied to a term that is not of the form {\small\verb%"t IN
-{t1,...,tn}"%}.  A call {\small\verb%IN_CONV conv "t IN {t1,...,tn}"%} fails unless the
-term {\small\verb%t%} is alpha-equivalent to some {\small\verb%ti%}, or {\small\verb%conv "t = ti"%} returns
-{\small\verb%|- (t = ti) = T%} for some {\small\verb%ti%}, or {\small\verb%conv "t = ti"%} returns
-{\small\verb%|- (t = ti) = F%} for every {\small\verb%ti%}.
-
-\ENDDOC
-
 \DOC{SET\_INDUCT\_TAC}
 
 \TYPE {\small\verb%SET_INDUCT_TAC : tactic%}\egroup