# Theory Digraph_Basic

```section ‹Relations interpreted as Directed Graphs›
theory Digraph_Basic
imports
"Automatic_Refinement.Misc"
"Automatic_Refinement.Refine_Util"
"HOL-Library.Omega_Words_Fun"
begin

text ‹
This theory contains some basic graph theory on directed graphs which are
modeled as a relation between nodes.

The theory here is very fundamental, and
also used by non-directly graph-related applications like the theory of
tail-recursion in the Refinement Framework. Thus, we decided to put it
in the basic theories of the refinement framework.
›

text ‹Directed graphs are modeled as a relation on nodes›
type_synonym 'v digraph = "('v×'v) set"

locale digraph = fixes E :: "'v digraph"

subsection ‹Paths›
text ‹Path are modeled as list of nodes, the last node of a path is not included
into the list. This formalization allows for nice concatenation and splitting
of paths.›
inductive path :: "'v digraph ⇒ 'v ⇒ 'v list ⇒ 'v ⇒ bool" for E where
path0: "path E u [] u"
| path_prepend: "⟦ (u,v)∈E; path E v l w ⟧ ⟹ path E u (u#l) w"

lemma path1: "(u,v)∈E ⟹ path E u [u] v"
by (auto intro: path.intros)

lemma path_empty_conv[simp]:
"path E u [] v ⟷ u=v"
by (auto intro: path0 elim: path.cases)

inductive_cases path_uncons: "path E u (u'#l) w"
inductive_simps path_cons_conv: "path E u (u'#l) w"

lemma path_no_edges[simp]: "path {} u p v ⟷ (u=v ∧ p=[])"
by (cases p) (auto simp: path_cons_conv)

lemma path_conc:
assumes P1: "path E u la v"
assumes P2: "path E v lb w"
shows "path E u (la@lb) w"
using P1 P2 apply induct
by (auto intro: path.intros)

lemma path_append:
"⟦ path E u l v; (v,w)∈E ⟧ ⟹ path E u (l@[v]) w"
using path_conc[OF _ path1] .

lemma path_unconc:
assumes "path E u (la@lb) w"
obtains v where "path E u la v" and "path E v lb w"
using assms
thm path.induct
apply (induct u "la@lb" w arbitrary: la lb rule: path.induct)
apply (auto intro: path.intros elim!: list_Cons_eq_append_cases)
done

lemma path_conc_conv:
"path E u (la@lb) w ⟷ (∃v. path E u la v ∧ path E v lb w)"
by (auto intro: path_conc elim: path_unconc)

lemma (in -) path_append_conv: "path E u (p@[v]) w ⟷ (path E u p v ∧ (v,w)∈E)"

lemmas path_simps = path_empty_conv path_cons_conv path_conc_conv

lemmas path_trans[trans] = path_prepend path_conc path_append
lemma path_from_edges: "⟦(u,v)∈E; (v,w)∈E⟧ ⟹ path E u [u] v"
by (auto simp: path_simps)

lemma path_edge_cases[case_names no_use split]:
assumes "path (insert (u,v) E) w p x"
obtains
"path E w p x"
| p1 p2 where "path E w p1 u" "path (insert (u,v) E) v p2 x"
using assms
apply induction
apply simp
apply (clarsimp)
apply (metis path_simps path_cons_conv)
done

lemma path_edge_rev_cases[case_names no_use split]:
assumes "path (insert (u,v) E) w p x"
obtains
"path E w p x"
| p1 p2 where "path (insert (u,v) E) w p1 u" "path E v p2 x"
using assms
apply (induction p arbitrary: x rule: rev_induct)
apply simp
apply (clarsimp simp: path_cons_conv path_conc_conv)
apply (metis path_simps path_append_conv)
done

lemma path_mono:
assumes S: "E⊆E'"
assumes P: "path E u p v"
shows "path E' u p v"
using P
apply induction
apply simp
using S
apply (auto simp: path_cons_conv)
done

lemma path_is_rtrancl:
assumes "path E u l v"
shows "(u,v)∈E⇧*"
using assms
by induct auto

lemma rtrancl_is_path:
assumes "(u,v)∈E⇧*"
obtains l where "path E u l v"
using assms
by induct (auto intro: path0 path_append)

lemma path_is_trancl:
assumes "path E u l v"
and "l≠[]"
shows "(u,v)∈E⇧+"
using assms
apply induct
apply auto []
apply (case_tac l)
apply auto
done

lemma trancl_is_path:
assumes "(u,v)∈E⇧+"
obtains l where "l≠[]" and "path E u l v"
using assms
by induct (auto intro: path0 path_append)

lemma path_nth_conv: "path E u p v ⟷ (let p'=p@[v] in
u=p'!0 ∧
(∀i<length p' - 1. (p'!i,p'!Suc i)∈E))"
apply (induct p arbitrary: v rule: rev_induct)
apply (auto simp: path_conc_conv path_cons_conv nth_append)
done

lemma path_mapI:
assumes "path E u p v"
shows "path (pairself f ` E) (f u) (map f p) (f v)"
using assms
apply induction
apply (simp)
apply (force simp: path_cons_conv)
done

