Isabelleのロケール宣言のインスタンス

Question

複数のものを修正する特定のロケールを宣言し、最初のものの新しいロケールを宣言しようとしています。ここで最初のロケールです：

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))" 

は、この宣言の終わりに、私は次のような出力が得られます。

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" 

だから私は、私は私が定義するために必要なものを最後の行から抽出できると思っていましたロケール "presheaf"の2つのインスタンスを含む新しいロケール。これは私が試したものです：

短い、私は2つのpresheaves FとGを修正して、このパラメータを修正したい「射」で

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) 

と「射」と「restrictionsmap」との「objectsmap」を含むものと仮定します式の中

違法自由変数：FおよびGは、私のこの試みはにつながった "T"、 "R"、 "opcatopensets"、 "restrictionsmap"

私はドンと仮定します」ロケールをインスタンシエートするときにこれを行う方法を理解するeは複数のものを修正します。このエラーの原因は何ですか？また、私は何をしたいのですか？

Answer 1

ロケールの複数のインスタンスを新しいインスタンスに簡単に結合できますが、通常はロケールのパラメータの名前を変更し、それに応じてforで宣言する必要があります。あなたのコードでは、パラメータobjectsmapをそれぞれFとGに変更し、2つのインスタンスを参照する接頭辞FとGを追加しました。ただし、その他のパラメータT,R,opcatopensets、およびrestrictionsmapは、ロケール宣言のfor句には名前が変更されておらず、存在しません。これがエラーメッセージの理由です。ですので、それらをfor節に追加するとうまくいくはずです。ただし、ロケールの両方のインスタンスでは、同じT,R,opcatopensetsおよびrestrictionsmapを使用します。これが意図したものでない場合は、名前を変更する必要があります。例えば

、次の宣言

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

は、2つのインスタンスのすべての引数を変更します。対照的に、次の例では、モルフォミックスの名前をFと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 ...