Re: [isabelle] Locale import
> 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
- 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
> 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
from "Jinja with Threads" in the AFP), but I must admit that getting
everything work smoothly with very complex locale structures is quite
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and