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
|
\DOC STRUCT_CASES_TAC
\TYPE {STRUCT_CASES_TAC : thm_tactic}
\SYNOPSIS
Performs very general structural case analysis.
\KEYWORDS
tactic, cases.
\DESCRIBE
When it is applied to a theorem of the form:
{
th = A' |- ?y11...y1m. x = t1 /\ (B11 /\ ... /\ B1k) \/ ... \/
?yn1...ynp. x = tn /\ (Bn1 /\ ... /\ Bnp)
}
\noindent in which there may be no existential quantifiers where a `vector' of
them is shown above, {STRUCT_CASES_TAC th} splits a goal {A ?- s} into {n}
subgoals as follows:
{
A ?- s
===============================================================
A u {{B11,...,B1k}} ?- s[t1/x] ... A u {{Bn1,...,Bnp}} ?- s[tn/x]
}
\noindent that is, performs a case split over the possible constructions (the
{ti}) of a term, providing as assumptions the given constraints, having
split conjoined constraints into separate assumptions. Note that unless {A'}
is a subset of {A}, this is an invalid tactic.
\FAILURE
Fails unless the theorem has the above form, namely a conjunction of
(possibly multiply existentially quantified) terms which assert the equality
of the same variable {x} and the given terms.
\EXAMPLE
Suppose we have the goal:
{
# g `~(l:(A)list = []) ==> LENGTH l > 0`;;
}
\noindent then we can get rid of the universal quantifier from the
inbuilt list theorem {list_CASES}:
{
list_CASES = !l. l = [] \/ (?h t. l = CONS h t)
}
\noindent and then use {STRUCT_CASES_TAC}. This amounts to applying the
following tactic:
{
# e(STRUCT_CASES_TAC (SPEC_ALL list_CASES));;
val it : goalstack = 2 subgoals (2 total)
`~(CONS h t = []) ==> LENGTH (CONS h t) > 0`
`~([] = []) ==> LENGTH [] > 0`
}
\noindent and both of these are solvable by {REWRITE_TAC[GT; LENGTH; LT_0]}.
\USES
Generating a case split from the axioms specifying a structure.
\SEEALSO
ASM_CASES_TAC, BOOL_CASES_TAC, COND_CASES_TAC, DISJ_CASES_TAC.
\ENDDOC
|
