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