1

There's an Isabelle/HOL library that I want to build on with new definitions and proofs. The library defines locale2, which I'd like to build upon. Inside locale2, there's an interpretation of locale1.

To extend locale2 in a separate theory, I define locale3 = locale2. Inside locale3, however, I can't figure out how to access locale2's interpretation of locale1. How can I do that? (Am I even going about this in the right way at all?)

Below is an MWE. This is the library theory with the locale I want to extend:

theory ExistingLibrary
  imports Main
begin

(* this is the locale with the function I want *)
locale locale1 = assumes True
begin

fun inc :: "nat ⇒ nat"
  where "inc n = n + 1"

end

(* this is the locale that interprets the locale I want *)
locale locale2 = assumes True
begin

interpretation I: locale1
  by unfold_locales auto

end
end

This is my extension theory. My attempt is at the bottom, causing an error:

theory MyExtension
  imports ExistingLibrary
begin

locale locale3 = locale2
begin

definition x :: nat
  where "x = I.inc 7" (* Undefined constant: "I.inc" *)

end
end

1 Answer 1

1

Interpretations inside a context last only until the end of the context. When the context is entered again, you have to repeat the interpretation to make the definitions and theorems available:

locale 3 = locale2 begin
interpretation I: locale1 <proof>

For this reason, I recommend to split the first interpretation step into two:

  1. A lemma with a name that proves the goal of the interpretation step.
  2. The interpretation command itself which can be proved by(rulelemma)

If you want the interpretation to take place whenever you open the locale and whenever you interpret the locale, then sublocale instead of interpretation might be better.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.