# Re: [isabelle] Can't access to a sublocale theorem

Dear Hernan,

`it seems to me that you are trying to use locales other than the "official" way.
``Noramlly, you should never need to access the theorems in a locale when the
``context does not contain the locale. (Although there are some special cases when
``this does not work, but then, you lose all support from the locale system.)
`Why do you have to access as outside the context of B and its interpretations?

`Every local leaves a trace of its declarations in the global theory context,
``which is what you are trying to utilize: A.as is the trace declaring the
``assumption "g A n" in locale A. Thus, there is no B.as as B does not declare a
``theorem as by itself. If you declare theorems with the same name multiple times,
``you get into trouble, as you have experienced yourself.
`
Note that A.as refers to the theorem
A ?A.0 ?n ==> g ?A.0 n
i.e., there is an explicit premise that states the assumptions of locale A.

`When working with locales, you usually never refer to the declarations in the
``global theory context - even if the global terms show up in output buffers.
``Instead, prove your lemmas in the context B or interpret B for specific
``parameters first (either globally with interpretation or locally in an Isar
``proof with interpret). Then, you can access as without prefixes.
`
Hope this helps,
Andreas
Hernan Ponce-De-Leon schrieb:

`Hi all,
``
`

`I have two locales A and B. I set B as a sublocale of A. The problem I have is when trying to access to the "part" of B that comes from A. Here is an example:
``
`

`locale A =
``fixes A n
``assumes as: g A n
``
`

`locale B =
``fixes A n
``assumes bs: "g A n"
``
`

`sublocale B < A
``sorry
``
`

`If I print the B locale I get:
``
`

`locale elements:
``fixes A :: "'a"
``and n :: "'b"
``assumes "PROP B A n"
``notes A_axioms
``=
``(`PROP A A n`) [attribute <attribute>]
``notes as
``=
```?f A n`
``notes B_axioms
``=
``(`PROP B A n`) [attribute <attribute>]
``notes bs
``=
```?g A n`
``
`

`but I can't access to B.as
``
`

`One way I found to solve this was:
``
`

`context B begin
``lemmas as = as
``end
``
`

`This solves the problem but produce a new one: when I set an interpretation of B, I get a "duplicate fact declaration" error. An obvious way to solve this is:
``
`

`context B begin
``lemmas as' = as
``end
``
`

`Is there any way to access to B.as with a renaming?
``
`

`Thank you very much.
``
`

`Hernan
`

--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe
Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de

`KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
``in der Helmholtz-Gemeinschaft
`

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*