Wie kann ich einfach einfache Taktiken auf der ML-Ebene von Isabelle schreiben?

Question

In einer Isabelle Theorie Datei, kann ich einfach einzeilige Taktik schreiben wie die folgenden:

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

finde ich aber, wenn ich anfangen zu schreiben ML Code Beweise zu automatisieren, ein ML tactic Objekt zu erzeugen, werden diese Einzeiler ziemlich ausführliche:

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 

gibt es einen einfacheren Weg, um die einfache einzeilige Taktik am Isabelle/ML Ebene zu schreiben?

Zum Beispiel, so etwas wie ein Anti-Zitat: @{tactic "clarsimp simp: split_def split: prod.splits"} produziert eine Funktion des Typs context -> tactic, wäre eine ideale Lösung.

Answer 1

ich eine Vielzahl von Möglichkeiten zu sehen, es hängt ein wenig von dem Kontext Ihrer Anwendung, was am besten ist. Beachten Sie, dass im Allgemeinen der individuelle ML-Code für den automatisierten Beweis in den sehr alten Zeiten üblich war, aber heute ist er relativ selten. Man vergleiche beispielsweise die Menge an individueller Taktik in eher kleinen HOL-Bali (seit 1997) mit den großen JinjaThreads in AFP (begann 2007 und dauerte bis vor kurzem).

Nesting ML Antiquitierungen wie @{tactic} würde im Prinzip funktionieren, aber Sie würden schnell auf weitere Fragen stoßen, wie was passiert, wenn Ihre Theorem Argumente wieder Isar oder ML-Quelle sein sollte.

Statt antiquoting Taktik Bausteine ​​in ML, ein grundlegenden Ansatz ist zu Zitat Ihr Beweis precedure in Isar durch reguläre Methode Syntax wie folgt geben:

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

Hier habe ich zum ersten Mal eine herkömmliche foo_tac Definition in Isabelle/ml und wickelte es dann auf die übliche Art und Weise als Beweis Isar Verfahren auf. Letzteres bedeutet, dass Sie Wrapper wie SIMPLE_METHOD drängen „gekettet Fakten“ in den Zielzustand kümmert, und CHANGED, um sicherzustellen, dass die Isar Methode Fortschritte macht (wie simp oder auto).

Das Beispiel foo_tac geht davon aus, dass Ihre Änderung des Kontexts (oder seines Simpset) durch die festverdrahteten Split-Regeln konstant ist. Wenn Sie dort weitere Parameter haben wollen, können Sie das in die konkrete Methoden-Syntax aufnehmen. Beachten Sie, dass Method.sections in dieser Hinsicht bereits ziemlich ausgereift ist. Weitere grundlegende Argumentparser sind im Abschnitt "Definieren von Prüfmethoden" des Handbuchs isar-ref beschrieben. Sie sollten auch an vorhandenen Beispielen suchen, indem Sie die Quellen für method_setup (in Isabelle/Isar) oder Method.setup (in Isabelle/ML) zu suchen.

Wenn Sie noch ML wollen antiquotations statt konkreter Methode Syntax zu tun, man eine Variante von @{context} versuchen könnte, die Modifikatoren wie dies ermöglicht:

@{context simp add: ...} 

, die ein wenig spekulativ ist, an Ort und Stelle erfunden, und könnte sich als schlechte Praxis herausstellen. Wie ich gesagt habe, wurde feinkörnige Taktik Programmierung in Isabelle ein wenig aus der Nutzung in der letzten Jahren, obwohl ML ein integraler Bestandteil des Isabelle Rahmen ist. Wenn Sie eine konkretere Frage mit mehr Anwendungskontext stellen, können wir den Antiquotationsansatz überdenken.

Answer 2

Die Method Klasse erscheinen genug von einer Schnittstelle, um eine Taktik zu extrahieren, über ein cases_tactic wie folgt:

(* 
* 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 

oder alternativ als ein Anti-Zitat:

(* 
* 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 

und Aufbau in einer Theorie-Datei wie folgt:

setup {* 
    tactic_antiquotation_setup 
*} 

was dann sein kann wie folgt verwendet:

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

wie gewünscht.

Answer 3

Zusätzlich zu den anderen Antworten, ich denke, es ist erwähnenswert, dass es eine neue High-Level Taktik/Proof-Methode Bau Sprache (ähnlich wie Ltac in Coq) Eisbach in Isabelle2015, die leichter zu verstehen und zu pflegen soll .