namedCases_on : term quotation -> string list -> tactic
STRUCTURE
SYNOPSIS
Case split on type of given term, using given names for introduced constructor arguments.
DESCRIPTION
An application of namedCases_on q [s1, ..., sn] to a goal A ?- P first parses q in the context of the goal to yield a term tm:ty, then uses ty to look up a a so-called "nchotomy" theorem installed in the system database of declared datatypes, then performs a case split on how tm can be constructed. The strings s1, ..., sn designate the names to be used as arguments of the constructor in each case. This yields the goals
    (A, tm = <constr>1 <names>1 ?- P)
     ,...,
    (A, tm = <constr>n <names>n ?- P)
For a datatype with n constructors, n strings are expected to be supplied. If no strings are supplied, the system will use a default naming scheme. If the ith constructor has no arguments, then si should be the empty string. If the ith constructor has k arguments, then si should consist of k space-separated names. In case a name does not need to be specified, an underscore _ or dash - can be supplied, in which case a default name will be conjured up.

In case ty is a product type ty1 # ... # tyi, namedCases_on q [s] will iteratively case split on all product types in ty, thus replacing x:ty by a tuple with i variables, the names of which are taken from s.

FAILURE
Fails if there is not an nchotomy theorem installed for the topmost type constructor of ty. If slist is not the empty list, namedCases_on q slist will fail if the length of slist is not equal to the number of constructors in the nchotomy theorem. Fails if the given names for arguments of an introduced constructor are not equinumerous with the arguments.
COMMENTS
This is a version of namedCases where the (free) term being split on is specified.
SEEALSO
HOL  Trindemossen-1