如何合并有限映射集？

Question

我可以按如下方式合并两个有限映射：

value "fmadd
  (fmap_of_list [(1::nat,2::nat)])
  (fmap_of_list [(2::nat,3::nat)])"

但是当我尝试合并一组地图时：

value "ffold fmadd fmempty {|
  fmap_of_list [(1::nat,2::nat)],
  fmap_of_list [(2::nat,3::nat)]|}"

我收到以下错误：

Wellsortedness error:
Type nat ⇀⇩f nat not of sort finite
No type arity fmap :: finite

根据fmap的定义，它的定义域是有限的：

typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a ⇀ 'b) set"
  morphisms fmlookup Abs_fmap
proof
  show "Map.empty ∈ {m. finite (dom m)}"
    by auto
qed

但为什么 fmap 不是有限的？

Answer 1

回答您的直接问题：

But why fmap is not finite?

每个fmap都有一个有限域，但不一定只有有限多个('a, 'b) fmap类型的值。例如，从 nat 到 nat.

有无限多个有限大小的映射

您观察到的问题比这更严重：我相信 ffold 没有正确的代码设置。如果我尝试计算

ffold funion fempty {|
  fset_of_list [(1::nat,2::nat)],
  fset_of_list [(2::nat,3::nat)]|}

...错误信息类似。现在，我建议在列表中将其重写为 fold：

fold fmadd [
  fmap_of_list [(1::nat,2::nat)],
  fmap_of_list [(2::nat,3::nat)]] fmempty

它不一样，但它可能对您的应用程序有用。

如何合并有限映射集？

How to merge set of finite maps?

isabelle