Certaines règles d'induction ont des noms de cas: la valeur par défaut est case 0 et case (Suc n) par exemple. Étant donné une règle, par ex. int_induct, comment puis-je trouver ses noms de cas (si, en effet, il a ceux-ci) sans regarder dans la théorie contenant ce lemme?Noms de cas de règles d'induction (Isabelle)
Je ne suis pas au courant d'un moyen de haut niveau pour ce faire. Les noms de cas sont stockés dans les balises d'un théorème qui peut être obtenu avec ML:
ML‹Thm.get_tags @{thm nat.induct}›
Cette impression:
val it = [("name", "Nat.nat.induct"), ("kind", "theorem"), ("case_names", "zero;Suc")]: Properties.T
Comme vous pouvez le voir, les noms de cas sont disponibles sous la clé case_names.
Vous pouvez également utiliser 'Rule_Cases.get', par ex. 'ML_val'. Et, bien sûr, vous pouvez simplement utiliser la règle dans Isar et ensuite utiliser 'print_cases'. –