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

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

For example, I want to see what ?thesis. The concrete semantics book says:

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

我愚蠢的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

Why can't I print ?thesis?

It's really annoying to have to write the statement I'm trying to proof if it's obvious. Perhaps it's meant to be explicit but in the examples in chapter 5 they get away with using ?thesis in:

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

but whenever I try to use ?thesis I always fail.

为什么?

请注意,这确实有效:

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

but I thought ?thesis was there to avoid this.

Also, thm ?thesis didn't work either.

另一个例子是当我使用:

let ?ys = take k1 xs

but I can't print ?ys value.

评论
et_ea
et_ea

You can find ?theorem and others in the print context window:

print context window

As for why ?thesis doesn't work, by applying the introduction rule proof (rule allI) you are changing the goal, so it no longer matches ?thesis. The example in the book uses proof- which prevents Isabelle from applying any introduction rule.

点赞
评论