FORALL_UNWIND_CONV : term -> thm

SYNOPSIS

Eliminates universally quantified variables that are equated to something.

DESCRIPTION

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 CONDITIONS

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)

SEE ALSO

UNWIND_CONV.