*To*: Stefan Berghofer <berghofe at in.tum.de>*Subject*: Re: [isabelle] Creating terms from sets*From*: Jesper Bengtson <jesperb at it.uu.se>*Date*: Thu, 05 Apr 2007 10:51:38 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4614B24C.1050209@in.tum.de>*References*: <4610F6C1.7040704@it.uu.se> <648847FF-46A0-4443-8928-D6DEE2D9A692@cam.ac.uk> <4614B24C.1050209@in.tum.de>*User-agent*: Mozilla Thunderbird 1.0 (X11/20050320)

Stefan Berghofer wrote:

Lawrence Paulson wrote:Isabelle/HOL provides fold functionals for sets, which can be usedprovided the result does not depend on the order in which setelements 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 tothe "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 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.

Many thanks /Jesper

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

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

**Re: [isabelle] Creating terms from sets***From:*Stefan Berghofer

- Previous by Date: Re: [isabelle] Creating terms from sets
- Next by Date: [isabelle] problem with polymorphism?
- Previous by Thread: Re: [isabelle] Creating terms from sets
- Next by Thread: Re: [isabelle] Question to "lemmas" - instruction
- 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