*To*: Jesper Bengtson <jesperb at it.uu.se>*Subject*: Re: [isabelle] Creating terms from sets*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Thu, 05 Apr 2007 10:24:44 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <648847FF-46A0-4443-8928-D6DEE2D9A692@cam.ac.uk>*Organization*: Technische Universität München*References*: <4610F6C1.7040704@it.uu.se> <648847FF-46A0-4443-8928-D6DEE2D9A692@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.13) Gecko/20060417

Lawrence Paulson wrote:

Isabelle/HOL provides fold functionals for sets, which can be usedprovided the result does not depend on the order in which set elementsare considered.

Hello Jesper, this is probably not the case for your "+" function. If it is a constructor of the datatype of processes of the Pi-calculus, it is neither associative nor commutative (at least with respect to the "ordinary" equality).

On 2 Apr 2007, at 13:27, Jesper Bengtson wrote: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? Isthere a way to create this function, or is inductively definedrelations the best way to do this?

Since there may be many ways of forming a sum from the elements of a set, using an inductive definition is probably the best option. You could either define consts sum :: "proc set => proc set" inductive "sum S" intros Nil: "Nil : sum S" Plus: "p : S ==> q : sum S ==> (p + q) : sum S" if you don't care how many elements of S are used in the process, or consts sum' :: "(proc set * proc) set" inductive "sum'" intros Nil: "({}, Nil) : sum'" Plus: "p : S ==> (S - {p}, q) : sum' ==> (S, p + q) : sum'" if you want each element in S to be used exactly once. The fold functional for sets mentioned by Larry, which is defined in Finite_Set.thy, is itself based on an inductively defined relation called foldSet, which works similarly to the sum' relation described above. Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3 Room: 01.11.059 85748 Garching, GERMANY http://www.in.tum.de/~berghofe

**Follow-Ups**:**Re: [isabelle] Creating terms from sets***From:*Jesper Bengtson

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

**Re: [isabelle] Creating terms from sets***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] build HOL and SUSE 10.2
- Next by Date: Re: [isabelle] Creating terms from sets
- Previous by Thread: Re: [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