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

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.

Best regards,
Andreas

--
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.edu
http://pp.info.uni-karlsruhe.de
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.