Цитируя взаимно-рекурсивное семейство типов данных

Question

Возможно ли классифицировать семейство взаимно-рекурсивных типов данных в Isabelle/HOL с использованием механизма quotient_type с семейством отношений эквивалентности?

Если да, то есть ли хороший пример этого где-то уже? Поиск документации Изабель и документ, описывающий обновленный механизм quotient_type, не очень полезны.

Answer 1

Команда quotient_type может обрабатывать только один тип за раз. Если вы хотите сделать частное по нескольким взаимным типам, вы должны сделать кодировку и декодирование вручную, но это довольно просто.

Предположим, что два ваши типы t1 и t2 с отношениями эквивалентности r1 :: t1 => t1 => bool и r2 :: t2 => t2 => bool. Затем

quotient_type q = "t1 + t2"/"rel_sum r1 r2" 

- комбинированный тип фактора. Затем можно определить два факторизации как проекции:

lift_definition Abs1 :: "t1 ⇒ q" is "Inl" . 
lift_definition Abs2 :: "t2 ⇒ q" is "Inr" . 

typedef q1 = "range Abs1" by blast 
typedef q2 = "range Abs2" by blast 

С setup_lifting, вы можете зарегистрировать q1 и q2 с пакетом подъемного тоже. Затем вы получаете приличную автоматизацию для подъема доказательств и определений. Вам просто нужно сделать две ступени подъема (сначала от t1 + t2 до q, а затем от q до q1 или q2) для определений и двух невыпадающих шагов для доказательств.