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"
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.
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.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and