Email Gateway (Aug 18 2022 at 17:45): Email Gateway (Aug 18 2022 at 17:45):From: Hernan Ponce-De-Leon <hernan.ponce-de-leon@inria.fr>
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
Email Gateway (Aug 18 2022 at 17:46):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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:
Email Gateway (Aug 18 2022 at 17:46):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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:
Email Gateway (Aug 18 2022 at 17:46):From: Hernan Ponce-De-Leon <hernan.ponce-de-leon@inria.fr>
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 -----
Last updated: Nov 21 2024 at 12:39 UTC