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

Question

是否可以在下面的归纳证明中使用名字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

Answer 1

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

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

案例的更多规范名称是 0 和 Suc，在这种特殊情况下，您也可以使用默认归纳规则 nat.induct，因为归纳规则为 pred 生成的与 nat.induct.

相同