Theory Catoid

(*
Title: Catoids
Author: Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Catoids›

theory Catoid
  imports Main

begin

subsection ‹Multimagmas›

text ‹Multimagmas are sets equipped with multioperations. Multioperations are isomorphic to ternary relations.›

class multimagma =
  fixes mcomp :: "'a ⇒ 'a ⇒ 'a set" (infixl "⊙" 70)

begin

text ‹I introduce notation for the domain of definition of the multioperation.›

abbreviation "Δ x y ≡ (x ⊙ y ≠ {})"

text ‹I extend the multioperation to powersets›

definition conv :: "'a set ⇒ 'a set ⇒ 'a set" (infixl "⋆" 70) where
  "X ⋆ Y = (⋃x ∈ X. ⋃y ∈ Y. x ⊙ y)"

lemma conv_exp: "X ⋆ Y = {z. ∃x y. z ∈ x ⊙ y ∧ x ∈ X ∧ y ∈ Y}"
  unfolding conv_def by fastforce

lemma conv_exp2: "(z ∈ X ⋆ Y) = (∃x y. z ∈ x ⊙ y ∧ x ∈ X ∧ y ∈ Y)"
  by (simp add: multimagma.conv_exp)

lemma conv_distl: "X ⋆ ⋃𝒴 = (⋃Y ∈ 𝒴. X ⋆ Y)"
  unfolding conv_def by blast

lemma conv_distr: "⋃𝒳 ⋆ Y = (⋃X ∈ 𝒳. X ⋆ Y)"
  unfolding conv_def by blast

lemma conv_distl_small: "X ⋆ (Y ∪ Z) = X ⋆ Y ∪ X ⋆ Z"
  unfolding conv_def by blast

lemma conv_distr_small: "(X ∪ Y) ⋆ Z  = X ⋆ Z ∪ Y ⋆ Z"
  unfolding conv_def by blast

lemma conv_isol: "X ⊆ Y ⟹ Z ⋆ X ⊆ Z ⋆ Y"
  using conv_exp2 by fastforce

lemma conv_isor: "X ⊆ Y ⟹ X ⋆ Z ⊆ Y ⋆ Z"
  using conv_exp2 by fastforce

lemma conv_atom [simp]: "{x} ⋆ {y} = x ⊙ y"
  by (simp add: conv_def)

end


subsection ‹Multisemigroups›

text ‹Sultisemigroups are associative multimagmas.›

class multisemigroup = multimagma +
  assumes assoc: "(⋃v ∈ y ⊙ z. x ⊙ v) = (⋃v ∈ x ⊙ y. v ⊙ z)"

begin

lemma assoc_exp: "(∃v. w ∈ x ⊙ v ∧ v ∈ y ⊙ z) = (∃v. v ∈ x ⊙ y ∧ w ∈ v ⊙ z)"
  using assoc by blast

lemma assoc_var: "{x} ⋆ (y ⊙ z) = (x ⊙ y) ⋆ {z}"
  unfolding conv_def assoc_exp using local.assoc by force

text ‹Associativity extends to powersets.›

lemma conv_assoc: "X ⋆ (Y ⋆ Z) = (X ⋆ Y) ⋆ Z"
  unfolding conv_exp using assoc_exp by fastforce

end


subsection ‹st-Multimagmas›

text ‹I equip multimagmas with source and target maps.›

class st_op =
  fixes src :: "'a ⇒ 'a" ("σ")
  and tgt :: "'a ⇒ 'a" ("τ")

class st_multimagma = multimagma + st_op +
  assumes Dst: "x ⊙ y ≠ {} ⟹ τ x = σ y"
  and s_absorb [simp]: "σ x ⊙ x = {x}"
  and t_absorb [simp]: "x ⊙ τ x = {x}"

text ‹The following sublocale proof sets up opposition/duality.›

sublocale st_multimagma ⊆ stopp: st_multimagma "λx y. y ⊙ x" tgt src
  rewrites "stopp.conv X Y = Y ⋆ X"
  by (unfold_locales, auto simp add: local.Dst multimagma.conv_def)

lemma (in st_multimagma) ts_compat [simp]: "τ (σ x) = σ x"
  by (simp add: Dst)

lemma (in st_multimagma) ss_idem [simp]: "σ (σ x) = σ x"
  by (metis local.stopp.ts_compat local.ts_compat)

lemma (in st_multimagma) st_fix: "(τ x = x) = (σ x = x)"
proof
  assume h1: "τ x = x"
  hence "σ x = σ (τ x)"
    by simp
  also have "… = x"
    by (metis h1 local.stopp.ts_compat)
  finally show "σ x = x".
next
  assume h2: "σ x = x"
  hence "τ x = τ (σ x)"
    by simp
  also have "… = x"
    by (metis h2 ts_compat)
  finally show "τ x = x".
qed

lemma (in st_multimagma) st_eq1: "σ x = x ⟹ σ x = τ x"
  by (simp add: local.stopp.st_fix)

lemma (in st_multimagma) st_eq2: "τ x = x ⟹ σ x = τ x"
  by (simp add: local.stopp.st_fix)

text ‹I extend source and target operations to powersets by taking images.›

abbreviation (in st_op) Src :: "'a set ⇒ 'a set" where
  "Src ≡ image σ"

abbreviation (in st_op) Tgt :: "'a set ⇒ 'a set" where
  "Tgt ≡ image τ"

text ‹Fixpoints of source and target maps model source and target elements.
These correspond to units.›

abbreviation (in st_op) sfix :: "'a set" where
  "sfix ≡ {x. σ x = x}"

abbreviation (in st_op) tfix :: "'a set" where
  "tfix ≡ {x. τ x = x}"

lemma (in st_multimagma) st_mm_rfix [simp]: "tfix = stopp.sfix"
  by simp

lemma (in st_multimagma) st_fix_set: "{x. σ x = x} = {x. τ x = x}"
  using local.st_fix by presburger

lemma (in st_multimagma) stfix_set: "sfix = tfix"
  using local.st_fix_set by blast

lemma (in st_multimagma) sfix_im: "sfix = Src UNIV"
  by (smt (verit, best) Collect_cong full_SetCompr_eq local.ss_idem)

lemma (in st_multimagma) tfix_im: "tfix = Tgt UNIV"
  using local.stopp.sfix_im by blast

lemma (in st_multimagma) ST_im: "Src UNIV = Tgt UNIV"
  using local.sfix_im local.stfix_set local.tfix_im by presburger

text ‹Source and target elements are "orthogonal" idempotents.›

lemma (in st_multimagma) s_idem [simp]: "σ x ⊙ σ x = {σ x}"
proof-
  have "{σ x} = σ x ⊙ τ (σ x)"
    using local.t_absorb by presburger
  also have "… = σ x ⊙ σ x"
    by simp
  finally show ?thesis..
qed

lemma (in st_multimagma) s_ortho:
  "Δ (σ x) (σ y) ⟹ σ x = σ y"
proof-
  assume "Δ (σ x) (σ y)"
  hence "τ (σ x) = σ (σ y)"
    using local.Dst by blast
  thus ?thesis
    by simp
qed

lemma (in st_multimagma) s_ortho_iff: "Δ (σ x) (σ y) = (σ x = σ y)"
  using local.s_ortho by auto

lemma (in st_multimagma) st_ortho_iff: "Δ (σ x) (τ y) = (σ x = τ y)"
  using local.Dst by fastforce

lemma (in st_multimagma) s_ortho_id: "(σ x) ⊙ (σ y) = (if (σ x = σ y) then {σ x} else {})"
  using local.s_ortho_iff by auto

lemma (in st_multimagma) s_absorb_var: "(σ y ≠ σ x) = (σ y ⊙ x = {})"
  using local.Dst by force

lemma (in st_multimagma) s_absorb_var2: "(σ y = σ x) = (σ y ⊙ x ≠ {})"
  using local.s_absorb_var by blast

lemma (in st_multimagma) s_absorb_var3: "(σ y = σ x) = Δ (σ x) y"
  by (metis local.s_absorb_var)

lemma (in st_multimagma) s_assoc: "{σ x} ⋆ (σ y ⊙ z) = (σ x ⊙ σ y) ⋆ {z}"
proof-
  {fix a
    have "(a ∈ {σ x} ⋆ (σ y ⊙ z)) = (∃b. a ∈ σ x ⊙ b ∧ b ∈ σ y ⊙ z)"
      by (simp add: local.conv_exp2)
    also have "… = (∃b. a ∈ σ x ⊙ b ∧ b ∈ σ y ⊙ z ∧ σ y = σ z)"
    using local.s_absorb_var by auto
  also have "… = (∃b. a ∈ σ x ⊙ b ∧ b ∈ σ y ⊙ z ∧ σ y = σ z ∧ σ x = σ y)"
    using local.stopp.Dst by fastforce
  also have "… = (∃b. b ∈ σ x ⊙ σ y ∧ a ∈ b ⊙ z ∧ σ y = σ z ∧ σ x = σ y)"
    by fastforce
  also have "… = (∃b. b ∈ σ x ⊙ σ y ∧ a ∈ b ⊙ z)"
    by (metis equals0D local.s_absorb_var3 local.s_idem singleton_iff)
  also have "… = (a ∈ (σ x ⊙ σ y) ⋆ {z})"
    using local.conv_exp2 by auto
  finally have "(a ∈ {σ x} ⋆ (σ y ⊙ z)) = (a ∈ (σ x ⊙ σ y) ⋆ {z})".}
  thus ?thesis
    by blast
qed

lemma (in st_multimagma) sfix_absorb_var [simp]: "(⋃e ∈ sfix. e ⊙ x) = {x}"
  apply safe
   apply (metis local.s_absorb local.s_absorb_var2 singletonD)
  by (smt (verit, del_insts) UNIV_I UN_iff imageI local.s_absorb local.sfix_im singletonI)

lemma (in st_multimagma) tfix_absorb_var: "(⋃e ∈ tfix. x ⊙ e) = {x}"
  using local.stopp.sfix_absorb_var by presburger

lemma (in st_multimagma) st_comm: "τ x ⊙ σ y = σ y ⊙ τ x"
  using local.Dst by fastforce

lemma (in st_multimagma) s_weak_twisted: "(⋃u ∈ x ⊙ y. σ u ⊙ x) ⊆ x ⊙ σ y"
  by (safe, metis empty_iff insertI1 local.Dst local.s_absorb local.t_absorb)

lemma (in st_multimagma) s_comm: "σ x ⊙ σ y = σ y ⊙ σ x"
  using local.Dst by force

lemma (in st_multimagma) s_export [simp]: "Src (σ x ⊙ y) = σ x ⊙ σ y"
  using local.Dst by force

lemma (in st_multimagma) st_prop: "(τ x = σ y) = Δ (τ x) (σ y)"
  by (metis local.stopp.s_absorb_var2 local.stopp.st_comm local.ts_compat)

lemma (in st_multimagma) weak_local_var: "τ x ⊙ σ y = {} ⟹ x ⊙ y = {}"
  using local.Dst local.st_prop by auto

text ‹The following facts hold by duality.›

lemma (in st_multimagma) st_compat: "σ (τ x) = τ x"
  by simp

lemma (in st_multimagma) tt_idem: "τ (τ x) = τ x"
  by simp

lemma (in st_multimagma) t_idem: "τ x ⊙ τ x = {τ x}"
  by simp

lemma (in st_multimagma)t_weak_twisted: "(⋃u ∈ y ⊙ x. x ⊙ τ u) ⊆ τ y ⊙ x"
  using local.stopp.s_weak_twisted by auto

lemma (in st_multimagma) t_comm: "τ x ⊙ τ y = τ y ⊙ τ x"
  by (simp add: stopp.s_comm)

lemma (in st_multimagma) t_export: "image τ (x ⊙ τ y) = τ x ⊙ τ y"
  by simp

lemma (in st_multimagma) tt_comp_prop: "Δ (τ x) (τ y) = (τ x = τ y)"
  using local.stopp.s_ortho_iff by force

text ‹The set of all sources (and targets) are units at powerset level.›

lemma (in st_multimagma) conv_uns [simp]: "sfix ⋆ X = X"
proof-
  {fix a
    have "(a ∈ sfix ⋆ X) = (∃b ∈ sfix. ∃c ∈ X. a ∈ b ⊙ c)"
      by (meson local.conv_exp2)
    also have "… = (∃b. ∃c ∈ X. σ b = b ∧ a ∈ b ⊙ c)"
      by blast
  also have "… = (∃b. ∃c ∈ X. a ∈ σ b ⊙ c)"
    by (metis local.ss_idem)
  also have "… = (∃c ∈ X. a ∈ σ c ⊙ c)"
    by (metis empty_iff local.s_absorb_var)
  also have "… = (a ∈ X)"
    by auto
  finally have "(a ∈ sfix ⋆ X) = (a ∈ X)".}
  thus ?thesis
    by blast
qed

lemma (in st_multimagma) conv_unt: "X ⋆ tfix = X"
  using stopp.conv_uns by blast

text ‹I prove laws of modal powerset quantales.›

lemma (in st_multimagma) Src_exp: "Src X = {σ x |x. x ∈ X}"
  by (simp add: Setcompr_eq_image)

lemma (in st_multimagma) ST_compat [simp]: "Src (Tgt X) = Tgt X"
  unfolding image_def by fastforce

lemma (in st_multimagma) TS_compat: "Tgt (Src X) = Src X"
  by (meson local.stopp.ST_compat)

lemma (in st_multimagma) Src_absorp [simp]: "Src X ⋆ X = X"
proof-
  {fix a
  have "(a ∈ Src X ⋆ X) = (∃b ∈ Src X. ∃c ∈ X. a ∈ b ⊙ c)"
    using local.conv_exp2 by auto
  also have "… = (∃b ∈ X. ∃c ∈ X. a ∈ σ b ⊙ c)"
    by blast
  also have "… = (∃c ∈ X. a ∈ σ c ⊙ c)"
    by (metis empty_iff local.s_absorb_var)
 also have "… = (a ∈ X)"
   by simp
  finally have "(a ∈ Src X ⋆ X) = (a ∈ X)".}
  thus ?thesis
    by force
qed

lemma (in st_multimagma) Tgt_absorp: "X ⋆ Tgt X = X"
  by simp

lemma (in st_multimagma) Src_Sup_pres: "Src (⋃𝒳) = (⋃X ∈ 𝒳. Src X)"
  unfolding Src_exp by auto

lemma (in st_multimagma) Tgt_Sup_pres: "Tgt (⋃𝒳) = (⋃ X ∈ 𝒳. Tgt X)"
  by blast

lemma (in st_multimagma) ST_comm: "Src X ⋆ Tgt Y = Tgt Y ⋆ Src X"
proof-
  {fix a
  have "(a ∈ Src X ⋆ Tgt Y) = (∃b ∈ Src X. ∃c ∈ Tgt Y. a ∈ b ⊙ c)"
    using local.conv_exp2 by auto
  also have "… = (∃b ∈ X. ∃c ∈ Y. a ∈ σ b ⊙ τ c)"
    by auto
  also have "… = (∃b ∈ X. ∃c ∈ Y. a ∈ τ c ⊙ σ b)"
    using local.st_comm by auto
  also have "… = (a ∈ Tgt Y ⋆ Src X)"
    using multimagma.conv_exp2 by fastforce
  finally have "(a ∈ Src X ⋆ Tgt Y) = (a ∈ Tgt Y ⋆ Src X)".}
  thus ?thesis
    by force
qed

lemma (in st_multimagma) Src_comm: "Src X ⋆ Src Y = Src Y ⋆ Src X"
  by (metis local.ST_comm local.TS_compat)

lemma (in st_multimagma) Tgt_comm: "Tgt X ⋆ Tgt Y = Tgt Y ⋆ Tgt X"
  using local.stopp.Src_comm by presburger

lemma (in st_multimagma) Src_subid: "Src X ⊆ sfix"
  by force

lemma (in st_multimagma) Tgt_subid: "Tgt X ⊆ tfix"
  using local.stopp.Src_subid by presburger

lemma (in st_multimagma) Src_export [simp]: "Src (Src X ⋆ Y) = Src X ⋆ Src Y"
proof-
  {fix a
  have "(a ∈ Src (Src X ⋆ Y)) = (∃b ∈ Src X ⋆ Y. a = σ b)"
    by (simp add: image_iff)
  also have "… = (∃b. ∃c ∈ Src X. ∃d ∈ Y. a = σ b ∧ b ∈ c ⊙ d)"
    by (meson local.conv_exp2)
  also have "… = (∃b. ∃c ∈ X. ∃d ∈ Y. a = σ b ∧ b ∈ σ c ⊙ d)"
    by simp
  also have "… = (∃c ∈ X. ∃d ∈ Y. a ∈ Src (σ c ⊙ d))"
    by (metis (mono_tags, lifting) image_iff)
  also have "… = (∃c ∈ X. ∃d ∈ Y. a ∈ σ c ⊙ σ d)"
    by auto
  also have "… = (∃c ∈ Src X. ∃d ∈ Src Y. a ∈ c ⊙ d)"
    by force
  also have "… = (a ∈ Src X ⋆ Src Y)"
    using local.conv_exp2 by auto
  finally have "(a ∈ Src (Src X ⋆ Y)) = (a ∈ Src X ⋆ Src Y)".}
  thus ?thesis
    by force
qed

lemma (in st_multimagma) Tgt_export [simp]: "Tgt (X ⋆ Tgt Y) = Tgt X ⋆ Tgt Y"
  by simp

text ‹Locality implies st-locality, which is the composition pattern of categories.›

lemma (in st_multimagma) locality:
  assumes src_local: "Src (x ⊙ σ y) ⊆ Src (x ⊙ y)"
  and tgt_local: "Tgt (τ x ⊙ y) ⊆ Tgt (x ⊙ y)"
  shows "Δ x y  = (τ x = σ y)"
  using local.Dst tgt_local by auto


subsection ‹Catoids›

class catoid = st_multimagma + multisemigroup

sublocale catoid ⊆ ts_msg: catoid "λx y. y ⊙ x"  tgt src
  by (unfold_locales, simp add: local.assoc)

lemma (in catoid) src_comp_aux: "v ∈ x ⊙ y ⟹ σ v = σ x"
  by (metis emptyE insert_iff local.assoc_exp local.s_absorb local.s_absorb_var3)

lemma (in catoid) src_comp: "Src (x ⊙ y) ⊆ {σ x}"
proof-
  {fix a
  assume "a ∈ Src (x ⊙ y)"
  hence "∃b ∈ x ⊙ y. a = σ b"
    by auto
  hence "∃b. σ b = σ x ∧ a = σ b"
    using local.src_comp_aux by blast
  hence "a = σ x"
    by blast}
  thus ?thesis
    by blast
qed

lemma (in catoid) src_comp_cond: "(Δ x y) ⟹ Src (x ⊙ y) = {σ x}"
  by (meson image_is_empty local.src_comp subset_singletonD)

lemma (in catoid) tgt_comp_aux: "v ∈ x ⊙ y ⟹ τ v = τ y"
  using local.ts_msg.src_comp_aux by fastforce

lemma (in catoid) tgt_comp: "Tgt (x ⊙ y) ⊆ {τ y}"
  by (simp add: local.ts_msg.src_comp)

lemma (in catoid) tgt_comp_cond: "Δ x y ⟹ Tgt (x ⊙ y) = {τ y}"
  by (simp add: local.ts_msg.src_comp_cond)

lemma (in catoid) src_weak_local: "Src (x ⊙ y) ⊆ Src (x ⊙ σ y)"
proof-
  {fix a
  assume "a ∈ Src (x ⊙ y)"
  hence "∃b ∈ x ⊙ y. a = σ b"
    by auto
  hence "∃b ∈ x ⊙ y. a = σ b"
    by blast
  hence "∃b ∈ x ⊙ y. a = σ b ∧ τ x = σ y"
    using local.Dst by auto
  hence "∃b ∈ x ⊙ σ y. a = σ b"
    by (metis insertI1 local.t_absorb local.ts_msg.tgt_comp_aux)
  hence "a ∈ Src (x ⊙ σ y)"
    by force}
  thus ?thesis
    by force
qed

lemma (in catoid) src_local_cond:
  "Δ x y ⟹ Src (x ⊙ y) = Src (x ⊙ σ y)"
  by (simp add: local.stopp.Dst local.ts_msg.tgt_comp_cond)

lemma (in catoid) tgt_weak_local: "Tgt (x ⊙ y) ⊆ Tgt (τ x ⊙ y)"
  by (simp add: local.ts_msg.src_weak_local)

lemma (in catoid) tgt_local_cond:
  "Δ x y ⟹ Tgt (x ⊙ y) = Tgt (τ x ⊙ y)"
  using local.ts_msg.src_local_cond by presburger

lemma (in catoid) src_twisted_aux:
  "u ∈ x ⊙ y ⟹ (x ⊙ σ y = σ u ⊙ x)"
  by (metis local.Dst local.s_absorb local.src_comp_aux local.t_absorb)

lemma (in catoid) src_twisted_cond:
  "Δ x y ⟹ x ⊙ σ y = ⋃{σ u ⊙ x |u. u ∈ x ⊙ y}"
   using local.stopp.Dst local.ts_msg.tgt_comp_aux by auto

lemma (in catoid) tgt_twisted_aux:
  "u ∈ x ⊙ y ⟹ (τ x ⊙ y = y ⊙ τ u)"
  by (simp add: local.ts_msg.src_twisted_aux)

lemma (in catoid) tgt_twisted_cond:
  "Δ x y  ⟹ τ x ⊙ y = ⋃{y ⊙ τ u |u. u ∈ x ⊙ y}"
  by (simp add: local.ts_msg.src_twisted_cond)

lemma (in catoid) src_funct:
  "x ∈ y ⊙ z ⟹ x' ∈ y ⊙ z ⟹ σ x = σ x'"
  using local.src_comp_aux by force

lemma (in catoid) st_local_iff:
  "(∀x y. Δ x y = (τ x = σ y)) = (∀v x y z. v ∈ x ⊙ y ⟶ Δ y z ⟶ Δ v z)"
  apply safe
    apply (metis local.ts_msg.src_comp_aux)
  using local.Dst apply blast
  by (metis local.s_absorb_var2 local.t_absorb singleton_iff)

text ‹Again one can lift to properties of modal semirings and quantales.›

lemma (in catoid) Src_weak_local: "Src (X ⋆ Y) ⊆ Src (X ⋆ Src Y)"
proof-
  {fix a
  assume "a ∈ Src (X ⋆ Y)"
  hence "∃b. ∃c ∈ X. ∃d ∈ Y. a = σ b ∧ b ∈ c ⊙ d"
    by (smt (verit) image_iff local.conv_exp2)
  hence "∃c ∈ X. ∃d ∈ Y. a ∈ Src (c ⊙ d)"
    by auto
  hence "∃c ∈ X. ∃d ∈ Y. a ∈ Src (c ⊙ σ d)"
    by (metis empty_iff image_empty local.src_local_cond)
  hence "∃b. ∃c ∈ X. ∃d ∈ Src Y. a = σ b ∧ b ∈ c ⊙ d"
    by auto
  hence "a ∈ Src (X ⋆ Src Y)"
    by (metis image_iff local.conv_exp2)}
  thus ?thesis
    by blast
qed

lemma (in catoid) Tgt_weak_local: "Tgt (X ⋆ Y) ⊆ Tgt (Tgt X ⋆ Y)"
  by (metis local.stopp.conv_exp local.ts_msg.Src_weak_local multimagma.conv_exp)

text ‹st-Locality implies locality.›

lemma (in catoid) st_locality_l_locality:
  assumes "Δ x y = (τ x = σ y)"
  shows "Src (x ⊙ y) = Src (x ⊙ σ y)"
proof-
  {fix a
  have "(a ∈ Src (x ⊙ σ y)) = (∃b ∈ x ⊙ σ y. a = σ b)"
    by auto
  also have "… = (∃b ∈ x ⊙ σ y. a = σ b ∧ τ x = σ y)"
    by (simp add: local.st_prop local.tgt_comp_aux local.tgt_twisted_aux)
  also have "… = (∃b ∈ x ⊙ y. a = σ b)"
    by (metis assms ex_in_conv local.t_absorb local.ts_msg.tgt_comp_aux singletonI)
  also have "… = (a ∈ Src (x ⊙ y))"
    by auto
  finally have "(a ∈ Src (x ⊙ σ y)) = (a ∈ Src (x ⊙ y))".}
  thus ?thesis
    by force
qed

lemma (in catoid) st_locality_r_locality:
  assumes lr_locality: "Δ x y = (τ x = σ y)"
  shows  "Tgt (x ⊙ y) = Tgt (τ x ⊙ y)"
  by (metis local.ts_msg.st_locality_l_locality lr_locality)

lemma (in catoid) st_locality_locality:
  "(Src (x ⊙ y) = Src (x ⊙ σ y) ∧ Tgt (x ⊙ y) = Tgt (τ x ⊙ y)) = (Δ x y = (τ x = σ y))"
  apply standard
   apply (simp add: local.locality)
  by (metis local.st_locality_l_locality local.ts_msg.st_locality_l_locality)


subsection ‹Locality›

text ‹For st-multimagmas there are different notions of locality. I do not develop this in detail.›

class local_catoid = catoid +
  assumes src_local: "Src (x ⊙ σ y) ⊆ Src (x ⊙ y)"
  and tgt_local: "Tgt (τ x ⊙ y) ⊆ Tgt (x ⊙ y)"

sublocale local_catoid ⊆ sts_msg: local_catoid "λx y. y ⊙ x" tgt src
  apply unfold_locales using local.tgt_local local.src_local by auto

lemma (in local_catoid) src_local_eq [simp]: "Src (x ⊙ σ y) = Src (x ⊙ y)"
  by (simp add: local.src_local local.src_weak_local order_class.order_eq_iff)

lemma (in local_catoid) tgt_local_eq: "Tgt (τ x ⊙ y) = Tgt (x ⊙ y)"
  by simp

lemma (in local_catoid) src_twisted: "x ⊙ σ y = (⋃u ∈ x ⊙ y. σ u ⊙ x)"
  by (metis Setcompr_eq_image Sup_empty empty_is_image local.src_twisted_cond local.sts_msg.tgt_local_eq)

lemma (in local_catoid) tgt_twisted: "τ x ⊙ y = (⋃u ∈ x ⊙ y. y ⊙ τ u)"
  using local.sts_msg.src_twisted by auto

lemma (in local_catoid) local_var: "Δ x y ⟹ Δ (τ x) (σ y)"
  by (simp add: local.stopp.Dst)

lemma (in local_catoid) local_var_eq [simp]: "Δ (τ x) (σ y) = Δ x y"
  by (simp add: local.locality)

text ‹I lift locality to powersets.›

lemma (in local_catoid) Src_local [simp]: "Src (X ⋆ Src Y) = Src (X ⋆ Y)"
proof-
  {fix a
  have "(a ∈ Src (X ⋆ Src Y)) = (∃b ∈ X ⋆ Src Y. a = σ b)"
    by (simp add: image_iff)
  also have "… = (∃b. ∃c ∈ X. ∃d ∈ Src Y. b ∈ c ⊙ d ∧ a = σ b)"
    by (meson local.conv_exp2)
  also have "… = (∃b. ∃c ∈ X. ∃d ∈ Y. b ∈ c ⊙ σ d ∧ a = σ b)"
    by simp
  also have "… = (∃c ∈ X. ∃d ∈ Y. a ∈ Src (c ⊙ σ d))"
    by blast
  also have "… = (∃c ∈ X. ∃d ∈ Y. a ∈ Src (c ⊙ d))"
    by auto
  also have "… = (∃b. ∃c ∈ X. ∃d ∈ Y. b ∈ c ⊙ d ∧ a = σ b)"
    by auto
  also have "… = (∃b ∈ X ⋆ Y. a = σ b)"
    by (meson local.conv_exp2)
  also have "… = (a ∈ Src (X ⋆ Y))"
    by (simp add: image_iff)
  finally have "(a ∈ Src (X ⋆ Src Y)) = (a ∈ Src (X ⋆ Y))".}
  thus ?thesis
    by force
qed

lemma (in local_catoid) Tgt_local [simp]: "Tgt (Tgt X ⋆ Y) = Tgt (X ⋆ Y)"
  by (metis local.stopp.conv_def local.sts_msg.Src_local multimagma.conv_def)

lemma (in local_catoid) st_local: "Δ x y = (τ x = σ y)"
  using local.stopp.locality by force


subsection ‹From partial magmas to single-set categories.›

class functional_magma = multimagma +
  assumes functionality: "x ∈ y ⊙ z ⟹ x' ∈ y ⊙ z ⟹ x = x'"

begin

text ‹Functional magmas could also be called partial magmas. The multioperation corresponds to a partial operation.›

lemma partial_card: "card (x ⊙ y) ≤ 1"
  by (metis One_nat_def card.infinite card_le_Suc0_iff_eq local.functionality zero_less_one_class.zero_le_one)

lemma fun_in_sgl: "(x ∈ y ⊙ z) = ({x} = y ⊙ z)"
  using local.functionality by fastforce

text ‹I introduce a partial operation.›

definition pcomp :: "'a ⇒ 'a ⇒ 'a" (infixl "⊗" 70) where
  "x ⊗ y = (THE z. z ∈ x ⊙ y)"

lemma functionality_var: "Δ x y ⟹ (∃!z. z ∈ x ⊙ y)"
  using local.functionality by auto

lemma functionality_lem: "(∃!z. z ∈ x ⊙ y) ∨ (x ⊙ y = {})"
  using functionality_var by blast

lemma functionality_lem_var: "Δ x y = (∃z. {z} = x ⊙ y)"
  using functionality_lem by blast

lemma pcomp_def_var: "(Δ x y ∧ x ⊗ y = z) = (z ∈ x ⊙ y)"
  unfolding pcomp_def by (smt (verit, del_insts) all_not_in_conv functionality_lem theI_unique)

lemma pcomp_def_var2: "Δ x y ⟹ ((x ⊗ y = z) = (z ∈ x ⊙ y))"
  using pcomp_def_var by blast

lemma pcomp_def_var3: "Δ x y ⟹ ((x ⊗ y = z) = ({z} = x ⊙ y))"
  by (simp add: fun_in_sgl pcomp_def_var2)

end

class functional_st_magma = functional_magma + st_multimagma

class functional_semigroup = functional_magma + multisemigroup

begin

lemma pcomp_assoc_defined: "(Δ u v ∧ Δ (u ⊗ v) w) = (Δ u (v ⊗ w) ∧ Δ v w)"
proof-
  have "(Δ u v ∧ Δ (u ⊗ v) w) = (∃x. Δ u v ∧ Δ x w  ∧ x = u ⊗ v)"
    by simp
  also have "... = (∃x. x ∈ u ⊙ v ∧ Δ x w)"
    by (metis local.pcomp_def_var)
  also have "... = (∃x. x ∈ v ⊙ w ∧ Δ u x)"
    using local.assoc_exp by blast
  also have "... = (∃x. Δ v w ∧ x = v ⊗ w ∧ Δ u x)"
    by (metis local.pcomp_def_var)
  also have "... = (Δ u (v ⊗ w) ∧ Δ v w)"
    by auto
  finally show ?thesis.
qed

lemma pcomp_assoc: "Δ x y ∧ Δ (x ⊗ y) z ⟹ (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)"
  by (metis (full_types) local.assoc_var local.conv_atom local.fun_in_sgl local.pcomp_def_var2 pcomp_assoc_defined)

end

class functional_catoid = functional_semigroup + catoid

text ‹Finally, here comes the definition of single-set categories as in Chapter 12 of Mac Lane's book,
but with partiality of arrow composition modelled using a multioperation, or a partial operation
based on it.›

class single_set_category = functional_catoid + local_catoid

begin

lemma st_assoc: "τ x = σ y ⟹ τ y = σ z ⟹ (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)"
  by (metis local.st_local local.pcomp_assoc local.pcomp_def_var2 local.tgt_comp_aux)

end


subsection  ‹Morphisms of multimagmas and lr-multimagmas›

text ‹In the context of single-set categories, these morphisms are functors. Bounded morphisms
are functional bisimulations. They are known as zig-zag morphisms or p-morphism in modal and
substructural logics.›

definition mm_morphism :: "('a::multimagma ⇒ 'b::multimagma) ⇒ bool" where
  "mm_morphism f = (∀x y. image f (x ⊙ y) ⊆ f x ⊙ f y)"

definition bounded_mm_morphism :: "('a::multimagma ⇒ 'b::multimagma) ⇒ bool" where
  "bounded_mm_morphism f = (mm_morphism f ∧ (∀x u v. f x ∈ u ⊙ v ⟶ (∃y z. u = f y ∧ v = f z ∧ x ∈ y ⊙ z)))"

definition st_mm_morphism :: "('a::st_multimagma ⇒ 'b::st_multimagma) ⇒ bool" where
  "st_mm_morphism f = (mm_morphism f ∧ f ∘ σ = σ ∘ f ∧ f ∘ τ = τ ∘ f)"

definition bounded_st_mm_morphism :: "('a::st_multimagma ⇒ 'b::st_multimagma) ⇒ bool" where
  "bounded_st_mm_morphism f = (bounded_mm_morphism f ∧ st_mm_morphism f)"


subsection ‹Relationship with categories›

text ‹Next I add a standard definition of a category following Moerdijk and Mac Lane's book and,
for good measure, show that categories form single set categories and vice versa.›

locale category =
  fixes id :: "'objects ⇒ 'arrows"
  and dom :: "'arrows ⇒ 'objects"
  and cod :: "'arrows ⇒ 'objects"
  and comp :: "'arrows ⇒ 'arrows ⇒ 'arrows" (infixl "∙" 70)
  assumes dom_id [simp]: "dom (id X) = X"
  and cod_id [simp]: "cod (id X) = X"
  and id_dom [simp]: "id (dom f) ∙ f = f"
  and id_cod [simp]: "f ∙ id (cod f) = f"
  and dom_loc [simp]: "cod f = dom g ⟹ dom (f ∙ g) = dom f"
  and cod_loc [simp]: "cod f = dom g ⟹ cod (f ∙ g) = cod g"
  and assoc: "cod f = dom g ⟹ cod g = dom h ⟹ (f ∙ g) ∙ h = f ∙ (g ∙ h)"

begin

lemma "cod f = dom g ⟹ dom (f ∙ g) = dom (f ∙ id (dom g))"
  by simp

abbreviation "LL f ≡ id (dom f)"

abbreviation "RR f ≡ id (cod f)"

abbreviation "Comp ≡ λf g. (if RR f = LL g then {f ∙ g} else {})"

end

typedef (overloaded) 'a::single_set_category st_objects = "{x::'a::single_set_category. σ x = x}"
  using stopp.tt_idem by blast

