----------------------------------------------------------------------
Cases_on                                                     (bossLib)
----------------------------------------------------------------------
Cases_on : term quotation -> tactic

SYNOPSIS
Performs case analysis on the type of a given term.

KEYWORDS
tactic

LIBRARY
BasicProvers

DESCRIBE
An application {Cases_on M} performs a case-split based on the type {ty}
of {M}, using the cases theorem for {ty} from the global {TypeBase}
database.

{Cases_on} can be used to specify variables that are buried
in the quantifier prefix. {Cases_on} can also be used to perform
case splits on non-variable terms. If {M} is a non-variable term that
does not occur bound in the goal, then the cases theorem is instantiated
with {M} and used to generate as many sub-goals as there are disjuncts
in the cases theorem.

FAILURE
Fails if {ty} does not have a case theorem in the {TypeBase}.

EXAMPLE
None yet.

SEEALSO
bossLib.Cases, bossLib.Induct, bossLib.Induct_on,
Tactic.STRUCT_CASES_TAC.

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