6

有时，当我在写应用风格的证明时，我想要一种方法来修改证明方法 foo以

尝试foo第一个目标。如果它解决了目标，很好；如果没有解决，恢复到原始状态并失败。

这出现在以下代码中：

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!])+

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

4

4 回答 4

3

Isabelle 没有这样的组合器，这也是我想念的。auto通常，如果我替换orsimp调用fastforceor force（具有解决或失败行为），我可以避免对这种组合器的需要。

因此，如果simp您的示例中的 应该解决目标（不循环），

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

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

于 2013-03-08T09:40:47.657 回答
3

自从Eisbach 证明脚本语言出现以来，现在就支持这一点。导入后"~~/src/HOL/Eisbach/Eisbach"可以替换

apply foo

和

apply (solves ‹foo›)

solves如果产生任何新目标，这条线将失败。这可以与[1]如下组合

apply (solves ‹(auto)[1]›)

如果需要。

的定义solves其实很简单：

method solves methods m = (m; fail)
于 2016-05-20T08:12:32.467 回答
1

虽然没有可用的内置策略或组合器，但您可以自己实现一个，如下所示：

ML {*
fun solved_tac thm =
  if nprems_of thm = 0 then Seq.single thm else Seq.empty
*}

method_setup solved = {*
  Scan.succeed (K (SIMPLE_METHOD solved_tac))
*}

这创建了一个新方法solved，如果当前目标已完全解决，则该方法将成功，如果仍然存在一个或多个子目标，则该方法将失败。

例如，它可以按如下方式使用：

lemma "a ∨ ¬ a "
  apply ((rule disjI1, solved) | (simp, solved))
  done

如果没有该solved子句，Isabelle 将选择步骤的rule disjI1一侧，给apply您留下一个无法解决的目标。solvedIsabelle 尝试使用每一边的子句rule disjI1，当它未能解决目标时，切换到simp即成功的子句。

这可以通过使用 Isabelle 的(...)[1]语法来解决个人目标。例如，以下语句将尝试使用 解决尽可能多的子目标，但如果无法完全解决simp子目标，则将保持子目标不变：simp

apply ((simp, solved)[1])+
于 2013-04-10T00:17:14.220 回答
0

Isabelle 的 Isar 语言不提供该功能。这是故意的，而不是错误，如isabelle 开发人员列表中所述：

Isar 证明方法语言以某种方式设计，以达到证明文本中某些操作方面的“风格化”规范。它故意排除了任何类型的编程或复杂的控制结构。

于 2013-03-15T22:25:18.417 回答