setup_lifting type_definition_st_objects

lemma Sfix_coerce [simp]: "Abs_st_objects (σ (Rep_st_objects X)) = X"
  by (smt (verit, best) Rep_st_objects Rep_st_objects_inverse mem_Collect_eq)

lemma Rfix_coerce [simp]: "Abs_st_objects (τ (Rep_st_objects X)) = X"
  by (smt (verit, best) Rep_st_objects Rep_st_objects_inverse mem_Collect_eq stopp.st_fix)

sublocale single_set_category ⊆ sscatcat: category Rep_st_objects "Abs_st_objects ∘ σ" "Abs_st_objects ∘ τ" "(⊗)"
  apply unfold_locales
        apply simp_all
      apply (metis (mono_tags, lifting) Abs_st_objects_inverse empty_not_insert functional_magma_class.pcomp_def_var2 insertI1 mem_Collect_eq st_multimagma_class.s_absorb st_multimagma_class.ss_idem)
     apply (metis (mono_tags, lifting) Abs_st_objects_inverse functional_magma_class.pcomp_def_var insert_iff mem_Collect_eq st_multimagma_class.stopp.s_absorb st_multimagma_class.stopp.ts_compat)
    apply (metis (mono_tags, lifting) Abs_st_objects_inject catoid_class.ts_msg.tgt_comp_aux functional_magma_class.pcomp_def_var2 local_catoid_class.sts_msg.st_local mem_Collect_eq st_multimagma_class.stopp.ts_compat st_multimagma_class.stopp.tt_idem)
   apply (metis (mono_tags, lifting) Abs_st_objects_inject functional_semigroup_class.pcomp_assoc_defined local_catoid_class.sts_msg.st_local mem_Collect_eq st_multimagma_class.stopp.s_absorb_var st_multimagma_class.stopp.st_compat)
  by (metis (mono_tags, lifting) Abs_st_objects_inverse mem_Collect_eq single_set_category_class.st_assoc st_multimagma_class.stopp.st_compat st_multimagma_class.stopp.ts_compat)

