Isabelle/HOLにsubset typeないかな〜と思って「Isabelle/HOL subset type」とか「Isabelle/HOL comprehension」とかで調べていましたが、全然見つからず、最終的にtypedefがその役割を担っていることが分かりました。これがあれば集合から型を作れるので、便利です。
Isabelle/HOLには他にもquotient typeがあるのですが、これはeffectiveでしょうか、そうではないのでしょうか。いずれ確認しましょう。今から楽しみですね。