Нетипизированные набор операций в Isabelle

Question

У меня есть следующий код в Isabelle:

typedecl type1 
typedecl type2 

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

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

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

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

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

PS: Другим обходным способом является литье типа, которое я написал в качестве отдельного вопроса here, чтобы лучше организовать мои вопросы.

Благодаря

Answer 1

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

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