DELETE_CONVpred_setLib.DELETE_CONV : conv -> convReduce {t1;...;tn} DELETE t by deleting t
from {t1;...;tn}.
The function DELETE_CONV is a parameterized conversion
for reducing finite sets of the form {t1;...;tn} DELETE t,
where the term t and the elements of
{t1;...;tn} are of some base type ty. The
first argument to DELETE_CONV is expected to be a
conversion that decides equality between values of the base type
ty. Given an equation e1 = e2, where
e1 and e2 are terms of type ty,
this conversion should return the theorem |- (e1 = e2) = T
or the theorem |- (e1 = e2) = F, as appropriate.
Given such a conversion conv, the function
DELETE_CONV returns a conversion that maps a term of the
form {t1;...;tn} DELETE t to the theorem
|- {t1;...;tn} DELETE t = {ti;...;tj}where {ti;...;tj} is the subset of
{t1;...;tn} for which the supplied equality conversion
conv proves
|- (ti = t) = F, ..., |- (tj = t) = Fand for all the elements tk in {t1;...;tn}
but not in {ti;...;tj}, either conv proves
|- (tk = t) = T or tk is alpha-equivalent to
t. That is, the reduced set {ti;...;tj}
comprises all those elements of the original set that are provably not
equal to the deleted element t.
In the following example, the conversion REDUCE_CONV is
supplied as a parameter and used to test equality of the deleted value
2 with the elements of the set.
- DELETE_CONV REDUCE_CONV ``{2; 1; SUC 1; 3} DELETE 2``;
> val it = |- {2; 1; SUC 1; 3} DELETE 2 = {1; 3} : thm’
DELETE_CONV conv fails if applied to a term not of the
form {t1;...;tn} DELETE t. A call
DELETE_CONV conv ``{t1;...;tn} DELETE t`` fails unless for
each element ti of the set {t1;...;tn}, the
term t is either alpha-equivalent to ti or
conv ``ti = t`` returns |- (ti = t) = T or
|- (ti = t) = F.