sublocale category ⊆ catlrm: st_multimagma Comp  LL RR
  by unfold_locales auto

sublocale category ⊆ catsscat: single_set_category Comp LL RR
  apply unfold_locales
     apply (smt (verit, ccfv_threshold) Sup_empty category.assoc category_axioms ccpo_Sup_singleton cod_id cod_loc dom_loc image_empty image_insert)
    apply (metis empty_iff singletonD)
   apply (smt (verit, best) category.dom_id category_axioms dom_loc image_insert set_eq_subset)
  by (smt (z3) category.cod_id category_axioms cod_loc image_insert subsetI)

subsection ‹A Mac Lane style variant›

text ‹Next I present an axiomatisation of single-set categories that follows Mac Lane's axioms
in Chapter I of his textbook more closely, but still uses a multioperation for arrow composition.›

class mlss_cat = functional_magma +
  fixes l0 :: "'a ⇒'a"
  fixes r0 :: "'a ⇒'a"
  assumes comp0_def: "(x ⊙ y ≠ {}) = (r0 x = l0 y)"
  assumes r0l0 [simp]: "r0 (l0 x) = l0 x"
  assumes l0r0 [simp]: "l0 (r0 x) = r0 x"
  assumes l0_absorb [simp]: "l0 x ⊗ x = x"
  assumes r0_absorb [simp] : "x ⊗ r0 x = x"
  assumes assoc_defined: "(u ⊙ v ≠ {} ∧ (u ⊗ v) ⊙ w ≠ {}) = (u ⊙ (v ⊗ w) ≠ {} ∧ v ⊙ w ≠ {})"
  assumes comp0_assoc: "r0 x = l0 y ⟹ r0 y = l0 z ⟹ x ⊗ (y ⊗ z) = (x ⊗ y) ⊗ z"
  assumes locall_var: "r0 x = l0 y ⟹ l0 (x ⊗ y) = l0 x"
  assumes localr_var: "r0 x = l0 y ⟹ r0 (x ⊗ y) = r0 y"

