如何在Isabelle中对map绑定执行fold及查键？是否有类Coq FMap模块？

Isabelle里有几个模块能满足你对find（查找）和fold（折叠）的需求，以下是最常用的选项：

Finite_Map 模块 #

位于HOL-Library.Finite_Map，是最接近Coq FMap的实现，专门处理有限映射：

• 查找操作：fm_lookup，传入键和映射即可获取对应的值（返回option类型），用法示例：fm_lookup k fm
• 折叠操作：fm_fold，遍历映射的所有键值对执行折叠逻辑，签名为('a => 'b => 'c => 'c) => 'a fmap => 'c => 'c

Mapping 模块 #

位于HOL-Library.Mapping，是一个通用的映射抽象类，适配多种映射实现：

• 查找操作：Mapping.lookup，对应你需要的find功能，适用于所有实现Mapping接口的映射类型
• 折叠操作：Mapping.fold，支持对映射的键值对进行折叠，签名为('k => 'v => 'a => 'a) => 'k => 'v mapping => 'a => 'a

AList 模块 #

如果你使用关联列表作为映射实现，HOL-Library.AList也提供对应功能：

• 查找操作：AList.lookup（要求键的类型具备相等性）
• 折叠操作：AList.fold，遍历列表中的键值对完成折叠

简单示例（Finite_Map） #

theory Map_Example
imports HOL-Library.Finite_Map
begin

(* 定义一个有限映射 *)
definition sample_fm :: "int fmap" where
  "sample_fm = fm_empty |⦇ 1 ↦ 10, 2 ↦ 20, 3 ↦ 30 ⦈"

(* 查找键2对应的值 *)
value "fm_lookup 2 sample_fm"  (* 输出: Some 20 *)

(* 折叠计算所有值的总和 *)
definition total_sum where
  "total_sum = fm_fold (λk v acc. acc + v) sample_fm 0"

value "total_sum"  (* 输出: 60 *)

end

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