Entfaltung automatisch eine Aufzeichnung Definition, wenn Accessor verwendet wird

Question

Angenommen, ich habe eine Satzart und eine konstante Definition dieser Art, wie:

record r = 
    r_x :: int 
    r_y :: int 
    r_z :: int 

definition "a ≡ ⦇r_x=1, r_y=2, r_z=3⦈" 

Jetzt möchte ich etwas über ein beweisen, zum Beispiel:

lemma "r_x a + r_y a = 3" 

Derzeit mache ich solche Beweise durch Vereinfachung Lemmata für die verschiedenen Zugriffsmethoden definieren:

schematic_goal [simp]: "r_x a = ?x" by (simp add: a_def) 
schematic_goal [simp]: "r_y a = ?x" by (simp add: a_def) 
schematic_goal [simp]: "r_z a = ?x" by (simp add: a_def) 

Meine Frage ist: Kann ich diese Lemmas automatisch irgendwie ableiten? Oder gibt es eine Methode zum Entfalten von Definitionen, wenn sie mit einer Accessor-Funktion verwendet wird?

Ich möchte das ursprüngliche Lemma nicht beweisen, indem ich a_def hinzufüge, weil ich normalerweise nur die Verwendungen von a entfalten möchte, wo ein Accessor verwendet wird.

Ich möchte keine Abkürzung verwenden, denn dann würde der Simplifier komplizierte Unterbegriffe innerhalb des Datensatzes bearbeiten.

Answer 1

Es gibt keine integrierte Möglichkeit, die Selektorsätze für benutzerdefinierte Datensätze in Isabelle2016 automatisch abzuleiten. Wenn Sie so etwas wie dies für mehrere Definitionen des gleichen Satztyp zu tun haben, können Sie die Ableitung ein bisschen wie folgt automatisieren:

lemma r_sel: 
    assumes "r ≡ ⦇r_x=x, r_y=y, r_z=z⦈" 
    shows "r_x r = x" "r_y r = y" "r_z r = z" 
using assms by(simp_all) 

lemmas a_sel [simp] = r_sel[OF a_def] 

Das Lemma r_sel wird nur einmal benötigt für jeden Datensatztyp. Dann erhalten Sie die Instanziierung (hier a_sel) mit einer Zeile. Für Record-Transformer (d. H. Etwas wie f r = r(|r_x = foo|)) können Sie ein entsprechendes Lemma r_upd beweisen und die Instanzen für Ihre Transformatoren ableiten.

Wenn Sie noch mehr Automatisierung (oder Flexibilität) benötigen, müssen Sie die Ableitung selbst in Isabelle/ML implementieren. Im Allgemeinen könnte man die Ctr_sugar Infrastruktur verwenden, um solche Selektorableitungen zu erstellen, aber das Aufzeichnungspaket in seiner aktuellen Form funktioniert nicht gut zusammen mit Ctr_sugar.