IN_CONV : conv -> conv

- STRUCTURE
- SYNOPSIS
- Decision procedure for membership in finite sets.
- LIBRARY
- pred_set
- DESCRIPTION
- The function IN_CONV is a parameterized conversion for proving or disproving membership assertions of the general form:where {t1;...;tn} is a set of type ty->bool and t is a value of the base type ty. The first argument to IN_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.
t IN {t1,...,tn}

Given such a conversion, the function IN_CONV returns a conversion that maps a term of the form t IN {t1;...;tn} to the theorem

|- t IN {t1;...;tn} = T

if t is alpha-equivalent to any ti, or if the supplied conversion proves |- (t = ti) = T for any ti. If the supplied conversion proves |- (t = ti) = F for every ti, then the result is the theorem

In all other cases, IN_CONV will fail.|- t IN {t1;...;tn} = F

- EXAMPLE
- In the following example, the conversion REDUCE_CONV is supplied as a parameter and used to test equality of the candidate element 1 with the actual elements of the given set.The result is T because REDUCE_CONV is able to prove that 2 is equal to SUC 1. An example of a negative result is:
- IN_CONV REDUCE_CONV ``2 IN {0;SUC 1;3}``; > val it = |- 2 IN {0; SUC 1; 3} = T : thm

Finally the behaviour of the supplied conversion is irrelevant when the value to be tested for membership is alpha-equivalent to an actual element:- IN_CONV REDUCE_CONV ``1 IN {0;2;3}``; > val it = |- 1 IN {0; 2; 3} = F : thm

The conversion NO_CONV always fails, but IN_CONV is nontheless able in this case to prove the required result.- IN_CONV NO_CONV ``1 IN {3;2;1}``; > val it = |- 1 IN {3; 2; 1} = T : thm

- FAILURE
- IN_CONV conv fails if applied to a term that is not of the form t IN {t1;...;tn}. A call IN_CONV conv t IN {t1;...;tn} fails unless the term t is alpha-equivalent to some ti, or conv ``t = ti`` returns |- (t = ti) = T for some ti, or conv ``t = ti`` returns |- (t = ti) = F for every ti.
- SEEALSO

HOL Kananaskis-14