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.