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