----------------------------------------------------------------------
PSTRIP_TAC                                                 (PairRules)
----------------------------------------------------------------------
PSTRIP_TAC : tactic

KEYWORDS
tactic.

LIBRARY
pair

SYNOPSIS
Splits a goal by eliminating one outermost connective.

DESCRIBE
Given a goal {(A,t)}, {PSTRIP_TAC} removes one outermost occurrence of one of
the connectives {!}, {==>}, {~} or {/\} from the conclusion of the goal {t}.
If {t} is a universally quantified term, then {STRIP_TAC} strips off the
quantifier. Note that {PSTRIP_TAC} will strip off paired quantifications.

     A ?- !p. u
   ==============  PSTRIP_TAC
    A ?- u[p'/p]

where {p'} is a primed variant of the pair {p} that does not contain
any variables that appear free in the assumptions {A}.  If {t} is a
conjunction, then {PSTRIP_TAC} simply splits the conjunction into two subgoals:

      A ?- v /\ w
   =================  PSTRIP_TAC
    A ?- v   A ?- w

If {t} is an implication, {PSTRIP_TAC} moves the antecedent into the
assumptions, stripping conjunctions, disjunctions and existential
quantifiers according to the following rules:

    A ?- v1 /\ ... /\ vn ==> v            A ?- v1 \/ ... \/ vn ==> v
   ============================        =================================
       A u {v1,...,vn} ?- v             A u {v1} ?- v ... A u {vn} ?- v

     A ?- (?p. w) ==> v
   =====================
    A u {w[p'/p]} ?- v

where {p'} is a primed variant of the pair {p} that does not appear
free in {A}. Finally, a negation {~t} is treated as the implication {t ==> F}.

FAILURE
{PSTRIP_TAC (A,t)} fails if {t} is not a paired universally quantified term,
an implication, a negation or a conjunction.

USES
When trying to solve a goal, often the best thing to do first
is {REPEAT PSTRIP_TAC} to split the goal up into manageable pieces.

SEEALSO
PairRules.PGEN_TAC, PairRules.PSTRIP_GOAL_THEN,
PairRules.FILTER_PSTRIP_THEN, Tactic.STRIP_TAC,
PairRules.FILTER_PSTRIP_TAC.

----------------------------------------------------------------------