# Re: [isabelle] Creating terms from sets

```Stefan Berghofer wrote:

```
```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).
```
```
The equality we are interested in is equality with respect to the axiomatisation. I am then proving that this axiomatisation is sound and complete with respect to strong late bisimilarity. For both of these equality classes the +-operator is both associative and commutative, so I think Larry's suggestion will do exactly what I want.
```
```
```
```
```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.
```
```
```
I had a few definitions such as these. I haven't implemented anything concretely yet, but these are good sugestions.
```
Many thanks

/Jesper

```

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