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



Dear Hernan,

I see your problem. It is already in the theories for Presburger Automata in the AFP. The lemma duplication

context aut_dfa begin
lemmas trans_is_node = trans_is_node
lemmas steps_is_node = steps_is_node
lemmas reach_is_node = reach_is_node
end

leads to the error about duplicate facts when you interpret aut_dfa. From what I realised from a quick look over the sources, aut_dfa is not meant to be interpreted. Rather, it serves to obtain a conditional interpretation of Automaton with the parameters instantiated as

Automaton "dfa_trans A" "dfa_is_node A" "is_alph n"

If your problem is simply to mimick the access to instantiated theorems from Automaton, would recommend the following scheme:

lemma (in aut_dfa) Automaton:
  "Automaton (dfa_trans A) (dfa_is_node A) (is_alph n)"
by unfold_locales

Then, Automaton.my_thm[OF aut_dfa.Automaton] yields the same theorem as you would get from aut_dfa.my_thm, if you had the declaration
lemmas my_thm = my_thm in the context aut_dfa.

In particular, declarations like

lemmas dfa_trans_is_node = aut_dfa.trans_is_node [OF aut_dfa.intro]

would then become

lemmas dfa_trans_is_node =
  Automaton.trans_is_node[OF aut_dfa.Automaton, OF aut_dfa.intro]

I would recommend to delete the above lemmas declarations in the AFP, as they are only used for instantiation in dfa_trans_is_node and others. Thus, one could interpret aut_dfa locale. Alternatively, one could add a prefix the sublocale declaration to disambiguate the theorem names. Possibly, Stefan and Markus have a better idea as this is their development.

Andreas


Hernan Ponce-De-Leon schrieb:
Dear Andreas,

thank you for your replay.

I have been working with Isabelle just for two month so there are still a lot of things I don't understand quite well.

I'm working with the Presburger_Automata theory from The Archive of Formal Proofs and is here where I have this problem. When I try to interpret eq_dfa as an aut_dfa I got the "duplicate fact declaration" error and that's why I renamed the lemmas, but this doesn't look as the most elegant answer to my problem.

aut_dfa is a sublocale of Automaton so, as I understand, I should have access to all Automatons lemmas. What is more, if I print the aut_dfa locale, I can see that the Automatons lemmas (i.e. steps_is_node) are there but I can't access them.
Is it something I'm missing?

Hernan.

----- Mensaje original -----
De: "Andreas Lochbihler" <andreas.lochbihler at kit.edu>
Para: "Hernan Ponce-De-Leon" <hernan.ponce-de-leon at inria.fr>
CC: isabelle-users at cl.cam.ac.uk
Enviados: Lunes, 30 de Mayo 2011 8:03:47
Asunto: 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.