Stream: Beginner Questions

Topic: Locale interpretation duplicate fact declaration

David Wang (Jan 05 2025 at 15:28):

Hello.
I have the following hierarchy of locales.

locale a =
  fixes a::"int"
    and b::"int"
  assumes a_le_b: "a < b"

locale b = a a b
  for a b::"int"
+ fixes c::"int"
assumes b_le_c: "b < c"

locale a' = a a b
  for a b::"int"
begin
sublocale b a "a + 1" "a + 2" apply standard
  by simp+
end

global_interpretation a' 0 1 apply standard by auto

The final line causes the error: "Duplicate fact declaration "Scratch.a_axioms" vs. "Scratch.a_axioms"

I guess this is because a_le_b: "a < b" is instantiated with "a < b" and "a < a + 1". Is there a way to hide one of these two copies?

irvin (Jan 05 2025 at 16:36):

sublocale namespace: b a "a + 1" "a + 2" apply standard
  by simp+

makes it so that lemmas are behind so the second b becomes
namespace.a_le_b

David Wang (Jan 05 2025 at 16:36):

Thank you.

Last updated: Feb 01 2025 at 20:19 UTC