有时,当我在写应用风格的证明时,我想要一种修改证明方法的方法foo
到
Try
foo
on the first goal. If it solves the goal, good; if it does not solve it, revert to the original state and fail.
这出现在以下代码中:
qed (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)+
在进一步进行一些更改后,调用
simp
将不再完全解决目标,然后这将循环。如果我可以指定类似的东西qed (solve_goal(subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail))+
或(替代建议的语法)
qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)!)+
或(也许更好的语法)
qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)[1!])+
它会停在这个脚本无法解决的第一个目标上。
最佳答案
Isabelle 没有这样的组合器,这也是我想念的。通常,如果我替换 auto
,我可以避免使用这样的组合器。或 simp
来电 fastforce
或 force
(具有解决或失败行为)。
所以,如果 simp
在您的示例中应该解决目标(不循环),
qed (subst fibs.simps, (subst fib.simps)?, fastforce simp: nth_zipWith nth_tail)+
可能是一个更强大的变体。
关于proof - 当且仅当它解决当前目标时应用方法,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/15290300/