¿Qué es un subtipo Isabelle / HOL? ¿Qué comandos de Isar producen subtipos?
Me gustaría saber acerca de los subtipos Isabelle / HOL. Explico un poco sobre por qué es importante para mí en mi respuesta parcial a mi última pregunta SO:
Intentar tratar clases y subtipos de tipos como conjuntos y subconjuntos
Básicamente, solo tengo un tipo, por lo que podría ser útil si pudiera explotar el poder de los tipos HOL a través de subtipos.
He realizado búsquedas en la documentación de Isabelle, en la Web y en las listas de correo de Isabelle. La palabra "subtipo" se usa, aunque no mucho, y parece que no es una parte muy importante del vocabulario de Isabelle.
En parte, solo me gustaría saber cómo usar la palabra "subtipo" correctamente. No quiero llamar a algo un subtipo en Isabelle que no sea un subtipo.
Según el Wiki, el subtipo es específico del idioma:
https://en.wikipedia.org/wiki/Subtyping
Importante última parte; los comandos por favor¿Alguien me puede dar una lista de los comandos de Isar que crean los subtipos de Isar? Estoy investigandotypedef
, tal como se explica en la pregunta vinculada anteriormente. Me inclino a llamar a ese subtipo, peroisar-ref.pdf no usa "subtipo" al explicar el comando.
Si hay otras formas de crear los subtipos Isabelle / HOL, me gustaría saberlo.