Re: [isabelle] Locale interpretations and imported theories
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and