Theory CZH_DG_Par

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹Par› as a digraph›
theory CZH_DG_Par
  imports
    CZH_DG_Rel
    CZH_DG_Subdigraph
begin



subsection‹Background›


text‹
‹Par› is usually defined as a category of sets and partial functions
(see nLab cite‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/partial+function}
}).
However, there is little that can prevent one from exposing ‹Par› 
as a digraph and provide additional structure gradually in subsequent
installments of this work. Thus, in this section, ‹α›-‹Par› is defined as a
digraph of sets and partial functions in ‹Vα› 
›

named_theorems dg_Par_cs_simps
named_theorems dg_Par_cs_intros

lemmas [dg_Par_cs_simps] = dg_Rel_shared_cs_simps
lemmas [dg_Par_cs_intros] = dg_Rel_shared_cs_intros



subsection‹Arrow for ‹Par››


subsubsection‹Definition and elementary properties›

locale arr_Par = 𝒵 α + vfsequence T + ArrVal: vsv ‹T⦇ArrVal⦈› for α T +
  assumes arr_Par_length[dg_Rel_shared_cs_simps, dg_Par_cs_simps]: 
    "vcard T = 3ℕ" 
    and arr_Par_ArrVal_vdomain: "𝒟∘ (T⦇ArrVal⦈) ⊆∘ T⦇ArrDom⦈"
    and arr_Par_ArrVal_vrange: "ℛ∘ (T⦇ArrVal⦈) ⊆∘ T⦇ArrCod⦈"
    and arr_Par_ArrDom_in_Vset: "T⦇ArrDom⦈ ∈∘ Vset α"
    and arr_Par_ArrCod_in_Vset: "T⦇ArrCod⦈ ∈∘ Vset α"


text‹Elementary properties.›

sublocale arr_Par ⊆ arr_Rel
  by unfold_locales 
    (
      simp_all add: 
        dg_Par_cs_simps
        arr_Par_ArrVal_vdomain 
        arr_Par_ArrVal_vrange
        arr_Par_ArrDom_in_Vset 
        arr_Par_ArrCod_in_Vset
    )

lemmas (in arr_Par) [dg_Par_cs_simps] = dg_Rel_shared_cs_simps


text‹Rules.›

lemma (in arr_Par) arr_Par_axioms'[dg_cs_intros, dg_Par_cs_intros]:
  assumes "α' = α"
  shows "arr_Par α' T"
  unfolding assms by (rule arr_Par_axioms)

mk_ide rf arr_Par_def[unfolded arr_Par_axioms_def]
  |intro arr_ParI|
  |dest arr_ParD[dest]|
  |elim arr_ParE[elim!]|

lemma (in 𝒵) arr_Par_vfsequenceI: 
  assumes "vsv r" 
    and "𝒟∘ r ⊆∘ a"
    and "ℛ∘ r ⊆∘ b"
    and "a ∈∘ Vset α"
    and "b ∈∘ Vset α"
  shows "arr_Par α [r, a, b]∘"
  by (intro arr_ParI) 
    (insert assms, auto simp: arr_Rel_components nat_omega_simps)

lemma arr_Par_arr_RelI:
  assumes "arr_Rel α T" and "vsv (T⦇ArrVal⦈)"
  shows "arr_Par α T"
proof-
  interpret arr_Rel α T by (rule assms(1))
  show ?thesis
    by (intro arr_ParI)
      (
        auto simp: 
          dg_Rel_cs_simps
          assms(2)
          vfsequence_axioms 
          arr_Rel_ArrVal_vdomain 
          arr_Rel_ArrVal_vrange 
          arr_Rel_ArrDom_in_Vset 
          arr_Rel_ArrCod_in_Vset
      )
qed 

lemma arr_Par_arr_RelD:
  assumes "arr_Par α T"
  shows "arr_Rel α T" and "vsv (T⦇ArrVal⦈)"
proof-
  interpret arr_Par α T by (rule assms)
  show "arr_Rel α T" and "vsv (T⦇ArrVal⦈)"
    by (rule arr_Rel_axioms) auto
qed

lemma arr_Par_arr_RelE:
  assumes "arr_Par α T"
  obtains "arr_Rel α T" and "vsv (T⦇ArrVal⦈)"
  using assms by (auto simp: arr_Par_arr_RelD)


text‹Further properties.›

lemma arr_Par_eqI:
  assumes "arr_Par α S" 
    and "arr_Par α T"
    and "S⦇ArrVal⦈ = T⦇ArrVal⦈"
    and "S⦇ArrDom⦈ = T⦇ArrDom⦈"
    and "S⦇ArrCod⦈ = T⦇ArrCod⦈"
  shows "S = T"
