Isabelle归纳证明中可否用自定义函数分支名替代数字型案例名

完全可以实现这种语义化的案例命名，这是Isabelle非常常规的优化写法，不需要任何特殊插件或者额外配置。

你现在看到的1、2这类数字标识，只是Isabelle的默认回退行为：当你调用induct rule: pred.induct且没有显式指定分支名称时，系统会按照归纳规则中前提的出现顺序，自动分配从1开始的数字作为临时案例标记，并非强制要求必须使用数字名。

只需要在调用induct的参数里，通过case_names把两个归纳分支按顺序绑定到你在函数定义时用的pred_Zero、pred_Suc，之后就可以直接用这两个语义名引用对应的分支，替代原来的数字名。
改进后的完整可运行代码如下：

fun pred where
  pred_Zero:
  "pred 0 = 0"
| pred_Suc:
  "pred (Suc n) = n"

lemma pred_le:
  "pred n ≤ n"
proof (induct rule: pred.induct case_names pred_Zero pred_Suc)
  case pred_Zero
  thus ?case by simp
next
  case (pred_Suc n)
  thus ?case by simp
qed

• 分支名的绑定顺序必须和归纳规则的前提顺序严格对应：第一个分支是0的边界情况，第二个分支是带递归变量的Suc情况，case_names里的名字顺序不能颠倒，否则会导致案例和逻辑分支错位。
• 绑定自定义案例名后，分支内的可用假设、绑定的变量和原来数字名的场景完全一致，不需要调整原有证明逻辑。
• 这种写法能大幅提升证明脚本的可读性：后续读代码的人不需要对照函数定义反推每个数字分支对应的逻辑，直接通过案例名就能和函数定义的分支语义一一对应。

内容的提问来源于stack exchange，提问作者Denis