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



Thanks Clemens, we'll give this a try.

Cheers,
-john

On Jul 1, 2008, at 4:41 AM, Clemens Ballarin wrote:

Dear John,

in my view, interpretations should not add names to the term language of the target at all. This feature has sneaked in and is now hard to get rid off, because some developments depend on it.

interpretation L [a] .

What you can to is make in interpretation qualified:

interpretation bla: L [a] .

The effect is that all names (theorem names and definitions) will be qualified by bla in the target, which causes less pollution of the target's name space.

Clemens


On 27 Jun 2008, at 2:27, John Matthews wrote:

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.