Theory CZH_DG_Digraph

(* Copyright 2021 (C) Mihails Milehins *)

theory CZH_DG_Digraph
  imports CZH_DG_Introduction


named_theorems dg_field_simps

definition Obj :: V where [dg_field_simps]: "Obj = 0"
definition Arr :: V where [dg_field_simps]: "Arr = 1"
definition Dom :: V where [dg_field_simps]: "Dom = 2"
definition Cod :: V where [dg_field_simps]: "Cod = 3"

subsection‹Arrow with a domain and a codomain›

The definition of and notation for an arrow with a domain and codomain is
adapted from Chapter I-1 in cite"mac_lane_categories_2010".
The definition is applicable to digraphs and all other relevant derived
entities, such as semicategories and categories, that are presented in
the subsequent chapters.

In this work, by convention, the definition of an arrow with a domain and a 
codomain is nearly always preferred to the explicit use of the domain 
and codomain functions for the specification of the fundamental properties 
of arrows.
Thus, to say that f› is an arrow with the domain a›, it is preferable
to write f : a ↦ b› (b› can be assumed to be arbitrary) instead
of termf  Arr and termDomf = a.

definition is_arr :: "V  V  V  V  bool"
  where "is_arr  a b f  f  Arr  Domf = a  Codf = b"

syntax "_is_arr" :: "V  V  V  V  bool" (‹_ : _ ı _› [51, 51, 51] 51)
translations "f : a b"  "CONST is_arr  a b f"


mk_ide is_arr_def
  |intro is_arrI|
  |dest is_arrD[dest]|
  |elim is_arrE[elim]|

lemmas [dg_shared_cs_intros, dg_cs_intros] = is_arrD(1)
lemmas [dg_shared_cs_simps, dg_cs_simps] = is_arrD(2,3)


text‹See Chapter I-8 in cite"mac_lane_categories_2010".›

abbreviation Hom :: "V  V  V  V" 
  where "Hom  a b  set {f. f : a b}"

lemma small_Hom[simp]: "small {f. f : a b}" unfolding is_arr_def by simp


lemma HomI[dg_shared_cs_intros, dg_cs_intros]:
  assumes "f : a b"
  shows "f  Hom  a b"
  using assms by auto

lemma in_Hom_iff[dg_shared_cs_simps, dg_cs_simps]: 
  "f  Hom  a b  f : a b" 
  by simp

The Hom›-sets in a given digraph are pairwise disjoint. This property 
was exposed as Axiom (v) in an alternative definition of a category presented 
in Chapter I-8 in cite"mac_lane_categories_2010". Within the scope of the 
definitional framework employed in this study, this property holds 

lemma Hom_vdisjnt: 
  assumes "a  a'  b  b'" 
    and "a  Obj"
    and "a'  Obj"
    and "b  Obj" 
    and "b'  Obj"
  shows "vdisjnt (Hom  a b) (Hom  a' b')"
proof(intro vdisjntI, unfold in_Hom_iff)
  fix g f assume "g : a b" and "f : a' b'" 
  then have "g  Arr"
    and "f  Arr"
    and "Domg = a"
    and "Codg = b"
    and "Domf = a'"
    and "Codf = b'"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
  with assms(1) have "Domg  Domf  Codg  Codf" by auto
  then show "g  f" by clarsimp

subsection‹Digraph: background information›

The definition of a digraph that is employed in this work is similar
to the definition of a directed graph› presented in Chapter I-2 in 
cite"mac_lane_categories_2010". However, there are notable differences.
More specifically, the definition is parameterized by a limit ordinal α›, 
such that ω < α›; the set of objects is assumed to be a subset 
of the set Vα in the von Neumann hierarchy of sets (e.g., 
see cite"takeuti_introduction_1971"). Such digraphs are called α›-digraphs› 
to make the dependence on the parameter α› explicit.\footnote{
The prefix ``α›-'' may be omitted whenever it is possible to infer the value 
of α› from the context. This applies not only to the digraphs, but all 
other entities that are parameterized by a limit ordinal α› such that 
ω < α›.} This definition was inspired by the ideas expressed in 
cite"feferman_set-theoretical_1969", cite"sica_doing_2006" and

