*To*: Clemens Ballarin <ballarin at in.tum.de>*Subject*: Re: [isabelle] Interpreting a locale on it's own underlying definitions*From*: John Matthews <matthews at galois.com>*Date*: Thu, 3 Jul 2008 14:38:15 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <5A27963F-879E-4AB0-A5DD-F638C35941E5@in.tum.de>*References*: <49FB7AA0-BA5B-47C5-98A1-06B7AE7E21A3@galois.com> <5A27963F-879E-4AB0-A5DD-F638C35941E5@in.tum.de>

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 termlanguage of the target at all. This feature has sneaked in and isnow 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 bequalified by bla in the target, which causes less pollution of thetarget'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 localeare 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 simprule "r" in L is installed for the locale's underlying globaldefinition L.x. This works, but with an unintended side-effect: Thedefinition of f below causes a type error, because theinterpretation 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 currentbackground theory, but that doesn't add the unqualified names ofthe locale definitions to the background theory? Note that some ofthese definitions may occur after the original interpretationcommand.Thanks, -john

**References**:**Re: [isabelle] Interpreting a locale on it's own underlying definitions***From:*Clemens Ballarin

- Previous by Date: Re: [isabelle] types and placeholders
- Next by Date: [isabelle] Finding theorems via intro
- Previous by Thread: Re: [isabelle] Interpreting a locale on it's own underlying definitions
- Next by Thread: [isabelle] UITP'08: Call for System Demonstrations
- Cl-isabelle-users July 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list