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

Question

I'm working on a theory that requires usage of rings, so I imported the following theories: https://www.isa-afp.org/browser_info/devel/AFP/Group-Ring-Module/

Right now, I have defined a set X of a certain type and I'd like to define operations on it to make it a ring, as in the locale "Ring" of the imported theory.

How do I define a ring with carrier X and have it recognized as an instance of the locale "Ring"?

The locale "Ring" is declared by extending "aGroup", which in turn is declared by extending "Group", which is in the theory "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"

Another possible problem I antecipate: if I'm not mistaken, the carrier must be of type 'a set, but my set X is of type ('a set \times 'a) set set. Is there a workaround?

EDIT: In order to better formulate the sequential question in the comments, here are some pieces of what I did. All that follows is within the context of a locale presheaf, that fixes (among other things):

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

I then introduced the following:

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

I then proved that for each x, stalkrel x is an equivalence relation, and defined:

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

I'm trying to show that for each x this stalk x is a ring, and the ring operation is "built" out of the ring operations of rings objectsmap (U∩V) , i.e, I'd like germ x U s + germ x V t to be germ x (U∩V) (restrictionsmap (U, (U∩V)) s + restrictionsmap (V, (U∩V)) t), where this last sum is the sum of ring objectsmap (U∩V).

Answer 1

A multiplicative Group in the AFP entry mentioned is a record with four fields: a set carrier for the carrier, the binary group operation top, the inverse operation iop and the neutral element one. Similarly, a Ring is a record which extends an additive group (record aGroup with fields carrier, pop, mop, zero) with the binary multiplicative operation tp and the multiplicative unit un. If you want to define an instance of a group or record, you must define something of the appropriate record type. For example,

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

where you have to replace all the <...> by the types and terms for your ring. That is, <el> is the type of the ring elements, <c> is the carrier set, etc. Note that you can specialise the type of ring elements as needed.

In order to prove that my_ring is indeed a ring, you must show that it satisfies the assumptions of the corresponding locale Ring:

lemma "Ring my_ring"
proof unfold_locales
  ...
qed

If you want to use the theorems that have been proven abstractly for arbitrary rings, you may want to interpret the locale using interpretation.