Re: [isabelle] Locale import

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 ...
definition foo where "foo = ... f ..."
lemma bar: "P foo" sorry -- "P is some property"

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 ( (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. (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 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.

Best regards,

Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at
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 MHonArc.