Some induction rules have case names: the default one has case 0 and case (Suc n) for example. Given a rule, e.g. int_induct, how do I find out its case names (if, indeed, it has these) without looking in the theory containing this lemma?
1
votes
1 Answers
2
votes
I'm not aware of any high-level way to do this. The case names are stored in the tags of a theorem that can be obtained with ML:
ML‹Thm.get_tags @{thm nat.induct}›
This prints:
val it = [("name", "Nat.nat.induct"), ("kind", "theorem"), ("case_names", "zero;Suc")]: Properties.T
As you can see, the case names are available under the key case_names.
