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
|
\DOC LIST_MK_EXISTS
\TYPE {LIST_MK_EXISTS : (term list -> thm -> thm)}
\SYNOPSIS
Multiply existentially quantifies both sides of an equation using the given
variables.
\KEYWORDS
rule, quantifier, existential.
\DESCRIBE
When applied to a list of terms {[x1;...;xn]}, where the {ti} are all
variables, and a theorem {A |- t1 = t2}, the inference rule
{LIST_MK_EXISTS} existentially quantifies both sides of the equation
using the variables given, none of which should be free in the assumption
list.
{
A |- t1 = t2
-------------------------------------- LIST_MK_EXISTS ["x1";...;"xn"]
A |- (?x1...xn. t1) = (?x1...xn. t2)
}
\FAILURE
Fails if any term in the list is not a variable or is free in the assumption
list, or if the theorem is not equational.
\SEEALSO
EXISTS_EQ, MK_EXISTS.
\ENDDOC
|
