eine Definition Mit Hilfe ein spezielles Beispiel einer locale in Isabelle

Question

Ich arbeite an einer Theorie zu produzieren, die Verwendung von Ringen erfordert, so importierte ich die folgenden Theorien: https://www.isa-afp.org/browser_info/devel/AFP/Group-Ring-Module/

Im Moment habe ich eine Menge X definiert von einem bestimmten Typ, und ich möchte Operationen darauf definieren, um es zu einem Ring zu machen, wie im Gebietsschema "Ring" der importierten Theorie.

Wie definiere ich einen Ring mit Träger X und habe es als eine Instanz des Gebiets "Ring" erkannt?

Die locale „Ring“ wird durch die Erweiterung „CGRUPPE“ erklärt, der wiederum durch die Erweiterung „Gruppe“ erklärt, die in der Theorie ist „Algebra2.thy“:

record 'a Group = "'a carrier" + 
    top  :: "['a, 'a ] ⇒ 'a" (infixl "⋅ı" 70) 
    iop  :: "'a ⇒ 'a" ("ρı _" [81] 80) 
    one  :: "'a" ("ı") 

locale Group = 
fixes G (structure) 
assumes top_closed: "top G ∈ carrier G → carrier G → carrier G" 
and  tassoc : "⟦a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ 
     (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)" 
and  iop_closed:"iop G ∈ carrier G → carrier G" 
and  l_i :"a ∈ carrier G ⟹ (ρ a) ⋅ a = " 
and  unit_closed: " ∈ carrier G" 
and  l_unit:"a ∈ carrier G ⟹ ⋅ a = a" 

Ein weiteres mögliches Problem, das ich antecipate: Wenn ich mich nicht irre, muss der Träger vom Typ 'a set sein, aber meine Menge X ist vom Typ (' a set \ times 'a) gesetzt. Gibt es eine Problemumgehung?

EDIT: Um die sequenzielle Frage in den Kommentaren besser zu formulieren, hier sind einige Teile von dem, was ich getan habe. ,

definition prestalk :: "'a ⇒('a set × 'a) set" where 
"prestalk x = { (U,s). (U ∈ T) ∧ x ∈U ∧ (s ∈ carrier (objectsmap U))}" 


definition stalkrel :: "'a ⇒ (('a set × 'a) × ('a set × 'a)) set" where 
"stalkrel x = {((U,s), (V,t)). (U,s) ∈ prestalk x ∧ (V,t) ∈ prestalk x ∧ (∃W. W ⊆ U∩V ∧ x∈W ∧ 
restrictionsmap (V,W) t = restrictionsmap (U,W)) s} " 

ich bewiesen dann, dass für jedes x: Alles, was im Rahmen eines Gebietsschema presheaf, das behebt folgt ist (unter anderem):

T :: 'a set set and 
objectsmap :: "'a set ⇒ ('a, 'm) Ring_scheme" and 
restrictionsmap:: "('a set ×'a set) ⇒ ('a ⇒ 'a)" 

Ich stellte dann die folgende stalkrel x ist eine Äquivalenzrelation und definiert:

definition germ:: "'a ⇒ 'a set ⇒ 'a ⇒ ('a set × 'a) set" where 
"germ x U s = {(V,t). ((U,s),(V,t)) ∈ stalkrel x}" 

definition stalk:: "'a ⇒(('a set × 'a) set) set" where 
"stalk x = {w. (∃ U s. w = germ x U s ∧ (U,s) ∈ prestalk x) }" 

ich versuche, dass jeder zu zeigen, für x diesen Stiel x ist ein Ring, und der Ring Betrieb ist „bui Aus den Ringoperationen von Ringen objectsmap (U∩V), d. h. ich möchte germ x U s + germ x V t zu germ x (U∩V) (restrictionsmap (U, (U∩V)) s + restrictionsmap (V, (U∩V)) t), wobei diese letzte Summe die Summe von Ring objectsmap (U∩V) ist.

Answer 1

A multiplikativen Group in der erwähnten AFP Eintrag ist ein Datensatz mit vier Feldern: ein Satz carrier für den Träger, die binäre Gruppenoperation top, die inverse Operation iop und das neutrale Element one. In ähnlicher Weise ist ein Ring ein Datensatz, der eine additive Gruppe (record aGroup mit Feldern carrier, pop, mop, zero) sich mit der binären multiplikativen Operation tp und die multiplikative Einheit un. Wenn Sie eine Instanz einer Gruppe oder eines Datensatzes definieren möchten, müssen Sie etwas vom entsprechenden Datensatztyp definieren. Zum Beispiel

definition my_ring :: "<el> Ring" where 
    "my_ring = 
    (|carrier = <c>, 
    pop = <plus>, 
    mop = <minus>, 
    zero = <0>, 
    tp = <times>, 
    un = <unit>|)" 

, wo Sie ersetzen alle <...> durch die Art und die Bedingungen für Ihren Ring. Das heißt, <el> ist der Typ der Ringelemente, <c> ist der Trägersatz usw. Beachten Sie, dass Sie die Art der Ringelemente nach Bedarf spezialisieren können.

Um diese my_ring ist in der Tat ein Ring zu beweisen, müssen Sie zeigen, dass es die Annahmen des entsprechenden locale erfüllt Ring:

lemma "Ring my_ring" 
proof unfold_locales 
    ... 
qed 

Wenn Sie die Sätze verwenden möchten, die für beliebige bewährt abstrakt haben Sie möchten möglicherweise das Gebietsschema mithilfe von interpretation interpretieren.