Re: [isabelle] Locale import


Thanks for your help on this. Your explanation of what the sublocale command actually does is the most lucid I have yet seen. Can the documentation maintainer(s) add something like this to the official docs please?

Now, to flog my dead horse a bit more:

On 18/02/2010, at 7:51 PM, Andreas Lochbihler wrote:

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

Ah, indeed! This is the behaviour I want. However:

> 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 think I gave up on this approach as the constants you mention take the locale-assumptions they use as parameters, separately. This means that if I change the definition of these constants, e.g. to use more or fewer of the locale-assumptions, then I may have to update all uses of them everywhere.

The limitations/irritations of the position-based locale setup are well illustrated by this theory:

by Stefan Berghofer and Markus Reiter. IMHO the locale interpretation commands are meaningless to the casual reader, whereas the lemmas (in e.g. the DFS theory) are as lucid one can hope for.

I adapted this theory to use records explicitly. Now the DFS lemmas are a bit obfuscated but using the theory has been a bit simpler and more robust to change. I originally did this because I did not understand sublocale.

>> 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.

I have. My issue is that they are not as abstract as I'd like them to be.

> 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.

This is a good point. I suggested the record-based constants be additional to the existing ones, so the limitations of using records does not get in the way of large locale hierarchies.

Locales strike me as very successful when the number of parameters are small, but are less so when used with lots of parameters, as in the DFS theory mentioned above. Perhaps the use-cases split into those with loads of parameters (e.g. parameterised algorithms like the DFS) and those with few (e.g. algebraic structures), and different naming mechanisms might be appropriate for each. Perhaps I have been too quick to propose records as the solution.

Thanks again Andreas!



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