Re: [isabelle] Generic reasoning with locales
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
> 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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and