Chciałbym wiedzieć o podtypach Isabelle / HOL. Wyjaśniam trochę, dlaczego jest to dla mnie ważne w częściowej odpowiedzi na moje ostatnie pytanie SO:

Próba traktowania klas i podtypów typu, takich jak zestawy i podzbiory

Zasadniczo mam tylko jeden typ, więc może mi się przydać, gdybym mógł wykorzystać moc typów HOL poprzez podtypy.

Szukałem w dokumentacji Isabelle, w Internecie i na listach dyskusyjnych Isabelle. Używa się słowa „podtyp”, choć niewiele, i wydaje się, że nie jest to bardzo ważna część słownictwa Isabelle.

Po części chciałbym tylko wiedzieć, jak poprawnie użyć słowa „podtyp”. Nie chcę nazywać czegoś podtypem Isabelle, który nie jest podtypem.

Zgodnie z Wiki podsystem jest specyficzny dla języka:

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

Ważna ostatnia część; polecenia proszę

Czy ktoś może mi podać listę poleceń Isar, które tworzą podtypy Isar? Śledzętypedef, jak wyjaśniono w pytaniu powiązanym z powyższym. Jestem skłonny nazwać to podtypowaniem, aleisar-ref.pdf nie używa „podtypu” podczas wyjaśniania polecenia.

Jeśli istnieją inne sposoby tworzenia podtypów Isabelle / HOL, chciałbym to wiedzieć.