lemma path_restrict:
assumes "path E u p v"
shows "path (E ∩ set p × insert v (set (tl p))) u p v"
using assms
proof induction
print_cases
case (path_prepend u v p w)
from path_prepend.IH have "path (E ∩ set (u#p) × insert w (set p)) v p w"
apply (rule path_mono[rotated])
by (cases p) auto
thus ?case using ‹(u,v)∈E›
by (cases p) (auto simp add: path_cons_conv)
qed auto

lemma path_restrict_closed:
assumes CLOSED: "E``D ⊆ D"
assumes I: "v∈D" and P: "path E v p v'"
shows "path (E∩D×D) v p v'"
using P CLOSED I
by induction (auto simp: path_cons_conv)

lemma path_set_induct:
assumes "path E u p v" and "u∈I" and "E``I ⊆ I"
shows "set p ⊆ I"
using assms
by (induction rule: path.induct) auto

lemma path_nodes_reachable: "path E u p v ⟹ insert v (set p) ⊆ E⇧*``{u}"
apply (auto simp: in_set_conv_decomp path_cons_conv path_conc_conv)
apply (auto dest!: path_is_rtrancl)
done

lemma path_nodes_edges: "path E u p v ⟹ set p ⊆ fst`E"
by (induction rule: path.induct) auto

lemma path_tl_nodes_edges:
assumes "path E u p v"
shows "set (tl p) ⊆ fst`E ∩ snd`E"
proof -
from path_nodes_edges[OF assms] have "set (tl p) ⊆ fst`E"
by (cases p) auto

moreover have "set (tl p) ⊆ snd`E"
using assms
apply (cases)
apply simp
apply simp
apply (erule path_set_induct[where I = "snd`E"])
apply auto
done
ultimately show ?thesis
by auto
qed

lemma path_loop_shift:
assumes P: "path E u p u"
assumes S: "v∈set p"
obtains p' where "set p' = set p" "path E v p' v"
proof -
from S obtain p1 p2 where [simp]: "p = p1@v#p2" by (auto simp: in_set_conv_decomp)
from P obtain v' where A: "path E u p1 v" "(v, v') ∈ E" "path E v' p2 u"
by (auto simp: path_simps)
hence "path E v (v#p2@p1) v" by (auto simp: path_simps)
thus ?thesis using that[of "v#p2@p1"] by auto
qed

lemma path_hd:
assumes "p ≠ []" "path E v p w"
shows "hd p = v"
using assms
by (auto simp: path_cons_conv neq_Nil_conv)

lemma path_last_is_edge:
assumes "path E x p y"
and "p ≠ []"
shows "(last p, y) ∈ E"
using assms
by (auto simp: neq_Nil_rev_conv path_simps)

lemma path_member_reach_end:
assumes P: "path E x p y"
and v: "v ∈ set p"
shows "(v,y) ∈ E⇧+"
using assms
by (auto intro!: path_is_trancl simp: in_set_conv_decomp path_simps)