begin

lemma ml_locall [simp]: "l0 (x ⊗ l0 y) = l0 (x ⊗ y)"
  by (metis local.comp0_def local.l0_absorb local.locall_var local.pcomp_def local.r0l0)

lemma ml_localr [simp]: "r0 (r0 x ⊗ y) = r0 (x ⊗ y)"
  by (metis local.comp0_def local.l0r0 local.localr_var local.pcomp_def local.r0l0)

lemma ml_locall_im [simp]: "image l0 (x ⊙ l0 y) = image l0 (x ⊙ y)"
  by (metis (no_types, lifting) image_insert image_is_empty local.comp0_def local.fun_in_sgl local.l0r0 local.pcomp_def_var local.r0_absorb local.r0l0 ml_locall)

lemma ml_localr_im [simp]: "image r0 (r0 x ⊙ y) = image r0 (x ⊙ y)"
  by (smt (verit, best) image_insert local.comp0_def local.fun_in_sgl local.functionality_lem local.l0_absorb local.l0r0 local.pcomp_def_var local.r0_absorb ml_localr)

end

sublocale single_set_category ⊆ sscatml: mlss_cat "(⊙)" "σ" "τ"
  apply unfold_locales
          apply (simp_all add: st_local pcomp_def_var2)
  using local.pcomp_assoc_defined local.st_local apply force
  using pcomp_assoc_defined st_assoc local.pcomp_def_var2 local.st_local local.src_comp_aux tgt_comp_aux by fastforce+

