Isabelle中下标式可实例化定义的用法及资料查询

核心本质：参数化容器绑定 #

你看到的_fs后缀并非单纯命名装饰，它是Isabelle/HOL中参数化数据类型结合特定容器类型的惯用写法，核心是通过后缀明确数据类型依赖的容器实现（这里fs对应fset有限集合类型），本质是利用Isabelle的类型系统实现可替换的容器实例化。

详细信息获取渠道 #

• 你参考的《(Co)datatype定义教程》后续章节（第3章及以后）：专门讲解了递归类型、参数化datatype与容器类型的结合规则，包含这类后缀式实例化的具体实现逻辑。
• Isabelle/HOL标准库源码：查看~~/src/HOL/Library/FSet.thy文件，里面有大量_fs后缀的类型定义，能直接看到这类绑定的实际写法。
• 《Programming and Proving in Isabelle/HOL》教程：其中递归类型与抽象容器的章节，有分步的实例化示例。

如何使用这类下标式定义 #

1. 基础绑定：直接关联容器类型 #

以tree_fs为例，它是将树的子节点集合绑定到fset的实例，写法拆解：

datatype 'a tree_fs = Node_fs (lbl_fs:'a) (sub_fs: "'a tree_fs fset")

若要替换为其他容器（比如普通列表list），只需修改后缀和容器类型：

datatype 'a tree_list = Node_list (lbl_list:'a) (sub_list: "'a tree_list list")

2. 类型类实现通用定义 #

如果需要避免重复写datatype定义，可通过类型类约束实现通用树类型，再为不同容器做实例化：

class container = fixes empty :: "'a" and insert :: "'b ⇒ 'a ⇒ 'a"
datatype 'a tree = Node (lbl:'a) (sub: "'a tree :: container")

为fset、list等容器实现container类型类的实例后，即可自动适配对应的树类型。

3. 局部化（Locale）封装实例 #

局部化是Isabelle实现参数化实例的常用方式，通过Locale绑定容器类型和操作，再生成对应的数据类型：

locale tree_container =
  fixes container_type :: "'a ⇒ 'b"
  fixes empty_container :: "'b"
begin
datatype 'a tree = Node (lbl:'a) (sub: "'a tree container_type")
end

(* 实例化到fset *)
interpretation tree_fset: tree_container "λx. x fset" "{}"
(* 此时得到tree_fset.tree，对应之前的tree_fs *)

关键注意事项 #

• 后缀是社区约定而非语法强制，统一后缀能提升代码可读性，明确类型依赖的容器。
• 递归类型与容器结合时，需确保容器支持递归类型实例化（比如fset支持递归，部分简单容器可能不允许）。

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