Re: [isabelle] Recursion on finite sets



If f does not take the remaining set A as an argument, then you can
define such a recursion operator completelty along the same lines as the
 fold operator currently provided. It will require f to be
left-commutative: f a (f b c) = f b (f a c). See the TPHOLs 2005 paper
by Larry and me for more details. In fact, such an operator would be
welcome.

If the same development could be generalized to your f I am not sure.

Tobias

Andreas Lochbihler wrote:
> Hi all,
> 
> I am looking for some way of defining a function recursively over finite
> sets.
> For a datatype t, the datatype package automatically generates a
> recursion operator t_rec with which primitive-recursively functions over
>  that datatype can be defined. For finite sets, I haven't found anything
> similar. The only thing I have found is the fold combinator in
> Finite_Set of type "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set =>
> 'a" where "fold f g z A" is f folded over the (multiset) image of A
> under g with initial value z.
> But I would rather like to have some function finite_rec :: "('b set =>
> 'b => 'a => 'a) => 'a => 'b set => 'a"  that satisfies
> 
> "finite_rec f z {} = z" and
> "[| finite A; ~ (x : A) |]
>  ==> finite f z (insert x A) = f A x (finite_rec f A z)"
> 
> for all "well-formed" functions f.
> 
> Is there already something there that I can use like finite_rec or can
> finite_rec be somehow defined using existing fold?
> 
> Best,
> Andreas





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