1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
\DOC CASES_THENL
\TYPE {CASES_THENL : (thm_tactic list -> thm_tactic)}
\SYNOPSIS
Applies the theorem-tactics in a list to corresponding disjuncts in a theorem.
\KEYWORDS
theorem-tactic, cases.
\DESCRIBE
When given a list of theorem-tactics {[ttac1;...;ttacn]} and a theorem whose
conclusion is a top-level disjunction of {n} terms, {CASES_THENL} splits a goal
into {n} subgoals resulting from applying to the original goal the result of
applying the {i}'th theorem-tactic to the {i}'th disjunct. This can be
represented as follows, where the number of existentially quantified variables
in a disjunct may be zero. If the theorem {th} has the form:
{
A' |- ?x11..x1m. t1 \/ ... \/ ?xn1..xnp. tn
}
\noindent where the number of existential quantifiers may be zero,
and for all {i} from {1} to {n}:
{
A ?- s
========== ttaci (|- ti[xi1'/xi1]..[xim'/xim])
Ai ?- si
}
\noindent where the primed variables have the same type as their unprimed
counterparts, then:
{
A ?- s
========================= CASES_THENL [ttac1;...;ttacn] th
A1 ?- s1 ... An ?- sn
}
\noindent Unless {A'} is a subset of {A}, this is an invalid tactic.
\FAILURE
Fails if the given theorem does not, at the top level,
have the same number of (possibly multiply existentially quantified) disjuncts
as the length of the theorem-tactic list (this includes the case where the
theorem-tactic list is empty), or if any of the tactics generated as specified
above fail when applied to the goal.
\USES
Performing very general disjunctive case splits.
\SEEALSO
DISJ_CASES_THENL, X_CASES_THENL.
\ENDDOC
|
