Klasseninstanzen in Isabelle drucken/abfragen

Question

Ich fange gerade mit Isabelle an. Ich habe eine Datei wie folgt aus:

theory Z 
    imports Main Int 
begin 

value "(2::int) + (2::int)" 

lemma "(n::int) + (m::int) = m + n" 
apply(auto) done 

print_locale comm_ring_1 
print_interps comm_ring_1 

end 

Die meisten dieser Werke wie ich erwartet hatte: Isabelle sagt mir, dass 2 + 2 = 4 ist, und er weiß, wie das zu beweisen, n + m = m + n, und er druckt die Axiome für einen kommutativen Unitalring.

Allerdings erwartete ich, dass die Zeile "print_interps comm_ring_1" dazu führen würde, dass Isabelle weiß, dass die Ganzzahlen eine Instanz der Klasse comm_ring_1 sind (da diese Tatsache in der Datei Int.thy in der Standardbibliothek, die wir importiert haben). Aber Isabelle sagt mir das nicht.

Gibt es eine andere Möglichkeit, Isabelle zu bitten, alle Instanzen von comm_ring_1 aufzulisten, von denen sie weiß? Oder um spezifisch abzufragen, ob int eine Instanz von comm_ring_1 ist? Ich habe im Referenzhandbuch nach einem solchen Befehl gesucht, kann aber keinen finden.

Answer 1

Jede Typenklasse in Isabelle definiert ein Gebietsschema mit demselben Namen, aber sie sind nicht identisch. Die Befehle print_locale und print_interps berücksichtigen nur den Gebietsschemaaspekt einer Typklasse. Die Typklassenregistrierung mit instance oder instantiation registriert den Typ nicht als Interpretation dieses Gebietsschemas. Daher listet print_interps nicht die Typen auf, die sich als Instanzen von Typklassen erwiesen haben. Dies geschieht mit dem Befehl print_classes.