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



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





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