Re: [isabelle] [Locales and Duplicate Facts]



On 05/06/18 17:58, Lawrence Paulson wrote:
> 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.

At the bottom of it is a generally looming danger with theory merges:
"containers" from either theory might be incompatible and fail to merge.
This happens so rarely in practice, that users often think of a merge as
total.

There might be workarounds for locale interpretation, but I can't say on
the spot how it works in detail.

Spontaneously, I would say it is a mistake in the HOL-Algebra library to
use such hidden duplicates. Wasn't it part of the project at Cambridge
to clean up fact names in this part?


	Makarius




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