[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
locale L =
fixes a :: int
x :: int where
"x = a"
lemma r[simp]: "x + a = 2 * a"
by (simp add: x_def)
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and