イザベルのMLレベルで単純な戦術を簡単に書く方法はありますか？

Question

イザベル理論ファイルでは、私は次のようなシンプルな1行の戦術を書くことができますが：

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レベルで簡単な1行の戦術を書くための簡単な方法はありますか？

たとえば、context -> tacticという種類の機能を生成する、アンチクォーテーション：@{tactic "clarsimp simp: split_def split: prod.splits"}のようなものは理想的な解決策です。

Answer 1

私は様々な可能性を見ていますが、アプリケーションのコンテキストに応じて最適なものが異なります。一般的に、校正自動化のための個々のMLコードは、古くは普通の場所であったが、今日は比較的まれであることに注意してください。たとえば、AFCのJinjaThreads（2007年に開始し、最近まで継続していた）の大規模な（1997年に始まった）のカスタム作戦の量を比較してください。

@{tactic}のようなネスティングMLの払い戻しは、原則として動作しますが、あなたの定理の引数が再びIsarまたはMLソースでなければならない場合のように、すぐにさらなる質問に遭遇します。 MLで戦術ビルディングブロックをantiquoting

代わりのは、より基本的なアプローチは引用にあるこのように、それを通常のメソッドの構文を与えることによってイザールであなたの証明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の定義を行い、それを証明する方法として通常のIsar方法でラップしました。後者の場合、SIMPLE_METHODのようなラッパーがあり、「連鎖した事実」を目標状態にすること、そしてCHANGEDを使ってIsarメソッドが進行することを保証します（simpまたはautoなど）。

foo_tac例では、ハードワイヤード分割ルールによってコンテキスト（またはそのsimpset）の変更が一定であることを前提としています。そこにさらにパラメータを追加したい場合は、具体的なメソッド構文にそのパラメータを含めることができます。 Method.sectionsは既にこの点でかなり洗練されています。より基本的な引数パーサーは、isar-refマニュアルの「証明方法の定義」のセクションにあります。 method_setup（Isabelle/Isarの場合）またはMethod.setup（Isabelle/MLの場合）のソースを検索して、既存の例を見てください。

それでも代わりに、具体的なメソッドの構文のMLのantiquotationsを行いたい場合は、1が可能に@{context}のバリアントを試みることができる。このような修飾子：

場で発明され、ビット投機的である

@{context simp add: ...} 

、および悪い練習になるかもしれない。私が言ったように、MLはIsabelleフレームワークの不可欠な部分ですが、Isabelleのきめ細かい戦術プログラミングは近年少し使い尽くされました。より多くのアプリケーションコンテキストを使用してより具体的な質問をする場合、反占有アプローチを再考することができます。次のように

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にはEisbachという新しい高水準の戦術/証明方法の構築言語（CoqのLtacに似ています）があり、理解しやすく維持することを目的としています。