## File: entries.tex

package info (click to toggle)
hol88 2.02.19940316-35
 123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524 \chapter{ML Functions in the Library}\label{entries}\input{entries-intro}\DOC{DELETE\_CONV} \TYPE {\small\verb%DELETE_CONV : conv -> conv%}\egroup \SYNOPSIS Reduce {\small\verb%{x1,...,xn} DELETE x%} by deleting {\small\verb%x%} from {\small\verb%{x1,...,xn}%}. \DESCRIBE The function {\small\verb%DELETE_CONV%} is a parameterized conversion for reducing finite sets of the form {\small\verb%"{t1,...,tn} DELETE t"%}, where the term {\small\verb%t%} and the elements of {\small\verb%{t1,...,tn}%} are of some base type {\small\verb%ty%}. The first argument to {\small\verb%DELETE_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 {\small\verb%conv%}, the function {\small\verb%DELETE_CONV%} returns a conversion that maps a term of the form {\small\verb%"{t1,...,tn} DELETE t"%} to the theorem {\par\samepage\setseps\small \begin{verbatim} |- {t1,...,tn} DELETE t = {ti,...,tj} \end{verbatim} } \noindent where {\small\verb%{ti,...,tj}%} is the subset of {\small\verb%{t1,...,tn}%} for which the supplied equality conversion {\small\verb%conv%} proves {\par\samepage\setseps\small \begin{verbatim} |- (ti = t) = F, ..., |- (tj = t) = F \end{verbatim} } \noindent and for all the elements {\small\verb%tk%} in {\small\verb%{t1,...,tn}%} but not in {\small\verb%{ti,...,tj}%}, either {\small\verb%conv%} proves {\small\verb%|- (tk = t) = T%} or {\small\verb%tk%} is alpha-equivalent to {\small\verb%t%}. That is, the reduced set {\small\verb%{ti,...,tj}%} comprises all those elements of the original set that are provably not equal to the deleted element {\small\verb%t%}. \EXAMPLE In the following example, the conversion {\small\verb%num_EQ_CONV%} is supplied as a parameter and used to test equality of the deleted value {\small\verb%2%} with the elements of the set. {\par\samepage\setseps\small \begin{verbatim} #DELETE_CONV num_EQ_CONV "{2,1,SUC 1,3} DELETE 2";; |- {2,1,SUC 1,3} DELETE 2 = {1,3} \end{verbatim} } \FAILURE {\small\verb%DELETE_CONV conv%} fails if applied to a term not of the form {\small\verb%"{t1,...,tn} DELETE t"%}. A call {\small\verb%DELETE_CONV conv "{t1,...,tn} DELETE t"%} fails unless for each element {\small\verb%ti%} of the set {\small\verb%{t1,...,tn}%}, the term {\small\verb%t%} is either alpha-equivalent to {\small\verb%ti%} or {\small\verb%conv "ti = t"%} returns {\small\verb%|- (ti = t) = T%} or {\small\verb%|- (ti = t) = F%}. \SEEALSO INSERT_CONV. \ENDDOC \DOC{FINITE\_CONV} \TYPE {\small\verb%FINITE_CONV : conv%}\egroup \SYNOPSIS Proves finiteness of sets of the form {\small\verb%"{x1,...,xn}"%}. \DESCRIBE The conversion {\small\verb%FINITE_CONV%} expects its term argument to be an assertion of the form {\small\verb%"FINITE {x1,...,xn}"%}. Given such a term, the conversion returns the theorem {\par\samepage\setseps\small \begin{verbatim} |- FINITE {x1,...,xn} = T \end{verbatim} } \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #FINITE_CONV "FINITE {1,2,3}";; |- FINITE{1,2,3} = T #FINITE_CONV "FINITE ({}:num->bool)";; |- FINITE{} = T \end{verbatim} } \FAILURE Fails if applied to a term not of the form {\small\verb%"FINITE {x1,...,xn}"%}. \ENDDOC \DOC{IMAGE\_CONV} \TYPE {\small\verb%IMAGE_CONV : conv -> conv -> conv%}\egroup \SYNOPSIS Compute the image of a function on a finite set. \DESCRIBE The function {\small\verb%IMAGE_CONV%} is a parameterized conversion for computing the image of a function {\small\verb%f:ty1->ty2%} on a finite set {\small\verb%"{t1,...,tn}"%} of type {\small\verb%ty1->bool%}. The first argument to {\small\verb%IMAGE_CONV%} is expected to be a conversion that computes the result of applying the function {\small\verb%f%} to each element of this set. When applied to a term {\small\verb%"f ti"%}, this conversion should return a theorem of the form {\small\verb%|- (f ti) = ri%}, where {\small\verb%ri%} is the result of applying the function {\small\verb%f%} to the element {\small\verb%ti%}. This conversion is used by {\small\verb%IMAGE_CONV%} to compute a theorem of the form {\par\samepage\setseps\small \begin{verbatim} |- IMAGE f {t1,...,tn} = {r1,...,rn} \end{verbatim} } \noindent The second argument to {\small\verb%IMAGE_CONV%} is used (optionally) to simplify the resulting image set {\small\verb%{r1,...,rn}%} by removing redundant occurrences of values. This conversion expected to decide equality of values of the result type {\small\verb%ty2%}; given an equation {\small\verb%"e1 = e2"%}, where {\small\verb%e1%} and {\small\verb%e2%} are terms of type {\small\verb%ty2%}, the conversion should return either {\small\verb%|- (e1 = e2) = T%} or {\small\verb%|- (e1 = e2) = F%}, as appropriate. Given appropriate conversions {\small\verb%conv1%} and {\small\verb%conv2%}, the function {\small\verb%IMAGE_CONV%} returns a conversion that maps a term of the form {\small\verb%"IMAGE f {t1,...,tn}"%} to the theorem {\par\samepage\setseps\small \begin{verbatim} |- IMAGE f {t1,...,tn} = {rj,...,rk} \end{verbatim} } \noindent where {\small\verb%conv1%} proves a theorem of the form {\small\verb%|- (f ti) = ri%} for each element {\small\verb%ti%} of the set {\small\verb%{t1,...,tn}%}, and where the set {\small\verb%{rj,...,rk}%} is the smallest subset of {\small\verb%{r1,...,rn}%} such no two elements are alpha-equivalent and {\small\verb%conv2%} does not map {\small\verb%"rl = rm"%} to the theorem {\small\verb%|- (rl = rm) = T%} for any pair of values {\small\verb%rl%} and {\small\verb%rm%} in {\small\verb%{rj,...,rk}%}. That is, {\small\verb%{rj,...,rk}%} is the set obtained by removing multiple occurrences of values from the set {\small\verb%{r1,...,rn}%}, where the equality conversion {\small\verb%conv2%} (or alpha-equivalence) is used to determine which pairs of terms in {\small\verb%{r1,...,rn}%} are equal. \EXAMPLE The following is a very simple example in which {\small\verb%REFL%} is used to construct the result of applying the function {\small\verb%f%} to each element of the set {\small\verb%{1,2,1,4}%}, and {\small\verb%NO_CONV%} is the supplied equality conversion'. {\par\samepage\setseps\small \begin{verbatim} #IMAGE_CONV REFL NO_CONV "IMAGE (f:num->num) {1,2,1,4}";; |- IMAGE f{1,2,1,4} = {f 2,f 1,f 4} \end{verbatim} } \noindent The result contains only one occurrence of {\small\verb%f 1%}', even though {\small\verb%NO_CONV%} always fails, since {\small\verb%IMAGE_CONV%} simplifies the resulting set by removing elements that are redundant up to alpha-equivalence. For the next example, we construct a conversion that maps {\small\verb%SUC n%} for any numeral {\small\verb%n%} to the numeral standing for the successor of {\small\verb%n%}. {\par\samepage\setseps\small \begin{verbatim} #let SUC_CONV tm = let n = int_of_string(fst(dest_const(rand tm))) in let sucn = mk_const(string_of_int(n+1), ":num") in SYM (num_CONV sucn);; SUC_CONV = - : conv \end{verbatim} } \noindent The result is a conversion that inverts {\small\verb%num_CONV%}: {\par\samepage\setseps\small \begin{verbatim} #num_CONV "4";; |- 4 = SUC 3 #SUC_CONV "SUC 3";; |- SUC 3 = 4 \end{verbatim} } \noindent The conversion {\small\verb%SUC_CONV%} can then be used to compute the image of the successor function on a finite set: {\par\samepage\setseps\small \begin{verbatim} #IMAGE_CONV SUC_CONV NO_CONV "IMAGE SUC {1,2,1,4}";; |- IMAGE SUC{1,2,1,4} = {3,2,5} \end{verbatim} } \noindent Note that {\small\verb%2%} (= {\small\verb%SUC 1%}) appears only once in the resulting set. Fianlly, here is an example of using {\small\verb%IMAGE_CONV%} to compute the image of a paired addition function on a set of pairs of numbers: {\par\samepage\setseps\small \begin{verbatim} #IMAGE_CONV (PAIRED_BETA_CONV THENC ADD_CONV) num_EQ_CONV "IMAGE (\(n,m).n+m) {(1,2), (3,4), (0,3), (1,3)}";; |- IMAGE(\(n,m). n + m){(1,2),(3,4),(0,3),(1,3)} = {7,3,4} \end{verbatim} } \FAILURE {\small\verb%IMAGE_CONV conv1 conv2%} fails if applied to a term not of the form {\small\verb%"IMAGE f {t1,...,tn}"%}. An application of {\small\verb%IMAGE_CONV conv1 conv2%} to a term {\small\verb%"IMAGE f {t1,...,tn}"%} fails unless for all {\small\verb%ti%} in the set {\small\verb%{t1,...,tn}%}, evaluating {\small\verb%conv1 "f ti"%} returns {\small\verb%|- (f ti) = ri%} for some {\small\verb%ri%}. \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->bool%} 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 \SYNOPSIS Reduce {\small\verb%x INSERT {x1,...,x,...,xn}%} to {\small\verb%{x1,...,x,...,xn}%}. \DESCRIBE The function {\small\verb%INSERT_CONV%} is a parameterized conversion for reducing finite sets of the form {\small\verb%"t INSERT {t1,...,tn}"%}, where {\small\verb%{t1,...,tn}%} is a set of type {\small\verb%ty->bool%} and {\small\verb%t%} is equal to some element {\small\verb%ti%} of this set. The first argument to {\small\verb%INSERT_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%INSERT_CONV%} returns a conversion that maps a term of the form {\small\verb%"t INSERT {t1,...,tn}"%} to the theorem {\par\samepage\setseps\small \begin{verbatim} |- t INSERT {t1,...,tn} = {t1,...,tn} \end{verbatim} } \noindent if {\small\verb%t%} is alpha-equivalent to any {\small\verb%ti%} in the set {\small\verb%{t1,...,tn}%}, or if the supplied conversion proves {\small\verb%|- (t = ti) = T%} for any {\small\verb%ti%}. \EXAMPLE In the following example, the conversion {\small\verb%num_EQ_CONV%} is supplied as a parameter and used to test equality of the inserted value {\small\verb%2%} with the remaining elements of the set. {\par\samepage\setseps\small \begin{verbatim} #INSERT_CONV num_EQ_CONV "2 INSERT {1,SUC 1,3}";; |- {2,1,SUC 1,3} = {1,SUC 1,3} \end{verbatim} } \noindent In this example, the supplied conversion {\small\verb%num_EQ_CONV%} is able to prove that {\small\verb%2%} is equal to {\small\verb%SUC 1%} and the set is therefore reduced. Note that {\small\verb%"2 INSERT {1,SUC 1,3}"%} is just {\small\verb%"{2,1,SUC 1,3}"%}. A call to {\small\verb%INSERT_CONV%} fails when the value being inserted is provably not equal to any of the remaining elements: {\par\samepage\setseps\small \begin{verbatim} #INSERT_CONV num_EQ_CONV "1 INSERT {2,3}";; evaluation failed INSERT_CONV \end{verbatim} } \noindent But this failure can, if desired, be caught using {\small\verb%TRY_CONV%}. The behaviour of the supplied conversion is irrelevant when the inserted value is alpha-equivalent to one of the remaining elements: {\par\samepage\setseps\small \begin{verbatim} #INSERT_CONV NO_CONV "(y:*) INSERT {x,y,z}";; |- {y,x,y,z} = {x,y,z} \end{verbatim} } \noindent The conversion {\small\verb%NO_CONV%} always fails, but {\small\verb%INSERT_CONV%} is nontheless able in this case to prove the required result. Note that {\small\verb%DEPTH_CONV(INSERT_CONV conv)%} can be used to remove duplicate elements from a finite set, but the following conversion is faster: {\par\samepage\setseps\small \begin{verbatim} #letrec REDUCE_CONV conv tm = (SUB_CONV (REDUCE_CONV conv) THENC (TRY_CONV (INSERT_CONV conv))) tm;; REDUCE_CONV = - : (conv -> conv) #REDUCE_CONV num_EQ_CONV "{1,2,1,3,2,4,3,5,6}";; |- {1,2,1,3,2,4,3,5,6} = {1,2,4,3,5,6} \end{verbatim} } \FAILURE {\small\verb%INSERT_CONV conv%} fails if applied to a term not of the form {\small\verb%"t INSERT {t1,...,tn}"%}. A call {\small\verb%INSERT_CONV conv "t INSERT {t1,...,tn}"%} fails unless {\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%}. \SEEALSO DELETE_CONV. \ENDDOC \DOC{SET\_INDUCT\_TAC} \TYPE {\small\verb%SET_INDUCT_TAC : tactic%}\egroup \SYNOPSIS Tactic for induction on finite sets. \DESCRIBE {\small\verb%SET_INDUCT_TAC%} is an induction tacic for proving properties of finite sets. When applied to a goal of the form {\par\samepage\setseps\small \begin{verbatim} !s. FINITE s ==> P[s] \end{verbatim} } \noindent {\small\verb%SET_INDUCT_TAC%} reduces this goal to proving that the property {\small\verb%\s.P[s]%} holds of the empty set and is preserved by insertion of an element into an arbitrary finite set. Since every finite set can be built up from the empty set {\small\verb%"{}"%} by repeated insertion of values, these subgoals imply that the property {\small\verb%\s.P[s]%} holds of all finite sets. The tactic specification of {\small\verb%SET_INDUCT_TAC%} is: {\par\samepage\setseps\small \begin{verbatim} A ?- !s. FINITE s ==> P ========================================================== SET_INDUCT_TAC A |- P[{}/s] A u {FINITE s', P[s'/s], ~e IN s'} ?- P[e INSERT s'/s] \end{verbatim} } \noindent where {\small\verb%e%} is a variable chosen so as not to appear free in the assumptions {\small\verb%A%}, and {\small\verb%s'%} is a primed variant of {\small\verb%s%} that does not appear free in {\small\verb%A%} (usually, {\small\verb%s'%} is just {\small\verb%s%}). \FAILURE {\small\verb%SET_INDUCT_TAC (A,g)%} fails unless {\small\verb%g%} has the form {\small\verb%!s. FINITE s ==> P%}, where the variable {\small\verb%s%} has type {\small\verb%ty->bool%} for some type {\small\verb%ty%}. \ENDDOC \DOC{SET\_SPEC\_CONV} \TYPE {\small\verb%SET_SPEC_CONV : conv%}\egroup \SYNOPSIS Axiom-scheme of specification for set abstractions. \DESCRIBE The conversion {\small\verb%SET_SPEC_CONV%} expects its term argument to be an assertion of the form {\small\verb%"t IN {E | P}"%}. Given such a term, the conversion returns a theorem that defines the condition under which this membership assertion holds. When {\small\verb%E%} is just a variable {\small\verb%v%}, the conversion returns: {\par\samepage\setseps\small \begin{verbatim} |- t IN {v | P} = P[t/v] \end{verbatim} } \noindent and when {\small\verb%E%} is not a variable but some other expression, the theorem returned is: {\par\samepage\setseps\small \begin{verbatim} |- t IN {E | P} = ?x1...xn. (t = E) /\ P \end{verbatim} } \noindent where {\small\verb%x1%}, ..., {\small\verb%xn%} are the variables that occur free both in the expression {\small\verb%E%} and in the proposition {\small\verb%P%}. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #SET_SPEC_CONV "12 IN {n | n > N}";; |- 12 IN {n | n > N} = 12 > N #SET_SPEC_CONV "p IN {(n,m) | n < m}";; |- p IN {(n,m) | n < m} = (?n m. (p = n,m) /\ n < m) \end{verbatim} } \FAILURE Fails if applied to a term that is not of the form {\small\verb%"t IN {E | P}"%}. \ENDDOC \DOC{UNION\_CONV} \TYPE {\small\verb%UNION_CONV : conv -> conv%}\egroup \SYNOPSIS Reduce {\small\verb%{t1,...,tn} UNION s%} to {\small\verb%t1 INSERT (... (tn INSERT s))%}. \DESCRIBE The function {\small\verb%UNION_CONV%} is a parameterized conversion for reducing sets of the form {\small\verb%"{t1,...,tn} UNION s"%}, where {\small\verb%{t1,...,tn}%} and {\small\verb%s%} are sets of type {\small\verb%ty->bool%}. The first argument to {\small\verb%UNION_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%UNION_CONV%} returns a conversion that maps a term of the form {\small\verb%"{t1,...,tn} UNION s"%} to the theorem {\par\samepage\setseps\small \begin{verbatim} |- t UNION {t1,...,tn} = ti INSERT ... (tj INSERT s) \end{verbatim} } \noindent where {\small\verb%{ti,...,tj}%} is the set of all terms {\small\verb%t%} that occur as elements of {\small\verb%{t1,...,tn}%} for which the conversion {\small\verb%IN_CONV conv%} fails to prove that {\small\verb%|- (t IN s) = T%} (that is, either by proving {\small\verb%|- (t IN s) = F%} instead, or by failing outright). \EXAMPLE In the following example, {\small\verb%num_EQ_CONV%} is supplied as a parameter to {\small\verb%UNION_CONV%} and used to test for membership of each element of the first finite set {\small\verb%{1,2,3}%} of the union in the second finite set {\small\verb%{SUC 0,3,4}%}. {\par\samepage\setseps\small \begin{verbatim} #UNION_CONV num_EQ_CONV "{1,2,3} UNION {SUC 0,3,4}";; |- {1,2,3} UNION {SUC 0,3,4} = {2,SUC 0,3,4} \end{verbatim} } \noindent The result is {\small\verb%{2,SUC 0,3,4}%}, rather than {\small\verb%{1,2,SUC 0,3,4}%}, because {\small\verb%UNION_CONV%} is able by means of a call to {\par\samepage\setseps\small \begin{verbatim} IN_CONV num_EQ_CONV "1 IN {SUC 0,3,4}" \end{verbatim} } \noindent to prove that {\small\verb%1%} is already an element of the set {\small\verb%{SUC 0,3,4}%}. The conversion supplied to {\small\verb%UNION_CONV%} need not actually prove equality of elements, if simplification of the resulting set is not desired. For example: {\par\samepage\setseps\small \begin{verbatim} #UNION_CONV NO_CONV "{1,2,3} UNION {SUC 0,3,4}";; |- {1,2,3} UNION {SUC 0,3,4} = {1,2,SUC 0,3,4} \end{verbatim} } \noindent In this case, the resulting set is just left unsimplified. Moreover, the second set argument to {\small\verb%UNION%} need not be a finite set: {\par\samepage\setseps\small \begin{verbatim} #UNION_CONV NO_CONV "{1,2,3} UNION s";; |- {1,2,3} UNION s = 1 INSERT (2 INSERT (3 INSERT s)) \end{verbatim} } \noindent And, of course, in this case the conversion argument to {\small\verb%UNION_CONV%} is irrelevant. \FAILURE {\small\verb%UNION_CONV conv%} fails if applied to a term not of the form {\small\verb%"{t1,...,tn} UNION s"%}. \SEEALSO IN_CONV. \ENDDOC