----------------------------------------------------------------------
ASM_CASES_TAC                                                 (Tactic)
----------------------------------------------------------------------
ASM_CASES_TAC : term -> tactic

SYNOPSIS
Given a term, produces a case split based on whether or not that
term is true.

KEYWORDS
tactic, case analysis.

LIBRARY
bool

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

{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
Tactic.BOOL_CASES_TAC, Tactic.COND_CASES_TAC, Tactic.DISJ_CASES_TAC,
Thm.SPEC, Tactic.STRUCT_CASES_TAC, BasicProvers.Cases,
bossLib.Cases_on.

----------------------------------------------------------------------