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.

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