How type casting is possible in isabelle

Question

Supose I have the following code in Isabelle:

typedecl type1
typedecl type2
typedecl type3

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! As a workaround I want to type cast A and B to both become sets of type "type3", so I can apply union operations to them. How this type casting is possible in isabelle in this specific example, and how it is possible in general.

Thanks

Answer 1

Type casts require explicit functions between the types, say,

consts cast_A :: "type1 ⇒ type3"
consts cast_B :: "type2 ⇒ type3"

Using these functions, you can state your axiom as follows:

axiomatization where
 c0: "cast_A ` A ∪ cast_B ` B = {}"

Isabelle can also automatically insert such coercion functions, but you have to enable it first:

declare
  [[coercion_enabled]]
  [[coercion cast_A, coercion cast_B]]
  [[coercion_map image]]

These three declarations do the following

1. Enable the coercion inference algorithm.
2. Declare the functions cast_A and cast_B as coercion functions, i.e., coercion inference may insert them if needed.
3. Declare the function image (written infix as ` ) as a map function for coercions. These map functions allow the inference system to apply coercions to the parameters of type constructors. Here, the declaration allows to coerce sets by applying a coercion function to all its elements.

With these preparations, the axiom can be written as before:

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

However, coercion insertion is only a means to remove clutter from the input notation. The coercions are explicit in the theorem and your proofs have to deal with them. If you look at the theorem c0, you will see the coercions.

Finally a comment on these kinds of embedings. The predefined sum type type1 + type2 consists exactly of all the elements of type type1 and those of type type2 with the cast functions Inl and Inr, respectively. So, if your type type3 has no other purpose than being the union of type1 and type2, the sum type might be more convenient to work with.

Also note that your axiom expresses that the sets A and B are empty.