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