ASM_CASES_TAC : term -> tactic
SYNOPSIS
Given a term, produces a case split based on whether or not that term is true.
LIBRARY
bool
STRUCTURE
Tactic
DESCRIPTION
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
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: 
  - let val u = Term `u:bool`
        val g = Term `(P:bool -> bool) u`
    in
    ASM_CASES_TAC u ([],g)
    end;

    ([([`u`],  `P u`),
      ([`~u`], `P u`)], fn) : tactic_result

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, Cases, Cases_on
HOL  Kananaskis-14