isabelle - Isabelle/Isar 的假设语义是什么？

Question

使用 Isar 时，我发现了一个令人惊讶的行为(对我而言)。
我尝试使用假设，有时 Isar 提示它无法解决未决目标，例如我最典型的例子是有一个假设但无法假设它:

lemma 
  assumes "A"
  shows "A"
proof -
  assume "A"
  from this show "A" by (simp)
qed

虽然以下确实有效:

lemma 
  shows "A⟹A"
proof -
  assume "A"
  from this show "A" by simp
qed

这并不奇怪。

但是下一个 是 鉴于我的第一个示例失败了，它的工作原理让我感到惊讶:

lemma 
  assumes "A"
  shows "A"
proof -
  have "A" by (simp add: assms)
  from this show "A" by (simp)
qed

为什么第一个和第二个不一样？

错误消息:

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (A) ⟹ A

Answer 1

您可以在文档 Isar-ref 的“第 6 章:证明”中找到答案。理想情况下，您希望通读本章的介绍以及第 6.1 和 6.2 节以完全解决您的疑虑。下面，我介绍最相关的段落:

The logical proof context consists of fixed variables and assumptions.

...

Similarly, introducing some assumption χ has two effects. On the one hand, a local theorem is created that may be used as a fact in subsequent proof steps. On the other hand, any result χ ⊢ φ exported from the context becomes conditional wrt. the assumption: ⊢ χ ==> φ. Thus, solving an enclosing goal using such a result would basically introduce a new subgoal stemming from the assumption. How this situation is handled depends on the version of assumption command used: while assume insists on solving the subgoal by unification with some premise of the goal, presume leaves the subgoal unchanged in order to be proved later by the user.

让我们看看你的第一个例子:

lemma 
  assumes "A"
  shows "A"
proof -
  assume "A"
  from this show "A" by (simp)
qed

只有一个子目标没有前提: A .鉴于没有前提，“与前提的统一”是不适用的。

在第二个例子中，

lemma 
  shows "A⟹A"
proof -
  assume "A"
  from this show "A" by simp
qed

子目标是 A⟹A与前提 A .因此，您可以使用 assume : 可以进行统一。

最后，

lemma 
  assumes "A"
  shows "A"
proof -
  have "A" by (simp add: assms)
  from this show "A" by (simp)
qed

与前面的情况不同，因为您没有引入任何假设。因此，您可以使用 show实现子目标。需要注意的是 from this show "A" by (simp)与 from assms show "A" by simp 相同或者，更好的是， from this show "A". :

lemma 
  assumes "A"
  shows "A"
proof -
  from assms show "A".
qed