Re: [isabelle] Locale import



Hello Peter,

I think this is similar to what I wanted to do. (You can try reading my earlier email to this list but it is nowhere as clear as yours is.)
It could be. Unfortunately, I don't understand fully what you are trying to do.

How do you expect to later instantiate 'c'?
The sublocale command

> > sublocale C < A "g c" for c by(rule A)

transports all definitions and lemmas from A into C, where f is instantiated by "g c". Since c is declared in the for clause, this becomes a new parameter to all definitions in A.

> > definition foo where "foo = ... f ..."
Im my example, the definition of foo in locale A depends on A's parameter f. The above sublocale command now introduces a variant of foo in locale C that takes an additional parameter c. To "instantiate" c later on, I simply pass it as a parameter to foo.

Behind the scenes, the following actually happens:
- The definition of foo in locale A defines a global constant A.foo, which takes all locale parameters that the definition depends on, additional to the parameters in the definition. It also produces an abbreviation foo inside the locale A, which abbreviates "A.foo f".

- The sublocale command introduces an abbreviation foo in C
where "foo == %c. A.foo (g c)".


Now back to your old post: If you just want the additional parameter "a" of locale A to be "lambda-abstractable", declare it explicitly in a for clause:

sublocale L < LsubA!: A x X a for a by unfold_locales.

Do not forget to give a name (like LsubA) to this import and make it an obligatory prefix (!). Otherwise, you will not be able to open the context A again. Then, in locale L, you get an abbreviation LsubA.f for the f from A which takes an extra parameter "a". Similarly, there are the facts LsubA.f_def, LsubA.g_def and LsubA.Q. Is this, what you wanted?

I overcame my parameterisation problem by rewriting the locale as a record (of variables that were 'fixes' in the locale) and a predicate (capturing the locale assumptions). I suggest the locale mechanism be extended to do this, in addition to whatever it now does.
The locale package already produces global definitions, but not a record. There is a predicate with the same name as the locale which contains all the assumptions (including those from imported locales). Every definition and abbreviation of X in a locale L produces a global definition/abbreviation L.X. Similarly, every fact T that is shown inside L corresponds to a global fact L.T, which has the locale predicate L as additional premise. So, this is very much what you want except for currying: The locale parameters are not collapsed into a record, but kept separately.
You might want to have a look at those.

Collapsing all parameters into a single record would make it easier to work with the global constants because one would have to pass only a single parameter to them. However, if you have definitions in different locales (one of which is a sublocale of the other), you would have to do many record conversions from the sublocale record to the superlocale record. So, a record is not a better option.

Regards,
Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft





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