MK_EXISTS : term -> thm -> thm
Existentially quantifies both sides of equational theorem.
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.
# 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))
- SEE ALSO
AP_TERM, AP_THM, MK_BINOP, MK_COMB, MK_CONJ, MK_DISJ, MK_FORALL.