proof(rule vsv_eqI)
  interpret S: arr_Par α S by (rule assms(1))
  interpret T: arr_Par α T by (rule assms(2))
  show "vsv S" by (rule S.vsv_axioms)
  show "vsv T" by (rule T.vsv_axioms)
  show "𝒟∘ S = 𝒟∘ T" 
    by (simp add: S.vfsequence_vdomain T.vfsequence_vdomain dg_Par_cs_simps) 
  have dom: "𝒟∘ S = 3ℕ" by (simp add: S.vfsequence_vdomain dg_Par_cs_simps)
  show "a ∈∘ 𝒟∘ S ⟹ S⦇a⦈ = T⦇a⦈" for a 
    by (unfold dom, elim_in_numeral, insert assms) 
      (auto simp: arr_field_simps)
qed

lemma small_arr_Par[simp]: "small {T. arr_Par α T}"
proof(rule smaller_than_small)
  show "{T. arr_Par α T} ⊆ {T. arr_Rel α T}" 
    by (simp add: Collect_mono arr_Par_arr_RelD(1))
qed simp

lemma set_Collect_arr_Par[simp]: 
  "T ∈∘ set (Collect (arr_Par α)) ⟷ arr_Par α T" 
  by auto


subsubsection‹Composition›

abbreviation (input) comp_Par :: "V ⇒ V ⇒ V" (infixl ‹∘Par› 55)
  where "comp_Par ≡ comp_Rel"

lemma arr_Par_comp_Par[dg_Par_cs_intros]:
  assumes "arr_Par α S" and "arr_Par α T"
  shows "arr_Par α (S ∘Par T)"
proof(intro arr_Par_arr_RelI)
  interpret S: arr_Par α S by (rule assms(1))
  interpret T: arr_Par α T by (rule assms(2))
  show "arr_Rel α (S ∘Par T)"
    by (auto simp: S.arr_Rel_axioms T.arr_Rel_axioms arr_Rel_comp_Rel)
  show "vsv ((S ∘Par T)⦇ArrVal⦈)"
    unfolding comp_Rel_components
    by (simp add: S.ArrVal.vsv_axioms T.ArrVal.vsv_axioms vsv_vcomp)
qed

lemma arr_Par_comp_Par_ArrVal_app:
  assumes "arr_Par α S" 
    and "arr_Par α T"
    and "x ∈∘ 𝒟∘ (T⦇ArrVal⦈)"
    and "T⦇ArrVal⦈⦇x⦈ ∈∘ 𝒟∘ (S⦇ArrVal⦈)"
  shows "(S ∘Par T)⦇ArrVal⦈⦇x⦈ = S⦇ArrVal⦈⦇T⦇ArrVal⦈⦇x⦈⦈"
  using assms unfolding comp_Rel_components by (intro vcomp_atI) auto


subsubsection‹Inclusion›

abbreviation (input) incl_Par :: "V ⇒ V ⇒ V"
  where "incl_Par ≡ incl_Rel"

lemma (in 𝒵) arr_Par_incl_ParI:
  assumes "A ∈∘ Vset α" and "B ∈∘ Vset α" and "A ⊆∘ B"
  shows "arr_Par α (incl_Par A B)"
proof(intro arr_Par_arr_RelI)
  from assms show "arr_Rel α (incl_Par A B)" 
    by (force intro: arr_Rel_incl_RelI)
qed (simp add: incl_Rel_components)


subsubsection‹Identity›

abbreviation (input) id_Par :: "V ⇒ V"
  where "id_Par ≡ id_Rel"

lemma (in 𝒵) arr_Par_id_ParI:
  assumes "A ∈∘ Vset α"
  shows "arr_Par α (id_Par A)"
  using assms
  by (intro arr_Par_arr_RelI) 
    (auto intro: arr_Rel_id_RelI simp: id_Rel_components)

lemma arr_Par_comp_Par_id_Par_left[dg_Par_cs_simps]:
  assumes "arr_Par α f" and "f⦇ArrCod⦈ = A"
  shows "id_Par A ∘Par f = f"
proof-
  interpret f: arr_Par α f by (rule assms(1))
  have "arr_Rel α f" by (simp add: f.arr_Rel_axioms)
  from arr_Rel_comp_Rel_id_Rel_left[OF this assms(2)] show ?thesis .
qed

lemma arr_Par_comp_Par_id_Par_right[dg_Par_cs_simps]:
  assumes "arr_Par α f" and "f⦇ArrDom⦈ = A"
  shows "f ∘Par id_Par A = f"