In ZFC in HOL, the predicate termsmall is used for distinguishing the
terms of any type of the form typ'a set that are isomorphic to elements 
of a term of the type typV (the elements can be exposed via the predicate
constelts). Thus, the collection of the elements associated with any term of 
the type typV (e.g., termelts (a::V)) is always small 
(see the theorem @{thm [source] small_elts} in cite"paulson_zermelo_2019").
Therefore, in this study, in an attempt to avoid confusion, the term ``small''
is never used to refer to digraphs. 
Instead, a new terminology is introduced in this body of work.

Thus, in this work, an α›-digraph is a tiny α›-digraph if and only if 
the set of its objects and the set of its arrows both belong to the set Vα. 
This notion is similar to the notion of a small category in the sense of 
the definition employed in Chapter I-6 in cite"mac_lane_categories_2010", 
if it is assumed that the ``smallness'' is determined with respect to the 
set Vα instead of the universe U›. Also, in what follows, any member of 
the set Vα will be referred to as an α›-tiny set.

All of the large (i.e. non-tiny) digraphs 
that are considered within the scope of this work have a slightly 
unconventional condition associated with the size of their Hom›-sets. 
This condition implies that all Hom›-sets of a digraph 
are tiny, but it is not equivalent to 
all Hom›-sets being tiny. The condition was introduced in an attempt to
resolve some of the issues related to the lack of an analogue of the 
Axiom Schema of Replacement closed with respect to Vα. 

subsection‹Digraph: definition and elementary properties›

locale digraph = 𝒵 α + vfsequence  + Dom: vsv Dom + Cod: vsv Cod 
  for α  +
  assumes dg_length[dg_cs_simps]: "vcard  = 4"  
    and dg_Dom_vdomain[dg_cs_simps]: "𝒟 (Dom) = Arr"    
    and dg_Dom_vrange: " (Dom)  Obj"
    and dg_Cod_vdomain[dg_cs_simps]: "𝒟 (Cod) = Arr"
    and dg_Cod_vrange: " (Cod)  Obj"
    and dg_Obj_vsubset_Vset: "Obj  Vset α"
    and dg_Hom_vifunion_in_Vset[dg_cs_intros]: 
      " A  Obj; B  Obj; A  Vset α; B  Vset α   
        (aA. bB. Hom  a b)  Vset α"

lemmas [dg_cs_simps] = 

lemmas [dg_cs_intros] = 


lemma (in digraph) digraph_axioms'[dg_cs_intros]:
  assumes "α' = α"
  shows "digraph α' "
  unfolding assms by (rule digraph_axioms)

mk_ide rf digraph_def[unfolded digraph_axioms_def]
  |intro digraphI|
  |dest digraphD[dest]|
  |elim digraphE[elim]|

text‹Elementary properties.›

lemma dg_eqI:
  assumes "digraph α 𝔄" 
    and "digraph α 𝔅"
    and "𝔄Obj = 𝔅Obj"
    and "𝔄Arr = 𝔅Arr"
    and "𝔄Dom = 𝔅Dom"
    and "𝔄Cod = 𝔅Cod"
  shows "𝔄 = 𝔅"
  interpret 𝔄: digraph α 𝔄 by (rule assms(1))
  interpret 𝔅: digraph α 𝔅 by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    have dom_lhs: "𝒟 𝔄 = 4" 
      by (cs_concl cs_shallow cs_simp: V_cs_simps dg_cs_simps)
    show "a  𝒟 𝔄  𝔄a = 𝔅a" for a 
      by (unfold dom_lhs, elim_in_numeral, insert assms)
        (auto simp: dg_field_simps)
      cs_concl cs_shallow 
        cs_simp: V_cs_simps dg_cs_simps cs_intro: V_cs_intros

lemma (in digraph) dg_def: " = [Obj, Arr, Dom, Cod]"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟  = 4" 
    by (cs_concl cs_shallow cs_simp: V_cs_simps dg_cs_simps)
  have dom_rhs: "𝒟 [Obj, Arr, Dom, Cod] = 4"
    by (simp add: nat_omega_simps)
  then show "𝒟  = 𝒟 [Obj, Arr, Dom, Cod]"
    unfolding dom_lhs dom_rhs by simp
  show "a  𝒟   a = [Obj, Arr, Dom, Cod]a" for a
    by (unfold dom_lhs, elim_in_numeral, unfold dg_field_simps)
      (simp_all add: nat_omega_simps)
qed (auto simp: vsv_axioms)

