Re: [isabelle] [Locales and Duplicate Facts]



Would any locale experts like to tackle this problem? It can be demonstrated by visiting HOL/Algebra/IntRing.thy and adding Divisibility to the list of imports. Suddenly you get failures all over the place, starting at the line

interpretation int: abelian_group 𝒵 

The problem is that Divisibility adds some duplicate names to the locale, such as l_cancel, r_cancel, Units_m_closed.

Larry

> On 24 May 2018, at 17:15, Paulo Emílio de Vilhena <pevilhena2 at gmail.com> wrote:
> 
> I’ve noticed an interesting behavior on locales and duplicate facts: it is
> possible to have duplicate facts (same name and result) for the same locale
> on different files, but if one tries to make an interpretation of this
> locale on a context that imports both files, Isabelle realizes the
> duplication and reports an error. This can get even more subtle:  if you
> prove a lemma for a locale B and prove that A is a sublocale of B, so if
> the fact was already given earlier for A, one gets the same problem only
> when trying to instantiate the locale A.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.