[isabelle-dev] Interpretation with definitions [was Locale interpretation with mixins]

[Florian Haftmann]

Hi Clemens,

> I appreciate that you now follow my reasoning that changes to the
> locales core machinery are not necessary for getting this
> functionality.

good point.

> Also, I'm afraid I fail to understand the difference between 'where x =
> t' and 'where x is t'.

Let me elaborate more on this.

>> The current syntax in Tools/interpretation_with_defs.ML is just a proof
>> of concept:
>>
>> interpretation L inst
>>   where
>>     "bar = t"
>>   defines f is foo

I guess until here everything is still obvious.

>> A much better idea could be to give the new defs in a for-clause:
>>
>> interpretation L inst
>>   for f :: T
>>   where
>>     "foo = f"
>>     "bar = t"

No, this has not been a »much better idea« since the existing locale
expressions already have »for« for free variables.  I did forget about
this, sorry.

(*) An alternative could be

interpretation L inst
  defining f :: T
  where
    "foo = f"
    "bar = t"

where the implicit definitions (f) are mentioned in the »defining«-clause.

The next variant

>> interpretation L inst
>>   defining f :: T
>>   where
>>     f is foo
>>     t is bar

would syntactically enforce that only equations which syntactically
describe definitions are permitted in where clauses, thus concealing the
full generality of equational rewrites from the user.  Internally, this
would expand to equations »foo = f« and »bar = t«.

>> Or the where clause could be integrated completely into the locale
>> expression using named syntax:
>>
>> interpretation L (| f := foo, t := bar |)
>>   defining f :: T

Admittedly, this would require more careful thinking.

Anyway, I am not so much concerned about syntax.  My primary intention
is to get rid of the experimental code in interpretation_with_defs.ML,
according to the following agenda:
a) Decide for a particular syntax (at the moment this can only be (*) as
it is conservative)
b) Enhance »interpretation« accordingly.  Also a different command can
be considered, but the interfaces in expression.ML must be extended in
any case.

I would continue that road, really getting hands on, unless objections
remain.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120906/8658b623/attachment.asc>