sublocale mlss_cat ⊆ mlsscat: single_set_category "(⊙)" "l0" "r0"
  apply unfold_locales
       apply (simp_all add: comp0_def)
    apply standard
     apply (clarsimp, smt (verit, ccfv_SIG) local.assoc_defined local.comp0_assoc local.comp0_def local.fun_in_sgl local.pcomp_def_var)
    apply (clarsimp, metis local.assoc_defined local.comp0_assoc local.comp0_def local.pcomp_def_var)
   apply (metis local.comp0_def local.fun_in_sgl local.l0_absorb local.pcomp_def_var2 local.r0l0)
  using local.comp0_def local.fun_in_sgl local.l0r0 local.pcomp_def_var2 local.r0_absorb by presburger


subsection ‹Product of catoids›

text ‹Finally I formalise products of categories as an exercise.›

instantiation prod :: (catoid, catoid) catoid
begin

definition "src_prod x = (σ (fst x), σ (snd x))"
  for x :: "'a × 'b"


definition "tgt_prod x = (τ (fst x), τ (snd x))"
  for x :: "'a × 'b"

definition "mcomp_prod x y = {(u,v) |u v. u ∈ fst x ⊙ fst y ∧ v ∈ snd x ⊙ snd y}"
  for x y :: "'a × 'b"

