Stream: General

Topic: factorial_monoid interpretation

view this post on Zulip 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"

interpretation factorial_monoid G sorry


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.

view this post on Zulip Wenda Li (Sep 06 2023 at 13:00):

I believe this is an issue with the library:

    divisor_chain_condition_monoid ?G 
    ?a  carrier ?G  ∃as. set as  carrier ?G  wfactors ?G as ?a
    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