Re: [isabelle] Creating terms from sets

Isabelle/HOL provides fold functionals for sets, which can be used provided the result does not depend on the order in which set elements are considered.

For details, see this paper:

Tobias Nipkow and L. C. Paulson. Proof Pearl: Defining Functions Over Finite Sets. In: Joe Hurd and Tom Melham (editors),Theorem Proving in Higher Order Logics (Springer LNCS 3603, 2005), 385–396.


Larry Paulson

On 2 Apr 2007, at 13:27, Jesper Bengtson wrote:

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.