CODEWITHSUNDEEP
isabelle
José Siqueira
José Siqueira

Reputation: 191

Instances in locale declaration for Isabelle

I've declared a certain locale which fixes multiple things and am trying to declare a new locale for morphisms of the first. Here's the first locale:

locale presheaf = topology + Ring +
fixes 
opcatopensets ::" ('a) PosetalCategory" and
objectsmap :: "'a set ⇒ ('a, 'm) Ring_scheme" and
restrictionsmap:: "('a set ×'a set) ⇒ ('a  ⇒ 'a)"
assumes 
"opcatopensets  ≡ ⦇ Obj = {x. x ∈ T} , Mor = {(x,y)| x y. (x,y) ∈ revpo} ,
 Dom = psheafdom , Cod  = psheafcod , Id  = psheafid  , Comp = psheafcomp ⦈" and
"∀y w. w ≠ y ⟶ (psheafcomp (x,y) (w,z) = undefined)" and
"∀x. x ∉ T ⟶ (objectsmap x = undefined)" and
"∀x y.(restrictionsmap (x,y)) ∈ rHom (objectsmap x) (objectsmap y)" and
"∀ x y . (restrictionsmap (x,x) y = y) " and
"∀ x y z .  ( (restrictionsmap (y,z))∘(restrictionsmap (x,y)) = restrictionsmap(x,z) )"

At the end of this declaration, I get the following output:

locale presheaf =
  fixes T :: "'a set set" 
    and R :: "('b, 'c) Ring_scheme" 
    and opcatopensets :: "'a PosetalCategory" 
    and objectsmap :: "'a set ⇒ ('a, 'm) Ring_scheme" 
    and restrictionsmap :: "'a set × 'a set ⇒ 'a ⇒ 'a" 
  assumes "presheaf T R opcatopensets objectsmap restrictionsmap"

So I thought I could extract from the last line what I needed in order to define a new locale involving two instances of the locale "presheaf". This is what I tried:

locale sheafmorphism = 
F: presheaf T  R opcatopensets F restrictionsmap + G: presheaf T R opcatopensets
G restrictionsmap 
for F and G  +
fixes morphism :: "'a set ⇒ ('a ⇒ 'a)"
assumes  (things)

In short, I want to fix two presheaves F and G and then fix this parameter "morphism" and assume things involving "morphism" and the "restrictionsmap" and "objectsmap" of F and G. This attempt of mine led to:

Illegal free variables in expression: "T", "R", "opcatopensets", "restrictionsmap"

I suppose I don't understand how to do this when the locale you want to instantiate fixes more than one thing. What is causing this error and how could I do what I'd like?

Upvotes: 1

Views: 205

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5078

You can easily combine several instances of a locale into a new one, but you typically must rename the parameters of the locales and declare them accordingly with for. In your code, you only renamed the parameter objectsmap to F and G respectively, and added the prefixes F and G to refer to the two instances. However, the other parameters T, R, opcatopensets, and restrictionsmap have not been renamed and are missing in the for clause of the locale declaration. That is the reason for the error message. So you should add them to the for clause and it should work. However, both instances of the locale will use the same T, R, opcatopensets and restrictionsmap. If this is not what you intended, then you should rename them, too.

For example, the following declaration

locale sheafmorphism = 
  F: presheaf T1 R1 opcatopensets1 F restrictionsmap1 +
  G: presheaf T2 R2 opcatopensets2 G restrictionsmap2 
  for T1 R1 opcatopensets1 F restrictionsmap1
      T2 R2 opcatopensets2 G restrictionsmap2 +
  fixes morphism :: "'a set ⇒ ('a ⇒ 'a)"
  assumes ...

renames all arguments of the two instances. In contrast, the following only renames the morphism to F and G.

locale sheafmorphism = 
  F: presheaf T R opcatopensets F restrictionsmap +
  G: presheaf T R opcatopensets G restrictionsmap 
  for T R opcatopensets F G restrictionsmap +
  fixes morphism :: "'a set ⇒ ('a ⇒ 'a)"
  assumes ...

Upvotes: 2

Related Questions