Email Gateway (Aug 18 2022 at 11:55): Email Gateway (Aug 18 2022 at 11:55):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
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
Email Gateway (Aug 18 2022 at 11:55):From: Makarius <makarius@sketis.net>
Yes, print_cases will tell you the names produced by the datatype rule.
Makarius
Last updated: May 03 2024 at 04:19 UTC