In einer Isabelle-Theoriedatei kann ich einfache einzeilige Taktiken wie die folgenden schreiben:
%Vor% Ich finde jedoch, wenn ich anfange, ML-Code zu schreiben, um Beweise zu automatisieren, um ein ML tactic -Objekt zu erzeugen, werden diese Einzeiler ziemlich ausführlich:
Gibt es eine einfachere Möglichkeit, die einfache einzeilige Taktik auf der Isabelle / ML-Ebene zu schreiben?
Zum Beispiel wäre so etwas wie ein Anti-Zitat: @{tactic "clarsimp simp: split_def split: prod.splits"} , das eine Funktion vom Typ context -> tactic erzeugt, eine ideale Lösung.
Ich sehe eine Vielzahl von Möglichkeiten, es hängt ein wenig vom Kontext Ihrer Anwendung ab, 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. Vergleichen Sie zum Beispiel die Menge an benutzerdefinierten Taktiken in einem ziemlich kleinen HOL-Bali ( begann im Jahr 1997) mit den großen JinjaThreads in AFP (begonnen 2007 und bis vor kurzem fortgesetzt).
Das Verschachteln von ML-Antiquatiken wie @{tactic} würde im Prinzip funktionieren, aber Sie würden schnell auf weitere Fragen stoßen, etwa was passiert, wenn Ihre Theoremargumente wieder Isar oder ML-Quelle sein sollten.
Anstelle antiquoter taktischer Bausteine in ML, ist ein grundlegenderer Ansatz, das Beweisverfahren in Isar
Hier habe ich zuerst eine konventionelle foo_tac -Definition in Isabelle / ML gemacht und dann die übliche Isar-Methode als Beweismethode eingearbeitet. Letzteres bedeutet, dass Wrapper wie SIMPLE_METHOD dafür sorgen, dass "verkettete Fakten" in den Zielstatus verschoben werden, und CHANGED , um sicherzustellen, dass die Isar-Methode Fortschritte macht (wie simp oder auto ).
Das foo_tac -Beispiel geht davon aus, dass Ihre Änderung des Kontextes (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 ausgefeilt ist. Weitere grundlegende Argument-Parser sind im Abschnitt "Definieren von Beweismethoden" des isar-ref Handbuchs beschrieben . Sie sollten sich auch die vorhandenen Beispiele anschauen, indem Sie die Quellen nach method_setup (in Isabelle / Isar) oder Method.setup (in Isabelle / ML) durchsuchen.
Wenn Sie immer noch ML-Antiqua statt der konkreten Methodensyntax machen wollen, könnte man eine Variante von @{context} ausprobieren, die Modifikatoren wie folgt zulässt:
Das ist ein bisschen spekulativ, an Ort und Stelle erfunden und könnte sich als schlechte Übung herausstellen. Wie ich bereits sagte, wurde die feinkörnige Taktik-Programmierung in Isabelle in den letzten Jahren etwas unbrauchbar, obwohl ML ein integraler Bestandteil des Isabelle-Frameworks ist. Wenn Sie eine konkretere Frage mit mehr Anwendungskontext stellen, können wir den Antiquotationsansatz überdenken.
Die Method -Klasse scheint genug von einer Schnittstelle zu bieten, um eine Taktik über eine cases_tactic wie folgt herauszuziehen:
oder alternativ als Anti-Zitat:
%Vor%und setup in einer Theorie-Datei wie folgt:
%Vor%was dann wie folgt verwendet werden kann:
%Vor%wie gewünscht.
Zusätzlich zu den anderen Antworten ist es meiner Meinung nach erwähnenswert, dass es eine neue High-Level-Taktik / Beweis-Methode gibt (ähnlich wie Ltac in Coq), genannt Eisbach in Isabelle2015, die leichter zu verstehen und zu pflegen ist.