我怎樣才能在伊莎貝爾的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，旨在更容易理解和維護。