[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
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and