[isabelle] fold definitions over sets

Dear all,

recently, I came across an alternative way to define
a fold on finite sets. In contrast to the Isabelle
library version (discussed in the recent TPHOLs Paper),
it has a slightly more general type:

   fold : [['a, 'b] => 'b, 'b, 'a set] => 'b

but still fulfills (for finite sets S) the computational

   fold f b {} = b

   \<forall> a b c. (f a (f b c)) = (f b (f a c)) ==> 
       fold f b (insert a S) = f a (fold f b (S - {a}))

It does neither assume ACn, although 
\<forall> a b c. (f a (f b c)) = (f b (f a c)) 
implies this, if f has type instance ['a, 'a] => 'a
and is furthermore right-neutral.

It is strictly more general: you can define the
cardinality of finite sets by this fold, but not
by the old one, for example.

The same algorithmic scheme would work for multi-sets too,
so one could think of using overloading for it.

A) Is this something widely known? (Refs ?)
   Is it existing in other libraries of HOL systems?

B) Wouldn't it be a better candidate
   for the Isabelle/HOL library?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.