Isabelle に次のコードがあるとします。
typedecl type1
typedecl type2
typedecl type3
consts
A::"type1 set"
B::"type2 set"
以下のように A と B でユニオン演算を使用したい場合:
axiomatization where
c0: "A ∪ B = {}"
A と B は異なる型のセットなので、型の衝突のエラーが発生します。これは理にかなっています! 回避策として、型キャスト A と B の両方が型 "type3" のセットになるようにしたいので、それらにユニオン操作を適用できます。この特定の例の isabelle でこのタイプのキャストがどのように可能であるか、および一般的にどのように可能であるか。
ありがとう