如何在 Isabelle 证明中打印局部变量和 ?thesis（在 Isabelle 中调试）？

Question

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

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

未知 ?thesis 隐含地与引理或 show 陈述的任何目标相匹配。下面是一个典型的例子：

我的愚蠢示例 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 章的示例中，他们使用?thesisin：

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价值。

---

去做：

为什么没有：

lemma "length(tl xs) = length xs - 1"
  thm (cases xs)

显示什么？（如果您用归纳替换案例，则相同）。

Answer 1

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

至于为什么?thesis不起作用，通过应用引入规则，proof (rule allI)您正在更改目标，因此它不再匹配?thesis。书中的示例使用proof-阻止伊莎贝尔应用任何介绍规则。