*To*: Jesper Bengtson <jesperb at it.uu.se>*Subject*: Re: [isabelle] Creating terms from sets*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 3 Apr 2007 11:40:35 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4610F6C1.7040704@it.uu.se>*References*: <4610F6C1.7040704@it.uu.se>

For details, see this paper:

<http://www.cl.cam.ac.uk/~lp15/papers/Reports/TPHOLs05.pdf> Larry Paulson On 2 Apr 2007, at 13:27, Jesper Bengtson wrote:

Greetings allI am currently working on proving soundness and completeness forthe axiomatisation of strong late bisimilarity of the pi calculus.A key notion here is that of summands which basically is a set ofall subterms which are constructed from the +-operator. I would,however, need a function which creates a term from the set of itssummands, 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 definedrelations the best way to do this?Thank you for your time /Jesper

**Follow-Ups**:**Re: [isabelle] Creating terms from sets***From:*Stefan Berghofer

**References**:**[isabelle] Creating terms from sets***From:*Jesper Bengtson

- Previous by Date: [isabelle] Subclasses with auxiliary defns
- Next by Date: Re: [isabelle] [polyml] Problems compiling polyml 5 on sparc/solaris
- Previous by Thread: [isabelle] Creating terms from sets
- Next by Thread: Re: [isabelle] Creating terms from sets
- Cl-isabelle-users April 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list