Eu gostaria de saber sobre os subtipos de Isabelle / HOL. Eu explico um pouco sobre por que é importante para mim na minha resposta parcial à minha última pergunta:

Tentando tratar classes de tipos e sub-tipos como conjuntos e subconjuntos

Basicamente, eu só tenho um tipo, então pode ser útil para mim explorar o poder dos tipos HOL através de subtipos.

Fiz buscas na documentação da Isabelle, na Web e nas listas de correio da Isabelle. A palavra "subtipo" é usada, embora não muito, e parece que não é uma parte super importante do vocabulário de Isabelle.

Em parte, gostaria apenas de saber como usar a palavra "subtipo" corretamente. Eu não quero estar chamando algo de um subtipo em Isabelle que não seja um subtipo.

De acordo com a Wiki, a subtipagem é específica da linguagem:

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

Importante última parte; os comandos por favor

Alguém pode me dar uma lista dos comandos do Isar que criam os subtipos do Isar? Estou investigandotypedef, como explicado na pergunta acima. Estou inclinado a chamar essa subtipagem, masisar-ref.pdf não usa "subtipo" ao explicar o comando.

Se existem outras maneiras de criar os subtipos Isabelle / HOL, gostaria de saber.