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

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.verified 项目），常见的证明风格主要是使用结构化证明。非结构化证明用于探索并且很少变得如此复杂以至于需要重命名变量。