Как определить подтипы в Isabelle и что они означают?

Вопрос о подтипах в Изабель очень длинный здесь. Итак, мой простой вопрос заключается в том, как я могу определить тип B как подтип A, если я определяю A, как показано ниже:

typedecl A

Делая это, я хотел бы сделать все операции и отношения, определенные над A (здесь они не печатаются), доступными для элементов типа B.

Немного более сложный пример — определить B и C как подтипы A, так что B и C не пересекаются, а каждый элемент A относится либо к типу B, либо к типу C.

Спасибо


person qartal    schedule 11.11.2014    source источник


Ответы (1)


У Isabelle нет подтипов, хотя некоторые аспекты создания подтипов можно эмулировать, как описано в другом потоке. Если вы хотите использовать одну и ту же операцию для разных типов, вы можете изучить классы типов Isabelle.

person Andreas Lochbihler    schedule 11.11.2014
comment
спасибо, есть ли средство доказательства теорем, основанное на логике, поддерживающей подтипы, которые я могу использовать? - person qartal; 11.11.2014