参考 Isabelle 中的当前假设

Question

当我有很多假设时，有时我会得到很多临时名称，使证明变得混乱。

我说的是这样的事情：

lemma foo: ...
proof
  assume P: ... and Q: ... and R: ...
  then have ...
  then have ... using P ...
  then have ... using P R ...
  then show ...
  proof
   assume A: ... and B: ... and C: ...
   then have ...
   then have ... using B C ...
   ...

你能想象这是如何演变的吗？很多语句的名称，在事物的宏伟计划中，不值得命名，但仍然命名，因为我们需要在几行之后引用它们。

另一方面，如果我们使用所有当前的假设，多余的名称就不会扰乱证明：

lemma foo: ...
proof
  assume ... and ... and ...
  then have ...
  then have ... using assumptions ...
  then have ... using assumptions ...
  then show ...
  proof
   assume ... and ... and ...
   then have ...
   then have ... using assumptions ...
   ...

当然，using assumptions 不是伊莎贝尔的有效陈述。我知道 assms，它引用了 assumes 子句，但我不知道 assume.

是否存在这样的东西

有没有办法引用 assume 创建的所有当前假设？

Answer 1

万一你真的需要它...

如果你想要的只是你最后做出的假设（而不是所有），你可以通过使用命名约定来模拟呈现的效果（例如assumptions 或 assmps) 并将假设捆绑在一起（即使用“"..." "..." "..."”而不是“"..." and "..." and "..."”）：

lemma foo: ...
proof
  assume assumptions: "..." "..." "..."
  then have ...
  then have ... using assumptions ...
  then have ... using assumptions ...
  then show ...
  proof
   assume assumptions: "..." "..." "..."
   then have ...
   then have ... using assumptions ...
   ...

在上面的示例中，第二个 assume assumptions 隐藏了第一个，因此如果您总是将您的假设命名为“assumptions”（或您喜欢的任何命名约定），那么 using assumptions 将始终参考最后一组假设。

请注意，一旦您使用 qed 关闭子证明，当前范围内的任何 assume assumptions 都会被遗忘，因此正如预期的那样，您可以在完成子证明后继续使用之前的假设。

此方法的缺点是，由于每个新名称都会影响其余名称，只有您在范围内的最新假设是可访问的，如果您打算这样做，这可能是个问题使用最近的假设之前所做的任何假设。

...但您可能不需要它。

虽然您可以使用它，但 Isabelle 有其他构造可以更好地解决同一问题，具体取决于具体情况。请牢记以下一些有用的工具：

您可以使用 assume A: "..." "..." "..." 将假设捆绑在一起，而无需 and
您可以使用 moreover ... ultimately ...
您可以使用 have ... and ... and ... by ...
如果您的假设处于引理级别，您可以使用 lemma foo: assumes ... shows ...，它们将以 assms
可以直接引用以前的事实‹...›

使用 1. 已经大大减少了混乱：

lemma foo: ...
proof
  assume A: "..." "..." "..."
  then have ...
  then have ... using A ...
  then have ... using A ...
  then show ...
  proof
   assume B: "..." "..." "..."
   then have ...
   then have ... using B ...
   ...

或者，使用 2. 和 3. 您可以将其格式化为：

lemma foo: ...
proof
  assume "..." "..." "..."
  moreover from calculation have ...
  moreover from calculation have ...
  ultimately have ...
  then show ...
  proof
   assume "..." "..." "..."
   moreover from this have ...
   ultimately have ... and ...
   ...

或者，使用 4. 和 5.:

lemma foo:
  assumes: "..." "..." "..."
  shows: ...
proof
  have ... using assms ...
  then have ... using assms ...
  then have ... using assms ...
  then show ...
  proof
    assume "..." "..." "..."
    then have ...
    then have ... using ‹...› ‹...› ...

参考 Isabelle 中的当前假设

Referencing current assumptions in Isabelle

isabelle

isar

万一你真的需要它...

...但您可能不需要它。