lemma (in digraph) dg_Obj_if_Dom_vrange:
  assumes "a   (Dom)"
  shows "a  Obj"
  using assms dg_Dom_vrange by auto

lemma (in digraph) dg_Obj_if_Cod_vrange:
  assumes "a   (Cod)"
  shows "a  Obj"
  using assms dg_Cod_vrange by auto

lemma (in digraph) dg_is_arrD:
  assumes "f : a b" 
  shows "f  Arr" 
    and "a  Obj"
    and "b  Obj"
    and "Domf = a" 
    and "Codf = b"
  from assms show prems: "f  Arr" 
    and fa[symmetric]: "Domf = a"
    and fb[symmetric]: "Codf = b"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
  from digraph_axioms prems have "f  𝒟 (Dom)" "f  𝒟 (Cod)"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps)+
  with assms show "a  Obj" "b  Obj"  
          cs_intro: dg_Obj_if_Dom_vrange dg_Obj_if_Cod_vrange V_cs_intros
          cs_simp: fa fb

lemmas [dg_cs_intros] = digraph.dg_is_arrD(1-3)

lemma (in digraph) dg_is_arrE[elim]:
  assumes "f : a b" 
  obtains "f  Arr" 
    and "a  Obj"
    and "b  Obj"
    and "Domf = a" 
    and "Codf = b"
  using assms by (blast dest: dg_is_arrD)

lemma (in digraph) dg_in_ArrE[elim]:
  assumes "f  Arr"
  obtains a b where "f : a b" and "a  Obj" and "b  Obj"
  using assms by (auto dest: dg_is_arrD(2,3) is_arrI)

lemma (in digraph) dg_Hom_in_Vset[dg_cs_intros]: 
  assumes "a  Obj" and "b  Obj"
  shows "Hom  a b  Vset α"
  let ?A = set {a} and ?B = set {b}
  from assms have A: "?A  Obj" and B: "?B  Obj" by auto
  from assms dg_Obj_vsubset_Vset have "a  Vset α" and "b  Vset α" by auto
  then have a: "set {a}  Vset α" and b: "set {b}  Vset α" 
    by (metis Axiom_of_Pairing insert_absorb2)+
  from dg_Hom_vifunion_in_Vset[OF A B a b] show "Hom  a b  Vset α" by simp

lemmas [dg_cs_intros] = digraph.dg_Hom_in_Vset


lemma (in digraph) dg_Arr_vsubset_Vset: "Arr  Vset α"
proof(intro vsubsetI)
  fix f assume "f  Arr"
  then obtain a b 
    where f: "f : a b" and a: "a  Obj" and b: "b  Obj"
    by blast
  show "f  Vset α"
    by (rule Vset_trans, rule HomI[OF f], rule dg_Hom_in_Vset[OF a b])

lemma (in digraph) dg_Dom_vsubset_Vset: "Dom  Vset α"
      rule Dom.vbrelation_Limit_vsubset_VsetI, 
      unfold dg_cs_simps, 
      insert dg_Dom_vrange dg_Obj_vsubset_Vset
    (auto intro!: dg_Arr_vsubset_Vset)

lemma (in digraph) dg_Cod_vsubset_Vset: "Cod  Vset α"
      rule Cod.vbrelation_Limit_vsubset_VsetI, 
      unfold dg_cs_simps, 
      insert dg_Cod_vrange dg_Obj_vsubset_Vset
    (auto intro!: dg_Arr_vsubset_Vset)

lemma (in digraph) dg_digraph_in_Vset_4: "  Vset (α + 4)"
  note [folded VPow_iff, folded Vset_succ[OF Ord_α], dg_cs_intros] =
  show ?thesis
    by (subst dg_def, succ_of_numeral)
          cs_simp: plus_V_succ_right V_cs_simps 
          cs_intro: dg_cs_intros V_cs_intros

lemma (in digraph) dg_Obj_in_Vset: 
  assumes "𝒵 β" and "α  β"
  shows "Obj  Vset β"
  using assms dg_Obj_vsubset_Vset Vset_in_mono by auto

lemma (in digraph) dg_in_Obj_in_Vset[dg_cs_intros]:
  assumes "a  Obj"
  shows "a  Vset α"
  using assms dg_Obj_vsubset_Vset by auto

