Re: [isabelle] [Locales and Duplicate Facts]



The problem is not just the sublocale declaration. For example, the lemma Units_m_closed in Divisibility is put into the locale monoid, but the same lemma has been proven in the same locale in theory Group. This is not detected in theory Divisibility because the names for the two theorems in the background theory are different due to the different theory names. The problem only manifests when an interpretation tries to interpret the monoid locale because this notes the theorem twice. There is no workaround in Isabelle2017 for this.

For the l_cancel problem, there is a workaround, but it needs two theories.

1. In theory 1, import only Group, but not Divisibility and add an interpretation of the locale monoid under a suitable qualifier q.

2. In theory 2, import theory 1 and Divisibility. Interpret the locale monoid_cancel with a different qualifier q'. Then interpret group with qualifier q.

In step 2, the first interpretation ensures that the locale roundup algorithm will not attempt to interpret monoid_cancel during the second interpretation. The drawbacks of this solution are:

a. The theorems that divisibility adds to monoid are not available in either theory.
b. The definitions and theorems from monoid_cancel must be reference with qualifier q' instead of q.

Best,
Andreas

On 06/06/18 15:21, Lawrence Paulson wrote:
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.