Re: [isabelle] simulating term-level abstraction using locales



Florian:

On 18/12/2009, at 7:37 PM, Florian Haftmann wrote:

>> sublocale L ⊆ A by (unfold_locales)
> 
> if you want to instantiate the 'a' parameter in locale 'A', this is your
> "only chance", e.g.
> 
> sublocale L ⊆ A x X x
> 
> Then you also should add a namespace prefix, e.g.
> 
> sublocale L ⊆ A: A x X x

Thanks for your comments.

I came to understand that I was asking for too much: at the very least, Isabelle has no syntax for (lambda-) abstracting a free variable from several definitions (like what happens in the example I posted).

So I gave up on these locales and went back to the tried and true record + predicate approach. I'm not so happy with that as I lose the syntactic niceties (e.g. a pleasant introduction mechanism) but it is not so bad.

cheers
peter




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