推测一个相互递归的数据类型家族

Question

是否有可能使用quotient_type机制和一族等价关系对Isabelle/HOL中的一系列相互递归数据类型进行商数？

如果是这样，那么这个地方有没有好的例子？搜索Isabelle文档以及描述改进的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）以获取定义和两个未举证步骤。