proof - 当且仅当它解决当前目标时应用方法

Question

有时，当我在写应用风格的证明时，我想要一种修改证明方法的方法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!])+

它会停在这个脚本无法解决的第一个目标上。

Answer 1

Isabelle 没有这样的组合器，这也是我想念的。通常，如果我替换 auto，我可以避免使用这样的组合器。或 simp来电 fastforce或 force (具有解决或失败行为)。

所以，如果 simp在您的示例中应该解决目标(不循环)，

qed (subst fibs.simps, (subst fib.simps)?, fastforce simp: nth_zipWith nth_tail)+

可能是一个更强大的变体。