如何在Isabelle证明中打印局部变量和主题？

Question

有时我发现很难使用Isabelle，因为我无法像普通编程中那样拥有“打印命令”。

例如，我想查看什么?thesis。具体的语义书说：

未知的命题与引理或表演提出的任何目标都暗含匹配。这是一个典型的例子：

我愚蠢的示例FOL证明是：

lemma
  assumes "(∃ x. ∀ y. x ≤ y)"
  shows "(∀x. ∃ y. y ≤ x)"
proof (rule allI)
  show ?thesis

但出现错误：

proof (state)
goal (1 subgoal):
 1. ⋀x. ∃y. y ≤ x 
Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  ∀x. ∃y. y ≤ x

但是我确实知道为什么。

我期望

?thesis === ⋀x. ∃y. y ≤ x

因为我的证明状态是：

proof (state)
goal (1 subgoal):
 1. ⋀x. ∃y. y ≤ x

为什么我不能打印?thesis？

不得不写我想​​证明的陈述是显而易见的，这真是令人讨厌。也许是为了明确起见，但在第5章的示例中，他们摆脱了在[]中使用?thesis的意图：

lemma fixes a b :: int assumes "b dvd (a+b)" shows "b dvd a" proof −
have "∃k′. a = b∗k′" if asm: "a+b = b∗k" for k proof
show "a = b∗(k − 1)" using asm by(simp add: algebra_simps) qed
then show ?thesis using assms by(auto simp add: dvd_def ) qed
但是每当我尝试使用?thesis时，我总是失败。

为什么？

请注意，这确实有效：

lemma
  assumes "(∃ x. ∀ y. x ≤ y)"
  shows "(∀x. ∃ y. y ≤ x)"
proof (rule allI)
  show "⋀x. ∃y. y ≤ x" proof -
但是我认为?thesis在那里避免这种情况。

---

[另外，thm ?thesis也不起作用。

---

另一个例子是当我使用：

let ?ys = take k1 xs
但是我无法打印?ys值。

我有时很难使用Isabelle，因为我无法像普通编程中那样拥有“打印命令”。例如，我想看什么主题。具体的语义书说：未知的？...

Answer 1

您可以在打印上下文窗口中找到?theorem和其他：

Answer 2

?thesis和?ys是术语的缩写。您可以使用命令term显示任何术语。例如，>

lemma
  assumes "(∃x. ∀y. x ≤ y)"
  shows "(∀x. ∃y. y ≤ x)"
proof (rule allI)
  term ?thesis
  (*"∀x. ∃y. y ≤ x":: "bool"*)
  let ?ys = "take 1"
  term ?ys
  (*"take 1":: "'c list ⇒ 'c list"*)