Re: [isabelle] Variables in locale assumptions



On 25 Feb 2014, at 9:23 am, Makarius <makarius at sketis.net> wrote:

> On Mon, 24 Feb 2014, Makarius wrote:
>
>> On Mon, 24 Feb 2014, Gerwin Klein wrote:
>>
>>> or if you need to constrain types?
>>
>> The 'constrains' element is easier to get rid of.  I would like to see some constructive proofs where you "need to constrain types", as you say. This is usually just a workaround to specify locale type arguments, but if that would be supported directly, the need would go away.
>
> Maybe you have actually missed the important locale expression improvements by Clemens Ballarin from Isabelle2009.  See the NEWS, e.g. this one:
>
>  - In locale expressions, instantiation replaces renaming.  Parameters
>  must be declared in a for clause.  To aid compatibility with previous
>  parameter inheritance, in locale declarations, parameters that are not
>  'touched' (instantiation position "_" or omitted) are implicitly added
>  with their syntax at the beginning of the for clause.
>
> In most situations a locale expression suffix "for x :: T" can be used to instantiate types in imports.  I had cleaned up AFP in this respect already some years ago, but in various newer entries old 'constrains' seem to have come back.  Time for spring cleaning?

Actually, yes this may do it. I’ve used it for new proofs, but somehow managed not to make the connection.

Let me try this out on the old proofs.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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