使用定义生成 Isabelle 语言环境的特定示例

Question

我正在研究一个需要使用环的理论，所以我导入了以下理论：https://www.isa-afp.org/browser_info/devel/AFP/Group-Ring-Module/

现在，我已经定义了一个特定类型的集合 X，我想在它上面定义操作使其成为一个环，就像在导入理论的语言环境 "Ring" 中一样。

如何定义带有运营商 X 的环并将其识别为区域设置实例 "Ring"？

locale "Ring" 是通过扩展 "aGroup" 声明的，而后者又是通过扩展 "Group" 声明的，理论上是 "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"

我预料的另一个可能的问题：如果我没记错的话，载体必须是'a set类型，但是我的集合X是类型('a set \times 'a) set set。有解决方法吗？

编辑：为了更好地表述评论中的顺序问题，这里是我所做的一些工作。以下所有内容都在区域设置 presheaf 的上下文中，它修复了（除其他外）：

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 是一个环，并且环操作是 "built" 在环 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确实是环，必须证明它满足对应locale的假设Ring:

lemma "Ring my_ring"
proof unfold_locales
  ...
qed

如果您想使用已被抽象证明的任意环定理，您可能需要使用 interpretation.

解释语言环境

使用定义生成 Isabelle 语言环境的特定示例

Using a definition to produce an specific example of a locale in Isabelle

isabelle