instance
proof
  fix x y z :: "'a × 'b"
  show "(⋃v ∈ y ⊙ z. x ⊙ v) = (⋃v ∈ x ⊙ y. v ⊙ z)"
  proof-
    {fix a b
      have "((a,b) ∈ (⋃ v ∈ y ⊙ z. x ⊙ v)) = (∃v. (a,b) ∈ x ⊙ v ∧ v ∈ y ⊙ z)"
        by blast
      also have "… = (∃v w. a ∈ fst x ⊙ v ∧ v ∈ fst y ⊙ fst z ∧ b ∈ snd x ⊙ w ∧ w ∈ snd y ⊙ snd z)"
        using mcomp_prod_def by auto
      also have "… = (∃v w. a ∈ v ⊙ fst z ∧ v ∈ fst x ⊙ fst y ∧ b ∈ w ⊙ snd z ∧ w ∈ snd x ⊙ snd y)"
        by (meson ts_msg.assoc_exp)
      also have "… = (∃v. (a,b) ∈ v ⊙ z ∧ v ∈ x ⊙ y)"
        using mcomp_prod_def by auto
      also have "… = ((a,b) ∈ (⋃v ∈ x ⊙ y. v ⊙ z))"
        by blast
      finally have "((a,b) ∈ (⋃v ∈ y ⊙ z. x ⊙ v)) = ((a,b) ∈ (⋃v ∈ x ⊙ y. v ⊙ z))".}
    thus ?thesis
      by (meson pred_equals_eq2)
  qed
  show "x ⊙ y ≠ {} ⟹ τ x = σ y"
    by (simp add: Catoid.mcomp_prod_def Dst src_prod_def tgt_prod_def)
  show "σ x ⊙ x = {x}"
    unfolding src_prod_def mcomp_prod_def by simp
  show "x ⊙ τ x = {x}"
    unfolding tgt_prod_def mcomp_prod_def by simp
