Fehler beim Definieren von Dataype in Isabelle

Question

Ich arbeite an einer Theorie, die Topologie verwendet, und es wäre hilfreich, eine Art von offenen Sätzen zu haben. Ich habe versucht, die folgenden:

context topology 
begin 
typedef openset = "{U. U ∈ T}" 
end 

wo Topologie ein Gebietsschema und das Kontextbefehl richtig die Ausgabe

locale topology = 
    fixes T :: "'a set set" 
    assumes "topology T" 

Allerdings gibt, ich die folgende Fehlermeldung erhalten:

Extra type variables in representing set: "'a" The error(s) above occurred in typedef "openset"

Was bedeutet es bedeuten? Hier ist T nur eine Menge von Mengen und ich möchte einen Typ haben, der aus den Mengen besteht, die zu T gehören. Gibt es eine Möglichkeit, dies zu tun?

Answer 1

Zunächst ist dies kein Datentyp - es ist eine 'normale' Typdefinition.

Das Problem ist, dass Sie keine Typdefinitionen haben können, die von den lokalen Parametern abhängen. Die logischen Grundlagen von Isabelle erlauben so etwas im Moment nicht. Vgl. auch diese Frage: What Kind of Type Definitions are Legal in Local Contexts?