Was ist ein Isabelle / HOL-Subtyp? Welche Isar-Befehle erzeugen Untertypen?

Ich würde gerne etwas über Isabelle / HOL-Subtypen erfahren. In meiner teilweisen Antwort auf meine letzte SO-Frage erkläre ich ein wenig, warum es mir wichtig ist:

Versuchen, Typklassen und Untertypen wie Mengen und Teilmengen zu behandeln

Grundsätzlich habe ich nur einen Typ, daher könnte es für mich nützlich sein, wenn ich die Leistung von HOL-Typen durch Subtypen ausnutzen könnte.

Ich habe in der Isabelle-Dokumentation, im Web und in den Isabelle-Mailinglisten gesucht. Das Wort "Subtyp" wird verwendet, wenn auch nicht viel, und es scheint, als sei es kein überaus wichtiger Teil des Isabelle-Vokabulars.

Zum Teil möchte ich nur wissen, wie man das Wort "Subtyp" richtig verwendet. Ich möchte in Isabelle nicht etwas als Subtyp bezeichnen, das kein Subtyp ist.

Laut Wiki ist die Untertypisierung sprachspezifisch:

https://en.wikipedia.org/wiki/Subtyping

Wichtiger letzter Teil; die befehle bitte

Kann mir jemand eine Liste der Isar-Befehle geben, mit denen Isar-Untertypen erstellt werden? Ich untersuchetypedef, wie in der Frage oben erläutert. Ich neige dazu, diese Untertypisierung zu nennen, aberisar-ref.pdf verwendet "subtype" nicht zur Erklärung des Befehls.

Wenn es andere Möglichkeiten gibt, Isabelle / HOL-Untertypen zu erstellen, würde ich gerne wissen.

Antworten auf die Frage(1)

Ihre Antwort auf die Frage