[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])
This archive was generated by a fusion of
Pipermail (Mailman edition) and