归纳证明中的命名函数案例

如何解决归纳证明中的命名函数案例

在下面的归纳证明中是否可以使用名称 pred_Zero 和 pred_Suc 代替 1 和 2？

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 1
  thus ?case by simp
next
  case (2 n)
  thus ?case by simp
qed

解决方法

您可以使用 induction 属性为 cases 或 case_names 规则的情况指定名称：

proof (induct rule: pred.induct [case_names pred_Zero pred_Suc])

案例的更多规范名称是 0 和 Suc，在这种特殊情况下，您不妨使用默认的归纳规则 nat.induct，因为归纳规则为pred 与 nat.induct 相同。