Re: [isabelle] Locale interpretations and imported theories



Hi Peter,

I encountered a problem/bug(?) with locales and imported theories.
I have four theories:
  def: Defines a locale
  add: Adds some lemma to the locale
  inst: Interprets the locale, but does *not* import add
  use: Imports add and inst

Brian was so kind to dig out my answer to an earlier enquiry of the same kind, so I can refer to his e-mail.

Even more strange things happen, if I try to reinterpret the locale in
theory "use": The re-interpretation (done with a different prefix name)
adds no lemmas, neither the ones originally defined in the locale, nor the
ones added by the theory "add".

It is not possible to force the re-interpretation of a locale instance. In fact, the interpretation does not take place for any locale fragments that are subsumed by existing interpretations (also indirect ones created by sublocale).

The only workarounds that I can currently figure out is instantiating
the missing lemmas by hand, i.e. lemmas xyz_lem = locale_name.lem[OF
xyz_is_interp] or trying to change the structure of the imports-graph.
Is there some better method how to get the desired lemmas, especially
the ones that are declared as [simp] and hence should be filled into the
simpset?

If you want too keep the diamond theory hierarchy because "inst" contains a lengthy proof of the interpretation theorem, you might consider leaving the proof in "inst" but move the interpretation to "use". This is, however, not going to work very well if you have a hierarchy of locales.

Clemens






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