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