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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
\DOC X_CASES_THEN
\TYPE {X_CASES_THEN : (term list list -> thm_tactical)}
\SYNOPSIS
Applies a theorem-tactic to all disjuncts of a theorem, choosing witnesses.
\KEYWORDS
theorem-tactic, cases, disjunction, quantifier, existential.
\DESCRIBE
Let {[yl1;...;yln]} represent a list of variable lists,
each of length zero or more, and {xl1,...,xln} each represent a
vector of zero or more variables, so that the variables in each of
{yl1...yln} have the same types as the corresponding {xli}.
{X_CASES_THEN} expects such a list of variable lists, {[yl1;...;yln]}, a tactic
generating function {f:thm->tactic}, and a disjunctive theorem,
where each disjunct may be existentially quantified:
{
th = |-(?xl1.B1) \/...\/ (?xln.Bn)
}
\noindent each disjunct having the form {(?xi1 ... xim. Bi)}. If
applying {f} to the theorem obtained by introducing witness variables {yli}
for the objects {xli} whose existence is asserted by each disjunct, typically
{({{Bi[yli/xli]}} |- Bi[yli/xli])}, produce the following results when
applied to a goal {(A ?- t)}:
{
A ?- t
========= f ({{B1[yl1/xl1]}} |- B1[yl1/xl1])
A ?- t1
...
A ?- t
========= f ({{Bn[yln/xln]}} |- Bn[yln/xln])
A ?- tn
}
\noindent then applying {(X_CHOOSE_THEN [yl1;...;yln] f th)}
to the goal {(A ?- t)} produces {n} subgoals.
{
A ?- t
======================= X_CHOOSE_THEN [yl1;...;yln] f th
A ?- t1 ... A ?- tn
}
\FAILURE
Fails (with {X_CHOOSE_THEN}) if any {yli} has more variables than the
corresponding {xli}, or (with {SUBST}) if corresponding variables have
different types. Failures may arise in the tactic-generating
function. An invalid tactic is produced if any variable in any of the
{yli} is free in the corresponding {Bi} or in {t}, or if the theorem
has any hypothesis which is not alpha-convertible to an assumption of
the goal.
\EXAMPLE
Given the goal {?- (x MOD 2) <= 1}, the following theorem may be
used to split into 2 cases:
{
th = |- (?m. x = 2 * m) \/ (?m. x = (2 * m) + 1)
}
\noindent by the tactic {X_CASES_THEN [["n:num"];["n:num"]] ASSUME_TAC th}
to produce the subgoals:
{
{{x = (2 * n) + 1}} ?- (x MOD 2) <= 1
{{x = 2 * n}} ?- (x MOD 2) <= 1
}
\SEEALSO
DISJ_CASES_THENL, X_CASES_THENL, X_CHOOSE_THEN.
\ENDDOC
|
