*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Can't access to a sublocale theorem*From*: Hernan Ponce-De-Leon <hernan.ponce-de-leon at inria.fr>*Date*: Mon, 30 May 2011 13:39:37 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4DE37FA4.6000701@kit.edu>

We thought in something like that but we didn't know how to do it. Thank you very much for your answer Andreas 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" <isabelle-users at cl.cam.ac.uk> > Enviados: Lunes, 30 de Mayo 2011 13:29:40 > Asunto: 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

**References**:**Re: [isabelle] Can't access to a sublocale theorem***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Can't access to a sublocale theorem
- Previous by Thread: Re: [isabelle] Can't access to a sublocale theorem
- Next by Thread: [isabelle] Exception in conv.ML
- Cl-isabelle-users May 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list