# Theory CZH_DG_Introduction

```(* Copyright 2021 (C) Mihails Milehins *)

chapter‹Digraphs›

section‹Introduction›
theory CZH_DG_Introduction
imports
"HOL-Library.Rewrite"
CZH_Sets_NOP
CZH_Sets_VNHS
begin

subsection‹Background›

text‹
Many concepts that are normally associated with category theory can be
generalized to directed graphs. It is the goal of
this chapter to expose these generalized concepts and provide the
relevant foundations for the development of the notion of a semicategory
in the next chapter.
It is important to note, however, that it is not the goal of this chapter
to present a comprehensive canonical theory of directed graphs.
Nonetheless, there is little that could prevent one from extending this
body of work by providing canonical results from the theory of directed
graphs.
›

subsection‹Preliminaries›

declare One_nat_def[simp del]

named_theorems slicing_simps
named_theorems slicing_commute
named_theorems slicing_intros

named_theorems dg_op_simps
named_theorems dg_op_intros

named_theorems dg_cs_simps
named_theorems dg_cs_intros

named_theorems dg_shared_cs_simps
named_theorems dg_shared_cs_intros

subsection‹CS setup for foundations›

named_theorems V_cs_simps
named_theorems V_cs_intros

named_theorems Ord_cs_simps
named_theorems Ord_cs_intros

subsubsection‹Basic ‹HOL››

lemma (in semilattice_sup) sup_commute':
shows "b' = b ⟹ a' = a ⟹ a ⊔ b = b' ⊔ a'"
and "b' = b ⟹ a' = a ⟹ a ⊔ b' = b ⊔ a'"
and "b' = b ⟹ a' = a ⟹ a' ⊔ b = b' ⊔ a"
and "b' = b ⟹ a' = a ⟹ a ⊔ b' = b ⊔ a'"
and "b' = b ⟹ a' = a ⟹ a' ⊔ b' = b ⊔ a"
by (auto simp: sup.commute)

lemma (in semilattice_inf) inf_commute':
shows "b' = b ⟹ a' = a ⟹ a ⊓ b = b' ⊓ a'"
and "b' = b ⟹ a' = a ⟹ a ⊓ b' = b ⊓ a'"
and "b' = b ⟹ a' = a ⟹ a' ⊓ b = b' ⊓ a"
and "b' = b ⟹ a' = a ⟹ a ⊓ b' = b ⊓ a'"
and "b' = b ⟹ a' = a ⟹ a' ⊓ b' = b ⊓ a"
by (auto simp: inf.commute)

lemmas [V_cs_simps] =
if_P
if_not_P
inf.absorb1
inf.absorb2
sup.absorb1
sup.absorb2

lemmas [V_cs_intros] =
conjI
sup_commute'
inf_commute'
sup.commute
inf.commute

subsubsection‹Lists for ‹HOL››

lemma list_all_singleton: "list_all P [x] = P x" by simp

lemma replicate_one: "replicate 1 x = [x]"

lemma list_all_mono:
assumes "list_all P xs" and "P ≤ Q"
shows "list_all Q xs"
using assms by (metis list.pred_mono_strong rev_predicate1D)

lemma pred_in_set_mono:
assumes "S ⊆ T"
shows "(λx. x ∈ S) ≤ (λx. x ∈ T)"
using assms by auto

lemma elts_subset_mono:
assumes "S ⊆⇩∘ T"
shows "elts S ⊆ elts T"
using assms by auto

lemma list_all_replicate:
assumes "P x"
shows "list_all P (replicate n x)"
using assms by (metis Ball_set in_set_replicate)

lemma list_all_set:
assumes "list_all P xs" and "x ∈ list.set xs"
shows "P x"
using assms by (induct xs) auto

lemma list_map_id:
assumes "list_all (λx. f x = x) xs"
shows "map f xs = xs"
using assms by (induct xs) auto

lemmas [V_cs_simps] =
List.append.append_Nil
List.append_Nil2
List.append.append_Cons
List.rev.simps(1)
list.map(1,2)
rev.simps(2)
List.map_append
list_all_append
replicate.replicate_0
rev_replicate
semiring_1_class.of_nat_0
replicate.replicate_Suc
replicate_one
list_all_singleton

lemmas [V_cs_intros] =
exI
pred_in_set_mono
elts_subset_mono
list_all_replicate

subsubsection‹Foundations›

abbreviation (input) if3 :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
where "if3 a b c ≡
(
λi. if i = 0 ⇒ a
| i = 1⇩ℕ ⇒ b
| otherwise ⇒ c
)"
lemma if3_0[V_cs_simps]: "if3 a b c 0 = a" by auto
lemma if3_1[V_cs_simps]: "if3 a b c (1⇩ℕ) = b" by auto
lemma if3_2[V_cs_simps]: "if3 a b c (2⇩ℕ) = c" by auto

lemma vinsertI1':
assumes "x' = x"
shows "x ∈⇩∘ vinsert x' A"
unfolding assms by (rule vinsertI1)

lemma in_vsingleton[V_cs_intros]:
assumes "f = a"
shows "f ∈⇩∘ set {a}"
unfolding assms by simp

lemma a_in_succ_a: "a ∈⇩∘ succ a" by simp

lemma a_in_succ_xI:
assumes "a ∈⇩∘ x"
shows "a ∈⇩∘ succ x"
using assms by simp

lemma vone_ne[V_cs_intros]: "1⇩ℕ ≠ 0" by clarsimp

lemmas [V_cs_simps] =
vinsert_set_insert_eq
beta
set_empty
vcard_0

lemmas [V_cs_intros] =
mem_not_refl
succ_notin_self
vset_neq_1
vset_neq_2
nin_vinsertI
vinsertI1'
vinsertI2
vfinite_vinsert
vfinite_vsingleton
vdisjnt_nin_right
vdisjnt_nin_left
vunionI1
vunionI2
vunion_in_VsetI
vintersection_in_VsetI
vsubset_reflexive
vsingletonI
small_insert small_empty
Limit_vtimes_in_VsetI
Limit_VPow_in_VsetI
a_in_succ_a
vsubset_vempty

subsubsection‹Binary relations›

lemma vtimesI'[V_cs_intros]:
assumes "ab = ⟨a, b⟩" and "a ∈⇩∘ A" and "b ∈⇩∘ B"
shows "ab ∈⇩∘ A ×⇩∘ B"
using assms by simp

lemma vrange_vcomp_vsubset[V_cs_intros]:
assumes "ℛ⇩∘ r ⊆⇩∘ B"
shows "ℛ⇩∘ (r ∘⇩∘ s) ⊆⇩∘ B"
using assms by auto

lemma vrange_vconst_on_vsubset[V_cs_intros]:
assumes "a ∈⇩∘ R"
shows "ℛ⇩∘ (vconst_on A a) ⊆⇩∘ R"
using assms by auto

lemma vrange_vcomp_eq_vrange[V_cs_simps]:
assumes "𝒟⇩∘ r = ℛ⇩∘ s"
shows "ℛ⇩∘ (r ∘⇩∘ s) = ℛ⇩∘ r"
using assms by (metis vimage_vdomain vrange_vcomp)

lemmas [V_cs_simps] =
vdomain_vsingleton
vdomain_vlrestriction
vdomain_vlrestriction_vsubset
vdomain_vcomp_vsubset
vdomain_vconverse
vrange_vconverse
vdomain_vconst_on
vconverse_vtimes
vdomain_VLambda

lemmas [V_cs_intros] = vcpower_vsubset_mono

subsubsection‹Single-valued functions›

lemmas (in vsv) [V_cs_intros] = vsv_axioms

lemma vpair_app:
assumes "j = a"
shows "set {⟨a, b⟩}⦇j⦈ = b"
unfolding assms by simp

lemmas [V_cs_simps] =
vpair_app
vsv.vlrestriction_app
vsv_vcomp_at
vid_on_atI

lemmas (in vsv) [V_cs_intros] = vsv_vimageI2'

lemmas [V_cs_intros] =
vsv_vsingleton
vsv.vsv_vimageI2'
vsv_vcomp

subsubsection‹Injective single-valued functions›

lemmas (in v11) [V_cs_intros] = v11_axioms

lemma (in v11) v11_vconverse_app_in_vdomain':
assumes "y ∈⇩∘ ℛ⇩∘ r" and "A = 𝒟⇩∘ r"
shows "r¯⇩∘⦇y⦈ ∈⇩∘ A"
using assms(1) unfolding assms(2) by (rule v11_vconverse_app_in_vdomain)

lemmas (in v11) [V_cs_intros] = v11_vconverse_app_in_vdomain'
lemmas [V_cs_intros] = v11.v11_vconverse_app_in_vdomain'

lemmas (in v11) [V_cs_simps] = (*only in the context of v11*)
v11_app_if_vconverse_app[rotated -2]
v11_app_vconverse_app
v11_vconverse_app_app

lemmas [V_cs_simps] =
v11.v11_vconverse_app[rotated -1]
v11.v11_app_vconverse_app
v11.v11_vconverse_app_app

lemmas [V_cs_intros] =
v11D(1)
v11.v11_vconverse
v11_vcomp

subsubsection‹Operations on indexed families of sets›

lemmas [V_cs_simps] =
vprojection_app
vprojection_vdomain

lemmas [V_cs_intros] = vprojection_vsv

subsubsection‹Finite sequences›

lemmas (in vfsequence) [V_cs_intros] = vfsequence_axioms

lemmas (in vfsequence) [V_cs_simps] = vfsequence_vdomain
lemmas [V_cs_simps] = vfsequence.vfsequence_vdomain

lemmas [V_cs_intros] =
vfsequence.vfsequence_vcons
vfsequence_vempty

lemmas [V_cs_simps] =
vfinite_0_left
vfinite_0_right

subsubsection‹Binary relation as a finite sequence›

lemmas [V_cs_simps] =
fconverse_vunion
fconverse_ftimes
vdomain_fflip

lemmas [V_cs_intros] =
ftimesI2
vcpower_two_ftimesI

subsubsection‹Ordinals›

lemmas [Ord_cs_intros] =
Limit_right_Limit_mult
Limit_left_Limit_mult
Ord_succ_mono
Limit_plus_omega_vsubset_Limit
Limit_plus_nat_in_Limit

subsubsection‹von Neumann hierarchy›

lemma (in 𝒵) omega_in_any[V_cs_intros]:
assumes "α ⊆⇩∘ β"
shows "ω ∈⇩∘ β"
using assms by auto

lemma Ord_vsubset_succ[V_cs_intros]:
assumes "Ord α" and "Ord β" and "α ⊆⇩∘ β"
shows "α ⊆⇩∘ succ β"
by (metis Ord_linear_le Ord_succ assms(1) assms(2) assms(3) leD succ_le_iff)

lemma Ord_in_Vset_succ[V_cs_intros]:
assumes "Ord α" and "a ∈⇩∘ Vset α"
shows "a ∈⇩∘ Vset (succ α)"
using assms by (auto simp: Ord_Vset_in_Vset_succI)

lemma Ord_vsubset_Vset_succ[V_cs_intros]:
assumes "Ord α" and "B ⊆⇩∘ Vset α"
shows "B ⊆⇩∘ Vset (succ α)"
by (intro vsubsetI)
(auto simp: assms Vset_trans Ord_vsubset_in_Vset_succI)

lemmas (in 𝒵) [V_cs_intros] =
omega_in_α
Ord_α
Limit_α

lemmas [V_cs_intros] =
vempty_in_Vset_succ
𝒵.ord_of_nat_in_Vset
Vset_in_mono
Limit_vpair_in_VsetI
Vset_vsubset_mono
Ord_succ
Limit_vempty_in_VsetI
Limit_insert_in_VsetI
vfsequence.vfsequence_Limit_vcons_in_VsetI
vfsequence.vfsequence_Ord_vcons_in_Vset_succI
Limit_vdoubleton_in_VsetI
Limit_omega_in_VsetI
Limit_ftimes_in_VsetI

subsubsection‹‹n›-ary operations›

lemmas [V_cs_simps] =
fflip_app
vdomain_fflip

subsubsection‹Countable ordinals as a set›

named_theorems omega_of_set
named_theorems nat_omega_simps_extra

lemmas [nat_omega_simps_extra] =
Suc_numeral
Suc_1
le_num_simps
less_numeral_simps(1,2)
less_num_simps
less_one
nat_omega_simps

lemmas [omega_of_set] = nat_omega_simps_extra

lemma set_insert_succ[omega_of_set]:
assumes [simp]: "small b" and "set b = a⇩ℕ"
shows "set (insert (a⇩ℕ) b) = succ (a⇩ℕ)"
unfolding assms(2)[symmetric] by auto

lemma set_0[omega_of_set]: "set {0} = succ 0" by auto

subsubsection‹Sequences›

named_theorems vfsequence_simps
named_theorems vfsequence_intros

lemmas [vfsequence_simps] =
vfsequence.vfsequence_at_last[rotated]
vfsequence.vfsequence_vcard_vcons[rotated]
vfsequence.vfsequence_at_not_last[rotated]

lemmas [vfsequence_intros] =
vfsequence.vfsequence_vcons
vfsequence_vempty

subsubsection‹Further numerals›

named_theorems nat_omega_intros

lemma [nat_omega_intros]:
assumes "a < b"
shows "a⇩ℕ ∈⇩∘ b⇩ℕ"
using assms by simp

lemma [nat_omega_intros]:
assumes "0 < b"
shows "0 ∈⇩∘ b⇩ℕ"
using assms by auto

lemma [nat_omega_intros]:
assumes "a = numeral b"
shows "(0::nat) < a"
using assms by auto

lemma nat_le_if_in[nat_omega_intros]:
assumes "x⇩ℕ ∈⇩∘ y⇩ℕ"
shows "x⇩ℕ ≤ y⇩ℕ"
using assms by auto

lemma vempty_le_nat[nat_omega_intros]: "0 ≤ y⇩ℕ" by auto

lemmas [nat_omega_intros] =
preorder_class.order_refl
preorder_class.eq_refl

subsubsection‹Generally available foundational results›

lemma (in 𝒵) 𝒵_β:
assumes "β = α"
shows "𝒵 β"
unfolding assms by auto

lemmas (in 𝒵) [dg_cs_intros] = 𝒵_β

text‹\newpage›

end```