PSTRIP_TAC
PairRules.PSTRIP_TAC : tactic
Splits a goal by eliminating one outermost connective.
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.
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.
See also
PairRules.PGEN_TAC,
PairRules.PSTRIP_GOAL_THEN,
PairRules.FILTER_PSTRIP_THEN,
Tactic.STRIP_TAC,
PairRules.FILTER_PSTRIP_TAC