1\DOC STRIP_THM_THEN 2 3\TYPE {STRIP_THM_THEN : thm_tactical} 4 5\SYNOPSIS 6{STRIP_THM_THEN} applies the given theorem-tactic using the result of 7stripping off one outer connective from the given theorem. 8 9\KEYWORDS 10theorem-tactic. 11 12\DESCRIBE 13Given a theorem-tactic {ttac}, a theorem {th} whose conclusion is a 14conjunction, a disjunction or an existentially quantified term, and a goal 15{(A,t)}, {STRIP_THM_THEN ttac th} first strips apart the conclusion of {th}, 16next applies {ttac} to the theorem(s) resulting from the stripping and then 17applies the resulting tactic to the goal. 18 19In particular, when stripping a conjunctive theorem {A'|- u /\ v}, the tactic 20{ 21 ttac(u|-u) THEN ttac(v|-v) 22} 23resulting from applying {ttac} to the conjuncts, is applied to the 24goal. When stripping a disjunctive theorem {A'|- u \/ v}, the tactics 25resulting from applying {ttac} to the disjuncts, are applied to split the goal 26into two cases. That is, if 27{ 28 A ?- t A ?- t 29 ========= ttac (u|-u) and ========= ttac (v|-v) 30 A ?- t1 A ?- t2 31} 32then: 33{ 34 A ?- t 35 ================== STRIP_THM_THEN ttac (A'|- u \/ v) 36 A ?- t1 A ?- t2 37} 38When stripping an existentially quantified theorem {A'|- ?x.u}, the 39tactic {ttac(u|-u)}, resulting from applying {ttac} to the body of the 40existential quantification, is applied to the goal. That is, if: 41{ 42 A ?- t 43 ========= ttac (u|-u) 44 A ?- t1 45} 46then: 47{ 48 A ?- t 49 ============= STRIP_THM_THEN ttac (A'|- ?x. u) 50 A ?- t1 51} 52 53The assumptions of the theorem being split are not added to the assumptions of 54the goal(s) but are recorded in the proof. If {A'} is not a subset of the 55assumptions {A} of the goal (up to alpha-conversion), {STRIP_THM_THEN ttac th} 56results in an invalid tactic. 57 58\FAILURE 59{STRIP_THM_THEN ttac th} fails if the conclusion of {th} is not a conjunction, 60a disjunction or an existentially quantified term. Failure also occurs if the 61application of {ttac} fails, after stripping the outer connective from the 62conclusion of {th}. 63 64\USES 65{STRIP_THM_THEN} is used enrich the assumptions of a goal with a stripped 66version of a previously-proved theorem. 67 68\SEEALSO 69Thm_cont.CHOOSE_THEN, Thm_cont.CONJUNCTS_THEN, Thm_cont.DISJ_CASES_THEN, Tactic.STRIP_ASSUME_TAC. 70\ENDDOC 71