有时我很难使用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.
You can find
?theoremand others in the print context window:As for why
?thesisdoesn't work, by applying the introduction ruleproof (rule allI)you are changing the goal, so it no longer matches?thesis. The example in the book usesproof-which prevents Isabelle from applying any introduction rule.