lemma path_tl_induct[consumes 2, case_names single step]:
assumes P: "path E x p y"
and NE: "x ≠ y"
and S: "⋀u. (x,u) ∈ E ⟹ P x u"
and ST: "⋀u v. ⟦(x,u) ∈ E⇧+; (u,v) ∈ E; P x u⟧ ⟹ P x v"
shows "P x y ∧ (∀ v ∈ set (tl p). P x v)"
proof -
from P NE have "p ≠ []" by auto
thus ?thesis using P
proof (induction p arbitrary: y rule: rev_nonempty_induct)
case (single u) hence "(x,y) ∈ E" by (simp add: path_cons_conv)
with S show ?case by simp
next
case (snoc u us) hence "path E x us u" by (simp add: path_append_conv)
with snoc path_is_trancl have
"P x u" "(x,u) ∈ E⇧+" "∀v ∈ set (tl us). P x v"
by simp_all
moreover with snoc have "∀v ∈ set (tl (us@[u])). P x v" by simp
moreover from snoc have "(u,y) ∈ E" by (simp add: path_append_conv)
ultimately show ?case by (auto intro: ST)
qed
qed

lemma path_restrict_tl:
"⟦ u∉R; path (E ∩ UNIV × -R) u p v ⟧ ⟹ path (rel_restrict E R) u p v"
apply (induction p arbitrary: u)
apply (auto simp: path_simps rel_restrict_def)
done

lemma path1_restr_conv: "path (E∩UNIV × -R) u (x#xs) v
⟷ (∃w. w∉R ∧ x=u ∧ (u,w)∈E ∧ path (rel_restrict E R) w xs v)"
proof -
have 1: "rel_restrict E R ⊆ E ∩ UNIV × - R" by (auto simp: rel_restrict_def)

show ?thesis
by (auto simp: path_simps intro: path_restrict_tl path_mono[OF 1])
qed

lemma dropWhileNot_path:
assumes "p ≠ []"
and "path E w p x"
and "v ∈ set p"
and "dropWhile ((≠) v) p = c"
shows "path E v c x"
using assms
proof (induction arbitrary: w c rule: list_nonempty_induct)
case (single p) thus ?case by (auto simp add: path_simps)
next
case (cons p ps) hence [simp]: "w = p" by (simp add: path_cons_conv)
show ?case
proof (cases "p=v")
case True with cons show ?thesis by simp
next
case False with cons have "c = dropWhile ((≠) v) ps" by simp
moreover from cons.prems obtain y where "path E y ps x"
using path_uncons by metis
moreover from cons.prems False have "v ∈ set ps" by simp
ultimately show ?thesis using cons.IH by metis
qed
qed

lemma takeWhileNot_path:
assumes "p ≠ []"
and "path E w p x"
and "v ∈ set p"
and "takeWhile ((≠) v) p = c"
shows "path E w c v"
using assms
proof (induction arbitrary: w c rule: list_nonempty_induct)
case (single p) thus ?case by (auto simp add: path_simps)
next
case (cons p ps) hence [simp]: "w = p" by (simp add: path_cons_conv)
show ?case
proof (cases "p=v")
case True with cons show ?thesis by simp
next
case False with cons obtain c' where
"c' = takeWhile ((≠) v) ps" and
[simp]: "c = p#c'"
by simp_all
moreover from cons.prems obtain y where
"path E y ps x" and "(w,y) ∈ E"
using path_uncons by metis+
moreover from cons.prems False have "v ∈ set ps" by simp
ultimately have "path E y c' v" using cons.IH by metis
with ‹(w,y) ∈ E› show ?thesis by (auto simp add: path_cons_conv)
qed
qed

subsection ‹Infinite Paths›
definition ipath :: "'q digraph ⇒ 'q word ⇒ bool"
― ‹Predicate for an infinite path in a digraph›
where "ipath E r ≡ ∀i. (r i, r (Suc i))∈E"

lemma ipath_conc_conv:
"ipath E (u ⌢ v) ⟷ (∃a. path E a u (v 0) ∧ ipath E v)"
apply (auto simp: conc_def ipath_def path_nth_conv nth_append)
by (metis Suc_diff_Suc diff_Suc_Suc not_less_eq)

