我有一个Isabelle证据结构如下:
proof (cases "n = 0")
case True
(* lots of stuff here *)
show ?thesis sorry
next
case False
(* lots of stuff here too *)
show ?thesis sorry
qed
第一种情况实际上是几页长,所以在阅读第二种情况时,对于一个随意的读者,甚至对我自己来说,它False所指的不再是清楚的.(嗯,它实际上是,但不是来自阅读,只能在交互式环境中:例如,如果在Isabelle/jEdit中,您将光标置于其后case False,您将n ? 0在"输出"面板中的"this"下看到.)
那么是否有一种语法允许假设"假"情况明确,这样读者既不必与IDE交互,也不必向上滚动到proof关键字,但是可以正确看待假设？
到目前为止,我在Isabelle的以下风格中使用矛盾来编写证据(使用Jeremy Siek的模式):
lemma "<expression>"
proof -
{
assume "¬ <expression>"
then have False sorry
}
then show ?thesis by blast
qed
有没有一种方法可以在没有嵌套的原始校样块的情况下工作{ ... }？
有时<statement> solve_direct（我通常通过调用<statement> try）列出一些库定理并说“当前的目标可以直接解决：……”。
设<theorem>一个搜索结果solve_direct，然后在大多数情况下我可以证明<statement> by (rule theorem)。
然而，有时这样的证明不被接受，导致错误信息“应用初始证明方法失败”。
是否有一种通用的、不同的技术来重用由 找到的定理solve_direct？
还是要看个人情况？我可以尝试找出一个最小的例子并将其附加到这个问题上。