PairRules.PSTRIP_THM

Given a theorem-tactic ttac, a theorem th whose conclusion is a conjunction, a disjunction or a paired existentially quantified term, and a goal (A,t), STRIP_THM_THEN ttac th first strips apart the conclusion of th, next applies ttac to the theorem(s) resulting from the stripping and then applies the resulting tactic to the goal.

In particular, when stripping a conjunctive theorem A'|- u /\ v, the tactic

   ttac(u|-u) THEN ttac(v|-v)

resulting from applying ttac to the conjuncts, is applied to the goal. When stripping a disjunctive theorem A'|- u \/ v, the tactics resulting from applying ttac to the disjuncts, are applied to split the goal into two cases. That is, if

    A ?- t                           A ?- t
   =========  ttac (u|-u)    and    =========  ttac (v|-v)
    A ?- t1                          A ?- t2

then:

         A ?- t
   ================== PSTRIP_THM_THEN ttac (A'|- u \/ v)
    A ?- t1  A ?- t2

When stripping a paired existentially quantified theorem A'|- ?p. u, the tactic resulting from applying ttac to the body of the paired existential quantification, ttac(u|-u), is applied to the goal. That is, if:

    A ?- t
   =========  ttac (u|-u)
    A ?- t1

then:

      A ?- t
   =============  PSTRIP_THM_THEN ttac (A'|- ?p. u)
      A ?- t1

The assumptions of the theorem being split are not added to the assumptions of the goal(s) but are recorded in the proof. If A' is not a subset of the assumptions A of the goal (up to alpha-conversion), PSTRIP_THM_THEN ttac th results in an invalid tactic.