lemma ipath_iter_conv:
assumes "p≠[]"
shows "ipath E (p⇧ω) ⟷ (path E (hd p) p (hd p))"
proof (cases p)
case Nil thus ?thesis using assms by simp
next
case (Cons u p') hence PLEN: "length p > 0" by simp
show ?thesis proof
assume "ipath E (iter (p))"
hence "∀i. (iter (p) i, iter (p) (Suc i)) ∈ E"
unfolding ipath_def by simp
hence "(∀i<length p. (p!i,(p@[hd p])!Suc i)∈E)"
apply safe
apply (drule_tac x=i in spec)
apply simp
apply (case_tac "Suc i = length p")
done
thus "path E (hd p) p (hd p)"
by (auto simp: path_nth_conv Cons nth_append nth_Cons')
next
assume "path E (hd p) p (hd p)"
thus "ipath E (iter p)"
apply (auto simp: path_nth_conv ipath_def assms Let_def)
apply (drule_tac x="i mod length p" in spec)
apply (auto simp: nth_append assms split: if_split_asm)
apply (metis less_not_refl mod_Suc)
by (metis PLEN diff_self_eq_0 mod_Suc nth_Cons_0 mod_less_divisor)
qed
qed

lemma ipath_to_rtrancl:
assumes R: "ipath E r"
assumes I: "i1≤i2"
shows "(r i1,r i2)∈E⇧*"
using I
proof (induction i2)
case (Suc i2)
show ?case proof (cases "i1=Suc i2")
assume "i1≠Suc i2"
with Suc have "(r i1,r i2)∈E⇧*" by auto
also from R have "(r i2,r (Suc i2))∈E" unfolding ipath_def by auto
finally show ?thesis .
qed simp
qed simp

lemma ipath_to_trancl:
assumes R: "ipath E r"
assumes I: "i1<i2"
shows "(r i1,r i2)∈E⇧+"
proof -
from R have "(r i1,r (Suc i1))∈E"
by (auto simp: ipath_def)
also have "(r (Suc i1),r i2)∈E⇧*"
using ipath_to_rtrancl[OF R,of "Suc i1" i2] I by auto
finally (rtrancl_into_trancl2) show ?thesis .
qed

lemma run_limit_two_connectedI:
assumes A: "ipath E r"
assumes B: "a ∈ limit r" "b∈limit r"
shows "(a,b)∈E⇧+"
proof -
from B have "{a,b} ⊆ limit r" by simp
with A show ?thesis
by (metis ipath_to_trancl two_in_limit_iff)
qed

lemma ipath_subpath:
assumes P: "ipath E r"
assumes LE: "l≤u"
shows "path E (r l) (map r [l..<u]) (r u)"
using LE
proof (induction "u-l" arbitrary: u l)
case (Suc n)
note IH=Suc.hyps(1)
from ‹Suc n = u-l› ‹l≤u› obtain u' where [simp]: "u=Suc u'"
and A: "n=u'-l" "l ≤ u'"
by (cases u) auto

note IH[OF A]
also from P have "(r u',r u)∈E"
by (auto simp: ipath_def)
finally show ?case using ‹l ≤ u'› by (simp add: upt_Suc_append)
qed auto

lemma ipath_restrict_eq: "ipath (E ∩ (E⇧*``{r 0} × E⇧*``{r 0})) r ⟷ ipath E r"
unfolding ipath_def
by (auto simp: relpow_fun_conv rtrancl_power)
lemma ipath_restrict: "ipath E r ⟹ ipath (E ∩ (E⇧*``{r 0} × E⇧*``{r 0})) r"

lemma ipathI[intro?]: "⟦⋀i. (r i, r (Suc i)) ∈ E⟧ ⟹ ipath E r"
unfolding ipath_def by auto

lemma ipathD: "ipath E r ⟹ (r i, r (Suc i)) ∈ E"
unfolding ipath_def by auto

lemma ipath_in_Domain: "ipath E r ⟹ r i ∈ Domain E"
unfolding ipath_def by auto

lemma ipath_in_Range: "⟦ipath E r; i≠0⟧ ⟹ r i ∈ Range E"
unfolding ipath_def by (cases i) auto

lemma ipath_suffix: "ipath E r ⟹ ipath E (suffix i r)"
unfolding suffix_def ipath_def by auto

subsection ‹Strongly Connected Components›

text ‹A strongly connected component is a maximal mutually connected set
of nodes›
definition is_scc :: "'q digraph ⇒ 'q set ⇒ bool"
where "is_scc E U ⟷ U×U⊆E⇧* ∧ (∀V. V⊃U ⟶ ¬ (V×V⊆E⇧*))"

lemma scc_non_empty[simp]: "¬is_scc E {}" unfolding is_scc_def by auto

lemma scc_non_empty'[simp]: "is_scc E U ⟹ U≠{}" unfolding is_scc_def by auto

lemma is_scc_closed:
assumes SCC: "is_scc E U"
assumes MEM: "x∈U"
assumes P: "(x,y)∈E⇧*" "(y,x)∈E⇧*"
shows "y∈U"
proof -
from SCC MEM P have "insert y U × insert y U ⊆ E⇧*"
unfolding is_scc_def
apply clarsimp
apply rule
apply clarsimp_all
apply (erule disjE1)
apply clarsimp
apply (metis in_mono mem_Sigma_iff rtrancl_trans)
apply auto []
apply (metis in_mono mem_Sigma_iff rtrancl_trans)
done
with SCC show ?thesis unfolding is_scc_def by blast
qed

lemma is_scc_connected:
assumes SCC: "is_scc E U"
assumes MEM: "x∈U" "y∈U"
shows "(x,y)∈E⇧*"
using assms unfolding is_scc_def by auto

text ‹In the following, we play around with alternative characterizations, and
prove them all equivalent .›

text ‹A common characterization is to define an equivalence relation
,,mutually connected'' on nodes, and characterize the SCCs as its
equivalence classes:›

definition mconn :: "('a×'a) set ⇒ ('a × 'a) set"
― ‹Mutually connected relation on nodes›
where "mconn E = E⇧* ∩ (E¯)⇧*"

lemma mconn_pointwise:
"mconn E = {(u,v). (u,v)∈E⇧* ∧ (v,u)∈E⇧*}"
by (auto simp add: mconn_def rtrancl_converse)

text ‹‹mconn› is an equivalence relation:›
lemma mconn_refl[simp]: "Id⊆mconn E"

lemma mconn_sym: "mconn E = (mconn E)¯"

lemma mconn_trans: "mconn E O mconn E = mconn E"

lemma mconn_refl': "refl (mconn E)"
by (auto intro: refl_onI simp: mconn_pointwise)

lemma mconn_sym': "sym (mconn E)"
by (auto intro: symI simp: mconn_pointwise)

lemma mconn_trans': "trans (mconn E)"
by (metis mconn_def trans_Int trans_rtrancl)

lemma mconn_equiv: "equiv UNIV (mconn E)"
using mconn_refl' mconn_sym' mconn_trans'
by (rule equivI)

lemma is_scc_mconn_eqclasses: "is_scc E U ⟷ U ∈ UNIV // mconn E"
― ‹The strongly connected components are the equivalence classes of the
mutually-connected relation on nodes›
proof
assume A: "is_scc E U"
then obtain x where "x∈U" unfolding is_scc_def by auto
hence "U = mconn E `` {x}" using A
unfolding mconn_pointwise is_scc_def
apply clarsimp
apply rule
apply auto []
apply clarsimp
by (metis A is_scc_closed)
thus "U ∈ UNIV // mconn E"
by (auto simp: quotient_def)
next
assume "U ∈ UNIV // mconn E"
thus "is_scc E U"
by (auto simp: is_scc_def mconn_pointwise quotient_def)
qed

(* For presentation in the paper *)
lemma "is_scc E U ⟷ U ∈ UNIV // (E⇧* ∩ (E¯)⇧*)"
unfolding is_scc_mconn_eqclasses mconn_def by simp

text ‹We can also restrict the notion of "reachability" to nodes
inside the SCC
›

lemma find_outside_node:
assumes "(u,v)∈E⇧*"
assumes "(u,v)∉(E∩U×U)⇧*"
assumes "u∈U" "v∈U"
shows "∃u'. u'∉U ∧ (u,u')∈E⇧* ∧ (u',v)∈E⇧*"
using assms
apply (induction)
apply auto []
apply clarsimp
by (metis IntI mem_Sigma_iff rtrancl.simps)

lemma is_scc_restrict1:
assumes SCC: "is_scc E U"
shows "U×U⊆(E∩U×U)⇧*"
using assms
unfolding is_scc_def
apply clarsimp
apply (rule ccontr)
apply (drule (2) find_outside_node[rotated])
apply auto []
by (metis is_scc_closed[OF SCC] mem_Sigma_iff rtrancl_trans subsetD)

lemma is_scc_restrict2:
assumes SCC: "is_scc E U"
assumes "V⊃U"
shows "¬ (V×V⊆(E∩V×V)⇧*)"
using assms
unfolding is_scc_def
apply clarsimp
using rtrancl_mono[of "E ∩ V × V" "E"]
apply clarsimp
apply blast
done

lemma is_scc_restrict3:
assumes SCC: "is_scc E U"
shows "((E⇧*``((E⇧*``U) - U)) ∩ U = {})"
apply auto
by (metis assms is_scc_closed is_scc_connected rtrancl_trans)

lemma is_scc_alt_restrict_path:
"is_scc E U ⟷ U≠{} ∧
(U×U ⊆ (E∩U×U)⇧*) ∧ ((E⇧*``((E⇧*``U) - U)) ∩ U = {})"
apply rule
apply (intro conjI)
apply simp
apply (blast dest: is_scc_restrict1)
apply (blast dest: is_scc_restrict3)

unfolding is_scc_def
apply rule
apply clarsimp
apply (metis (full_types) Int_lower1 in_mono mem_Sigma_iff rtrancl_mono_mp)
apply blast
done

lemma is_scc_pointwise:
"is_scc E U ⟷
U≠{}
∧ (∀u∈U. ∀v∈U. (u,v)∈(E∩U×U)⇧*)
∧ (∀u∈U. ∀v. (v∉U ∧ (u,v)∈E⇧*) ⟶ (∀u'∈U. (v,u')∉E⇧*))"
― ‹Alternative, pointwise characterization›
unfolding is_scc_alt_restrict_path
by blast

lemma is_scc_unique:
assumes SCC: "is_scc E scc" "is_scc E scc'"
and v: "v ∈ scc" "v ∈ scc'"
shows "scc = scc'"
proof -
from SCC have "scc = scc' ∨ scc ∩ scc' = {}"
using quotient_disj[OF mconn_equiv]
with v show ?thesis by auto
qed

lemma is_scc_ex1:
"∃!scc. is_scc E scc ∧ v ∈ scc"
proof (rule ex1I, rule conjI)
let ?scc = "mconn E `` {v}"
have "?scc ∈ UNIV // mconn E" by (auto intro: quotientI)
thus "is_scc E ?scc" by (simp add: is_scc_mconn_eqclasses)
moreover show "v ∈ ?scc" by (blast intro: refl_onD[OF mconn_refl'])
ultimately show "⋀scc. is_scc E scc ∧ v ∈ scc ⟹ scc = ?scc"
by (metis is_scc_unique)
qed

lemma is_scc_ex:
"∃scc. is_scc E scc ∧ v ∈ scc"
by (metis is_scc_ex1)

lemma is_scc_connected':
"⟦is_scc E scc; x ∈ scc; y ∈ scc⟧ ⟹ (x,y)∈(Restr E scc)⇧*"
unfolding is_scc_pointwise
by blast

definition scc_of :: "('v×'v) set ⇒ 'v ⇒ 'v set"
where
"scc_of E v = (THE scc. is_scc E scc ∧ v ∈ scc)"

lemma scc_of_is_scc[simp]:
"is_scc E (scc_of E v)"
using is_scc_ex1[of E v]
by (auto dest!: theI' simp: scc_of_def)

lemma node_in_scc_of_node[simp]:
"v ∈ scc_of E v"
using is_scc_ex1[of E v]
by (auto dest!: theI' simp: scc_of_def)

lemma scc_of_unique:
assumes "w ∈ scc_of E v"
shows "scc_of E v = scc_of E w"
proof -
have "is_scc E (scc_of E v)" by simp
moreover note assms
moreover have "is_scc E (scc_of E w)" by simp
moreover have "w ∈ scc_of E w" by simp
ultimately show ?thesis using is_scc_unique by metis
qed

end
```