如何映射映射的键和值？

我需要定义将键映射和有限地图的值转换为一组键 - 值对的一个函数：如何映射映射的键和值？

theory Test 
    imports Main "~~/src/HOL/Library/Finite_Map" 
begin 

definition denorm :: "('a, 'b) fmap ⇒ ('a × 'b) fset" where 
    "denorm m ≡ " 

end

的问题是，我不能定义通过递归此功能，因为fmap ISN是一种归纳数据类型，它没有任何构造函数。

我想fmap被表示为内部对的列表。是否有可能将fmap转换成列表？我需要一个fmap_of_list函数的反函数。

来源

2017-09-05 Denis

一种可能的方式是组成图像，域和查找：表达式

λ m. (λ k. (k, the (fmlookup m k))) |`| fmdom m

具有所需类型

('a, 'b) fmap ⇒ ('a × 'b) fset

和应计算所希望的设定为地图m。

来源

2017-09-05 19:42:58

这个功能已经存在：

fset_of_fmap :: "('a, 'b) fmap ⇒ ('a × 'b) fset"

来源

2017-09-06 07:25:03 larsrh

在Isabelle2016-1我找不到它。也许它在最新的不稳定版本？ – Denis

是的，我在2017年添加了它，其中第一个候选版本可用。 – larsrh

如何映射映射的键和值？

回答

相关问题