Используя определение, чтобы произвести конкретный пример локали в Isabelle

Question

Я работаю над теорией, которая требует использования колец, так что я ввозимые следующие теории: https://www.isa-afp.org/browser_info/devel/AFP/Group-Ring-Module/

Прямо сейчас, я определил множество X определенного типа, и я бы хотел определить операции над ним, чтобы сделать его кольцом, как в локали «Кольцо» импортируемой теории.

Как определить кольцо с несущей X и распознать его как экземпляр локали «Кольцо»?

Языковой «Кольцо» объявляется путем расширения «AGroup», который, в свою очередь, определяется как путем расширения «Группа», которая в теории «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" 

Другая возможная проблема I antecipate: если я не ошибаюсь, оператор должен иметь тип «набор», но мой набор X имеет тип («набор \ times» a) установленный набор. Есть ли обходной путь?

EDIT: Чтобы лучше сформулировать последовательный вопрос в комментариях, вот несколько частей того, что я сделал. Все, что следует находится в контексте языковой предпучка, который фиксирует (среди прочего):

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

я тогда доказал, что для каждого х, stalkrel х является отношением эквивалентности, и определяются:

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

Я пытаюсь показать, что для каждой й этой ножки х представляет собой кольцо, а операция кольца «Буй 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.