[isabelle] Interpreting a locale on it's own underlying definitions



I'm trying to ensure that any theorem attributes given in a locale are propagated to the locale's underlying global definitions. Here's an example:

locale L =
  fixes a :: int
begin

definition
   x :: int where
  "x = a"

lemma r[simp]: "x + a = 2 * a"
by (simp add: x_def)

end

interpretation L [a] .

I then use the interpretation command above to ensure that the simp rule "r" in L is installed for the locale's underlying global definition L.x. This works, but with an unintended side-effect: The definition of f below causes a type error, because the interpretation command has also installed the unqualified name "x" into the namespace.

definition
  f :: "('a \<Rightarrow> 'a)" where
 "f x = foo"

How can I perform a locale interpretation that targets the current background theory, but that doesn't add the unqualified names of the locale definitions to the background theory? Note that some of these definitions may occur after the original interpretation command.

Thanks,
-john






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