案例分析生成的变量可以命名吗？

Question

是否可以为使用案例分析或归纳时生成的变量指定我自己的名称？

Answer 1

如果您使用结构化证明(以proof关键字开始)，则可以使用case键盘选择要证明的案例，并为案例分析/归纳创建的变量命名：

lemma "length (rev xs) = length xs"
proof (induct xs)
  case Nil
  then show ?case ...
next
  case (Cons x xs)
  then show ?case ...
qed

这里，case (Cons x xs)告诉Isabelle，您希望证明列表由一个开始元素和一个剩余列表(即归纳步骤)组成的情况，并将变量命名为x和xs。

在证明块中，您可以看到使用print_cases命令的案例列表。

另一方面，如果您使用的是apply-style，则没有直接的方法来命名这些变量(而且，在这种情况下，您可能需要使用case_tac而不是cases，因为您必须处理绑定变量而不是自由变量)。有一种方法rename_tac，可用于重命名最外层的元量化变量。

对于大多数项目(除了程序验证的显著例外，如在L4.verated项目中)，常见的证明风格主要是使用结构化的证明。非结构化证明用于探索，很少会变得如此复杂，以至于有必要重命名变量。