Email Gateway (Jan 04 2023 at 03:29): Email Gateway (Jan 04 2023 at 03:29):From: Qiyuan XU ????? <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle users,
I am trying to figure out the behavior of a locale when its sub-locales constitute a graph instead of a tree.
And I find its behavior is a bit strange in the following example where the order of locale instances in a locale expression is significant, though I think it should not be like this,
locale AA =
fixes x :: nat
assumes th: ‹0 < x›
locale BB = AA x1 + a2: AA x2
for x1 and x2
locale CC = BB x1 x2 + a2: AA x1
―‹Note, in ‹BB x1 x2› a2 qualifies ‹AA x2› whereas in the right hand side of the ‹+› in CC, a2 qualifies ‹AA x1››
for x1 x2
locale CC' = a2: AA x1 + BB x1 x2
for x1 x2
Note a2 qualifies both AA x1 and AA x2. CC and CC' are different only in the order of the local instance.
A really interesting thing happens in this example. First, the above declaration works, but once we are going to interpret it:
interpretation c: CC 1 2 by (standard; auto)
interpretation c': CC' 1 2 by (standard; auto)
this works. c.a2.th is 0 < 2, besides c'.a2.th is not defined.
However, once we interpret c' first,
interpretation c': CC' 1 2 by (standard; auto)
interpretation c: CC 1 2 by (standard; auto)
an error occurs, telling:
Duplicate fact declaration "Scratch.c'.a2.AA_axioms" vs. "Scratch.c'.a2.AA_axioms"
The above error(s) occurred while activating facts of locale instance c'.a2 : AA "2"
The reason why I am playing on this a bit strange example is that, I am facing a problem with interpreting a large locale in my current work. The dependence of the locale is a graph but different from this example, the parameters of every locale instance are consistent, so the multi-dependence should work well. However, the error of "Duplicate fact declaration" keeps occurring annoyingly and I cannot address them. So, may I enquiry more materials or documents explaining the behavior of multi-dependence of a locale?
Thank you
Qiyuan Xu
CONFIDENTIALITY: This email is intended solely for the person(s) named and may be confidential and/or privileged. If you are not the intended recipient, please delete it, notify us and do not copy, use, or disclose its contents.
Towards a sustainable earth: Print only when necessary. Thank you.
Email Gateway (Jan 09 2023 at 21:53):From: Clemens Ballarin <ballarin@in.tum.de>
Dear Qiyuan Xu,
The reference documentation is C. Ballarin. Locales: A module system for
mathematical theories. Journal of Automated Reasoning, 52(2):123–153,
2014
You can enable 'trace_locale' and perhaps 'show_types' to see what's
happening:
declare [[trace_locale, show_types]]
You can also insert more (and distinct!) qualifiers to try isolate the
problem.
Clemens
Last updated: Jan 04 2025 at 20:18 UTC