proof-
  interpret f: arr_Par α f by (rule assms(1))
  have "arr_Rel α f" by (simp add: f.arr_Rel_axioms)
  from arr_Rel_comp_Rel_id_Rel_right[OF this assms(2)] show ?thesis.
qed



subsection‹‹Par› as a digraph›


subsubsection‹Definition and elementary properties›

definition dg_Par :: "V ⇒ V"
  where "dg_Par α =
    [
      Vset α,
      set {T. arr_Par α T},
      (λT∈∘set {T. arr_Par α T}. T⦇ArrDom⦈),
      (λT∈∘set {T. arr_Par α T}. T⦇ArrCod⦈)
    ]∘"


text‹Components.›

lemma dg_Par_components:
  shows "dg_Par α⦇Obj⦈ = Vset α"
    and "dg_Par α⦇Arr⦈ = set {T. arr_Par α T}"
    and "dg_Par α⦇Dom⦈ = (λT∈∘set {T. arr_Par α T}. T⦇ArrDom⦈)"
    and "dg_Par α⦇Cod⦈ = (λT∈∘set {T. arr_Par α T}. T⦇ArrCod⦈)"
  unfolding dg_Par_def dg_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object›

lemma dg_Par_Obj_iff: "x ∈∘ dg_Par α⦇Obj⦈ ⟷ x ∈∘ Vset α" 
  unfolding dg_Par_components by auto


subsubsection‹Arrow›

lemma dg_Par_Arr_iff[dg_Par_cs_simps]: "x ∈∘ dg_Par α⦇Arr⦈ ⟷ arr_Par α x" 
  unfolding dg_Par_components by auto


subsubsection‹Domain›

mk_VLambda dg_Par_components(3)
  |vsv dg_Par_Dom_vsv[dg_Par_cs_intros]|
  |vdomain dg_Par_Dom_vdomain[dg_Par_cs_simps]|
  |app dg_Par_Dom_app[unfolded set_Collect_arr_Par, dg_Par_cs_simps]|

lemma dg_Par_Dom_vrange: "ℛ∘ (dg_Par α⦇Dom⦈) ⊆∘ dg_Par α⦇Obj⦈"
  unfolding dg_Par_components
  by (rule vrange_VLambda_vsubset, unfold set_Collect_arr_Par) auto


subsubsection‹Codomain›

mk_VLambda dg_Par_components(4)
  |vsv dg_Par_Cod_vsv[dg_Par_cs_intros]|
  |vdomain dg_Par_Cod_vdomain[dg_Par_cs_simps]|
  |app dg_Par_Cod_app[unfolded set_Collect_arr_Par, dg_Par_cs_simps]|

lemma dg_Par_Cod_vrange: "ℛ∘ (dg_Par α⦇Cod⦈) ⊆∘ dg_Par α⦇Obj⦈"
  unfolding dg_Par_components
  by (rule vrange_VLambda_vsubset, unfold set_Collect_arr_Par) auto


subsubsection‹Arrow with a domain and a codomain›


text‹Rules.›

lemma dg_Par_is_arrI:
  assumes "arr_Par α S" and "S⦇ArrDom⦈ = A" and "S⦇ArrCod⦈ = B"
  shows "S : A ↦⇘dg_Par α⇙ B"
  using assms by (intro is_arrI, unfold dg_Par_components) simp_all

lemmas [dg_Par_cs_intros] = dg_Par_is_arrI

lemma dg_Par_is_arrD:
  assumes "S : A ↦⇘dg_Par α⇙ B"
  shows "arr_Par α S" 
    and [dg_cs_simps]: "S⦇ArrDom⦈ = A" 
    and [dg_cs_simps]: "S⦇ArrCod⦈ = B"
  using is_arrD[OF assms] unfolding dg_Par_components by simp_all

lemma dg_Par_is_arrE:
  assumes "S : A ↦⇘dg_Par α⇙ B"
  obtains "arr_Par α S" and "S⦇ArrDom⦈ = A" and "S⦇ArrCod⦈ = B"
  using is_arrD[OF assms] unfolding dg_Par_components by simp_all


text‹Elementary properties.›

lemma dg_Par_is_arr_dg_Rel_is_arr:
  assumes "r : a ↦⇘dg_Par α⇙ b" 
  shows "r : a ↦⇘dg_Rel α⇙ b"
  using assms arr_Par_arr_RelD(1) 
  by (intro dg_Rel_is_arrI; elim dg_Par_is_arrE) auto

