Re: [isabelle] Locale import



Hi Peter,

> 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.
If you ever refer to the global constants somewhere, you are right. I experienced this myself often enough, but as long as you stay within the locale framework, this all is very convenient - provided that you make sure that the order of parameters stays the same when extending locales.
This is particularly tricky if they have a lot of parameters.

Here are two hints on how I use locales:

1. Split your locale into two: Let one only fix the parameters and let the other inherit from it and add the locale assumptions. Then, put all your constant definitions (definition/inductive/fun/primrec/...) into the first locale and all your lemmas into the second locale, if possible. (I think, only function definitions whose termination proof relies on locale assumptions cannot go that way). This has the following advantages:

- The definitional facts, simplification/introduction rules, etc. have no additional locale predicate as premise, i.e. you can use them whenever you like without having to make sure that the locale assumptions are currently satisfied. This also allows the code generator to use them.

- You can have the locale parameters already implicit when you make your definitions (unlike in the Presburger-Automaton AFP entry).


2. Try to avoid as hard as you can to refer to global constants anytime. Always use the sublocale command or conditional interpretation (see the locale tutorial, sec. 7). Then, the locale infrastructure keeps track of all implicit parameters - even if you change your definitions in a locale. If you finally decide to change the parameter order, you only have to adapt the sublocale/conditional interpretations, but not the uses.

> 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.
I myself have found locales very helpful even if there are a lot of parameters around (see e.g. my theory http://afp.sourceforge.net/browser_info/current/HOL/JinjaThreads/FWBisimulation.html from "Jinja with Threads" in the AFP), but I must admit that getting everything work smoothly with very complex locale structures is quite challenging.

What I would like is to be able to automatically generate a locale inheritance graph (similar to the theory graph produced by the graph browser) with all locale morphisms shown.

Chees,
Andreas





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