如何合并一组有限地图？

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 

这是不一样的，但它可能是您的应用程序非常有用。