如何在 Isabelle 的 ML 级别轻松编写简单的策略？

在 Isabelle 理论文件中，我可以编写简单的一行策略，如下所示：

apply (clarsimp simp: split_def split: prod.splits)

然而，我发现，当我开始编写 ML 代码来自动化证明、生成 MLtactic对象，这些俏皮话变得相当冗长：

clarsimp_tac (Context.proof_map (
    Simplifier.map_ss (fold Splitter.add_split @{thms prod.splits})
    #> Simplifier.map_ss (fn ss => ss addsimps [@{thm split_def}]))
  @{context}) 1

有没有一种更简单的方法可以在 Isabelle/ML 级别编写简单的单行策略？

例如，类似反引号的内容：@{tactic "clarsimp simp: split_def split: prod.splits"}产生类型的函数context -> tactic，将是一个理想的解决方案。

我看到了多种可能性，这在一定程度上取决于您的应用程序的上下文，什么是最好的。请注意，一般来说，用于自动化证明的单独 ML 代码在过去很常见，但如今相对较少。例如，比较自定义策略的数量相当少HOL-Bali http://isabelle.in.tum.de/library/HOL/HOL-Bali/index.html（1997年开始）JinjaThreads http://afp.sourceforge.net/entries/JinjaThreads.shtml法新社（从 2007 年开始，一直持续到最近）。

嵌套 ML 反引号，例如@{tactic}原则上是可行的，但你很快就会遇到进一步的问题，比如如果你的定理论证再次是 Isar 或 ML 源，会发生什么。

代替反引用ML 中的策略构建块，一个更基本的方法是quote通过给 Isar 中的常规方法语法提供如下所示的证明过程：

ML {*
  (*foo_tac -- the payload of what you want to do,
    note the dependency on ctxt: Proof.context*)
  fun foo_tac ctxt =
    let
      val my_ctxt =
        ctxt |> Simplifier.map_simpset
         (fold Splitter.add_split @{thms prod.splits} #>
          Simplifier.add_simp @{thm split_def})
    in ALLGOALS (clarsimp_tac my_ctxt) end
*}

method_setup foo = {*
  (*concrete syntax like "clarsimp", "auto" etc.*)
  Method.sections Clasimp.clasimp_modifiers >>
    (*Isar method boilerplate*)
    (fn _ => fn ctxt => SIMPLE_METHOD (CHANGED (foo_tac ctxt)))  
*}

这里我先做了一个常规的foo_tacIsabelle/ML 中的定义，然后将其包装为通常的 Isar 方式作为证明方法。后者意味着你有像这样的包装器SIMPLE_METHOD负责将“连锁事实”推入您的目标状态，并且CHANGED确保 Isar 方法取得进展（例如simp or auto).

The foo_tac示例假设您对上下文（或其 simpset）的修改是恒定的，通过硬连接的分割规则。如果您想在那里有更多参数，您可以将其包含在具体方法语法中。注意Method.sections在这方面已经相当成熟了。更基本的参数解析器在“定义证明方法”部分给出isar-ref http://isabelle.in.tum.de/doc/isar-ref.pdf手动的。您还应该通过搜索源来查看现有示例method_setup（伊莎贝尔/伊萨尔）或Method.setup（伊莎贝尔/ML）。

如果您仍然想使用 ML 反引号而不是具体的方法语法，可以尝试一种变体@{context}允许这样的修饰符：

@{context simp add: ...}

这有点投机，是当场发明的，可能会被证明是不好的做法。正如我所说，尽管 ML 是 Isabelle 框架不可或缺的一部分，但 Isabelle 中的细粒度策略编程近年来已经有点过时了。如果您提出具有更多应用程序上下文的更具体问题，我们可以重新考虑反引用方法。