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 .

在证明 block 中，您可以看到带有 print_cases 的案例列表。命令。

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

对于大多数项目(程序验证除外，如 L4.verified 项目)，常见的证明风格主要是使用结构化证明。非结构化证明用于探索并且很少变得如此复杂以至于需要重命名变量。