1\DOC ASM_CASES_TAC
2
3\TYPE {ASM_CASES_TAC : term -> tactic}
4
5\SYNOPSIS
6Given a term, produces a case split based on whether or not that
7term is true.
8
9\KEYWORDS
10tactic, case analysis.
11
12\LIBRARY
13bool
14
15\STRUCTURE
16Tactic
17
18\DESCRIBE
19Given a term {u}, {ASM_CASES_TAC} applied to a goal produces two
20subgoals, one with {u} as an assumption and one with {~u}:
21{
22               A ?-  t
23   ================================  ASM_CASES_TAC u
24    A u {u} ?- t   A u {~u} ?- t
25}
26{ASM_CASES_TAC u} is implemented by
27{DISJ_CASES_TAC(SPEC u EXCLUDED_MIDDLE)}, where {EXCLUDED_MIDDLE} is
28the axiom {|- !u. u \/ ~u}.
29
30\FAILURE
31By virtue of the implementation (see above), the decomposition fails if
32{EXCLUDED_MIDDLE} cannot be instantiated to {u}, e.g. if {u} does not
33have boolean type.
34
35\EXAMPLE
36The tactic {ASM_CASES_TAC u} can be used to produce a case analysis
37on {u}:
38{
39  - let val u = Term `u:bool`
40        val g = Term `(P:bool -> bool) u`
41    in
42    ASM_CASES_TAC u ([],g)
43    end;
44
45    ([([`u`],  `P u`),
46      ([`~u`], `P u`)], fn) : tactic_result
47}
48
49
50\USES
51Performing a case analysis according to whether a given term is true or false.
52
53\SEEALSO
54Tactic.BOOL_CASES_TAC, Tactic.COND_CASES_TAC, Tactic.DISJ_CASES_TAC, Thm.SPEC,
55Tactic.STRUCT_CASES_TAC, BasicProvers.Cases, bossLib.Cases_on.
56
57\ENDDOC
58