Altes Isabelle-Projekt importiert ml-Datei mit 'Verwendungen' Wie soll ich das ersetzen?

Question

Ich habe ein altes Isabelle Projekt geerbt und möchte es auf dem neuesten Stand bringen, mit Isabelle 2016. zu arbeiten, wenn das Projekt es oft deine Datei beginnt beginnt:

theory my_theory 
imports Main uses "my_theory.ML" 
begin 
lemma my_lemma: ... 
by ... 
end 

Das Schlüsselwort verwendet scheint nicht mehr zu existieren, so ich das versucht habe zu ändern:

theory my_theory 
imports Main 
begin 
ML_file "my_theory.ML" 

lemma my_lemma: ... 
by ... 

end 

Dies schließt die Datei richtig, aber ich mit Fehlern in der ML-Datei am Ende, die in Beziehung gesetzt werden können oder auch nicht, wie: Undefined fact: "my_lemma" auf einer Linie Code mit @ {thm my_lemma}.

Ist meine Änderung, die ML-Datei mit ML_file Befehl korrekt zu enthalten? und hat dies Auswirkungen auf die ML-Fehler, die ich erhalte?

Answer 1

Ich bin nicht vertraut mit dem Schlüsselwort uses; das muss einige Zeit vorher fallen gelassen worden sein, bevor ich anfing, Isabelle zu benutzen.

ML_file sollte der Weg sein zu gehen; Sie müssen jedoch ML_filezwischen die begin und end Befehle schreiben, die die Theorie starten/abschließen. Darüber hinaus ist der ML_file Aufruf nach die Definition von etwas sein muss, die Sie in der ML-Datei verwenden (Konstanten, Fakten, Satz Sammlungen, simprocs, ...)

In Ihrem Beispiel, sollte es so aussehen:

theory my_theory 
imports Main 
begin 

lemma my_lemma: ... 
    by ... 

ML_file "my_theory.ML" 

end 

Beachten Sie, dass Isabelle viel ändert. Jeder ML-Code, den Sie haben - besonders wenn er so alt ist - wird wahrscheinlich viele Änderungen erfordern, bevor er mit modernen Isabelle-Versionen funktioniert. Es ist vielleicht einfacher, es von Grund auf neu zu schreiben. Deshalb sollten Isabelle-Projekte in die Archive of Formal Proofs gestellt werden, wo sie von den Entwicklern auf etwaige Änderungen im Isabelle-System aktualisiert werden. Alle Isabelle-Projekte außerhalb der AFP werden in wenigen Jahren der Bitfäule erliegen.