1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
\DOC UNION_CONV
\TYPE {UNION_CONV : conv -> conv}
\SYNOPSIS
Reduce {{{t1,...,tn}} UNION s} to {t1 INSERT (... (tn INSERT s))}.
\LIBRARY sets
\DESCRIBE
The function {UNION_CONV} is a parameterized conversion for reducing sets of
the form {"{{t1,...,tn}} UNION s"}, where {{{t1,...,tn}}} and {s} are sets of
type {(ty)set}. The first argument to {UNION_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, the function {UNION_CONV} returns a conversion that
maps a term of the form {"{{t1,...,tn}} UNION s"} to the theorem
{
|- t UNION {{t1,...,tn}} = ti INSERT ... (tj INSERT s)
}
\noindent where {{{ti,...,tj}}} is the set of all terms {t} that occur as
elements of {{{t1,...,tn}}} for which the conversion {IN_CONV conv} fails to
prove that {|- (t IN s) = T} (that is, either by proving {|- (t IN s) = F}
instead, or by failing outright).
\EXAMPLE
In the following example, {num_EQ_CONV} is supplied as a parameter to
{UNION_CONV} and used to test for membership of each element of the first
finite set {{{1,2,3}}} of the union in the second finite set {{{SUC 0,3,4}}}.
{
#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}}
}
\noindent The result is {{{2,SUC 0,3,4}}}, rather than {{{1,2,SUC 0,3,4}}},
because {UNION_CONV} is able by means of a call to
{
IN_CONV num_EQ_CONV "1 IN {{SUC 0,3,4}}"
}
\noindent to prove that {1} is already an element of the set {{{SUC 0,3,4}}}.
The conversion supplied to {UNION_CONV} need not actually prove equality of
elements, if simplification of the resulting set is not desired. For example:
{
#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}}
}
\noindent In this case, the resulting set is just left unsimplified. Moreover,
the second set argument to {UNION} need not be a finite set:
{
#UNION_CONV NO_CONV "{{1,2,3}} UNION s";;
|- {{1,2,3}} UNION s = 1 INSERT (2 INSERT (3 INSERT s))
}
\noindent And, of course, in this case the conversion argument to {UNION_CONV}
is irrelevant.
\FAILURE
{UNION_CONV conv} fails if applied to a term not of the form
{"{{t1,...,tn}} UNION s"}.
\SEEALSO
IN_CONV.
\ENDDOC
|
