Email Gateway (Aug 18 2022 at 10:23): Email Gateway (Aug 18 2022 at 10:23):From: Stefan Berghofer <berghofe@in.tum.de>
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
Email Gateway (Aug 18 2022 at 10:23):From: Jesper Bengtson <jesperb@it.uu.se>
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 defineconsts 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
Email Gateway (Aug 18 2022 at 10:26):From: Jesper Bengtson <jesperb@it.uu.se>
Greetings all
I am currently working on proving soundness and completeness for the
axiomatisation of strong late bisimilarity of the pi calculus. A key
notion here is that of summands which basically is a set of all subterms
which are constructed from the +-operator. I would, however, need a
function which creates a term from the set of its summands, i.e.
SUM(summands P) = P.
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?
Thank you for your time
/Jesper
Email Gateway (Aug 18 2022 at 10:27):From: Lawrence Paulson <lp15@cam.ac.uk>
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.
For details, see this paper:
Tobias Nipkow and L. C. Paulson. Proof Pearl: Defining Functions Over
Finite Sets. In: Joe Hurd and Tom Melham (editors),Theorem Proving in
Higher Order Logics (Springer LNCS 3603, 2005), 385–396.
<http://www.cl.cam.ac.uk/~lp15/papers/Reports/TPHOLs05.pdf>
Larry Paulson
Last updated: May 03 2024 at 12:27 UTC