# Re: [isabelle] Creating terms from sets

```Lawrence Paulson wrote:
```
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.
```
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? Is there a way to create this function, or is inductively defined relations 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

```

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