*To*: Hernan Ponce-De-Leon <hernan.ponce-de-leon at inria.fr>*Subject*: Re: [isabelle] Can't access to a sublocale theorem*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Mon, 30 May 2011 13:29:40 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <749621591.1301472.1306750013118.JavaMail.root@zmbs2.inria.fr>*References*: <749621591.1301472.1306750013118.JavaMail.root@zmbs2.inria.fr>*User-agent*: Thunderbird 2.0.0.17 (X11/20080925)

Dear Hernan,

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

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

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

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]

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

**Follow-Ups**:**Re: [isabelle] Can't access to a sublocale theorem***From:*Hernan Ponce-De-Leon

- Previous by Date: Re: [isabelle] lattices, typeclasses, notations?
- Next 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: Re: [isabelle] Can't access to a sublocale theorem
- 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