isabelle - 如何在 Isabelle 证明中打印局部变量和 ?thesis(在 Isabelle 中调试)？

Question

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

比如我想看什么?thesis .具体语义书说:

The unknown ?thesis is implicitly matched against any goal stated by lemma or show. Here is a typical example:

我的愚蠢样本 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值(value)。

去做:

为什么没有:

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

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

Answer 1

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



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