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

I had a few definitions such as these. I haven't implemented anything concretely yet, but these are good sugestions.

Many thanks


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