PairRules.FILTER_PSTRIP

STRUCTURE

LIBRARY

pair

SYNOPSIS

Conditionally strips a goal, handing an antecedent to the theorem-tactic.

DESCRIPTION

Given a theorem-tactic ttac, a term u and a goal (A,t), FILTER_STRIP_THEN ttac u removes one outer connective (!, ==>, or ~) from t, if the term being stripped does not contain a free instance of u. Note that FILTER_PSTRIP_THEN will strip paired universal quantifiers. A negation ~t is treated as the implication t ==> F. The theorem-tactic ttac is applied only when stripping an implication, by using the antecedent stripped off. FILTER_PSTRIP_THEN also breaks conjunctions.

FILTER_PSTRIP_THEN behaves like PSTRIP_GOAL_THEN, if the term being stripped does not contain a free instance of u. In particular, FILTER_PSTRIP_THEN PSTRIP_ASSUME_TAC behaves like FILTER_PSTRIP_TAC.

FAILURE

FILTER_PSTRIP_THEN ttac u (A,t) fails if t is not a paired universally quantified term, an implication, a negation or a conjunction; or if the term being stripped contains the term u (conjunction excluded); or if the application of ttac fails, after stripping the goal.

USES

FILTER_PSTRIP_THEN is used to manipulate intermediate results using theorem-tactics, after stripping outer connectives from a goal in a more delicate way than PSTRIP_GOAL_THEN.

SEEALSO

PGEN_TAC, PSTRIP_GOAL_THEN, FILTER_STRIP_THEN, PSTRIP_TAC, FILTER_PSTRIP_TAC