Untyped set operations in Isabelle

I have the following code in Isabelle:

typedecl type1
typedecl type2

consts 
  A::"type1 set"
  B::"type2 set"

When I want to use union operation with A and B as bellow:

axiomatization where
 c0: "A  ∩ B = {}"

Since A and B are sets of different types, I get an error of clash of types which makes sense!

I am wondering if there are any counterparts for set operations that they implicitly consider their operands as pure sets (i.e., ignore their types), therefore something like A ∩' B become possible ( ∩' is ∩ operation counterpart in above sense).

PS: Another workaround is type casting that I wrote this as a separate question here to better organize my questions.

Thanks

Solution

Sets in Isabelle/HOL are always typed, i.e., they contain only elements of one type. If you want to have untyped sets, you have to switch to another logic such as Isabelle/ZF.

Similarly, all values in HOL are annotated with their type, and this is fundamental to the logic. Equality, for example, can only be applied to two values of the same type. Hence, there is no notion of equality between values of different types. Consequently, there is no set operation that ignores the type of values, because such an operation would necessarily have to know how to identify values of different types.