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"
    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'"
    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


Dr. Stefan Berghofer               E-Mail: berghofe at
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  

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