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
|
\DOC FORALL_UNWIND_CONV
\TYPE {FORALL_UNWIND_CONV : term -> thm}
\SYNOPSIS
Eliminates universally quantified variables that are equated to something.
\KEYWORDS
conversion.
\DESCRIBE
The conversion {FORALL_UNWIND_CONV}, applied to a formula with one or more
universal quantifiers around an implication, eliminates any quantifiers where
the antecedent of the implication contains a conjunct equating its variable to
some other term (with that variable not free in it).
\FAILURE
{FORALL_UNWIND_CONV tm} fails if {tm} is not reducible according to that
description.
\EXAMPLE
{
# FORALL_UNWIND_CONV
`!a b c d. a + 1 = b /\ b + 1 = c + 1 /\ d = e ==> a + b + c + d + e = 2`;;
val it : thm =
|- (!a b c d.
a + 1 = b /\ b + 1 = c + 1 /\ d = e ==> a + b + c + d + e = 2) <=>
(!a c. (a + 1) + 1 = c + 1 ==> a + (a + 1) + c + e + e = 2)
# FORALL_UNWIND_CONV `!a b c. a = b /\ b = c ==> a + b = b + c`;;
val it : thm =
|- (!a b c. a = b /\ b = c ==> a + b = b + c) <=> (!c. c + c = c + c)
}
\SEEALSO
UNWIND_CONV.
\ENDDOC
|
