Email Gateway (Aug 18 2022 at 14:39): Email Gateway (Aug 18 2022 at 14:39):From: Peter Gammie <peteg42@gmail.com>
Andreas,
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. A.foo (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:
http://afp.sourceforge.net/entries/Presburger-Automata.shtml
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!
cheers
peter
Email Gateway (Aug 18 2022 at 14:39):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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:
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).
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
Email Gateway (Aug 18 2022 at 14:44):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hello all,
I want to import a locale A into a locale B such that one of A's
parameters is replaced by a fixed parameter of B applied to an arbitrary
value. Here's a short example what I would like to write:
locale A =
fixes f :: "'a"
assume "f"
locale B = A "g b"
for g :: "'b => 'a"
assumes ...
However, Isabelle complains at B's declaration that b is an illegal free
variable. Adding b to the for clause is no solution to my problem,
because this fixes b. I am currently doing the following:
locale B = fixes g :: "'b => 'a"
assumes A: "A (g b)"
and ...
sublocale B < A "g b"
for b
by(rule A)
Although this works for the moment, I am not happy with this solution:
I can only use definitions from A in the other assumptions of B via
their full name with all parameters explicitly provided.
So my question is:
What is the best way to import A in B?
Regards,
Andreas
Email Gateway (Aug 18 2022 at 14:44):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Andreas,
I want to import a locale A into a locale B such that one of A's
parameters is replaced by a fixed parameter of B applied to an
arbitrary value. Here's a short example what I would like to write:locale A =
fixes f :: "'a"
assume "f"locale B = A "g b"
for g :: "'b => 'a"
assumes ...
I am not sure what your ultimate goal is, and I don't see what
semantics of b should be here. Locale parameters are "arbitrary but
fixed". I don't know what "arbitrary and not fixed" should mean when
it comes to applying the module in another context.
However, Isabelle complains at B's declaration that b is an illegal
free variable. Adding b to the for clause is no solution to my problem,
because this fixes b. I am currently doing the following:locale B = fixes g :: "'b => 'a"
assumes A: "A (g b)"
and ...sublocale B < A "g b"
for b
by(rule A)Although this works for the moment, I am not happy with this solution:
I can only use definitions from A in the other assumptions of B via
their full name with all parameters explicitly provided.
The declaration of B is still strange and should probably be rejected.
Don't rely on this in future version of Isabelle.
What is the best way to import A in B?
Since both declarations of B are "strange" this question is not well-defined.
Possibly you want to redeclare syntax for definitions that was
disabled since inherited through a non-identical morphism (cf. Section
6 of the tutorial, immediately before Section 6.1 starts.)
Best regards,
Clemens
Email Gateway (Aug 18 2022 at 14:45):From: Clemens Ballarin <ballarin@in.tum.de>
Contrary to my previous message, this is, of course, well-defined. b
is here universally quantified in the assumption. I am still at loss
what you are trying to achieve, though.
Clemens
Email Gateway (Aug 18 2022 at 14:45):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Clemens,
probably my example was too reduced to convey my problem, so I try again
with a (hopefully better) example.
Suppose we have two locales A and B that are independent of each other:
locale A =
fixes f :: "'a => 'b"
assumes ...
begin
definition foo where "foo = ... f ..."
lemma bar: "P foo" sorry -- "P is some property"
end
locale B =
fixes g :: "'c => 'a => 'b"
assumes ...
Now, I want to combine both A and B in a new locale C such that A's
parameter f is instantiated with B's parameter g applied to any value.
locale C = B +
assumes A: "A (g c)"
and Q: "Q g c (A.foo (g c))" -- "Q is some predicate"
sublocale C < A "g c" for c by(rule A)
In context C, the sublocale introduces an abbreviation foo for
"%c. A.foo (g c)"
and the inherited lemma bar from locale A is now
"P (foo c)" where c is a free variable.
This is what I want to achieve. Two things are unsatisfactory here:
I mention a locale predicate as an assumption of a locale instead of
properly importing it. The first step after the locale declaration is to
change the locale graph to include this import.
The assumption Q in locale C involves a constant defined in A. Since
I do not know how to add A to the import list, I must resort to the
global constant A.foo. In my real case, A (and B) have a lot more fixed
parameters and writing all of them makes the assumptions hard to read.
I hope that this illustrates better what I am trying to achieve: In
locale C, I want to use everything from locale A with f instantiated by
"g c", where I can use a different c each time.
Is there a better way to achieve something like this?
I do not want to change locale A because I need to interpret it
elsewhere with parameters that only take one argument.
No, this has nothing to do with syntax declarations for constants, but
with the abbreviations introduced by the locales.
Best regards,
Andreas
Email Gateway (Aug 18 2022 at 14:46):From: Peter Gammie <peteg42@gmail.com>
Andreas,
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.)
I have a question for you and a suggestion for the locale implementors. Please excuse my top posting: your context is important.
How do you expect to later instantiate 'c'?
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. Concretely, imagine:
locale A =
fixes f :: "''c => 'c"
fixes g :: "'c => 'c"
assumes "P f"
assumes "Q g"
begin
definition "h = f o g"
lemma HX: "h x = f (g x)" ...
end
Could the locale mechanism produce extra definitions of the form:
record 'c A_fixes =
f :: "'c => 'c"
g :: "'c => 'c"
(* captures "fixes" *)
definition
A_pred :: "'c A_fixes => bool"
(* captures the two "assumes" *)
definition
"A_h :: 'c A_fixes => 'c => 'c"
lemma A_HX: "A_pred A ==> h x = f (g x)"
The idea is to shift from the curried form where external definitions capture only the locale-fixed variables used in the expression to an uncurried form where the record aggregates all locale-fixed variables. I intend this to be a purely syntactic matter.
This idea is essentially the same as using records to simulate type classes in Haskell, sometimes termed an evidence-passing translation. This implies it might have typing implications (viz require higher-ranked polymorphism) but I'm yet to run into any.
In my case I would get the benefit of being able to state things in the locale conveniently and later uniformly abstract at the term level using the record-based external definitions.
I admit I have no deep understanding of locales, so there is a good chance this proposal stumbles on some key matter.
cheers
peter
Email Gateway (Aug 18 2022 at 14:47):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Email Gateway (Aug 18 2022 at 14:56):From: Clemens Ballarin <ballarin@in.tum.de>
After some off-line discussion with Andreas Lochbihler, I would like
to summarise the most important points.
Suppose we have two locales A and B that are independent of each other:
locale A =
fixes f :: "'a => 'b"
assumes ...
begin
definition foo where "foo = ... f ..."
lemma bar: "P foo" sorry -- "P is some property"
endlocale B =
fixes g :: "'c => 'a => 'b"
assumes ...Now, I want to combine both A and B in a new locale C such that A's
parameter f is instantiated with B's parameter g applied to any value.locale C = B +
assumes A: "A (g c)"
and Q: "Q g c (A.foo (g c))" -- "Q is some predicate"
sublocale C < A "g c" for c by(rule A)In context C, the sublocale introduces an abbreviation foo for
"%c. A.foo (g c)"
and the inherited lemma bar from locale A is now
"P (foo c)" where c is a free variable.This is what I want to achieve. Two things are unsatisfactory here:
1. I mention a locale predicate as an assumption of a locale instead of
properly importing it. The first step after the locale declaration is to
change the locale graph to include this import.
Locales enrich the context by syntax and theorems. Therefore, direct
import of infinite families of locale instances is not possible.
Locale predicates, on the other hand, are first-class citizens of the
logic and can be used to emulate this. Those instances that are
required in proofs, and for which syntax and theorems are needed, may
be added to either the proof context or a locale with either
"sublocale" or "interpret" respectively. This idea is explored in
Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
Proof Contexts. In
J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108, pages 3143, 2006.
(http://www4.in.tum.de/~ballarin/publications/mkm2006.pdf)
in Section 5, proofs for the discussed examples are in HOL-Algebra.
- The assumption Q in locale C involves a constant defined in A. Since
I do not know how to add A to the import list, I must resort to the
global constant A.foo. In my real case, A (and B) have a lot more fixed
parameters and writing all of them makes the assumptions hard to read.
This is generally unavoidable since the parameters are bound in the
assumption. The best you can do here is introduce syntax for A.foo
with the parameters that are fixed with a locale inserted into the
hierarchy.
Clemens
Last updated: Apr 27 2024 at 01:05 UTC