MK_EXISTS : term -> thm -> thm

SYNOPSIS

Existentially quantifies both sides of equational theorem.

DESCRIPTION

Given a theorem th whose conclusion is a Boolean equation (iff), the rule MK_EXISTS `v` th existentially quantifies both sides of th over the variable v, provided it is not free in the hypotheses

             A |- p <=> q
      ---------------------------- MK_EXISTS `v` [where v not free in A]
        A |- (?v. p) <=> (?v. q)

FAILURE CONDITIONS

Fails if the term is not a variable or is free in the hypotheses of the theorem, or if the theorem does not have a Boolean equation for its conclusion.

EXAMPLE

  # let th = ARITH_RULE `f(x:A) >= 1 <=> ~(f(x) = 0)`;;
  val th : thm = |- f x >= 1 <=> ~(f x = 0)

  # MK_EXISTS `x:A` th;;
  val it : thm = |- (?x. f x >= 1) <=> (?x. ~(f x = 0))