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