lemma dg_Par_Hom_vsubset_dg_Rel_Hom:
  assumes "a ∈∘ dg_Par α⦇Obj⦈" "b ∈∘ dg_Par α⦇Obj⦈" 
  shows "Hom (dg_Par α) a b ⊆∘ Hom (dg_Rel α) a b"
  by (rule vsubsetI) (simp add: dg_Par_is_arr_dg_Rel_is_arr)

lemma (in 𝒵) dg_Par_incl_Par_is_arr:
  assumes "A ∈∘ dg_Par α⦇Obj⦈" and "B ∈∘ dg_Par α⦇Obj⦈" and "A ⊆∘ B"
  shows "incl_Par A B : A ↦⇘dg_Par α⇙ B"
  by (rule dg_Par_is_arrI)
    (
      auto 
        simp: incl_Rel_components 
        intro!: arr_Par_incl_ParI assms[unfolded dg_Par_components(1)]
    )

lemma (in 𝒵) dg_Par_incl_Par_is_arr'[dg_Par_cs_intros]:
  assumes "A ∈∘ dg_Par α⦇Obj⦈" 
    and "B ∈∘ dg_Par α⦇Obj⦈" 
    and "A ⊆∘ B"
    and "A' = A"
    and "B' = B"
  shows "incl_Par A B : A' ↦⇘dg_Par α⇙ B'"
  using assms(1-3) unfolding assms(4,5) by (rule dg_Par_incl_Par_is_arr)

lemmas [dg_Par_cs_intros] = 𝒵.dg_Par_incl_Par_is_arr'


subsubsection‹‹Par› is a digraph›

lemma (in 𝒵) dg_Par_Hom_vifunion_in_Vset:
  assumes "X ∈∘ Vset α" and "Y ∈∘ Vset α"
  shows "(⋃∘A∈∘X. ⋃∘B∈∘Y. Hom (dg_Par α) A B) ∈∘ Vset α"
proof-
  have 
    "(⋃∘A∈∘X. ⋃∘B∈∘Y. Hom (dg_Par α) A B) ⊆∘
      (⋃∘A∈∘X. ⋃∘B∈∘Y. Hom (dg_Rel α) A B)"
  proof(intro vsubsetI)
    fix F assume "F ∈∘ (⋃∘A∈∘X. ⋃∘B∈∘Y. Hom (dg_Par α) A B)"
    then obtain B where B: "B ∈∘ Y" and "F ∈∘ (⋃∘A∈∘X. Hom (dg_Par α) A B)" 
      by fast
    then obtain A where A: "A ∈∘ X" and F_AB: "F ∈∘ Hom (dg_Par α) A B" by fast
    from A B assms have "A ∈∘ dg_Par α⦇Obj⦈" "B ∈∘ dg_Par α⦇Obj⦈"
      unfolding dg_Par_components by auto
    from F_AB A B dg_Par_Hom_vsubset_dg_Rel_Hom[OF this] show 
      "F ∈∘ (⋃∘A∈∘X. ⋃∘B∈∘Y. Hom (dg_Rel α) A B)"
      by (intro vifunionI) (auto elim!: vsubsetE simp: in_Hom_iff) 
  qed
  with dg_Rel_Hom_vifunion_in_Vset[OF assms] show ?thesis by blast
qed

lemma (in 𝒵) digraph_dg_Par: "digraph α (dg_Par α)"
proof(intro digraphI)
  show "vfsequence (dg_Par α)" unfolding dg_Par_def by simp
  show "vcard (dg_Par α) = 4ℕ" 
    unfolding dg_Par_def by (simp add: nat_omega_simps)
  show "ℛ∘ (dg_Par α⦇Dom⦈) ⊆∘ dg_Par α⦇Obj⦈" by (simp add: dg_Par_Dom_vrange)
  show "ℛ∘ (dg_Par α⦇Cod⦈) ⊆∘ dg_Par α⦇Obj⦈" by (simp add: dg_Par_Cod_vrange)
qed (auto simp: dg_Par_components dg_Par_Hom_vifunion_in_Vset)


subsubsection‹‹Par› is a wide subdigraph of ‹Rel››

lemma (in 𝒵) wide_subdigraph_dg_Par_dg_Rel: "dg_Par α ⊆DG.wide⇘α⇙ dg_Rel α"
proof(intro wide_subdigraphI)
  show "dg_Par α ⊆DG⇘α⇙ dg_Rel α"
    by (intro subdigraphI, unfold dg_Par_components)
      (
        auto simp: 
          dg_Rel_components 
          digraph_dg_Par 
          digraph_dg_Rel 
          dg_Par_is_arr_dg_Rel_is_arr
      )
qed (simp_all add: dg_Rel_components dg_Par_components)

text‹\newpage›

end