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
|
\DOC ASM_CASES_TAC
\TYPE {ASM_CASES_TAC : (term -> tactic)}
\SYNOPSIS
Given a term, produces a case split based on whether or not that
term is true.
\KEYWORDS
tactic, cases.
\DESCRIBE
Given a term {u}, {ASM_CASES_TAC} applied to a goal produces two
subgoals, one with {u} as an assumption and one with {~u}:
{
A ?- t
================================ ASM_CASES_TAC "u"
A u {{u}} ?- t A u {{~u}} ?- t
}
\noindent {ASM_CASES_TAC u} is implemented by
{DISJ_CASES_TAC(SPEC u EXCLUDED_MIDDLE)}, where {EXCLUDED_MIDDLE} is
the axiom {|- !u. u \/ ~u}.
\FAILURE
By virtue of the implementation (see above), the decomposition fails if
{EXCLUDED_MIDDLE} cannot be instantiated to {u}, e.g. if {u} does not
have boolean type.
\EXAMPLE
The tactic {ASM_CASES_TAC "u"} can be used to produce a case analysis
on {"u"}:
{
ASM_CASES_TAC "u:bool" ([],"(P:bool -> bool) u");;
([(["u"], "P u"); (["~u"], "P u")], -) : subgoals
}
\USES
Performing a case analysis according to whether a given term is true or false.
\SEEALSO
BOOL_CASES_TAC, COND_CASES_TAC, DISJ_CASES_TAC, SPEC, STRUCT_CASES_TAC.
\ENDDOC
|
