Re: [isabelle] Locale import
It could be. Unfortunately, I don't understand fully what you are trying
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.)
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
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?
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
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.
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.
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.
Karlsruher Institut für Technologie
Adenauerring 20a, Gebäude 50.41, Raum 023
Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
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