使用定義產生伊莎貝爾

Question

我的工作，需要環的使用理論區域設置的一個具體的例子，所以我輸入以下理論：https://www.isa-afp.org/browser_info/devel/AFP/Group-Ring-Module/

現在，我已經定義了一組X我想定義一個操作來使它成爲一個環，就像導入理論的「環」一樣。

如何定義帶載體X的環並將其識別爲區域設置「環」的實例？

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" 

另一個可能的問題我：

語言環境「環」通過延長「aGroup」，而這又是通過延長「集團」，這是在理論上「Algebra2.thy」聲明宣佈預測：如果我沒有弄錯，承運人必須是'一組'的類型，但是我的集合X是類型的（'集合\時間'a）集合集合。有沒有解決方法？

編輯：爲了更好地制定評論中的順序問題，這裏有一些我做了什麼。所有下面是一個語言環境預層，用於固定的範圍內（除其他外）：

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

我接着介紹了以下內容：

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

我然後證明，對於每個x stalkrel x是一個等價關係，以及定義：

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

我試圖表明，對每個x此稈x是一個環，環的操作是「BUI lt「出環objectsmap (U∩V)的環操作，即，我想germ x U s + germ x V t爲germ x (U∩V) (restrictionsmap (U, (U∩V)) s + restrictionsmap (V, (U∩V)) t)，其中最後的總和是環objectsmap (U∩V)的總和。

Answer 1

中提到的AFP條目乘法Group是具有四個字段的記錄：用於載體的一組carrier，二進制組操作top，逆運算iop和中性元素one。類似地，Ring是其延伸的加法羣（記錄aGroup與字段carrier，pop，mop，zero）與二進制乘法運算tp和乘法單元un的記錄。如果要定義組或記錄的實例，則必須定義適當的記錄類型。例如，

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

，你必須全部更換<...>的種類和條款戒指。也就是說，<el>是環形元素的類型，<c>是載體集合等。請注意，您可以根據需要專門設計環形元素的類型。

爲了證明my_ring確實是一個戒指，你必須表明它滿足相應的語言環境Ring的假設：

lemma "Ring my_ring" 
proof unfold_locales 
    ... 
qed 

如果你想使用已抽象地證明任意定理環，您可能需要使用interpretation來解釋區域設置。