Email Gateway (Aug 18 2022 at 15:31): Email Gateway (Aug 18 2022 at 15:31):From: Giuliano Losa <giuliano.losa@epfl.ch>
Dear Isabelle users,
I'd like to reason about a family of network protocols. This family is
defined as a state transition system parameterized by a number of parameters
of generic type.
Suppose I use a locale to define this family of protocols.
Now I'd like to prove properties of the composition of two protocols
belonging to the family, and in a generic way. I wanted to proceed as
follows: get two different generic instances of the family, apply the
composition operator to the two instances, and prove something about the
result. But I cannot provide generic parameters when instantiating (using
"interpretation").
Is there a way to do what I've described using locales?
For now, I've defined the family as a function from the generic parameters I
need to a state transition system. However it quickly gets very cluttered.
Thanks for reading,
Giuliano
Email Gateway (Aug 18 2022 at 15:31):From: Peter Gammie <peteg42@gmail.com>
Giuliano,
On 17/06/2010, at 11:00 PM, Giuliano Losa wrote:
[...] Suppose I use a locale to define this family of protocols.
[..] But I cannot provide generic parameters when instantiating (using
"interpretation").Is there a way to do what I've described using locales?
Make friends with "sublocale". Search the list archives for posts by Andreas Lochbihler on this topic.
Also have a poke around the Archive of Formal Proof for some structuring ideas.
For now, I've defined the family as a function from the generic parameters I
need to a state transition system. However it quickly gets very cluttered.
Indeed it does. "sublocale" commands get messy but your lemmas etc. stay clean.
Hope this helps!
cheers
peter
Last updated: Apr 25 2024 at 04:18 UTC