lemma (in digraph) dg_Arr_in_Vset: 
  assumes "𝒵 β" and "α  β"
  shows "Arr  Vset β"
  using assms dg_Arr_vsubset_Vset Vset_in_mono by auto

lemma (in digraph) dg_in_Arr_in_Vset[dg_cs_intros]:
  assumes "a  Arr"
  shows "a  Vset α"
  using assms dg_Arr_vsubset_Vset by auto

lemma (in digraph) dg_Dom_in_Vset: 
  assumes "𝒵 β" and "α  β"
  shows "Dom  Vset β"
  by (meson assms dg_Dom_vsubset_Vset Vset_in_mono vsubset_in_VsetI)

lemma (in digraph) dg_Cod_in_Vset:
  assumes "𝒵 β" and "α  β"
  shows "Cod  Vset β"
  by (meson assms dg_Cod_vsubset_Vset Vset_in_mono vsubset_in_VsetI)

lemma (in digraph) dg_in_Vset:
  assumes "𝒵 β" and "α  β"
  shows "  Vset β"
  interpret β: 𝒵 β by (rule assms(1))
  note [dg_cs_intros] = 
    dg_Obj_in_Vset dg_Arr_in_Vset dg_Dom_in_Vset dg_Cod_in_Vset 
  from assms(2) show ?thesis
    by (subst dg_def) 
      (cs_concl cs_shallow cs_intro: dg_cs_intros V_cs_intros)

lemma (in digraph) dg_digraph_if_ge_Limit:
  assumes "𝒵 β" and "α  β"
  shows "digraph β "
proof(rule digraphI)
  show "vfsequence " by (simp add: vfsequence_axioms)
  show "Obj  Vset β"
    by (rule vsubsetI) 
      (meson Vset_in_mono Vset_trans assms(2) dg_Obj_vsubset_Vset vsubsetE)
  fix A B assume "A  Obj" "B  Obj" "A  Vset β" "B  Vset β"
  then have "(aA. bB. Hom  a b)  Arr" by auto
  moreover note dg_Arr_vsubset_Vset
  moreover have "Vset α  Vset β" by (simp add: Vset_in_mono assms(2))
  ultimately show "(aA. bB. Hom  a b)  Vset β" by auto
qed (auto simp: assms(1) dg_Dom_vrange dg_Cod_vrange dg_cs_simps)

lemma small_digraph[simp]: "small {. digraph α }"
proof(cases 𝒵 α)
  case True
  with digraph.dg_in_Vset show ?thesis
    by (intro down[of _ Vset (α + ω)] subsetI)
      (auto simp: 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
  case False
  then have "{. digraph α } = {}" by auto
  then show ?thesis by simp

lemma (in 𝒵) digraphs_in_Vset: 
  assumes "𝒵 β" and "α  β"
  shows "set {. digraph α }  Vset β"
proof(rule vsubset_in_VsetI)
  interpret β: 𝒵 β by (rule assms(1))
  show "set {. digraph α }  Vset (α + 4)"
  proof(intro vsubsetI)
    fix  assume "  set {. digraph α }"
    then interpret digraph α  by simp
    show "  Vset (α + 4)"
      unfolding VPow_iff by (rule dg_digraph_in_Vset_4)
  from assms(2) show "Vset (α + 4)  Vset β"
    by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)

lemma digraph_if_digraph:
  assumes "digraph β "
    and "𝒵 α"
    and "Obj  Vset α"
    and "A B.  A  Obj; B  Obj; A  Vset α; B  Vset α  
      (aA. bB. Hom  a b)  Vset α"
  shows "digraph α "
  interpret digraph β  by (rule assms(1))
  interpret α: 𝒵 α by (rule assms(2))
  show ?thesis
  proof(intro digraphI)
    show "vfsequence " by (simp add: vfsequence_axioms)
    show "(aA. bB. Hom  a b)  Vset α"
      if "A  Obj" "B  Obj" "A  Vset α" "B  Vset α" for A B
      by (rule assms(4)[OF that])
  qed (auto simp: assms(3) dg_Cod_vrange dg_cs_simps intro!: dg_Dom_vrange)

text‹Further properties.›

lemma (in digraph) dg_Dom_app_in_Obj:
  assumes "f  Arr"
  shows "Domf  Obj"
  using assms dg_Dom_vrange by (auto simp: Dom.vsv_vimageI2)

