【发布时间】：2017-08-18 11:17:41
【问题描述】：
一些归纳规则有案例名称：例如，默认的有case 0 和case (Suc n)。给定一个规则，例如int_induct，我如何在不查看包含此引理的理论的情况下找出它的案例名称（如果确实有这些名称）？
【问题讨论】：
【发布时间】：2017-08-18 11:17:41
【问题描述】：
我不知道有任何高级方法可以做到这一点。案例名称存储在可以使用 ML 获得的定理的 标签 中：
ML‹Thm.get_tags @{thm nat.induct}›
打印出来：
val it = [("name", "Nat.nat.induct"), ("kind", "theorem"), ("case_names", "zero;Suc")]: Properties.T
如您所见，案例名称在 case_names 键下可用。
【讨论】：
-
您也可以使用
Rule_Cases.get，例如ML_val ‹Rule_Cases.get @{thm nat.induct}›。当然，您可以只使用 Isar 中的规则，然后使用print_cases。