[isabelle] Locale interpretations and imported theories



Hi all,

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

The problem is, that I need to use the added lemma in the
interpretation. However, it is not visible in the theory "use".
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".

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?

Regards,
  Peter

Here follows a boiled-down example: (I also attached a tgz with the four
thy-files)

theory "use"
imports inst add
begin

  thm int.orig   -- "Works"
  thm l.added    -- "The theorem is in the locale"
  (* thm int.added  -- "Does not work ... ok, would have to be merged on
import" *)

  interpretation xxx: l .

  -- "The namespace below xxx seems to be empty ?"
  thm xxx.orig  -- "Does not work"
  thm xxx.added -- "Does not work"

end

-------------------------------------------

theory "def"
imports Main
begin
  locale l
  begin
    lemma orig: True ..

  end
end

------------------------------------------

theory add
imports "def"
begin

  context l begin
    lemma added: "x=x" ..
  end

end

------------------------------------------

theory inst
imports "def"
begin


  interpretation int: l .

  thm int.orig

end
------------------------------------------


Attachment: strange.tgz
Description: application/compressed-tar



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