localeisabelleinterpretation

Locale inheritance after interpretation

I am trying to understand how "inheritance" work at locale/interpretation level. I have an abstract locale (locA), with a method (g) defined within it. I have a concrete locale (locB), which is an instance/model of the abstract one. Is there a way to use the g method in such a way that I don't get a "type unification" error?

Below is a toy example of what I am trying to achieve

theory InstOverwrite

imports Main
begin

locale locA = 
  fixes f :: "'a ⇒ 'b"
begin

definition g :: "'a set ⇒ 'b set" where 
  "g X = f`X"
end

locale locB = 
  fixes fb :: "nat ⇒ nat"
  assumes fb_def: "fb n = n*2"
begin

interpretation locA
  apply unfold_locales
  done
end

context locB
begin
definition fx :: "nat set ⇒ nat set" where
  "fx X = {n+1 | n::nat. n ∈ locA.g X}"
end

end

Unsurprisingly, I get the following error:

Type unification failed: Clash of types "_ set" and "_ ⇒ _"

Type error in application: incompatible operand type

Operator:  locA.g :: (??'a ⇒ ??'b) ⇒ ??'a set ⇒ ??'b set
Operand:   X :: nat set
Solution

  • Quick fix

    Within your code, you have not actually connected the two locales.

    locA.g exists “outside” the locale context in the sense that it must be supplied an f :: "'a ⇒ 'b" in order to be used. This is what Isabelle tries to express by stressing Operator: locA.g :: (??'a ⇒ ??'b) ⇒ ??'a set ⇒ ??'b set. So, in order to make the type checker happy here, you would need to explicitly say that fb should serve as f in the function application.

    definition fx :: "nat set ⇒ nat set" where
  "fx X = {n+1 | n::nat. n ∈ locA.g fb X}"

    (The only difference is writing locA.g fb X instead of locA.g X.)

    Providing parameters to interpretation

    From your description of the problem, I gather that you hoped interpretation locA would have taken care of establishing this connection. This is not the case.

    To establish the instantiation that f := fb, you would need to supply parameters to the interpretation. The following would work:

    interpretation locA fb .

definition fx :: "nat set ⇒ nat set" where
  "fx X = {n+1 | n::nat. n ∈ g X}"

    (Note that it's now g X instead of locA.g fb X!)

    Maybe rather sublocale?

    I conveniently dropped the end/begin context from the example script. The reason being that the context jumps would kill the interpretation. If you want the connection to persist across contexts, the sublocale keyword is more appropriate:

    sublocale "locA" fb .
end (* of locale context locB *)

(* somewhere else we may add to the locale again: *)

definition (in locB) fy :: "nat set ⇒ nat set" where
  "fy X = {n+1 | n::nat. n ∈ g X}"

    Further notes on locale inheritance

    Depending on what you're actually wanting to do, an even more different formulation might make sense. I assume that the listing is just the way it is to have some minimal example.

    For people bumping into this question, I want to note that the locale inheritance situation here might be expressed more conveniently by one of the two following approaches:

    A) Make locB extend locA:

    The following will use the same f for both locales directly and just add the defining assumption:

    locale locB = 
  locA f for f :: "nat ⇒ nat" +
  assumes f_def: "f n = n*2"

    B) Make locB instantiate parameters for locA

    definition fb :: "nat ⇒ nat" where "fb n ≡ n * 2"

locale locB = 
  locA fb