Email Gateway (Aug 23 2022 at 08:35): Email Gateway (Aug 23 2022 at 08:35):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I cannot seem to understand certain aspects of the locale interpretation
mechanism. Consider the following example (please try not to pay any
attention to the meaning of the locales, as this is a superficial
close-to-minimal example) :
theory Scratch
imports Main
begin
locale graph =
fixes G :: 'a and is_arr is_vertex dom cod
assumes dom: "is_arr G f ⟹ is_vertex G (dom G f)"
and cod: "is_arr G f ⟹ is_vertex G (cod G f)"
locale op_graph = graph +
fixes op
assumes op_dom: "is_arr (op G) f ⟹ is_vertex (op G) (dom (op G) f)"
and op_cod: "is_arr (op G) f ⟹ is_vertex (op G) (cod (op G) f)"
begin
sublocale opop: graph ‹op (op G)› is_arr is_vertex cod dom
sorry
thm opop.dom
(is_arr (op (op G)) ?f ⟹ is_vertex (op (op G)) (cod (op (op G)) ?f))
end
interpretation op: op_graph G is_arr is_vertex dom cod op
for G is_arr is_vertex dom cod op
sorry
print_theorems
(*
op.cod: ?is_arr ?G ?f ⟹ ?is_vertex ?G (?cod ?G ?f)
op.dom: ?is_arr ?G ?f ⟹ ?is_vertex ?G (?dom ?G ?f)
op.graph_axioms: graph ?G ?is_arr ?is_vertex ?dom ?cod
op.op_cod: ?is_arr (?op ?G) ?f ⟹ ?is_vertex (?op ?G) (?cod (?op ?G) ?f)
op.op_dom: ?is_arr (?op ?G) ?f ⟹ ?is_vertex (?op ?G) (?dom (?op ?G) ?f)
op.op_graph_axioms: op_graph ?G ?is_arr ?is_vertex ?dom ?cod ?op
*)
find_theorems name: ".opop." (found nothing)
thm op.opop.dom (Undefined fact)
end
I find it difficult to understand why the theorems associated with the
interpretation "opop" inside the context of the locale op_graph do not
appear in the global context after the interpretation of op_graph itself.
In certain similar cases, the theorems associated with the interpretation
do appear in the global context, as I would expect. Do there exist any
methodologies for the interpretation that avoid this problem in the example
presented above?
Kind Regards,
Mikhail Chekhov
Email Gateway (Aug 23 2022 at 08:35):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Mikhail,
interpretation and sublocale skip the generation of theorem names if the new
interpretation is subsumed by another interpretation. In your example, the interpretation
op first generates an interpretation with arbitrary parameters as they are all listed in
the for clause. Therefore, when the sublocale declaration is inspected, it finds that
there's no need for the nested op interpretation as this interpretation would create
theorems that are instances of the more general ones that are aleady available. This is
hard-coded into the locale mechanism and cannot be configured. The details of this
round-up algorithm are described in Clemens Ballarin's JAR paper:
http://www21.in.tum.de/~ballarin/publications/jar2013.pdf
Best,
Andreas
Email Gateway (Aug 23 2022 at 08:36):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Andreas Lochbihler,
Thank you for the explanation and for providing the reference. Regrettably,
I was aware of the part of the algorithm that you mentioned. Therefore,
most likely, at the time of asking, I became wrongly convinced that it is
not applicable to my use case. Please accept my apologies for the confusion.
Kind Regards,
Mikhail Chekhov
Last updated: Apr 20 2024 at 08:16 UTC