qed

end

instantiation prod :: (single_set_category, single_set_category) single_set_category
begin

instance
proof
  fix x y z x' :: "'a × 'b"
  show "x ∈ y ⊙ z ⟹ x' ∈ y ⊙ z ⟹ x = x'"
    unfolding mcomp_prod_def by (smt (verit, best) functionality mem_Collect_eq)
  show a: "stopp.Tgt (x ⊙ σ y) ⊆ stopp.Tgt (x ⊙ y)"
  proof-
    {fix a b
      have "((a,b) ∈ stopp.Tgt (x ⊙ σ y)) = ((a,b) ∈ Src {(c,d) |c d. c ∈ fst x ⊙ σ (fst y) ∧ d ∈ snd x ⊙ σ (snd y)})"
        by (simp add: mcomp_prod_def src_prod_def)
      also have "… = (a ∈ Src (fst x ⊙ σ (fst y)) ∧ b ∈ Src (snd x ⊙ σ (snd y)))"
        by (smt (z3) Setcompr_eq_image fst_conv mem_Collect_eq snd_conv src_prod_def stopp.tt_idem)
      also have "… = (a ∈ Src (fst x ⊙ fst y) ∧ b ∈ Src (snd x ⊙ snd y))"
        by simp
      also have "… = ((a,b) ∈ Src {(c,d) |c d. c ∈ (fst x ⊙ fst y) ∧ d ∈ (snd x ⊙ snd y)})"
        by (smt (z3) Setcompr_eq_image fst_conv mem_Collect_eq snd_conv src_prod_def stopp.tt_idem)
      also have "… = ((a,b) ∈ stopp.Tgt (x ⊙ y))"
        by (simp add: mcomp_prod_def src_prod_def)
      finally have "((a,b) ∈ stopp.Tgt (x ⊙ σ y)) = ((a,b) ∈ stopp.Tgt (x ⊙ y))".}
    thus ?thesis
      by auto
  qed
  show "Tgt (τ x ⊙ y) ⊆ Tgt (x ⊙ y)"
    by (metis (no_types, lifting) a bot.extremum_uniqueI empty_is_image stopp.s_absorb_var3 tgt_local_cond tgt_weak_local ts_msg.st_locality_l_locality)
qed

end

end