PSELECT_ELIM

PairRules.PSELECT_ELIM : thm -> term * thm -> thm

Eliminates a paired epsilon term, using deduction from a particular instance.

PSELECT_ELIM expects two arguments, a theorem th1, and a pair (p,th2): term * thm. The conclusion of th1 must have the form P($@ P), which asserts that the epsilon term $@ P denotes some value at which P holds. The paired variable structure p appears only in the assumption P p of the theorem th2. The conclusion of the resulting theorem matches that of th2, and the hypotheses include the union of all hypotheses of the premises excepting P p.

    A1 |- P($@ P)     A2 u {P p} |- t
   -------------------------------------  PSELECT_ELIM th1 (p ,th2)
              A1 u A2 |- t

where p is not free in A2. If p appears in the conclusion of th2, the epsilon term will NOT be eliminated, and the conclusion will be t[$@ P/p].

Failure

Fails if the first theorem is not of the form A1 |- P($@ P), or if any of the variables from the variable structure p occur free in any other assumption of th2.

See also

Drule.SELECT_ELIM, PairRules.PCHOOSE, PairRules.PSELECT_CONV, PairRules.PSELECT_INTRO, PairRules.PSELECT_RULE