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
|
\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
}
\FAILURE
Fails if {u} does not have boolean type.
\EXAMPLE
The tactic {ASM_CASES_TAC `&0 <= u`} can be used to produce a case analysis
on {`&0 <= u`}:
{
# g `&0 <= (u:real) pow 2`;;
Warning: Free variables in goal: u
val it : goalstack = 1 subgoal (1 total)
`&0 <= u pow 2`
# e(ASM_CASES_TAC `&0 <= u`);;
val it : goalstack = 2 subgoals (2 total)
0 [`~(&0 <= u)`]
`&0 <= u pow 2`
0 [`&0 <= u`]
`&0 <= u pow 2`
}
\USES
Performing a case analysis according to whether a given term is true or false.
\SEEALSO
BOOL_CASES_TAC, COND_CASES_TAC, ITAUT, DISJ_CASES_TAC, STRUCT_CASES_TAC, TAUT.
\ENDDOC
|
