EXISTS_LEFT1
Drule.EXISTS_LEFT1 : term -> thm -> thm
Existentially quantifes hypotheses of a theorem.
In this example, assume that h1 and h3 (only) involve the free
variable x.
h1, h2, h3 |- t
--------------------- EXISTS_LEFT1 ``x``
?x. h1 /\ h3, h2 |- t
Failure
EXISTS_LEFT1 will fail unless the term supplied is a free variable
which appears in one or more hypotheses but not the conclusion of the
given theorem
Example
Where th is [p, q, g x, h y, f x y] |- r, and fvx and fvy are
``x`` and ``y``,
EXISTS_LEFT1 fvx th is [p, q, h y, ?x. g x /\ f x y] |- r
EXISTS_LEFT1 fvy th is [p, q, g x, ?y. h y /\ f x y] |- r
Comments
EXISTS_LEFT1 fv is just like EXISTS_LEFT [fv] except that
EXISTS_LEFT1 fv fails where EXISTS_LEFT [fv] returns the theorem
unchanged
See EXISTS_LEFT for further discussion
See also
Drule.EXISTS_LEFT, Thm.CHOOSE,
Thm.EXISTS, Tactic.CHOOSE_TAC,
Tactic.EXISTS_TAC