对码公式的左边

Question

我需要使用nat_plus_commute.fold_set_fold_remdups码公式，而不是Finite_Set.fold_def部分应用的不断：

interpretation nat_plus_commute: comp_fun_commute "plus :: nat ⇒ nat ⇒ nat" 
    by standard auto 

declare Finite_Set.fold_def [code del] 
declare nat_plus_commute.fold_set_fold_remdups [code] 

的问题是，第一个方程只被定义为plus操作，所以我得到以下警告：

Partially applied constant "Groups.plus_class.plus" on left hand side of equation, in theorem: 
Finite_Set.fold op + ?y (set ?xs) ≡ fold op + (remdups ?xs) ?y 

至于导致下面的语句

value "Finite_Set.fold plus 0 (set [1::nat, 2])" 

返回异常：

exception Fail raised (line 29 of "generated code"): Finite_Set.fold 

是否可以使用特定的操作（plus）和类型（nat）一个专门的代码方程？

Answer 1

我不能肯定希望要实现，但要注意Finite_Set.fold是一种低层次的结构，它与实际可用的属性等操作只能以相当大的努力，参见导出理论src/HOL/Finite_Set.thy和src/HOL/Groups_Big.thy有一个粗略的想法。

有关有限集合和列表求和，还有总和和sum_list其中已经装备了代码方程。