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
> "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!



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