我怎样才能在伊莎贝尔的ML水平轻松写出简单的战术？

Question

在伊莎贝尔理论文件，我可以写简单的单行策略，如下列：

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 

有没有写在伊莎贝尔/ ML级的简单的线战法更简单的方法？

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

Answer 1

我看到了各种可能性，它取决于您的应用程序的上下文什么是最好的。请注意，一般来说，用于证明自动化的单个ML代码在过去很常见，但现在比较少见。例如，比较法新社（从2007年开始，一直持续到最近）的非常小的HOL-Bali（1997年开始）与大JinjaThreads的自定义战术的数量。

嵌套ML反语（如@{tactic}）原则上可以工作，但您很快会遇到更多问题，比如如果您的定理参数应该是Isar或ML来源，会发生什么情况。

代替antiquoting在ML战术积木，一个更基本的做法是报价在伊萨尔你证明precedure通过给予普通方法的语法如下：

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))) 
*} 

在这里，我第一次在Isabelle/ML中定义了一个传统的foo_tac定义，然后用通常的伊萨尔方式作为证明方法。后者意味着你有像SIMPLE_METHOD这样的包装将“连锁事实”推送到你的目标状态，CHANGED确保Isar方法取得进展（如simp或auto）。

foo_tac示例假定您通过硬连线拆分规则对上下文（或其simpset）的修改是恒定的。如果你想在那里有更多的参数，你可以在具体的方法语法中包含它。请注意，Method.sections在这方面已经相当复杂。在isar-ref手册的“Defining proof methods”一节中给出了更多基本的参数解析器。您还应该通过搜索method_setup（位于Isabelle/Isar）或Method.setup（位于Isabelle/ML）的源代码查看现有示例。

如果你还想做ML antiquotations，而不是具体的方法的语法，一个可以尝试的@{context}一个变种，它允许修饰符是这样的：

@{context simp add: ...} 

这是一个有点投机，发明了当场，和可能会变成糟糕的做法。正如我所说的，近年来，伊莎贝尔细致的策略编程已经有些失用了，尽管ML是伊莎贝尔框架的一个组成部分。如果你用更多的应用上下文提出更具体的问题，我们可以重新考虑反引用方法。

Answer 2

的Method类似乎提供一个接口，以提取出一个策略的足够，经由cases_tactic如下：

(* 
* Generate an ML tactic object of the given Isar string. 
* 
* For example, 
* 
* mk_tac "auto simp: field_simps intro!: ext" @{context} 
* 
* will generate the corresponding "tactic" object. 
*) 
fun mk_tac str ctxt = 
let 
    val parsed_str = Outer_Syntax.scan Position.start str 
     |> filter Token.is_proper 
     |> Args.name 
    val meth = Method.method (Proof_Context.theory_of ctxt) 
     (Args.src (parsed_str, Position.start)) ctxt 
in 
    Method.apply (K meth) ctxt [] #> Seq.map snd 
end 

或备选地作为抗报价：

(* 
* Setup an antiquotation of the form: 
* 
* @{tactic "auto simp: foo intro!: bar"} 
* 
* which returns an object of type "context -> tactic". 
* 
* While this doesn't provide any benefits over a direct call to "mk_tac" just 
* yet, in the future it may generate code to avoid parsing the tactic at 
* run-time. 
*) 
val tactic_antiquotation_setup = 
let 
    val parse_string = 
    ((Args.context -- Scan.lift Args.name) >> snd) 
     #>> ML_Syntax.print_string 
     #>> (fn s => "mk_tac "^s) 
     #>> ML_Syntax.atomic 
in 
    ML_Antiquote.inline @{binding "tactic"} parse_string 
end 

和设置在理论文件中如下：

setup {* 
    tactic_antiquotation_setup 
*} 

然后可以使用如下：

lemma "(a :: nat) * (b + 1) = (a * b) + a" 
    by (tactic {* @{tactic "metis Suc_eq_plus1 mult_Suc_right nat_add_commute"} @{context} *}) 

根据需要。

Answer 3

除了其他答案，我认为值得一提的是，Isabelle2015中有一种新的高级策略/证明方法构造语言（类似于Coq中的Ltac），名为Eisbach，旨在更容易理解和维护。