# Re: [isabelle] Locale import

`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"
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:
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 31?43, 2006.
(http://www4.in.tum.de/~ballarin/publications/mkm2006.pdf)
in Section 5, proofs for the discussed examples are in HOL-Algebra.

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.

`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

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