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))"

执行导出命令：

export_code constraint
    in SML module_name SML_constraint
    in Haskell module_name haskell_constraint

触发Wellsortedness错误：

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

替换为自然数类型并限定取值范围后导出成功，但需要保留原抽象类型的定义。

两种解决方法 #

方法1：为抽象类型添加enum类实例 #

Isabelle导出全称量词∀的代码时，要求目标类型属于enum类（即可枚举所有元素）。若type_a和type_b是有限集合，可直接用datatype定义枚举类型（自动生成enum实例）：

-- 直接枚举type_a的所有可能值
datatype type_a = A_One | A_Two | A_Three
-- 同理定义type_b
datatype type_b = B_One | B_Two

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))"

若需保留typedecl的抽象性，需手动为类型添加enum实例并实现枚举逻辑：

typedecl type_a
instance type_a :: enum by(intro_classes)

-- 定义type_a的所有元素列表（需根据实际场景填充）
definition enum_type_a :: "type_a list" where "enum_type_a = [A1, A2]"
-- 实现全称量词的枚举遍历逻辑
definition enum_all_type_a :: "('a ⇒ bool) ⇒ bool" where 
    "enum_all_type_a P = list_all P enum_type_a"

-- 重载全称量词操作
overloading all_type_a ≡ "ALL x::type_a. P x" begin
  definition "ALL x::type_a. P x ≡ enum_all_type_a P"
end

-- 对type_b执行相同的实例化操作
typedecl type_b
instance type_b :: enum by(intro_classes)
definition enum_type_b :: "type_b list" where "enum_type_b = [B1, B2]"
definition enum_all_type_b :: "('a ⇒ bool) ⇒ bool" where 
    "enum_all_type_b P = list_all P enum_type_b"
overloading all_type_b ≡ "ALL x::type_b. P x" begin
  definition "ALL x::type_b. P x ≡ enum_all_type_b P"
end

方法2：改写约束避免全称量词 #

原约束的语义等价于pair集合是aset × bset的子集，可直接用集合子集操作替代全称量词，无需依赖类型的可枚举性：

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 = (pair rcd ⊆ aset rcd × bset rcd)"

可在Isabelle中验证两种定义的等价性：

lemma constraint_equiv:
  "constraint rcd = (∀ a b. (a, b) ∈ pair rcd ⟶ (a ∈ aset rcd ∧ b ∈ bset rcd))"
  by(auto simp: constraint_def subset_def)

这种方法更通用，尤其适用于type_a/type_b为无限类型的场景，代码导出时只需遍历pair中的元素进行检查，无需枚举整个类型。

内容的提问来源于stack exchange，提问作者gfs