[isabelle] Locale import



Hello all,

I want to import a locale A into a locale B such that one of A's parameters is replaced by a fixed parameter of B applied to an arbitrary value. Here's a short example what I would like to write:

locale A =
  fixes f :: "'a"
  assume "f"

locale B = A "g b"
  for g :: "'b => 'a"
  assumes ...

However, Isabelle complains at B's declaration that b is an illegal free variable. Adding b to the for clause is no solution to my problem, because this fixes b. I am currently doing the following:

locale B = fixes g :: "'b => 'a"
  assumes A: "A (g b)"
  and ...

sublocale B < A "g b"
  for b
by(rule A)

Although this works for the moment, I am not happy with this solution:
I can only use definitions from A in the other assumptions of B via their full name with all parameters explicitly provided.

So my question is:
What is the best way to import A in B?

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.