Theory CZH_DG_Introduction
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
add_0_right
add_0
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]"
by (simp add: One_nat_def)
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
group_add_class.minus_zero
group_add_class.minus_minus
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] =
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
lemmas [nat_omega_simps_extra] =
add_num_simps
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