Artem Khovanov (Sep 05 2023 at 18:23): Artem Khovanov (Sep 05 2023 at 18:23):It seems to be impossible use interpretation with the locale factorial_monoid from HOL-Algebra.Ring_Divisibility. The commands sublocale and interpret still work. This issue extends to sublocales of factorial_monoid such as factorial_domain, euclidean_domain and field. Here is a MWE:
theory Scratch
imports "HOL-Algebra.Ring_Divisibility"
begin
interpretation factorial_monoid G sorry
end
The error printout is
Duplicate fact declaration "Scratch.wfactors_exist" vs. "Scratch.wfactors_exist"⌂
The above error(s) occurred while activating facts of locale instance
factorial_monoid "G"
Indeed, find_theorems gives two matches: Divisibility.divisor_chain_condition_monoid.wfactors_exist and Divisibility.factorial_monoid.wfactors_exist. I think the issue might come from the fact that factorial_monoid is a sublocale of divisor_chain_condition_monoid.
Is this an issue with the library, or am I doing something wrong? I am trying to create a global interpretation of the (HOL-Algebra) field locale.
Wenda Li (Sep 06 2023 at 13:00):I believe this is an issue with the library:
Divisibility.divisor_chain_condition_monoid.wfactors_exist:
divisor_chain_condition_monoid ?G ⟹
?a ∈ carrier ?G ⟹ ∃as. set as ⊆ carrier ?G ∧ wfactors ?G as ?a
Divisibility.factorial_monoid.wfactors_exist:
factorial_monoid ?G ⟹
?a ∈ carrier ?G ⟹ ∃fs. set fs ⊆ carrier ?G ∧ wfactors ?G fs ?a
Apart from the names and the locale precondition, these two lemma statements are identical. Moreover, considering factorial_monoid is a sublocale of divisor_chain_condition_monoid:
sublocale factorial_monoid ⊆ divisor_chain_condition_monoid
using divisor_chain_condition_monoid_axioms .
The factorial_monoid one should be able to be inherited from divisor_chain_condition_monoid.
Last updated: Nov 07 2025 at 16:23 UTC