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

使用Isar时，我发现了一个令人惊讶的行为（对我来说）。我尝试使用假设，有时Isar抱怨它无法解决未完成的目标，例如，我最典型的示例是假设...

Answer 1

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