lemma (in digraph) dg_Cod_app_in_Obj:
  assumes "f  Arr"
  shows "Codf  Obj"
  using assms dg_Cod_vrange by (auto simp: Cod.vsv_vimageI2)

lemma (in digraph) dg_Arr_vempty_if_Obj_vempty:
  assumes "Obj = 0"
  shows "Arr = 0"
  by (metis assms eq0_iff dg_Cod_app_in_Obj)

lemma (in digraph) dg_Dom_vempty_if_Arr_vempty:
  assumes "Arr = 0"
  shows "Dom = 0"
  using assms Dom.vdomain_vrange_is_vempty 
  by (auto intro: Dom.vsv_vrange_vempty simp: dg_cs_simps)

lemma (in digraph) dg_Cod_vempty_if_Arr_vempty:
  assumes "Arr = 0"
  shows "Cod = 0"
  using assms Cod.vdomain_vrange_is_vempty 
  by (auto intro: Cod.vsv_vrange_vempty simp: dg_cs_simps)

subsection‹Opposite digraph›

subsubsection‹Definition and elementary properties›

text‹See Chapter II-2 in cite"mac_lane_categories_2010".›

definition op_dg :: "V  V"
  where "op_dg  = [Obj, Arr, Cod, Dom]"


lemma op_dg_components[dg_op_simps]:
  shows "op_dg Obj = Obj"
    and "op_dg Arr = Arr"
    and "op_dg Dom = Cod"
    and "op_dg Cod = Dom"
  unfolding op_dg_def dg_field_simps by (auto simp: nat_omega_simps)

lemma op_dg_component_intros[dg_op_intros]:
  shows "a  Obj  a  op_dg Obj"
    and "f  Arr  f  op_dg Arr"
  unfolding dg_op_simps by simp_all

text‹Elementary properties.›

lemma op_dg_is_arr[dg_op_simps]: "f : b op_dg a  f : a b"
  unfolding dg_op_simps is_arr_def by auto

lemmas [dg_op_intros] = op_dg_is_arr[THEN iffD2]

lemma op_dg_Hom[dg_op_simps]: "Hom (op_dg ) a b = Hom  b a"
  unfolding dg_op_simps by simp

subsubsection‹Further properties›

lemma (in digraph) digraph_op[dg_op_intros]: "digraph α (op_dg )"
proof(intro digraphI, unfold op_dg_components dg_op_simps)
  show "vfsequence (op_dg )" unfolding op_dg_def by simp
  show "vcard (op_dg ) = 4"
    unfolding op_dg_def by (simp add: nat_omega_simps)
  fix A B assume "A  Obj" "B  Obj" "A  Vset α" "B  Vset α"
  then show "((λaA. ((λaaB. Hom  aa a) ` B)) ` A)  Vset α"
    by (subst vifunion_vifunion_flip) (intro dg_Hom_vifunion_in_Vset)
qed (auto simp: dg_Dom_vrange dg_Cod_vrange dg_Obj_vsubset_Vset dg_cs_simps)

lemmas digraph_op[dg_op_intros] = digraph.digraph_op

lemma (in digraph) dg_op_dg_op_dg[dg_op_simps]: "op_dg (op_dg ) = "
  by (rule dg_eqI[of α], unfold dg_op_simps)
    (simp_all add: digraph_axioms digraph.digraph_op digraph_op)

lemmas dg_op_dg_op_dg[dg_op_simps] = digraph.dg_op_dg_op_dg

lemma eq_op_dg_iff[dg_op_simps]: 
  assumes "digraph α 𝔄" and "digraph α 𝔅"
  shows "op_dg 𝔄 = op_dg 𝔅  𝔄 = 𝔅"
  interpret 𝔄: digraph α 𝔄 by (rule assms(1))
  interpret 𝔅: digraph α 𝔅 by (rule assms(2))
  assume prems: "op_dg 𝔄 = op_dg 𝔅"
  show "𝔄 = 𝔅"
  proof(rule dg_eqI[of α])
    from prems show 
      "𝔄Obj = 𝔅Obj" "𝔄Arr = 𝔅Arr" "𝔄Dom = 𝔅Dom" "𝔄Cod = 𝔅Cod"
      by (metis prems 𝔄.dg_op_dg_op_dg 𝔅.dg_op_dg_op_dg)+
  qed (simp_all add: assms)
qed auto