Re: [isabelle] Locale import
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"
definition foo where "foo = ... f ..."
lemma bar: "P foo" sorry -- "P is some property"
locale B =
fixes g :: "'c => 'a => 'b"
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.
2. 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.
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.)
No, this has nothing to do with syntax declarations for constants, but
with the abbreviations introduced by the locales.
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