Theory Axioms_Complement

section ‹Axioms of complements›

theory Axioms_Complement
  imports Laws With_Type.With_Type
begin

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

setup ‹ (* Supporting with-type for the dummy class `domain` *)
With_Type.add_with_type_info_global {
  class = \<^class>‹domain›,
  rep_class = \<^const_name>‹WITH_TYPE_CLASS_type›,
  rep_rel = \<^const_name>‹WITH_TYPE_REL_type›,
  with_type_wellformed = @{thm with_type_wellformed_type},
  param_names = [],
  transfer = NONE,
  rep_rel_itself = NONE
}›

class domain_with_simple_complement = 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_with_simple_complement ..

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

(* Short for "complement domain carrier" *)
axiomatization cdc :: ‹('a::domain update ⇒ 'b::domain update) ⇒ ('a,'b) complement_domain set› where 
  complement_exists: ‹register F ⟹ let 'c::domain = cdc F in
                      ∃G :: 'c 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