Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Interpreting a locale on it's own underlying d...

Email Gateway (Aug 18 2022 at 12:06):

From: John Matthews <matthews@galois.com>
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

Last updated: May 03 2024 at 04:19 UTC