[isabelle] Generic reasoning with locales



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




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