在Isabelle中导出带有通用量词的定义代码

我试图使用Isabelle定理证明器的代码提取工具从中导出代码。我试图提取的代码基于一个完整性约束,该约束从由两种不同类型的集合以及一组这些类型的对组成的记录中返回一个布尔值,如下所示:

typedecl type_a
typedecl type_b

record my_record =
    aset :: "type_a set"
    bset :: "type_b set"
    pair :: "(type_a × type_b) set"

definition constraint :: "my_record ⇒ bool" where"
    constraint rcd = (∀ a b. (a, b) ∈ pair rcd ⟶ (a ∈ aset rcd ∧ b ∈ bset rcd))"

以下是我尝试将代码提取到Haskell和SML文件的地方:

export_code constraint
    in SML module_name SML_constraint
    in Haskell module_name haskell_constraint

但这样做时,我会得到一个排序错误,我认为这是由于我使用的类型不可枚举造成的?这是它的样子:

Wellsortedness error
(in code equation constraint ?rcd ≡ 
    ∀a b. (a, b) ∈ pair ?rcd ⟶ a ∈ aset ?rcd ∧ b ∈ bset ?rcd):
Type type_a not of sort enum
No type arity type_a :: enum

值得注意的是,如果我更换了 type_a 和 type_b 具有自然数的类型,并在约束中为它们定义一个有限的值范围,例如最大值为100:

record my_record =
    aset :: "nat set"
    bset :: "nat set"
    pair :: "(nat × nat) set"

definition constraint :: "my_record ⇒ bool" where
    "constraint rcd = (∀ a < 100. ∀ b < 100. (a, b) ∈ pair rcd ⟶ (a ∈ aset rcd ∧ b ∈ bset rcd))"

为此,代码导出是有效的。但是,我需要使用我之前定义的抽象类型。有没有一种方法可以枚举这些类型,这样就不会发生错误,或者以一种不需要量词(这似乎是错误的原因)但其含义保持不变的不同方式定义约束?