[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


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