## Stream: General

### Topic: factorial_monoid interpretation

#### 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: Dec 07 2023 at 08:19 UTC