# Theory Axioms

```section ‹Axioms of registers›

theory Axioms
imports Main
begin

class domain
instance prod :: (domain,domain) domain
by intro_classes

typedecl 'a update
axiomatization comp_update :: "'a::domain update ⇒ 'a update ⇒ 'a update" where
comp_update_assoc: "comp_update (comp_update a b) c = comp_update a (comp_update b c)"
axiomatization id_update :: "'a::domain update" where
id_update_left: "comp_update id_update a = a" and
id_update_right: "comp_update a id_update = a"

axiomatization preregister :: ‹('a::domain update ⇒ 'b::domain update) ⇒ bool›
axiomatization where
comp_preregister: "preregister F ⟹ preregister G ⟹ preregister (G ∘ F)" and
id_preregister: ‹preregister id›
for F :: ‹'a::domain update ⇒ 'b::domain update› and G :: ‹'b update ⇒ 'c::domain update›

axiomatization where
preregister_mult_right: ‹preregister (λa. comp_update a z)› and
preregister_mult_left: ‹preregister (λa. comp_update z a)›
for z :: "'a::domain update"

axiomatization tensor_update :: ‹'a::domain update ⇒ 'b::domain update ⇒ ('a×'b) update›
where tensor_extensionality: "preregister F ⟹ preregister G ⟹ (⋀a b. F (tensor_update a b) = G (tensor_update a b)) ⟹ F = G"
for F G :: ‹('a×'b) update ⇒ 'c::domain update›

axiomatization where tensor_update_mult: ‹comp_update (tensor_update a c) (tensor_update b d) = tensor_update (comp_update a b) (comp_update c d)›
for a b :: ‹'a::domain update› and c d :: ‹'b::domain update›

axiomatization register :: ‹('a update ⇒ 'b update) ⇒ bool›
axiomatization where
register_preregister: "register F ⟹ preregister F" and
register_comp: "register F ⟹ register G ⟹ register (G ∘ F)"  and
register_mult: "register F ⟹ comp_update (F a) (F b) = F (comp_update a b)" and
register_of_id: ‹register F ⟹ F id_update = id_update› and
register_id: ‹register (id :: 'a update ⇒ 'a update)›
for F :: "'a::domain update ⇒ 'b::domain update" and G :: "'b update ⇒ 'c::domain update"

axiomatization where register_tensor_left: ‹register (λa. tensor_update a id_update)›
axiomatization where register_tensor_right: ‹register (λa. tensor_update id_update a)›

axiomatization register_pair ::
‹('a::domain update ⇒ 'c::domain update) ⇒ ('b::domain update ⇒ 'c update)
⇒ (('a×'b) update ⇒ 'c update)› where
register_pair_is_register: ‹register F ⟹ register G ⟹ (⋀a b. comp_update (F a) (G b) = comp_update (G b) (F a))
⟹ register (register_pair F G)› and
register_pair_apply: ‹register F ⟹ register G ⟹ (⋀a b. comp_update (F a) (G b) = comp_update (G b) (F a))
⟹ (register_pair F G) (tensor_update a b) = comp_update (F a) (G b)›

end
```