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.