Instanzen in Gebietsschema-Deklaration für Isabelle

Question

Ich habe ein bestimmtes Gebietsschema deklariert, das mehrere Dinge behebt und versuche, ein neues Gebietsschema für Morphismen des ersten zu deklarieren. Hier ist der erste 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))" 

Am Ende dieser Erklärung, erhalte ich die folgende Ausgabe:

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" 

Also dachte ich, ich von der letzten Zeile extrahieren konnte, was ich benötigen, um ein definieren neues Gebietsschema mit zwei Instanzen des Gebiets "presheaf" Das ist, was ich versuchte:

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) 

Kurz gesagt, ich zwei presheaves F und G reparieren will und dann fix diesen Parameter „morphism“ und die Dinge übernehmen „morphism“ beteiligt und das „restrictionsmap“ und „objectsmap“ von F und G. Dieser Versuch von mir führte zu:

Illegal freien Variablen im Ausdruck: "T", "R", "opcatopensets", "restrictionsmap"

ich glaube, ich don‘ Ich verstehe, wie Sie dies tun, wenn das Gebietsschema, das Sie instantiieren möchten e behebt mehr als eine Sache. Was verursacht diesen Fehler und wie könnte ich tun, was ich möchte?

Answer 1

Sie können mehrere Instanzen eines Gebietsschemas problemlos zu einem neuen kombinieren, aber normalerweise müssen Sie die Parameter der Gebietsschemas umbenennen und sie entsprechend mit for deklarieren. In Ihrem Code haben Sie nur den Parameter objectsmap in F bzw. G umbenannt und die Präfixe F und G hinzugefügt, um auf die beiden Instanzen zu verweisen. Die anderen Parameter T, R, opcatopensets und restrictionsmap wurden jedoch nicht umbenannt und fehlen in der Klausel for der Gebietsschemaerklärung. Das ist der Grund für die Fehlermeldung. Also sollten Sie sie zur for Klausel hinzufügen und es sollte funktionieren. Beide Instanzen des Gebietsschemas verwenden jedoch dieselben T, R, opcatopensets und restrictionsmap. Wenn das nicht beabsichtigt ist, sollten Sie sie auch umbenennen.

Zum Beispiel die folgende Erklärung

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 ... 

umbenennt alle Argumente der beiden Instanzen. Im Gegensatz dazu benennt das Folgende den Morphismus nur in F und G um.

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 ...