tmCases_on : term -> string list -> tactic
STRUCTURE
bossLib
SYNOPSIS
Begins a “cases” proof on the provided term
DESCRIPTION
A call to tmCases_on t names will do the equivalent of a FULL_STRUCT_CASES_TAC on the term t, using the cases (or “nchotomy”) theorem stored in the TypeBase for t’s type. If the names list is not empty, the names encoded there will be used to give names to any existentially quantified names in the cases theorem. Each element of the names list corresponds to the cases of the theorem, and, as constructors may take multiple arguments, each corresponding to an existentially quantified variable, the element is itself a list of names, separated by spaces. For example, the cases theorem for lists could be passed a string list of the form ["", "head tail"]. If the names is empty, then the system will choose names for the existentially quantified variables.

As a convenience, if the term argument is a variable, and there are variables of that name free in the goal, or bound by top-level universal quantifiers in the goal’s conclusion, then the type of the variable is ignored and its name is used to generate the argument to the tactic. If a goal has multiple variables of the same name (always a bad idea!) the choice of variable is unspecified.

FAILURE
Fails if the term is not of a type occurring in the TypeBase.
EXAMPLE
Note how in this example, the parser will give the argument l bare type “:α”, but it still picks the appropriately instantiated list cases theorem for the l that appears in the goal, which may have type “:num list”, for example. 
            ?- MAP f l = []
   =========================================   tmCases_on “l” ["", "e es"]
   ?- MAP f [] = []    ?- MAP f (e::es) = []
SEEALSO
Cases_on, FULL_STRUCT_CASES_TAC
HOL  Kananaskis-14