Нетипизированные операции над множествами в Изабель

Question

У меня есть следующий код в Изабель:

typedecl type1
typedecl type2

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

Когда я хочу использовать операцию объединения с A и B, как показано ниже:

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

Так как A и B - это наборы разных типов, я получаю ошибку столкновения типов, которая имеет смысл!

Мне интересно, есть ли какие-нибудь аналоги для операций над множествами, которые они неявно рассматривают своими операндами как чистые множества (то есть игнорируют их типы), поэтому становится возможным что-то вроде A ∩' B ( ∩' - это counter аналог операции в вышеприведенном смысле).

PS: Еще один обходной путь - приведение типов, который я написал здесь как отдельный вопрос, чтобы лучше организовать свои вопросы.

Спасибо

Answer 1

Наборы в Изабель /HOL всегда набираются, т. Е. Содержат только элементы одного типа. Если вы хотите иметь нетипизированные наборы, вы должны переключиться на другую логику, такую ​​как Isabelle/ZF.

Точно так же все значения в HOL аннотируются их типом, и это является фундаментальным для логики. Равенство, например, может применяться только к двум значениям одного типа. Следовательно, нет понятия равенства между значениями разных типов. Следовательно, не существует операции set, которая игнорирует тип значений, потому что такая операция обязательно должна знать, как идентифицировать значения разных типов.