Theory Axioms_Complement

section ‹Axioms of complements›

theory Axioms_Complement
  imports Laws
begin

typedecl ('a, 'b) complement_domain
instance complement_domain :: (domain, domain) domain..

― ‹We need that there is at least one object in our category. We call is \<^term>‹some_domain›.›
typedecl some_domain
instance some_domain :: domain..

axiomatization where 
  complement_exists: ‹register F ⟹ ∃G :: ('a, 'b) complement_domain update ⇒ 'b update. compatible F G ∧ iso_register (F;G)› for F :: ‹'a::domain update ⇒ 'b::domain update›

axiomatization where complement_unique: ‹compatible F G ⟹ iso_register (F;G) ⟹ compatible F H ⟹ iso_register (F;H)
          ⟹ equivalent_registers G H› 
    for F :: ‹'a::domain update ⇒ 'b::domain update› and G :: ‹'g::domain update ⇒ 'b update› and H :: ‹'h::domain update ⇒ 'b update›

end