Re: [isabelle] [Locales and Duplicate Facts]



The name clashes come about in pretty obscure ways. Theory Group proves certain lemmas in the locale group. Theory Divisibility creates a new locale, monoid_cancel, assuming the exact same lemmas as axioms and with the same names. Then it goes on to prove

sublocale group ⊆ monoid_cancel
  by standard simp_all

There is still no sign of anything wrong, although already (I think) locale group now has conflicting names and can't be instantiated any more. The name clash should be flagged at this point.

Larry

> On 5 Jun 2018, at 22:52, Makarius <makarius at sketis.net> wrote:
> 
>> 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?





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