# [isabelle] Creating terms from sets

Greetings all

`I am currently working on proving soundness and completeness for the
``axiomatisation of strong late bisimilarity of the pi calculus. A key
``notion here is that of summands which basically is a set of all subterms
``which are constructed from the +-operator. I would, however, need a
``function which creates a term from the set of its summands, i.e.
``SUM(summands P) = P.
`
On paper, the function would look like this:
SUM {} = Nil
SUM (insert P S) = P + (SUM S).

`Not too complex, but what is the best way to do this in isabelle? Is
``there a way to create this function, or is inductively defined relations
``the best way to do this?
`
Thank you for your time
/Jesper

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