如何在伊莎贝尔的ML级别轻松编写简单的策略？

Question

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

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

然而,我发现,当我开始编写ML代码来自动化证明,生成一个ML tactic对象时,这些单行变得相当冗长:

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,将是一个理想的解决方案.

Answer 1

我看到了各种各样的可能性,它取决于你的应用程序的上下文什么是最好的.请注意,一般情况下,自动校对的单个ML代码曾经在过去很常见,但今天相对较少.例如,将相当小的HOL-Bali(1997年开始)的定制战术数量与AFP中的大型JinjaThreads(2007年开始并持续到最近)进行比较.

嵌入ML反引号@{tactic}原则上会起作用,但是你会很快遇到更多的问题,比如你的定理论点应该再次是Isar或ML源会发生什么.

而不是在ML 中反引用战术构建块,更基本的方法是在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_tac在Isabelle/ML中做出了一个传统的定义,然后用通常的Isar方式将它作为证明方法.后者意味着您拥有包装,如SIMPLE_METHOD将"链式事实"推入您的目标状态,并CHANGED确保Isar方法取得进展(如simp或auto).

该foo_tac示例假定您通过硬连线拆分规则修改上下文(或其simpset)是不变的.如果您想在那里有更多参数,可以在具体方法语法中包含它.请注意,Method.sections在这方面已经相当复杂.更多基本的参数解析器在isar-ref手册的"定义证明方法"一节中给出.您还应该通过搜索method_setup(在Isabelle/Isar中)或Method.setup(在Isabelle/ML中)的来源来查看现有示例.

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

@{context simp add: ...}

这有点推测,在现场发明,可能会变成不好的做法.正如我所说,尽管ML是Isabelle框架中不可或缺的一部分,但近年来Isabelle的细粒度战术编程变得有点用完了.如果您在更多应用程序上下文中提出更具体的问题,我们可以重新考虑反引用方法.