Quelle  Axioms.thy

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