Theory Graph
section ‹Directed Graphs›
theory Graph
imports "../lib/Base_MEC"
begin
subsection ‹Basic Definitions›
type_synonym 'q digraph = "('q × 'q) set"
text ‹Finite-reachable graph: Graph with finitely many nodes that are reachable from a set fo start nodes.›
locale fr_graph_defs =
fixes E :: "'v digraph" and V0 :: "'v set"
locale fr_graph = fr_graph_defs E V0 for E :: "'v digraph" and V0 :: "'v set" +
assumes finite_reachableE_V0[simp, intro!]: "finite (E⇧* `` V0)"
begin
definition "successors V = SPEC (λ xs. set xs = (E `` V))"
lemma finite_V0[simp, intro!]: "finite V0"
by (meson Image_iff finite_reachableE_V0 rev_finite_subset rtrancl.rtrancl_refl subset_eq)
lemma finite_succ:
assumes "v ∈ (E⇧* `` V0)"
shows "finite (E `` {v})"
proof -
obtain v0 where "v0 ∈ V0" and A: "(v0,v) ∈ E⇧*" using assms by blast
hence "E⇧* `` {v0} ⊆ E⇧* `` V0" by blast
hence "finite (E⇧* `` {v0})" using finite_subset by blast
thus ?thesis using finite_reachable_advance A
by (metis finite_Image_subset r_le_rtrancl)
qed
lemma finite_out_edges:
assumes "v ∈ (E⇧* `` V0)"
shows "finite (E ∩ {v} × UNIV)"
proof -
{
fix w
assume "(v,w) ∈ E ∩ {v} × UNIV"
hence "w ∈ E `` {v}" by blast
}
hence A: "E ∩ {v} × UNIV ⊆ {(v,w) | w. w ∈ E `` {v}}" by blast
note finite_succ[OF assms]
hence "finite {(v,w) | w. w ∈ E `` {v}}"
using finite_image_set[of "λw. w ∈ E `` {v}" "λw. (v,w)"]
by (metis Collect_mem_eq)
then show ?thesis using finite_subset[OF A] by blast
qed
end
subsection ‹List of Successors›
definition mop_graph_succ :: "'v digraph ⇒ 'v ⇒ 'v list nres" where
"mop_graph_succ E v ≡ SPEC (λxs. set xs = (E``{v}))"
lemma (in fr_graph) mop_graph_succ_conv[simp]: "mop_graph_succ E v = successors {v}"
unfolding mop_graph_succ_def successors_def by simp
sepref_register mop_graph_succ
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
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)"
by (simp add: path_cons_conv path_conc_conv)
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 Omega_Words_Fun.word ⇒ bool"
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)
apply (metis add_Suc_right diff_add_inverse not_add_less1)
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 (simp add: assms)
apply safe
apply (drule_tac x=i in spec)
apply simp
apply (case_tac "Suc i = length p")
apply (simp add: Cons)
apply (simp add: nth_append)
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"
by (simp add: ipath_restrict_eq)
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 (Omega_Words_Fun.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; clarsimp)
apply (meson SigmaI rtrancl_trans subset_iff)
by (meson SigmaI rtrancl_trans subset_eq)
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"
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"
by (auto simp add: mconn_def)
lemma mconn_sym: "mconn E = (mconn E)¯"
by (auto simp add: mconn_pointwise)
lemma mconn_trans: "mconn E O mconn E = mconn E"
by (auto simp add: mconn_def)
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"
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
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 (meson Int_lower1 SigmaI in_mono rtrancl_mono)
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⇧*))"
unfolding is_scc_alt_restrict_path
by blast
lemma scc_disj_or_eq: assumes SCC: "is_scc E scc" "is_scc E scc'" shows "scc = scc' ∨ scc ∩ scc' = {}"
using SCC quotient_disj[OF mconn_equiv]
by (simp add: is_scc_mconn_eqclasses)
lemma is_scc_unique:
assumes SCC: "is_scc E scc" "is_scc E scc'"
and v: "v ∈ scc" "v ∈ scc'"
shows "scc = scc'"
using scc_disj_or_eq[OF SCC] v
by blast
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 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 assms by metis
qed
subsubsection ‹SCC Additions›
lemma scc_nodes_eq_reach:
assumes SCC: "is_scc E U"
assumes MEM: "x∈U" "y∈U"
shows "E⇧* `` {x} = E⇧* `` {y}"
apply safe
apply(subgoal_tac "(y,x) ∈ E⇧*")
apply simp
using is_scc_connected assms apply metis
apply(subgoal_tac "(x,y) ∈ E⇧*")
apply simp
using is_scc_connected assms by metis
lemma non_singleton_scc_node_succ_aux:
assumes SCC: "is_scc E U"
assumes NE: "x ≠ y"
assumes MEM: "x∈U" "y∈U"
shows "(E ∩ U × U) `` {x} ≠ {}"
apply(subgoal_tac "(x, y) ∈ (E ∩ U × U)⇧+")
apply (metis Image_empty_trancl_Image_empty Image_singleton_iff empty_iff)
using is_scc_restrict1[OF SCC] MEM NE
by (metis SCC is_scc_pointwise rtranclD)
lemma non_singleton_scc_node_succ:
assumes SCC: "is_scc E U"
assumes NE: "¬ is_singleton U"
assumes MEM: "x∈U"
shows "(E ∩ U × U) `` {x} ≠ {}"
using non_singleton_scc_node_succ_aux MEM NE SCC is_singletonI' memb_imp_not_empty
by metis
subsection ‹Bottom Strongly Connected Components›
text ‹A bottom SCC is an SCC without outgoing edges.›
definition "is_bottom_scc E V ≡ is_scc E V ∧ (∀ (u,v) ∈ E. u ∈ V ⟶ v ∈ V)"
lemma bscc_not_leaving: assumes "is_bottom_scc E U" and "u ∈ U" shows "E `` {u} ⊆ U"
using assms
unfolding is_bottom_scc_def is_scc_def Image_def
by fastforce
end