[isabelle] Case names for induct with datatypes



I have a datatype which has a recursive constructor where the recursive parameter is packed into another datatype, e.g.
datatype T = ... | C "T list"

Induction on T involves doing simultaneously induction on lists, i.e. the "induct T and Ts" tactic produces subgoals for all constructors of T and those for lists.

Now, in an Isar proof, picking a particular case of T is done by writing "case (C ...)" for all constructors C of T. But what are the case names that induct gives to the constructors of the wrapper datatype, i.e. for Nil and Cons?

Does induct give case names to them at all? Or do I have to name them explicitly by myself like in

proof(induct T and Ts rule: T.induct[case_names ... C Nil Cons])


Andreas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.