# Theory Rtrancl_On

(* Title:  Rtrancl_On.thy
Author: Lars Noschinski, TU München
Author: René Neumann, TU München
*)

theory Rtrancl_On
imports Main
begin

section ‹Reflexive-Transitive Closure on a Domain›

text ‹
In this section we introduce a variant of the reflexive-transitive closure
of a relation which is useful to formalize the reachability relation on
digraphs.
›

inductive_set
rtrancl_on :: "'a set ⇒ 'a rel ⇒ 'a rel"
for F :: "'a set" and r :: "'a rel"
where
rtrancl_on_refl [intro!, Pure.intro!, simp]: "a ∈ F ⟹ (a, a) ∈ rtrancl_on F r"
| rtrancl_on_into_rtrancl_on [Pure.intro]:
"(a, b) ∈ rtrancl_on F r  ⟹ (b, c) ∈ r ⟹ c ∈ F
⟹ (a, c) ∈ rtrancl_on F r"

definition symcl :: "'a rel ⇒ 'a rel" ("(_⇧s)"  999) where
"symcl R = R ∪ (λ(a,b). (b,a))  R"

lemma in_rtrancl_on_in_F:
assumes "(a,b) ∈ rtrancl_on F r" shows "a ∈ F" "b ∈ F"
using assms by induct auto

lemma rtrancl_on_induct[consumes 1, case_names base step, induct set: rtrancl_on]:
assumes "(a, b) ∈ rtrancl_on F r"
and "a ∈ F ⟹ P a"
"⋀y z. ⟦(a, y) ∈ rtrancl_on F r; (y,z) ∈ r; y ∈ F; z ∈ F; P y⟧ ⟹ P z"
shows "P b"
using assms by (induct a b) (auto dest: in_rtrancl_on_in_F)

lemma rtrancl_on_trans:
assumes "(a,b) ∈ rtrancl_on F r" "(b,c) ∈ rtrancl_on F r" shows "(a,c) ∈ rtrancl_on F r"
using assms(2,1)
by induct (auto intro: rtrancl_on_into_rtrancl_on)

lemma converse_rtrancl_on_into_rtrancl_on:
assumes "(a,b) ∈ r" "(b, c) ∈ rtrancl_on F r" "a ∈ F"
shows "(a, c) ∈ rtrancl_on F r"
proof -
have "b ∈ F" using ‹(b,c) ∈ _› by (rule in_rtrancl_on_in_F)
show ?thesis
apply (rule rtrancl_on_trans)
apply (rule rtrancl_on_into_rtrancl_on)
apply (rule rtrancl_on_refl)
by fact+
qed

lemma rtrancl_on_converseI:
assumes "(y, x) ∈ rtrancl_on F r" shows "(x, y) ∈ rtrancl_on F (r¯)"
using assms
proof induct
case (step a b)
then have "(b,b) ∈ rtrancl_on F (r¯)" "(b,a) ∈ r¯" by auto
then show ?case using step
by (metis rtrancl_on_trans rtrancl_on_into_rtrancl_on)
qed auto

theorem rtrancl_on_converseD:
assumes "(y, x) ∈ rtrancl_on F (r¯)" shows "(x, y) ∈ rtrancl_on F r"
using assms by - (drule rtrancl_on_converseI, simp)

lemma converse_rtrancl_on_induct[consumes 1, case_names base step, induct set: rtrancl_on]:
assumes major: "(a, b) ∈ rtrancl_on F r"
and cases: "b ∈ F ⟹ P b"
"⋀x y. ⟦(x,y) ∈ r; (y,b) ∈ rtrancl_on F r; x ∈ F; y ∈ F; P y⟧ ⟹ P x"
shows "P a"
using rtrancl_on_converseI[OF major] cases
by induct (auto intro: rtrancl_on_converseD)

lemma converse_rtrancl_on_cases:
assumes "(a, b) ∈ rtrancl_on F r"
obtains (base) "a = b" "b ∈ F"
| (step) c where "(a,c) ∈ r" "(c,b) ∈ rtrancl_on F r"
using assms by induct auto

lemma rtrancl_on_sym:
assumes "sym r" shows "sym (rtrancl_on F r)"
using assms by (auto simp: sym_conv_converse_eq intro: symI dest: rtrancl_on_converseI)

lemma rtrancl_on_mono:
assumes "s ⊆ r" "F ⊆ G" "(a,b) ∈ rtrancl_on F s" shows "(a,b) ∈ rtrancl_on G r"
using assms(3,1,2)
proof induct
case (step x y) show ?case
using step assms by (intro converse_rtrancl_on_into_rtrancl_on[OF _ step(5)]) auto
qed auto

lemma rtrancl_consistent_rtrancl_on:
assumes "(a,b) ∈ r⇧*"
and "a ∈ F" "b ∈ F"
and consistent: "⋀a b. ⟦ a ∈ F; (a,b) ∈ r ⟧ ⟹ b ∈ F"
shows "(a,b) ∈ rtrancl_on F r"
using assms(1-3)
proof (induction rule: converse_rtrancl_induct)
case (step y z) then have "z ∈ F" by (rule_tac consistent) simp
with step have "(z,b) ∈ rtrancl_on F r" by simp
with step.prems ‹(y,z) ∈ r› ‹z ∈ F› show ?case
using converse_rtrancl_on_into_rtrancl_on
by metis
qed simp

lemma rtrancl_on_rtranclI:
"(a,b) ∈ rtrancl_on F r ⟹ (a,b) ∈ r⇧*"
by (induct rule: rtrancl_on_induct) simp_all

lemma rtrancl_on_sub_rtrancl:
"rtrancl_on F r ⊆ r^*"
using rtrancl_on_rtranclI
by auto

end


# Theory Stuff

(* Title:  Stuff.thy
Author: Lars Noschinski, TU München
*)

theory Stuff
imports
Main
"HOL-Library.Extended_Real"

begin

section ‹Additional theorems for base libraries›

text ‹
This section contains lemmas unrelated to graph theory which might be
interesting for the Isabelle distribution
›

lemma ereal_Inf_finite_Min:
fixes S :: "ereal set"
assumes "finite S" and "S ≠ {}"
shows "Inf S = Min S"
using assms
by (induct S rule: finite_ne_induct) (auto simp: min_absorb1)

lemma finite_INF_in:
fixes f :: "'a ⇒ ereal"
assumes "finite S"
assumes "S ≠ {}"
shows "(INF s∈ S. f s) ∈ f  S"
proof -
from assms
have "finite (f  S)" "f  S ≠ {}" by auto
then show "Inf (f  S) ∈ f  S"
using ereal_Inf_finite_Min [of "f  S"]  by simp
qed

lemma not_mem_less_INF:
fixes f :: "'a ⇒ 'b :: complete_lattice"
assumes "f x < (INF s∈ S. f s)"
assumes "x ∈ S"
shows "False"
using assms by (metis INF_lower less_le_not_le)

lemma sym_diff:
assumes "sym A" "sym B" shows "sym (A - B)"
using assms by (auto simp: sym_def)

subsection ‹List›

lemmas list_exhaust2 = list.exhaust[case_product list.exhaust]

lemma list_exhaust_NSC:
obtains (Nil) "xs = []" | (Single) x where "xs = [x]" | (Cons_Cons) x y ys where "xs = x # y # ys"
by (metis list.exhaust)

lemma tl_rev:
"tl (rev p) = rev (butlast p)"
by (induct p) auto

lemma butlast_rev:
"butlast (rev p) = rev (tl p)"
by (induct p) auto

lemma take_drop_take:
"take n xs @ drop n (take m xs) = take (max n m) xs"
proof cases
assume "m < n" then show ?thesis by (auto simp: max_def)
next
assume "¬m < n"
then have "take n xs = take n (take m xs)" by (auto simp: min_def)
then show ?thesis by (simp del: take_take add: max_def)
qed

lemma drop_take_drop:
"drop n (take m xs) @ drop m xs = drop (min n m) xs"
proof cases
assume A: "¬m < n"
then show ?thesis
using drop_append[of n "take m xs" "drop m xs"]
by (cases "length xs < n") (auto simp: not_less min_def)
qed (auto simp: min_def)

lemma not_distinct_decomp_min_prefix:
assumes "¬ distinct ws"
shows "∃ xs ys zs y. ws = xs @ y # ys @ y # zs ∧ distinct xs ∧ y ∉ set xs ∧ y ∉ set ys "
proof -
obtain xs y ys where "y ∈ set xs" "distinct xs" "ws = xs @ y # ys"
using assms by (auto simp: not_distinct_conv_prefix)
moreover then obtain xs' ys' where "xs = xs' @ y # ys'" by (auto simp: in_set_conv_decomp)
ultimately show ?thesis by auto
qed

lemma not_distinct_decomp_min_not_distinct:
assumes "¬ distinct ws"
shows "∃xs y ys zs. ws = xs @ y # ys @ y # zs ∧ distinct (ys @ [y])"
using assms
proof (induct ws)
case (Cons w ws)
show ?case
proof (cases "distinct ws")
case True
then obtain xs ys where "ws = xs @ w # ys" "w ∉ set xs"
using Cons.prems by (fastforce dest: split_list_first)
then have "distinct (xs @ [w])" "w # ws = [] @ w # xs @ w # ys"
using ‹distinct ws› by auto
then show ?thesis by blast
next
case False
then obtain xs y ys zs where "ws = xs @ y # ys @ y # zs ∧ distinct (ys @ [y])"
using Cons by auto
then have "w # ws = (w # xs) @ y # ys @ y # zs ∧ distinct (ys @ [y])"
by simp
then show ?thesis by blast
qed
qed simp

lemma card_Ex_subset:
"k ≤ card M ⟹ ∃N. N ⊆ M ∧ card N = k"
by (induct rule: inc_induct) (auto simp: card_Suc_eq)

lemma list_set_tl: "x ∈ set (tl xs) ⟹ x ∈ set xs"
by (cases xs) auto

section ‹NOMATCH simproc›

text ‹
The simplification procedure can be used to avoid simplification of terms of a certain form
›

definition NOMATCH :: "'a ⇒ 'a ⇒ bool" where "NOMATCH val pat ≡ True"
lemma NOMATCH_cong[cong]: "NOMATCH val pat = NOMATCH val pat" by (rule refl)

simproc_setup NOMATCH ("NOMATCH val pat") = ‹fn _ => fn ctxt => fn ct =>
let
val thy = Proof_Context.theory_of ctxt
val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
in if m then NONE else SOME @{thm NOMATCH_def} end
›

text ‹
This setup ensures that a rewrite rule of the form @{term "NOMATCH val pat ⟹ t"}
is only applied, if the pattern @{term pat} does not match the value @{term val}.
›

end


# Theory Digraph

(* Title:  Digraph.thy
Author: Lars Noschinski, TU München
Author: René Neumann
*)

theory Digraph
imports
Main
Rtrancl_On
Stuff
begin

section ‹Digraphs›

record ('a,'b) pre_digraph =
verts :: "'a set"
arcs :: "'b set"
tail :: "'b ⇒ 'a"

definition arc_to_ends :: "('a,'b) pre_digraph ⇒ 'b ⇒ 'a × 'a" where
"arc_to_ends G e ≡ (tail G e, head G e)"

locale pre_digraph =
fixes G :: "('a, 'b) pre_digraph" (structure)

locale wf_digraph = pre_digraph +
assumes tail_in_verts[simp]: "e ∈ arcs G ⟹ tail G e ∈ verts G"
assumes head_in_verts[simp]: "e ∈ arcs G ⟹ head G e ∈ verts G"
begin

lemma wf_digraph: "wf_digraph G" by intro_locales

end

definition arcs_ends :: "('a,'b) pre_digraph ⇒ ('a × 'a) set" where
"arcs_ends G ≡ arc_to_ends G  arcs G"

definition symmetric :: "('a,'b) pre_digraph ⇒ bool" where
"symmetric G ≡ sym (arcs_ends G)"

text ‹
Matches "pseudo digraphs" from \cite{bangjensen2009digraphs}, except for
allowing the null graph. For a discussion of that topic,
›
locale fin_digraph = wf_digraph +
assumes finite_verts[simp]: "finite (verts G)"
and finite_arcs[simp]: "finite (arcs G)"

locale loopfree_digraph = wf_digraph +
assumes no_loops: "e ∈ arcs G ⟹ tail G e ≠ head G e"

locale nomulti_digraph = wf_digraph +
assumes no_multi_arcs: "⋀e1 e2. ⟦e1 ∈ arcs G; e2 ∈ arcs G;
arc_to_ends G e1 = arc_to_ends G e2⟧ ⟹ e1 = e2"

locale sym_digraph = wf_digraph +
assumes sym_arcs[intro]: "symmetric G"

locale digraph = fin_digraph + loopfree_digraph + nomulti_digraph

text ‹
We model graphs as symmetric digraphs. This is fine for many purposes,
but not for all. For example, the path $a,b,a$ is considered to be a cycle
in a digraph (and hence in a symmetric digraph), but not in an undirected
graph.
›
locale pseudo_graph = fin_digraph + sym_digraph

locale graph = digraph + pseudo_graph

lemma (in wf_digraph) fin_digraphI[intro]:
assumes "finite (verts G)"
assumes "finite (arcs G)"
shows "fin_digraph G"
using assms by unfold_locales

lemma (in wf_digraph) sym_digraphI[intro]:
assumes "symmetric G"
shows "sym_digraph G"
using assms by unfold_locales

lemma (in digraph) graphI[intro]:
assumes "symmetric G"
shows "graph G"
using assms by unfold_locales

definition (in wf_digraph) arc :: "'b ⇒ 'a × 'a ⇒ bool" where
"arc e uv ≡ e ∈ arcs G ∧ tail G e = fst uv ∧ head G e = snd uv"

lemma (in fin_digraph) fin_digraph: "fin_digraph G"
by unfold_locales

lemma (in nomulti_digraph) nomulti_digraph: "nomulti_digraph G" by unfold_locales

lemma arcs_ends_conv: "arcs_ends G = (λe. (tail G e, head G e))  arcs G"
by (auto simp: arc_to_ends_def arcs_ends_def)

lemma symmetric_conv: "symmetric G ⟷ (∀e1 ∈ arcs G. ∃e2 ∈ arcs G. tail G e1 = head G e2 ∧ head G e1 = tail G e2)"
unfolding symmetric_def arcs_ends_conv sym_def by auto

lemma arcs_ends_symmetric:
assumes "symmetric G"
shows "(u,v) ∈ arcs_ends G ⟹ (v,u) ∈ arcs_ends G"
using assms unfolding symmetric_def sym_def by auto

lemma (in nomulti_digraph) inj_on_arc_to_ends:
"inj_on (arc_to_ends G) (arcs G)"
by (rule inj_onI) (rule no_multi_arcs)

subsection ‹Reachability›

abbreviation dominates :: "('a,'b) pre_digraph ⇒ 'a ⇒ 'a ⇒ bool" ("_ →ı _" [100,100] 40) where
"dominates G u v ≡ (u,v) ∈ arcs_ends G"

abbreviation reachable1 :: "('a,'b) pre_digraph ⇒ 'a ⇒ 'a ⇒ bool" ("_ →⇧+ı _" [100,100] 40) where
"reachable1 G u v ≡ (u,v) ∈ (arcs_ends G)^+"

definition reachable :: "('a,'b) pre_digraph ⇒ 'a ⇒ 'a ⇒ bool" ("_ →⇧*ı _" [100,100] 40) where
"reachable G u v ≡ (u,v) ∈ rtrancl_on (verts G) (arcs_ends G)"

lemma reachableE[elim]:
assumes "u →⇘G⇙ v"
obtains e where "e ∈ arcs G" "tail G e = u" "head G e = v"
using assms by (auto simp add: arcs_ends_conv)

assumes "a → a" shows "False"
using assms by (rule reachableE) (auto dest: no_loops)

lemma reachable_in_vertsE:
assumes "u →⇧*⇘G⇙ v" obtains "u ∈ verts G" "v ∈ verts G"
using assms unfolding reachable_def by induct auto

lemma symmetric_reachable:
assumes "symmetric G" "v →⇧*⇘G⇙ w" shows "w →⇧*⇘G⇙ v"
proof -
have "sym (rtrancl_on (verts G) (arcs_ends G))"
using assms by (auto simp add: symmetric_def dest: rtrancl_on_sym)
then show ?thesis using assms unfolding reachable_def by (blast elim: symE)
qed

lemma reachable_rtranclI:
"u →⇧*⇘G ⇙ v ⟹ (u, v) ∈ (arcs_ends G)⇧*"
unfolding reachable_def by (rule rtrancl_on_rtranclI)

context wf_digraph begin

assumes "u →⇘G⇙ v" shows "u ∈ verts G" "v ∈ verts G"
using assms unfolding arcs_ends_conv by auto

lemma dominatesI: assumes "arc_to_ends G a = (u,v)" "a ∈ arcs G" shows "u →⇘G⇙ v"
using assms by (auto simp: arcs_ends_def intro: rev_image_eqI)

lemma reachable_refl [intro!, Pure.intro!, simp]: "v ∈ verts G ⟹ v →⇧* v"
unfolding reachable_def by auto

assumes "a →⇘G⇙ b" "b →⇧*⇘G⇙ c" shows "a →⇧*⇘G⇙ c"
using assms by (auto simp: reachable_def intro: converse_rtrancl_on_into_rtrancl_on adj_in_verts)

assumes "a →⇧*⇘G⇙ b" "b →⇘G⇙ c" shows "a →⇧*⇘G⇙ c"
using assms by (auto simp: reachable_def intro: rtrancl_on_into_rtrancl_on adj_in_verts)

lemma reachable_adjI [intro, simp]: "u → v ⟹ u →⇧* v"

lemma reachable_trans[trans]:
assumes "u →⇧*v" "v →⇧* w" shows "u →⇧* w"
using assms unfolding reachable_def by (rule rtrancl_on_trans)

lemma reachable_induct[consumes 1, case_names base step]:
assumes major: "u →⇧*⇘G⇙ v"
and cases: "u ∈ verts G ⟹ P u"
"⋀x y. ⟦u →⇧*⇘G⇙ x; x →⇘G⇙ y; P x⟧ ⟹ P y"
shows "P v"
using assms unfolding reachable_def by (rule rtrancl_on_induct) auto

lemma converse_reachable_induct[consumes 1, case_names base step, induct pred: reachable]:
assumes major: "u →⇧*⇘G⇙ v"
and cases: "v ∈ verts G ⟹ P v"
"⋀x y. ⟦x →⇘G⇙ y; y →⇧*⇘G⇙ v; P y⟧ ⟹ P x"
shows "P u"
using assms unfolding reachable_def by (rule converse_rtrancl_on_induct) auto

lemma (in pre_digraph) converse_reachable_cases:
assumes "u →⇧*⇘G⇙ v"
obtains (base) "u = v" "u ∈ verts G"
| (step) w where "u →⇘G⇙ w" "w →⇧*⇘G⇙ v"
using assms unfolding reachable_def by (cases rule: converse_rtrancl_on_cases) auto

lemma reachable_in_verts:
assumes "u →⇧* v" shows "u ∈ verts G" "v ∈ verts G"

lemma reachable1_in_verts:
assumes "u →⇧+ v" shows "u ∈ verts G" "v ∈ verts G"
using assms

lemma reachable1_reachable[intro]:
"v →⇧+ w ⟹ v →⇧* w"
unfolding reachable_def

lemmas reachable1_reachableE[elim] = reachable1_reachable[elim_format]

lemma reachable_neq_reachable1[intro]:
assumes reach: "v →⇧* w"
and neq: "v ≠ w"
shows "v →⇧+ w"
proof -
from reach have "(v,w) ∈ (arcs_ends G)^*" by (rule reachable_rtranclI)
with neq show ?thesis by (auto dest: rtranclD)
qed

lemmas reachable_neq_reachable1E[elim] = reachable_neq_reachable1[elim_format]

lemma reachable1_reachable_trans [trans]:
"u →⇧+ v ⟹ v →⇧* w ⟹ u →⇧+ w"
by (metis trancl_trans reachable_neq_reachable1)

lemma reachable_reachable1_trans [trans]:
"u →⇧* v ⟹ v →⇧+ w ⟹ u →⇧+ w"
by (metis trancl_trans reachable_neq_reachable1)

lemma reachable_conv:
"u →⇧* v ⟷ (u,v) ∈ (arcs_ends G)^* ∩ (verts G × verts G)"
apply (auto intro: reachable_in_verts)
apply (induct rule: rtrancl_induct)
apply auto
done

lemma reachable_conv':
assumes "u ∈ verts G"
shows "u →⇧* v ⟷ (u,v) ∈ (arcs_ends G)⇧*" (is "?L = ?R")
proof
assume "?R" then show "?L" using assms  by induct auto
qed (auto simp: reachable_conv)

end

lemma (in sym_digraph) symmetric_reachable':
assumes "v →⇧*⇘G⇙ w" shows "w →⇧*⇘G⇙ v"
using sym_arcs assms by (rule symmetric_reachable)

subsection ‹Degrees of vertices›

definition in_arcs :: "('a, 'b) pre_digraph ⇒ 'a ⇒ 'b set" where
"in_arcs G v ≡ {e ∈ arcs G. head G e = v}"

definition out_arcs :: "('a, 'b) pre_digraph ⇒ 'a ⇒ 'b set" where
"out_arcs G v ≡ {e ∈ arcs G. tail G e = v}"

definition in_degree :: "('a, 'b) pre_digraph ⇒ 'a ⇒ nat" where
"in_degree G v ≡ card (in_arcs G v)"

definition out_degree :: "('a, 'b) pre_digraph ⇒ 'a ⇒ nat" where
"out_degree G v ≡ card (out_arcs G v)"

lemma (in fin_digraph) finite_in_arcs[intro]:
"finite (in_arcs G v)"
unfolding in_arcs_def by auto

lemma (in fin_digraph) finite_out_arcs[intro]:
"finite (out_arcs G v)"
unfolding out_arcs_def by auto

lemma in_in_arcs_conv[simp]:
"e ∈ in_arcs G v ⟷ e ∈ arcs G ∧ head G e = v"
unfolding in_arcs_def by auto

lemma in_out_arcs_conv[simp]:
"e ∈ out_arcs G v ⟷ e ∈ arcs G ∧ tail G e = v"
unfolding out_arcs_def by auto

lemma inout_arcs_arc_simps[simp]:
assumes "e ∈ arcs G"
shows "tail G e = u ⟹ out_arcs G u ∩ insert e E = insert e (out_arcs G u ∩ E)"
"tail G e ≠ u ⟹ out_arcs G u ∩ insert e E = out_arcs G u ∩ E"
"out_arcs G u ∩ {} = {}" (* XXX: should be unnecessary *)
"head G e = u ⟹ in_arcs G u ∩ insert e E = insert e (in_arcs G u ∩ E)"
"head G e ≠ u ⟹ in_arcs G u ∩ insert e E = in_arcs G u ∩ E"
"in_arcs G u ∩ {} = {}" (* XXX: should be unnecessary *)
using assms by auto

lemma in_arcs_int_arcs[simp]: "in_arcs G u ∩ arcs G = in_arcs G u" and
out_arcs_int_arcs[simp]: "out_arcs G u ∩ arcs G = out_arcs G u"
by auto

lemma in_arcs_in_arcs: "x ∈ in_arcs G u ⟹ x ∈ arcs G"
and out_arcs_in_arcs: "x ∈ out_arcs G u ⟹ x ∈ arcs G"
by (auto simp: in_arcs_def out_arcs_def)

subsection ‹Graph operations›

context pre_digraph begin

definition add_arc :: "'b ⇒  ('a,'b) pre_digraph" where
"add_arc a = ⦇ verts = verts G ∪ {tail G a, head G a}, arcs = insert a (arcs G), tail = tail G, head = head G ⦈"

definition  del_arc :: "'b ⇒ ('a,'b) pre_digraph" where
"del_arc a = ⦇ verts = verts G, arcs = arcs G - {a}, tail = tail G, head = head G ⦈"

definition add_vert :: "'a ⇒  ('a,'b) pre_digraph" where
"add_vert v = ⦇ verts = insert v (verts G), arcs = arcs G, tail = tail G, head = head G ⦈"

definition del_vert :: "'a ⇒  ('a,'b) pre_digraph" where
"del_vert v = ⦇ verts = verts G - {v}, arcs = {a ∈ arcs G. tail G a ≠ v ∧ head G a ≠ v}, tail = tail G, head = head G ⦈"

lemma
verts_add_arc: "⟦ tail G a ∈ verts G; head G a ∈ verts G ⟧ ⟹ verts (add_arc a) = verts G"  and

lemma
verts_del_arc: "verts (del_arc a) = verts G"  and
arcs_del_arc: "arcs (del_arc a) = arcs G - {a}" and
tail_del_arc: "tail (del_arc a) = tail G" and
by (auto simp: del_arc_def)

lemmas del_arc_simps[simp] = verts_del_arc arcs_del_arc tail_del_arc head_del_arc

lemma

lemma
verts_del_vert: "verts (pre_digraph.del_vert G u) = verts G - {u}" and
arcs_del_vert: "arcs (pre_digraph.del_vert G u) = {a ∈ arcs G. tail G a ≠ u ∧ head G a ≠ u}" and
tail_del_vert: "tail (pre_digraph.del_vert G u) = tail G" and
ends_del_vert: "arc_to_ends (pre_digraph.del_vert G u) = arc_to_ends G"
by (auto simp: pre_digraph.del_vert_def arc_to_ends_def)

lemmas del_vert_simps = verts_del_vert arcs_del_vert tail_del_vert head_del_vert

"⟦ tail G a ∈ verts G; head G a ∈ verts G ⟧ ⟹ pre_digraph.del_arc (add_arc a) a = del_arc a"

lemma del_del_arc_collapse[simp]: "pre_digraph.del_arc (del_arc a) a = del_arc a"

lemma del_arc_commute: "pre_digraph.del_arc (del_arc b) a = pre_digraph.del_arc (del_arc a) b"
by (auto simp: pre_digraph.del_arc_def)

lemma del_arc_in: "a ∉ arcs G ⟹ del_arc a = G"
by (rule pre_digraph.equality) (auto simp: add_arc_def)

"in_arcs (add_arc a) u = (if head G a = u then insert a (in_arcs G u) else in_arcs G u)"
by auto

"out_arcs (add_arc a) u = (if tail G a = u then insert a (out_arcs G u) else out_arcs G u)"
by auto

lemma in_arcs_del_arc_iff:
"in_arcs (del_arc a) u = (if head G a = u then in_arcs G u - {a} else in_arcs G u)"
by auto

lemma out_arcs_del_arc_iff:
"out_arcs (del_arc a) u = (if tail G a = u then out_arcs G u - {a} else out_arcs G u)"
by auto

lemma (in wf_digraph) add_arc_in: "a ∈ arcs G ⟹ add_arc a = G"
by (rule pre_digraph.equality) (auto simp: add_arc_def)

end

context wf_digraph begin

lemma wf_digraph_del_arc[intro]:
"wf_digraph (del_arc a)" by unfold_locales (auto simp: verts_add_arc_conv)

lemma wf_digraph_del_vert: "wf_digraph (del_vert u)"
by standard (auto simp: del_vert_simps)

assumes "u ∉ verts G"
shows "pre_digraph.del_vert (add_vert u) u = G"
using assms by (intro pre_digraph.equality) (auto simp: pre_digraph.del_vert_def add_vert_def)

end

context fin_digraph begin

"in_degree (add_arc a) u = (if head G a = u ∧ a ∉ arcs G then in_degree G u + 1 else in_degree G u)"
proof -
have "a ∉ arcs G ⟹ a ∉ in_arcs G u" by (auto simp: in_arcs_def)
with finite_in_arcs show ?thesis
unfolding in_degree_def by (auto simp: in_arcs_add_arc_iff intro: arg_cong[where f=card])
qed

"out_degree (add_arc a) u = (if tail G a = u ∧ a ∉ arcs G then out_degree G u + 1 else out_degree G u)"
proof -
have "a ∉ arcs G ⟹ a ∉ out_arcs G u" by (auto simp: out_arcs_def)
with finite_out_arcs show ?thesis
unfolding out_degree_def by (auto simp: out_arcs_add_arc_iff intro: arg_cong[where f=card])
qed

lemma in_degree_del_arc_iff:
"in_degree (del_arc a) u = (if head G a = u ∧ a ∈ arcs G then in_degree G u - 1 else in_degree G u)"
proof -
have "a ∉ arcs G ⟹ a ∉ in_arcs G u" by (auto simp: in_arcs_def)
with finite_in_arcs show ?thesis
unfolding in_degree_def by (auto simp: in_arcs_del_arc_iff intro: arg_cong[where f=card])
qed

lemma out_degree_del_arc_iff:
"out_degree (del_arc a) u = (if tail G a = u ∧ a ∈ arcs G then out_degree G u - 1 else out_degree G u)"
proof -
have "a ∉ arcs G ⟹ a ∉ out_arcs G u" by (auto simp: out_arcs_def)
with finite_out_arcs show ?thesis
unfolding out_degree_def by (auto simp: out_arcs_del_arc_iff intro: arg_cong[where f=card])
qed

lemma fin_digraph_del_vert: "fin_digraph (del_vert u)"
by standard (auto simp: del_vert_simps)

lemma fin_digraph_del_arc: "fin_digraph (del_arc a)"
by standard (auto simp: del_vert_simps)

end

end


# Theory Bidirected_Digraph

theory Bidirected_Digraph
imports
Digraph
"HOL-Combinatorics.Permutations"
begin

section ‹Bidirected Graphs›

locale bidirected_digraph = wf_digraph G for G +
fixes arev :: "'b ⇒ 'b"
assumes arev_dom: "⋀a. a ∈ arcs G ⟷ arev a ≠ a"
assumes arev_arev_raw: "⋀a. a ∈ arcs G ⟹ arev (arev a) = a"
assumes tail_arev[simp]: "⋀a. a ∈ arcs G ⟹ tail G (arev a) = head G a"

lemma (in wf_digraph) bidirected_digraphI:
assumes arev_eq: "⋀a. a ∉ arcs G ⟹ arev a = a"
assumes arev_neq: "⋀a. a ∈ arcs G ⟹ arev a ≠ a"
assumes arev_arev_raw: "⋀a. a ∈ arcs G ⟹ arev (arev a) = a"
assumes tail_arev: "⋀a. a ∈ arcs G ⟹ tail G (arev a) = head G a"
shows "bidirected_digraph G arev"
using assms by unfold_locales (auto simp: permutes_def)

context bidirected_digraph begin

lemma bidirected_digraph[intro!]: "bidirected_digraph G arev"
by unfold_locales

lemma arev_arev[simp]: "arev (arev a) = a"
using arev_dom by (cases "a ∈ arcs G") (auto simp: arev_arev_raw)

lemma arev_o_arev[simp]: "arev o arev = id"

lemma arev_eq: "a ∉ arcs G ⟹ arev a = a"

lemma arev_neq: "a ∈ arcs G ⟹ arev a ≠ a"

lemma arev_in_arcs[simp]: "a ∈ arcs G ⟹ arev a ∈ arcs G"
by (metis arev_arev arev_dom)

assumes "a ∈ arcs G" shows "head G (arev a) = tail G a"
proof -
from assms have "head G (arev a) = tail G (arev (arev a)) "
by (simp only: tail_arev arev_in_arcs)
then show ?thesis by simp
qed

lemma ate_arev[simp]:
assumes "a ∈ arcs G" shows "arc_to_ends G (arev a) = prod.swap (arc_to_ends G a)"
using assms by (auto simp: arc_to_ends_def)

lemma bij_arev: "bij arev"
using arev_arev by (metis bij_betw_imageI inj_on_inverseI surjI)

lemma arev_permutes_arcs: "arev permutes arcs G"
using arev_dom bij_arev by (auto simp: permutes_def bij_iff)

lemma arev_eq_iff: "⋀x y. arev x = arev y ⟷ x = y"
by (metis arev_arev)

lemma in_arcs_eq: "in_arcs G w = arev  out_arcs G w"
by auto (metis arev_arev arev_in_arcs image_eqI in_out_arcs_conv tail_arev)

lemma inj_on_arev[intro!]: "inj_on arev S"
by (metis arev_arev inj_on_inverseI)

lemma even_card_loops:
"even (card (in_arcs G w ∩ out_arcs G w))" (is "even (card ?S)")
proof -
{ assume "¬finite ?S"
then have ?thesis by simp
}
moreover
{ assume A:"finite ?S"
have "card ?S = card (⋃{{a,arev a} | a. a ∈ ?S})" (is "_ = card (⋃ ?T)")
by (rule arg_cong[where f=card]) (auto intro!: exI[where x="{x, arev x}" for x])
also have "…= sum card ?T"
proof (rule card_Union_disjoint)
show "⋀A. A∈{{a, arev a} |a. a ∈ ?S} ⟹ finite A" by auto
show "pairwise disjnt {{a, arev a} |a. a ∈ in_arcs G w ∩ out_arcs G w}"
unfolding pairwise_def disjnt_def
qed
also have "… = sum (λa. 2) ?T"
by (intro sum.cong) (auto simp: card_insert_if dest: arev_neq)
also have "… = 2 * card ?T" by simp
finally have ?thesis by simp
}
ultimately
show ?thesis by blast
qed

end

(*XXX*)
sublocale bidirected_digraph ⊆ sym_digraph
proof (unfold_locales, unfold symmetric_def, intro symI)
fix u v assume "u →⇘G⇙ v"
then obtain a where "a ∈ arcs G" "arc_to_ends G a = (u,v)" by (auto simp: arcs_ends_def)
then have "arev a ∈ arcs G" "arc_to_ends G (arev a) = (v,u)"
by (auto simp: arc_to_ends_def)
then show "v →⇘G⇙ u" by (auto simp: arcs_ends_def intro: rev_image_eqI)
qed

end


# Theory Arc_Walk

(* Title:  Arc_Walk.thy
Author: Lars Noschinski, TU München
*)

theory Arc_Walk
imports
Digraph
begin

section ‹Arc Walks›

text ‹
We represent a walk in a graph by the list of its arcs.
›

type_synonym 'b awalk = "'b list"

context pre_digraph begin

text ‹
The list of vertices of a walk. The additional vertex
argument is there to deal with the case of empty walks.
›
primrec awalk_verts :: "'a ⇒ 'b awalk ⇒ 'a list" where
"awalk_verts u [] = [u]"
| "awalk_verts u (e # es) = tail G e # awalk_verts (head G e) es"

abbreviation awhd :: "'a ⇒ 'b awalk ⇒ 'a" where
"awhd u p ≡ hd (awalk_verts u p)"

abbreviation awlast:: "'a ⇒ 'b awalk ⇒ 'a" where
"awlast u p ≡ last (awalk_verts u p)"

text ‹
Tests whether a list of arcs is a consistent arc sequence,
i.e. a list of arcs, where the head G node of each arc is
the tail G node of the following arc.
›
fun cas :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where
"cas u [] v = (u = v)" |
"cas u (e # es) v = (tail G e = u ∧ cas (head G e) es v)"

lemma cas_simp:
assumes "es ≠ []"
shows "cas u es v ⟷ tail G (hd es) = u ∧ cas (head G (hd es)) (tl es) v"
using assms by (cases es) auto

definition awalk :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where
"awalk u p v ≡ u ∈ verts G ∧ set p ⊆ arcs G ∧ cas u p v"

(* XXX: rename to atrail? *)
definition (in pre_digraph) trail :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where
"trail u p v ≡ awalk u p v ∧ distinct p"

definition apath :: "'a ⇒'b awalk ⇒ 'a ⇒ bool" where
"apath u p v ≡ awalk u p v ∧ distinct (awalk_verts u p)"

end

subsection ‹Basic Lemmas›

lemma (in pre_digraph) awalk_verts_conv:
"awalk_verts u p = (if p = [] then [u] else map (tail G) p @ [head G (last p)])"
by (induct p arbitrary: u) auto

lemma (in pre_digraph) awalk_verts_conv':
assumes "cas u p v"
shows "awalk_verts u p = (if p = [] then [u] else tail G (hd p) # map (head G) p)"
using assms by (induct u p v rule: cas.induct) (auto simp: cas_simp)

lemma (in pre_digraph) length_awalk_verts:
"length (awalk_verts u p) = Suc (length p)"

lemma (in pre_digraph) awalk_verts_ne_eq:
assumes "p ≠ []"
shows "awalk_verts u p = awalk_verts v p"
using assms by (auto simp: awalk_verts_conv)

lemma (in pre_digraph) awalk_verts_non_Nil[simp]:
"awalk_verts u p ≠ []"

context wf_digraph begin

lemma
assumes "cas u p v"
shows awhd_if_cas: "awhd u p = u" and awlast_if_cas: "awlast u p = v"
using assms by (induct p arbitrary: u) auto

lemma awalk_verts_in_verts:
assumes "u ∈ verts G" "set p ⊆ arcs G" "v ∈ set (awalk_verts u p)"
shows "v ∈ verts G"
using assms by (induct p arbitrary: u) (auto intro: wellformed)

lemma
assumes "u ∈ verts G" "set p ⊆ arcs G"
shows awhd_in_verts: "awhd u p ∈ verts G"
and awlast_in_verts: "awlast u p ∈ verts G"
using assms by (auto elim: awalk_verts_in_verts)

lemma awalk_conv:
"awalk u p v = (set (awalk_verts u p) ⊆ verts G
∧ set p ⊆ arcs G
∧ awhd u p = u ∧ awlast u p = v ∧ cas u p v)"
unfolding awalk_def using hd_in_set[OF awalk_verts_non_Nil, of u p]
by (auto intro: awalk_verts_in_verts awhd_if_cas awlast_if_cas simp del: hd_in_set)

lemma awalkI:
assumes "set (awalk_verts u p) ⊆ verts G" "set p ⊆ arcs G" "cas u p v"
shows "awalk u p v"
using assms by (auto simp: awalk_conv awhd_if_cas awlast_if_cas)

lemma awalkE[elim]:
assumes "awalk u p v"
obtains "set (awalk_verts u p) ⊆ verts G" "set p ⊆ arcs G" "cas u p v"
"awhd u p = u" "awlast u p = v"
using assms by (auto simp add: awalk_conv)

lemma awalk_Nil_iff:
"awalk u [] v ⟷ u = v ∧ u ∈ verts G"
unfolding awalk_def by auto

lemma trail_Nil_iff:
"trail u [] v ⟷ u = v ∧ u ∈ verts G"
by (auto simp: trail_def awalk_Nil_iff)

lemma apath_Nil_iff: "apath u [] v ⟷ u = v ∧ u ∈ verts G"
by (auto simp: apath_def awalk_Nil_iff)

lemma awalk_hd_in_verts: "awalk u p v ⟹ u ∈ verts G"
by (cases p) auto

lemma awalk_last_in_verts: "awalk u p v ⟹ v ∈ verts G"
unfolding awalk_conv by auto

lemma hd_in_awalk_verts:
"awalk u p v ⟹ u ∈ set (awalk_verts u p)"
"apath u p v ⟹ u ∈ set (awalk_verts u p)"
by (case_tac [!]p) (auto simp: apath_def)

lemma awalk_Cons_iff:
"awalk u (e # es) w ⟷ e ∈ arcs G ∧ u = tail G e ∧ awalk (head G e) es w"
by (auto simp: awalk_def)

lemma trail_Cons_iff:
"trail u (e # es ) w ⟷ e ∈ arcs G ∧ u = tail G e ∧ e ∉ set es ∧ trail (head G e) es w"
by (auto simp: trail_def awalk_Cons_iff)

lemma apath_Cons_iff:
"apath u (e # es) w ⟷ e ∈ arcs G ∧ tail G e = u ∧ apath (head G e) es w
∧ tail G e ∉ set (awalk_verts (head G e) es)" (is "?L ⟷ ?R")
by (auto simp: apath_def awalk_Cons_iff)

lemmas awalk_simps = awalk_Nil_iff awalk_Cons_iff
lemmas trail_simps = trail_Nil_iff trail_Cons_iff
lemmas apath_simps = apath_Nil_iff apath_Cons_iff

lemma arc_implies_awalk:
"e ∈ arcs G ⟹ awalk (tail G e) [e] (head G e)"

lemma apath_nonempty_ends:
assumes "apath u p v"
assumes "p ≠ []"
shows "u ≠ v"
using assms
proof (induct p arbitrary: u)
case (Cons e es)
then have "apath (head G e) es v" "u ∉ set (awalk_verts (head G e) es)"
by (auto simp: apath_Cons_iff)
moreover then have "v ∈ set (awalk_verts (head G e) es)" by (auto simp: apath_def)
ultimately show "u ≠ v" by auto
qed simp

(* replace by awalk_Cons_iff?*)
lemma awalk_ConsI:
assumes "awalk v es w"
assumes "e ∈ arcs G" and "arc_to_ends G e = (u,v)"
shows "awalk u (e # es) w"
using assms by (cases es) (auto simp: awalk_def arc_to_ends_def)

lemma (in pre_digraph) awalkI_apath:
assumes "apath u p v" shows "awalk u p v"
using assms by (simp add: apath_def)

lemma arcE:
assumes "arc e (u,v)"
assumes "⟦e ∈ arcs G; tail G e = u; head G e = v⟧ ⟹ P"
shows "P"
using assms by (auto simp: arc_def)

lemma in_arcs_imp_in_arcs_ends:
assumes "e ∈ arcs G"
shows "(tail G e, head G e) ∈ arcs_ends G"
using assms by (auto simp: arcs_ends_conv)

lemma set_awalk_verts_cas:
assumes "cas u p v"
shows "set (awalk_verts u p) = {u} ∪ set (map (tail G) p) ∪ set (map (head G) p)"
using assms
proof (induct p arbitrary: u)
case Nil then show ?case by simp
next
case (Cons e es)
then have "set (awalk_verts (head G e) es)
= {head G e} ∪ set (map (tail G) es) ∪ set (map (head G) es)"
by (auto simp: awalk_Cons_iff)
with Cons.prems show ?case by auto
qed

lemma set_awalk_verts_not_Nil_cas:
assumes "cas u p v" "p ≠ []"
shows "set (awalk_verts u p) = set (map (tail G) p) ∪ set (map (head G) p)"
proof -
have "u ∈ set (map (tail G) p)" using assms by (cases p) auto
with assms show ?thesis  by (auto simp: set_awalk_verts_cas)
qed

lemma set_awalk_verts:
assumes "awalk u p v"
shows "set (awalk_verts u p) = {u} ∪ set (map (tail G) p) ∪ set (map (head G) p)"
using assms by (intro set_awalk_verts_cas) blast

lemma set_awalk_verts_not_Nil:
assumes "awalk u p v" "p ≠ []"
shows "set (awalk_verts u p) = set (map (tail G) p) ∪ set (map (head G) p)"
using assms by (intro set_awalk_verts_not_Nil_cas) blast

lemma
awhd_of_awalk: "awalk u p v ⟹ awhd u p = u" and
awlast_of_awalk: "awalk u p v ⟹ NOMATCH (awlast u p) v ⟹ awlast u p = v"
unfolding NOMATCH_def by auto
lemmas awends_of_awalk[simp] = awhd_of_awalk awlast_of_awalk

lemma awalk_verts_arc1:
assumes "e ∈ set p"
shows "tail G e ∈ set (awalk_verts u p)"
using assms by (auto simp: awalk_verts_conv)

lemma awalk_verts_arc2:
assumes "awalk u p v" "e ∈ set p"
shows "head G e ∈ set (awalk_verts u p)"
using assms by (simp add: set_awalk_verts)

lemma awalk_induct_raw[case_names Base Cons(*, induct pred: awalk*)]:
assumes "awalk u p v"
assumes "⋀w1. w1 ∈ verts G ⟹ P w1 [] w1"
assumes "⋀w1 w2 e es. e ∈ arcs G ⟹ arc_to_ends G e = (w1, w2)
⟹ P w2 es v ⟹ P w1 (e # es) v"
shows "P u p v"
using assms
proof (induct p arbitrary: u v)
case Nil then show ?case using Nil.prems by auto
next
case (Cons e es)
from Cons.prems(1) show ?case
by (intro Cons) (auto intro: Cons(2-) simp: arc_to_ends_def awalk_Cons_iff)
qed

subsection ‹Appending awalks›

lemma (in pre_digraph) cas_append_iff[simp]:
"cas u (p @ q) v ⟷ cas u p (awlast u p) ∧ cas (awlast u p) q v"
by (induct u p v rule: cas.induct) auto

lemma cas_ends:
assumes "cas u p v" "cas u' p v'"
shows "(p ≠ [] ∧ u = u' ∧ v = v') ∨ (p = [] ∧ u = v ∧ u' = v')"
using assms by (induct u p v arbitrary: u u' rule: cas.induct) auto

lemma awalk_ends:
assumes "awalk u p v" "awalk u' p v'"
shows "(p ≠ [] ∧ u = u' ∧ v = v') ∨ (p = [] ∧ u = v ∧ u' = v')"
using assms by (simp add: awalk_def cas_ends)

lemma awalk_ends_eqD:
assumes "awalk u p u" "awalk v p w"
shows "v = w"
using awalk_ends[OF assms(1,2)] by auto

lemma awalk_empty_ends:
assumes "awalk u [] v"
shows "u = v"
using assms by (auto simp: awalk_def)

lemma apath_ends:
assumes "apath u p v" and "apath u' p v'"
shows "(p ≠ [] ∧ u ≠ v ∧ u = u' ∧ v = v') ∨ (p = [] ∧ u = v ∧ u' = v')"
using assms unfolding apath_def by (metis assms(2) apath_nonempty_ends  awalk_ends)

lemma awalk_append_iff[simp]:
"awalk u (p @ q) v ⟷ awalk u p (awlast u p) ∧ awalk (awlast u p) q v" (is "?L ⟷ ?R")
by (auto simp: awalk_def intro: awlast_in_verts)

lemma awlast_append:
"awlast u (p @ q) = awlast (awlast u p) q"

lemma awhd_append:
"awhd u (p @ q) = awhd (awhd u q) p"

declare awalkE[rule del]

lemma awalkE'[elim]:
assumes "awalk u p v"
obtains "set (awalk_verts u p) ⊆ verts G" "set p ⊆ arcs G" "cas u p v"
"awhd u p = u" "awlast u p = v" "u ∈ verts G" "v ∈ verts G"
proof -
have "u ∈ set (awalk_verts u p)" "v ∈ set (awalk_verts u p)"
using assms by (auto simp: hd_in_awalk_verts elim: awalkE)
then show ?thesis using assms by (auto elim: awalkE intro: that)
qed

lemma awalk_appendI:
assumes "awalk u p v"
assumes "awalk v q w"
shows "awalk u (p @ q) w"
using assms
proof (induct p arbitrary: u)
case Nil then show ?case by auto
next
case (Cons e es)
from Cons.prems have ee_e: "arc_to_ends G e = (u, head G e)"
unfolding arc_to_ends_def by auto

have "awalk (head G e) es v"
using ee_e Cons(2) awalk_Cons_iff by auto
then show ?case using Cons ee_e by (auto simp: awalk_Cons_iff)
qed

lemma awalk_verts_append_cas:
assumes "cas u (p @ q) v"
shows "awalk_verts u (p @ q) = awalk_verts u p @ tl (awalk_verts (awlast u p) q)"
using assms
proof (induct p arbitrary: u)
case Nil then show ?case by (cases q) auto
qed (auto simp: awalk_Cons_iff)

lemma awalk_verts_append:
assumes "awalk u (p @ q) v"
shows "awalk_verts u (p @ q) = awalk_verts u p @ tl (awalk_verts (awlast u p) q)"
using assms by (intro awalk_verts_append_cas) blast

lemma awalk_verts_append2:
assumes "awalk u (p @ q) v"
shows "awalk_verts u (p @ q) = butlast (awalk_verts u p) @ awalk_verts (awlast u p) q"
using assms by (auto simp: awalk_verts_conv)

lemma apath_append_iff:
"apath u (p @ q) v ⟷ apath u p (awlast u p) ∧ apath (awlast u p) q v ∧
set (awalk_verts u p) ∩ set (tl (awalk_verts (awlast u p) q)) = {}" (is "?L ⟷ ?R")
proof
assume ?L
then have "distinct (awalk_verts (awlast u p) q)" by (auto simp: apath_def awalk_verts_append2)
with ‹?L› show ?R by (auto simp: apath_def awalk_verts_append)
next
assume ?R
then show ?L by (auto simp: apath_def awalk_verts_append dest: distinct_tl)
qed

lemma (in wf_digraph) set_awalk_verts_append_cas:
assumes "cas u p v" "cas v q w"
shows "set (awalk_verts u (p @ q)) = set (awalk_verts u p) ∪ set (awalk_verts v q)"
proof -
from assms have cas_pq: "cas u (p @ q) w"
moreover
from assms have "v ∈ set (awalk_verts u p)"
by (metis awalk_verts_non_Nil awlast_if_cas last_in_set)
ultimately show ?thesis using assms
by (auto simp: set_awalk_verts_cas)
qed

lemma (in wf_digraph) set_awalk_verts_append:
assumes "awalk u p v" "awalk v q w"
shows "set (awalk_verts u (p @ q)) = set (awalk_verts u p) ∪ set (awalk_verts v q)"
proof -
from assms have "awalk u (p @ q) w" by auto
moreover
with assms have "v ∈ set (awalk_verts u (p @ q))"
by (auto simp: awalk_verts_append)
ultimately show ?thesis using assms
by (auto simp: set_awalk_verts)
qed

lemma cas_takeI:
assumes "cas u p v" "awlast u (take n p) = v'"
shows "cas u (take n p) v'"
proof -
from assms have "cas u (take n p @ drop n p) v" by simp
with assms show ?thesis unfolding cas_append_iff by simp
qed

lemma cas_dropI:
assumes "cas u p v" "awlast u (take n p) = u'"
shows "cas u' (drop n p) v"
proof -
from assms have "cas u (take n p @ drop n p) v" by simp
with assms show ?thesis unfolding cas_append_iff by simp
qed

lemma awalk_verts_take_conv:
assumes "cas u p v"
shows "awalk_verts u (take n p) = take (Suc n) (awalk_verts u p)"
proof -
from assms have "cas u (take n p) (awlast u (take n p))" by (auto intro: cas_takeI)
with assms show ?thesis
by (cases n p rule: nat.exhaust[case_product list.exhaust])
(auto simp: awalk_verts_conv' take_map simp del: awalk_verts.simps)
qed

lemma awalk_verts_drop_conv:
assumes "cas u p v"
shows "awalk_verts u' (drop n p) = (if n < length p then drop n (awalk_verts u p) else [u'])"
using assms by (auto simp: awalk_verts_conv drop_map)

lemma awalk_decomp_verts:
assumes cas: "cas u p v" and ev_decomp: "awalk_verts u p = xs @ y # ys"
obtains q r where "cas u q y" "cas y r v" "p = q @ r" "awalk_verts u q = xs @ [y]" "awalk_verts y r = y # ys"
using assms
proof -
define q r where "q = take (length xs) p" and "r = drop (length xs) p"
then have p: "p = q @ r" by simp
moreover from p have "cas u q (awlast u q)" "cas (awlast u q) r v"
using ‹cas u p v› by auto
moreover have "awlast u q = y"
using q_def and assms by (auto simp: awalk_verts_take_conv)
moreover have *: "awalk_verts u q = xs @ [awlast u q]"
using assms q_def by (auto simp: awalk_verts_take_conv)
moreover from * have "awalk_verts y r = y # ys"
unfolding q_def r_def using assms by (auto simp: awalk_verts_drop_conv not_less)
ultimately show ?thesis by (intro that) auto
qed

lemma awalk_decomp:
assumes "awalk u p v"
assumes "w ∈ set (awalk_verts u p)"
shows "∃q r. p = q @ r ∧ awalk u q w ∧ awalk w r v"
proof -
from assms have "cas u p v" by auto
moreover from assms obtain xs ys where
"awalk_verts u p = xs @ w # ys" by (auto simp: in_set_conv_decomp)
ultimately
obtain q r where "cas u q w" "cas w r v" "p = q @ r" "awalk_verts u q = xs @ [w]"
by (auto intro: awalk_decomp_verts)
with assms show ?thesis by auto
qed

lemma awalk_not_distinct_decomp:
assumes "awalk u p v"
assumes "¬ distinct (awalk_verts u p)"
shows "∃q r s. p = q @ r @ s ∧ distinct (awalk_verts u q)
∧ 0 < length r
∧ (∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v)"
proof -
from assms
obtain xs ys zs y where
pv_decomp: "awalk_verts u p = xs @ y # ys @ y # zs"
and xs_y_props: "distinct xs" "y ∉ set xs" "y ∉ set ys"
using not_distinct_decomp_min_prefix by blast

obtain q p' where "cas u q y" "p = q @ p'" "awalk_verts u q = xs @ [y]"
and p'_props: "cas y p' v"  "awalk_verts y p' = (y # ys) @ y # zs"
using assms pv_decomp by - (rule awalk_decomp_verts, auto)
obtain r s where "cas y r y" "cas y s v" "p' = r @ s"
"awalk_verts y r = y # ys @ [y]" "awalk_verts y s = y # zs"
using p'_props by (rule awalk_decomp_verts) auto

have "p = q @ r @ s" using ‹p = q @ p'› ‹p' = r @ s› by simp
moreover
have "distinct (awalk_verts u q)" using ‹awalk_verts u q = xs @ [y]› and xs_y_props  by simp
moreover
have "0 < length r" using ‹awalk_verts y r = y # ys @ [y]› by auto
moreover
from pv_decomp assms have "y ∈ verts G" by auto
then have "awalk u q y" "awalk y r y" "awalk y s v"
using ‹awalk u p v› ‹cas u q y› ‹cas y r y› ‹cas y s v› unfolding ‹p = q @ r @ s›
by (auto simp: awalk_def)
ultimately show ?thesis by blast
qed

lemma apath_decomp_disjoint:
assumes "apath u p v"
assumes "p = q @ r"
assumes "x ∈ set (awalk_verts u q)" "x ∈ set (tl (awalk_verts (awlast u q) r))"
shows False
using assms by (auto simp: apath_def awalk_verts_append)

subsection ‹Cycles›

definition closed_w :: "'b awalk ⇒ bool" where
"closed_w p ≡ ∃u. awalk u p u ∧ 0 < length p"

text ‹
The definitions of cycles in textbooks vary w.r.t to the minimial length
of a cycle.

The definition given here matches \cite{diestel2010graph}.
\cite{bangjensen2009digraphs} excludes loops from being cycles.
Volkmann (Lutz Volkmann: Graphen an allen Ecken und Kanten, 2006 (?))
places no restriction on the length in the definition, but later
usage assumes cycles to be non-empty.
›
definition (in pre_digraph) cycle :: "'b awalk ⇒ bool" where
"cycle p ≡ ∃u. awalk u p u ∧ distinct (tl (awalk_verts u p)) ∧ p ≠ []"

lemma cycle_altdef:
"cycle p ⟷ closed_w p ∧ (∃u. distinct (tl (awalk_verts u p)))"
by (cases p) (auto simp: closed_w_def cycle_def)

lemma (in wf_digraph) distinct_tl_verts_imp_distinct:
assumes "awalk u p v"
assumes "distinct (tl (awalk_verts u p))"
shows "distinct p"
proof (rule ccontr)
assume "¬distinct p"
then obtain e xs ys zs where p_decomp: "p = xs @ e # ys @ e # zs"
by (blast dest: not_distinct_decomp_min_prefix)
then show False
using assms p_decomp by (auto simp: awalk_verts_append awalk_Cons_iff set_awalk_verts)
qed

lemma (in wf_digraph) distinct_verts_imp_distinct:
assumes "awalk u p v"
assumes "distinct (awalk_verts u p)"
shows "distinct p"
using assms by (blast intro: distinct_tl_verts_imp_distinct distinct_tl)

lemma (in wf_digraph) cycle_conv:
"cycle p ⟷ (∃u. awalk u p u ∧ distinct (tl (awalk_verts u p)) ∧ distinct p ∧ p ≠ [])"
unfolding cycle_def by (auto intro: distinct_tl_verts_imp_distinct)

lemma (in loopfree_digraph) cycle_digraph_conv:
"cycle p ⟷ (∃u. awalk u p u ∧ distinct (tl (awalk_verts u p)) ∧ 2 ≤ length p)" (is "?L ⟷ ?R")
proof
assume "cycle p"
then obtain u where *: "awalk u p u" "distinct (tl (awalk_verts u p))" "p ≠ []"
unfolding cycle_def by auto
have "2 ≤ length p"
proof (rule ccontr)
assume "¬?thesis" with * obtain e where "p=[e]"
by (cases p) (auto simp: not_le)
then show False using * by (auto simp: awalk_simps dest: no_loops)
qed
then show ?R using * by auto
qed (auto simp: cycle_def)

lemma (in wf_digraph) closed_w_imp_cycle:
assumes "closed_w p" shows "∃p. cycle p"
using assms
proof (induct "length p" arbitrary: p rule: less_induct)
case less
then obtain u where *: "awalk u p u" "p ≠ []" by (auto simp: closed_w_def)
show ?thesis
proof cases
assume "distinct (tl (awalk_verts u p))"
with less show ?thesis by (auto simp: closed_w_def cycle_altdef)
next
assume A: "¬distinct (tl (awalk_verts u p))"
then obtain e es where "p = e # es" by (cases p) auto
with A * have **: "awalk (head G e) es u" "¬distinct (awalk_verts (head G e) es)"
by (auto simp: awalk_Cons_iff)
obtain q r s where "es = q @ r @ s" "∃w. awalk w r w" "closed_w r"
using awalk_not_distinct_decomp[OF **] by (auto simp: closed_w_def)
then have "length r < length p" using ‹p = _› by auto
then show ?thesis using ‹closed_w r› by (rule less)
qed
qed

subsection ‹Reachability›

lemma reachable1_awalk:
"u →⇧+ v ⟷ (∃p. awalk u p v ∧ p ≠ [])"
proof
assume "u →⇧+ v" then show "∃p. awalk u p v ∧ p ≠ []"
proof (induct rule: converse_trancl_induct)
case (base y) then obtain e where "e ∈ arcs G" "tail G e = y" "head G e = v" by auto
with arc_implies_awalk show ?case by auto
next
case (step x y)
then obtain p where "awalk y p v" "p ≠ []" by auto
moreover
from ‹x → y› obtain e where "tail G e = x" "head G e = y" "e ∈ arcs G"
by auto
ultimately
have "awalk x (e # p) v"
by (auto simp: awalk_Cons_iff)
then show ?case by auto
qed
next
assume "∃p. awalk u p v ∧ p ≠ []" then obtain p where "awalk u p v" "p ≠ []" by auto
thus "u →⇧+ v"
proof (induct p arbitrary: u)
case (Cons a as) then show ?case
by (cases "as = []") (auto simp: awalk_simps trancl_into_trancl2 dest: in_arcs_imp_in_arcs_ends)
qed simp
qed

lemma reachable_awalk:
"u →⇧* v ⟷ (∃p. awalk u p v)"
proof cases
assume "u = v"
have "u →⇧*u ⟷ awalk u [] u" by (auto simp: awalk_Nil_iff reachable_in_verts)
also have "… ⟷ (∃p. awalk u p u)"
by (metis awalk_Nil_iff awalk_hd_in_verts)
finally show ?thesis using ‹u = v› by simp
next
assume "u ≠ v"
then have "u →⇧* v ⟷ u →⇧+ v" by auto
also have "… ⟷ (∃p. awalk u p v)"
using ‹u ≠ v› unfolding reachable1_awalk by force
finally show ?thesis .
qed

lemma reachable_awalkI[intro?]:
assumes "awalk u p v"
shows "u →⇧* v"
unfolding reachable_awalk using assms by auto

lemma reachable1_awalkI:
"awalk v p w ⟹ p ≠ [] ⟹ v →⇧+ w"

lemma reachable_arc_trans:
assumes "u →⇧* v" "arc e (v,w)"
shows "u →⇧* w"
proof -
from ‹u →⇧* v› obtain p where "awalk u p v"
by (auto simp: reachable_awalk)
moreover have "awalk v [e] w"
using ‹arc e (v,w)›
by (auto simp: arc_def awalk_def)
ultimately have "awalk u (p @ [e]) w"
by (rule awalk_appendI)
then show ?thesis ..
qed

lemma awalk_verts_reachable_from:
assumes "awalk u p v" "w ∈ set (awalk_verts u p)" shows "u →⇧*⇘G⇙ w"
proof  -
obtain s where "awalk u s w" using awalk_decomp[OF assms] by blast
then show ?thesis by (metis reachable_awalk)
qed

lemma awalk_verts_reachable_to:
assumes "awalk u p v" "w ∈ set (awalk_verts u p)" shows "w →⇧*⇘G⇙ v"
proof  -
obtain s where "awalk w s v" using awalk_decomp[OF assms] by blast
then show ?thesis by (metis reachable_awalk)
qed

subsection ‹Paths›

lemma (in fin_digraph) length_apath_less:
assumes "apath u p v"
shows "length p < card (verts G)"
proof -
have "length p < length (awalk_verts u p)" unfolding awalk_verts_conv
by (auto simp: awalk_verts_conv)
also have "length (awalk_verts u p) = card (set (awalk_verts u p))"
using ‹apath u p v› by (auto simp: apath_def distinct_card)
also have "… ≤ card (verts G)"
using ‹apath u p v› unfolding apath_def awalk_conv
by (auto intro: card_mono)
finally show ?thesis .
qed

lemma (in fin_digraph) length_apath:
assumes "apath u p v"
shows "length p ≤ card (verts G)"
using length_apath_less[OF assms] by auto

lemma (in fin_digraph) apaths_finite_triple:
shows "finite {(u,p,v). apath u p v}"
proof -
have "⋀u p v. awalk u p v ⟹ distinct (awalk_verts u p) ⟹length p ≤ card (verts G)"
by (rule length_apath) (auto simp: apath_def)
then have "{(u,p,v). apath u p v} ⊆ verts G × {es. set es ⊆ arcs G ∧ length es ≤ card (verts G)} × verts G"
by (auto simp: apath_def)
moreover have "finite ..."
using finite_verts finite_arcs
by (intro finite_cartesian_product finite_lists_length_le)
ultimately show ?thesis by (rule finite_subset)
qed

lemma (in fin_digraph) apaths_finite:
shows "finite {p. apath u p v}"
proof -
have "{p. apath u p v} ⊆ (fst o snd)  {(u,p,v). apath u p v}"
by force
with apaths_finite_triple show ?thesis  by (rule finite_surj)
qed

fun is_awalk_cyc_decomp :: "'b awalk =>
('b awalk × 'b awalk × 'b awalk) ⇒ bool" where
"is_awalk_cyc_decomp p (q,r,s) ⟷ p = q @ r @ s
∧ (∃u v w. awalk u q v ∧ awalk v r v ∧ awalk v s w)
∧ 0 <length r
∧ (∃u. distinct (awalk_verts u q))"

definition awalk_cyc_decomp :: "'b awalk
⇒ 'b awalk × 'b awalk × 'b awalk" where
"awalk_cyc_decomp p = (SOME qrs. is_awalk_cyc_decomp p qrs)"

function awalk_to_apath :: "'b awalk ⇒ 'b awalk" where
"awalk_to_apath p = (if ¬(∃u. distinct (awalk_verts u p)) ∧ (∃u v. awalk u p v)
then (let (q,r,s) = awalk_cyc_decomp p in awalk_to_apath (q @ s))
else p)"
by auto

lemma awalk_cyc_decomp_has_prop:
assumes "awalk u p v" and "¬distinct (awalk_verts u p)"
shows "is_awalk_cyc_decomp p (awalk_cyc_decomp p)"
proof -
obtain q r s where *: "p = q @ r @ s ∧ distinct (awalk_verts u q)
∧ 0 < length r
∧ (∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v)"
by (atomize_elim) (rule awalk_not_distinct_decomp[OF assms])
then have "∃x. is_awalk_cyc_decomp p x"
by (intro exI[where x="(q,r,s)"]) auto
then show ?thesis unfolding awalk_cyc_decomp_def ..
qed

lemma awalk_cyc_decompE:
assumes dec: "awalk_cyc_decomp p = (q,r,s)"
assumes p_props: "awalk u p v" "¬distinct (awalk_verts u p)"
obtains "p = q @ r @ s" "distinct (awalk_verts u q)" "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" "closed_w r"
proof
show "p = q @ r @ s" "distinct (awalk_verts u q)" "closed_w r"
using awalk_cyc_decomp_has_prop[OF p_props] and dec
by (auto simp: closed_w_def awalk_verts_conv)
then have "p ≠ []" by (auto simp: closed_w_def)

(* TODO: Can we find some general rules to prove the last property?*)
obtain u' w' v' where obt_awalk: "awalk u' q w'" "awalk w' r w'" "awalk w' s v'"
using awalk_cyc_decomp_has_prop[OF p_props] and dec by auto
then have "awalk u' p v'"
using ‹p = q @ r @ s› by simp
then have "u = u'" and "v = v'" using ‹p ≠ []› ‹awalk u p v› by (metis awalk_ends)+
then have "awalk u q w'" "awalk w' r w'" "awalk w' s v"
using obt_awalk by auto
then show "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" by auto
qed

lemma awalk_cyc_decompE':
assumes p_props: "awalk u p v" "¬distinct (awalk_verts u p)"
obtains q r s where "p = q @ r @ s" "distinct (awalk_verts u q)" "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" "closed_w r"
proof -
obtain q r s where "awalk_cyc_decomp p = (q,r,s)"
by (cases "awalk_cyc_decomp p") auto
then have "p = q @ r @ s" "distinct (awalk_verts u q)" "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" "closed_w r"
using assms by (auto elim: awalk_cyc_decompE)
then show ?thesis ..
qed

termination awalk_to_apath
proof (relation "measure length")
fix G p qrs rs q r s

have X: "⋀x y. closed_w r ⟹ awalk x r y ⟹ x = y"
unfolding closed_w_def by (blast dest: awalk_ends)

assume "¬(∃u. distinct (awalk_verts u p)) ∧(∃u v. awalk u p v)"
and **:"qrs = awalk_cyc_decomp p" "(q, rs) = qrs" "(r, s) = rs"
then obtain u v where *: "awalk u p v" "¬distinct (awalk_verts u p)"
by (cases p) auto
then have "awalk_cyc_decomp p = (q,r,s)" using ** by simp
then have "is_awalk_cyc_decomp p (q,r,s)"
apply (rule awalk_cyc_decompE[OF _ *])
using X[of "awlast u q"  "awlast (awlast u q) r"] *(1)
by (auto simp: closed_w_def)
then show "(q @ s, p) ∈ measure length"
by (auto simp: closed_w_def)
qed simp
declare awalk_to_apath.simps[simp del]

lemma awalk_to_apath_induct[consumes 1, case_names path decomp]:
assumes awalk: "awalk u p v"
assumes dist: "⋀p. awalk u p v ⟹ distinct (awalk_verts u p) ⟹ P p"
assumes dec: "⋀p q r s. ⟦awalk u p v; awalk_cyc_decomp p = (q,r,s);
¬distinct (awalk_verts u p); P (q @ s)⟧ ⟹ P p"
shows "P p"
using awalk
proof (induct "length p" arbitrary: p rule: less_induct)
case less
show ?case
proof (cases "distinct (awalk_verts u p)")
case True then show ?thesis by (auto intro: dist less.prems)
next
case False
obtain q r s where p_cdecomp: "awalk_cyc_decomp p = (q,r,s)"
by (cases "awalk_cyc_decomp p") auto
then have "is_awalk_cyc_decomp p (q,r,s)" "p = q @ r @ s"
using awalk_cyc_decomp_has_prop[OF less.prems(1) False] by auto
then have "length (q @ s) < length p" "awalk u (q @ s) v"
using less.prems by (auto dest!: awalk_ends_eqD)
then have "P (q @ s)" by (auto intro: less)

with p_cdecomp False show ?thesis by (auto intro: dec less.prems)
qed
qed

lemma step_awalk_to_apath:
assumes awalk: "awalk u p v"
and decomp: "awalk_cyc_decomp p = (q, r, s)"
and dist: "¬ distinct (awalk_verts u p)"
shows "awalk_to_apath p = awalk_to_apath (q @ s)"
proof -
from dist have "¬(∃u. distinct (awalk_verts u p))"
by (auto simp: awalk_verts_conv)
with awalk and decomp show "awalk_to_apath p = awalk_to_apath (q @ s)"
by (auto simp: awalk_to_apath.simps)
qed

lemma apath_awalk_to_apath:
assumes "awalk u p v"
shows "apath u (awalk_to_apath p) v"
using assms
proof (induct rule: awalk_to_apath_induct)
case (path p)
then have "awalk_to_apath p = p"
by (auto simp: awalk_to_apath.simps)
then show ?case using path by (auto simp: apath_def)
next
case (decomp p q r s)
then show ?case using step_awalk_to_apath[of _ p _ q r s] by simp
qed

lemma (in wf_digraph) awalk_to_apath_subset:
assumes "awalk u p v"
shows "set (awalk_to_apath p) ⊆ set p"
using assms
proof (induct rule: awalk_to_apath_induct)
case (path p)
then have "awalk_to_apath p = p"
by (auto simp: awalk_to_apath.simps)
then show ?case by simp
next
case (decomp p q r s)
have *: "¬(∃u. distinct (awalk_verts u p)) ∧ (∃u v. awalk u p v)"
using decomp by (cases p) auto
have "set (awalk_to_apath (q @ s)) ⊆ set p"
using decomp by (auto elim!: awalk_cyc_decompE)
then
show ?case by (subst awalk_to_apath.simps) (simp only: * simp_thms if_True decomp Let_def prod.simps)
qed

lemma reachable_apath:
"u →⇧* v ⟷ (∃p. apath u p v)"
by (auto intro: awalkI_apath apath_awalk_to_apath simp: reachable_awalk)

lemma no_loops_in_apath:
assumes "apath u p v" "a ∈ set p" shows "tail G a ≠ head G a"
proof -
from ‹a ∈ set p› obtain p1 p2 where "p = p1 @ a # p2" by (auto simp: in_set_conv_decomp)
with ‹apath u p v› have "apath (tail G a) ([a] @ p2) (v)"
by (auto simp: apath_append_iff apath_Cons_iff apath_Nil_iff)
then have "apath (tail G a) [a] (head G a)" by - (drule apath_append_iff[THEN iffD1], simp)
then show ?thesis by (auto simp:  apath_Cons_iff)
qed

end

end


# Theory Pair_Digraph

(* Title:  Pair_Digraph.thy
Author: Lars Noschinski, TU München
*)

theory Pair_Digraph
imports
Digraph
Bidirected_Digraph
Arc_Walk
begin

section ‹Digraphs without Parallel Arcs›

text ‹
If no parallel arcs are desired, arcs can be accurately described as pairs of
This is the natural representation for Digraphs without multi-arcs.
and @{term "head G"}, making it easier to deal with multiple related graphs
and to modify a graph by adding edges.

This theory introduces such a specialisation of digraphs.
›

record 'a pair_pre_digraph = pverts :: "'a set" parcs :: "'a rel"

definition with_proj :: "'a pair_pre_digraph ⇒ ('a, 'a × 'a) pre_digraph" where
"with_proj G = ⦇ verts = pverts G, arcs = parcs G, tail = fst, head = snd ⦈"

declare [[coercion with_proj]]

primrec pawalk_verts :: "'a ⇒ ('a × 'a) awalk ⇒ 'a list" where
"pawalk_verts u [] = [u]" |
"pawalk_verts u (e # es) = fst e # pawalk_verts (snd e) es"

fun pcas :: "'a ⇒ ('a × 'a) awalk ⇒ 'a ⇒ bool" where
"pcas u [] v = (u = v)" |
"pcas u (e # es) v = (fst e = u ∧ pcas (snd e) es v)"

lemma with_proj_simps[simp]:
"verts (with_proj G) = pverts G"
"arcs (with_proj G) = parcs G"
"arcs_ends (with_proj G) = parcs G"
"tail (with_proj G) = fst"
by (auto simp: with_proj_def arcs_ends_conv)

lemma cas_with_proj_eq: "pre_digraph.cas (with_proj G) = pcas"
proof (unfold fun_eq_iff, intro allI)
fix u es v show "pre_digraph.cas (with_proj G) u es v = pcas u es v"
by (induct es arbitrary: u) (auto simp:  pre_digraph.cas.simps)
qed

lemma awalk_verts_with_proj_eq: "pre_digraph.awalk_verts (with_proj G) = pawalk_verts"
proof (unfold fun_eq_iff, intro allI)
fix u es show "pre_digraph.awalk_verts (with_proj G) u es = pawalk_verts u es"
by (induct es arbitrary: u) (auto simp: pre_digraph.awalk_verts.simps)
qed

locale pair_pre_digraph = fixes G :: "'a pair_pre_digraph"
begin

lemmas [simp] = cas_with_proj_eq awalk_verts_with_proj_eq

end

locale pair_wf_digraph = pair_pre_digraph +
assumes arc_fst_in_verts: "⋀e. e ∈ parcs G ⟹ fst e ∈ pverts G"
assumes arc_snd_in_verts: "⋀e. e ∈ parcs G ⟹ snd e ∈ pverts G"
begin

lemma in_arcsD1: "(u,v) ∈ parcs G ⟹ u ∈ pverts G"
and in_arcsD2: "(u,v) ∈ parcs G ⟹ v ∈ pverts G"
by (auto dest: arc_fst_in_verts arc_snd_in_verts)

lemmas wellformed' = in_arcsD1 in_arcsD2

end

locale pair_fin_digraph = pair_wf_digraph +
assumes pair_finite_verts: "finite (pverts G)"
and pair_finite_arcs: "finite (parcs G)"

locale pair_sym_digraph = pair_wf_digraph +
assumes pair_sym_arcs: "symmetric G"

locale pair_loopfree_digraph = pair_wf_digraph  +
assumes pair_no_loops: "e ∈ parcs G ⟹ fst e ≠ snd e"

locale pair_bidirected_digraph = pair_sym_digraph + pair_loopfree_digraph

locale pair_pseudo_graph = pair_fin_digraph + pair_sym_digraph

locale pair_digraph = pair_fin_digraph  + pair_loopfree_digraph

locale pair_graph = pair_digraph + pair_pseudo_graph

sublocale pair_pre_digraph ⊆ pre_digraph "with_proj G"
rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
and "arcs_ends G = parcs G"
and "pre_digraph.awalk_verts G = pawalk_verts"
and "pre_digraph.cas G = pcas"
by unfold_locales auto

sublocale pair_wf_digraph ⊆ wf_digraph "with_proj G"
rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
and "arcs_ends G = parcs G"
and "pre_digraph.awalk_verts G = pawalk_verts"
and "pre_digraph.cas G = pcas"
by unfold_locales (auto simp: arc_fst_in_verts arc_snd_in_verts)

sublocale pair_fin_digraph ⊆ fin_digraph "with_proj G"
rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
and "arcs_ends G = parcs G"
and "pre_digraph.awalk_verts G = pawalk_verts"
and "pre_digraph.cas G = pcas"
using pair_finite_verts pair_finite_arcs by unfold_locales auto

sublocale pair_sym_digraph ⊆ sym_digraph "with_proj G"
rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
and "arcs_ends G = parcs G"
and "pre_digraph.awalk_verts G = pawalk_verts"
and "pre_digraph.cas G = pcas"
using pair_sym_arcs by unfold_locales auto

sublocale pair_pseudo_graph ⊆ pseudo_graph "with_proj G"
rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
and "arcs_ends G = parcs G"
and "pre_digraph.awalk_verts G = pawalk_verts"
and "pre_digraph.cas G = pcas"
by unfold_locales auto

sublocale pair_loopfree_digraph ⊆ loopfree_digraph "with_proj G"
rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
and "arcs_ends G = parcs G"
and "pre_digraph.awalk_verts G = pawalk_verts"
and "pre_digraph.cas G = pcas"
using pair_no_loops by unfold_locales auto

sublocale pair_digraph ⊆ digraph "with_proj G"
rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
and "arcs_ends G = parcs G"
and "pre_digraph.awalk_verts G = pawalk_verts"
and "pre_digraph.cas G = pcas"
by unfold_locales (auto simp: arc_to_ends_def)

sublocale pair_graph ⊆ graph "with_proj G"
rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
and "arcs_ends G = parcs G"
and "pre_digraph.awalk_verts G = pawalk_verts"
and "pre_digraph.cas G = pcas"
by unfold_locales auto

sublocale pair_graph ⊆ pair_bidirected_digraph by unfold_locales

lemma wf_digraph_wp_iff: "wf_digraph (with_proj G) = pair_wf_digraph G" (is "?L ⟷ ?R")
proof
assume ?L then interpret wf_digraph "with_proj G" .
show ?R using wellformed by unfold_locales auto
next
assume ?R then interpret pair_wf_digraph G .
show ?L by unfold_locales
qed

lemma (in pair_fin_digraph) pair_fin_digraph[intro!]: "pair_fin_digraph G" ..

context pair_digraph begin

lemma pair_wf_digraph[intro!]: "pair_wf_digraph G" by intro_locales

lemma pair_digraph[intro!]: "pair_digraph G" ..

lemma (in pair_loopfree_digraph) no_loops':
"(u,v) ∈ parcs G ⟹ u ≠ v"
by (auto dest: no_loops)

end

lemma (in pair_wf_digraph) apath_succ_decomp:
assumes "apath u p v"
assumes "(x,y) ∈ set p"
assumes "y ≠ v"
shows "∃p1 z p2. p = p1 @ (x,y) # (y,z) # p2 ∧ x ≠ z ∧ y ≠ z"
proof -
from ‹(x,y) ∈ set p› obtain p1 p2 where p_decomp: "p = p1 @ (x,y) # p2"
by (metis (no_types) in_set_conv_decomp_first)
from p_decomp ‹apath u p v› ‹y ≠ v› have "p2 ≠ []" "awalk y p2 v"
by (auto simp: apath_def awalk_Cons_iff)
then obtain z p2' where p2_decomp: "p2 = (y,z) # p2'"
by atomize_elim (cases p2, auto simp: awalk_Cons_iff)
then have "x ≠ z ∧ y ≠ z" using p_decomp p2_decomp ‹apath u p v›
by (auto simp: apath_append_iff apath_simps hd_in_awalk_verts)
with p_decomp p2_decomp have "p = p1 @ (x,y) # (y,z) # p2' ∧ x ≠ z ∧ y ≠ z"
by auto
then show ?thesis by blast
qed

lemma (in pair_sym_digraph) arcs_symmetric:
"(a,b) ∈ parcs G ⟹ (b,a) ∈ parcs G"
using sym_arcs by (auto simp: symmetric_def elim: symE)

lemma (in pair_pseudo_graph) pair_pseudo_graph[intro]: "pair_pseudo_graph G" ..

lemma (in pair_graph) pair_graph[intro]: "pair_graph G" by unfold_locales
lemma (in pair_graph) pair_graphD_graph: "graph G" by unfold_locales

lemma pair_graphI_graph:
assumes "graph (with_proj G)" shows "pair_graph G"
proof -
interpret G: graph "with_proj G" by fact
show ?thesis
using G.wellformed G.finite_arcs G.finite_verts G.no_loops
by unfold_locales auto
qed

lemma pair_loopfreeI_loopfree:
assumes "loopfree_digraph (with_proj G)" shows "pair_loopfree_digraph G"
proof -
interpret loopfree_digraph "with_proj G" by fact
show ?thesis using wellformed no_loops by unfold_locales auto
qed

subsection ‹Path reversal for Pair Digraphs›

text ‹This definition is only meaningful in @{term Pair_Digraph}›

primrec rev_path :: "('a × 'a) awalk ⇒ ('a × 'a) awalk" where
"rev_path [] = []" |
"rev_path (e # es) = rev_path es @ [(snd e, fst e)]"

lemma rev_path_append[simp]: "rev_path (p @ q) = rev_path q @ rev_path p"
by (induct p) auto

lemma rev_path_rev_path[simp]:
"rev_path (rev_path p) = p"
by (induct p) auto

lemma rev_path_empty[simp]:
"rev_path p = [] ⟷ p = []"
by (induct p) auto

lemma rev_path_eq: "rev_path p = rev_path q ⟷ p = q"
by (metis rev_path_rev_path)

lemma (in pair_sym_digraph)
assumes "awalk u p v"
shows awalk_verts_rev_path: "awalk_verts v (rev_path p) = rev (awalk_verts u p)"
and awalk_rev_path': "awalk v (rev_path p) u"
using assms
proof (induct p arbitrary: u)
case Nil case 1 then show ?case by auto
next
case Nil case 2 then show ?case by (auto simp: awalk_Nil_iff)
next
case (Cons e es) case 1
with Cons have walks: "awalk v (rev_path es) (snd e)"
"awalk (snd e) [(snd e, fst e)] u"
and verts: "awalk_verts v (rev_path es) = rev (awalk_verts (snd e) es)"
by (auto simp: awalk_simps intro: arcs_symmetric)

from walks have "awalk v (rev_path es @ [(snd e, fst e)]) u"
by simp
moreover
have "tl (awalk_verts (awlast v (rev_path es)) [(snd e, fst e)]) = [fst e]"
by auto
ultimately
show ?case using 1 verts by (auto simp: awalk_verts_append)
next
case (Cons e es) case 2
with Cons have "awalk v (rev_path es) (snd e)"
by (auto simp: awalk_Cons_iff)
moreover
have "rev_path (e # es) = rev_path es @ [(snd e, fst e)]"
by auto
moreover
from Cons 2 have "awalk (snd e) [(snd e, fst e)] u"
by (auto simp: awalk_simps intro: arcs_symmetric)
ultimately show "awalk v (rev_path (e # es)) u"
by simp
qed

lemma (in pair_sym_digraph) awalk_rev_path[simp]:
"awalk v (rev_path p) u = awalk u p v" (is "?L = ?R")
by (metis awalk_rev_path' rev_path_rev_path)

lemma (in pair_sym_digraph) apath_rev_path[simp]:
"apath v (rev_path p) u = apath u p v"
by (auto simp: awalk_verts_rev_path apath_def)

subsection ‹Subdividing Edges›

text ‹subdivide an edge (=two associated arcs) in graph›
fun subdivide :: "'a pair_pre_digraph ⇒ 'a × 'a ⇒ 'a ⇒ 'a pair_pre_digraph" where
"subdivide G (u,v) w = ⦇
pverts = pverts G ∪ {w},
parcs = (parcs G - {(u,v),(v,u)}) ∪ {(u,w), (w,u), (w, v), (v, w)}⦈"

declare subdivide.simps[simp del]

text ‹subdivide an arc in a path›
fun sd_path :: "'a × 'a ⇒ 'a ⇒ ('a × 'a) awalk ⇒ ('a × 'a) awalk" where
"sd_path _ _ [] = []"
| "sd_path (u,v) w (e # es) = (if e = (u,v)
then [(u,w),(w,v)]
else if e = (v,u)
then [(v,w),(w,u)]
else [e]) @ sd_path (u,v) w es"

text ‹contract an arc in a path›
fun co_path :: "'a × 'a ⇒ 'a ⇒ ('a × 'a) awalk ⇒ ('a × 'a) awalk" where
"co_path _ _ [] = []"
| "co_path _ _ [e] = [e]"
| "co_path (u,v) w (e1 # e2 # es) = (if e1 = (u,w) ∧ e2 = (w,v)
then (u,v) # co_path (u,v) w es
else if e1 = (v,w) ∧ e2 = (w,u)
then (v,u) # co_path (u,v) w es
else e1 # co_path (u,v) w (e2 # es))"

lemma co_path_simps[simp]:
"⟦e1 ≠ (fst e, w); e1 ≠ (snd e,w)⟧ ⟹ co_path e w (e1 # es) = e1 # co_path e w es"
"⟦e1 = (fst e, w); e2 = (w, snd e)⟧ ⟹ co_path e w (e1 # e2 # es) = e # co_path e w es"
"⟦e1 = (snd e, w); e2 = (w, fst e)⟧
⟹ co_path e w (e1 # e2 # es) = (snd e, fst e) # co_path e w es"
"⟦e1 ≠ (fst e, w) ∨ e2 ≠ (w, snd e); e1 ≠ (snd e, w) ∨ e2 ≠ (w, fst e)⟧
⟹ co_path e w (e1 # e2 # es) = e1 # co_path e w (e2 # es)"
apply (cases es; auto)
apply (cases e; auto)
apply (cases e; auto)
apply (cases e; cases "fst e = snd e"; auto)
apply (cases e; cases "fst e = snd e"; auto)
done

lemma co_path_nonempty[simp]: "co_path e w p = [] ⟷ p = []"
by (cases e) (cases p rule: list_exhaust_NSC, auto)

declare co_path.simps(3)[simp del]

lemma verts_subdivide[simp]: "pverts (subdivide G e w) = pverts G ∪ {w}"
by (cases e) (auto simp: subdivide.simps)

lemma arcs_subdivide[simp]:
shows "parcs (subdivide G (u,v) w) = (parcs G - {(u,v),(v,u)}) ∪ {(u,w), (w,u), (w, v), (v, w)}"
by (auto simp: subdivide.simps)

lemmas subdivide_simps = verts_subdivide arcs_subdivide

lemma sd_path_induct[case_names empty pass sd sdrev]:
assumes A: "P e []"
and B: "⋀e' es. e' ≠ e ⟹ e' ≠ (snd e , fst e) ⟹ P e es ⟹ P e (e' # es)"
"⋀es. P e es ⟹ P e (e # es)"
"⋀es. fst e ≠ snd e ⟹ P e es ⟹ P e ((snd e, fst e) # es)"
shows "P e es"
by (induct es) (rule A, metis B prod.collapse)

lemma co_path_induct[case_names empty single co corev pass]:
fixes e :: "'a × 'a"
and w :: "'a"
and p :: "('a × 'a) awalk"
assumes Nil: "P e w []"
and ConsNil:"⋀e'. P e w [e']"
and ConsCons1: "⋀e1 e2 es. e1 = (fst e, w) ∧ e2 = (w, snd e) ⟹ P e w es ⟹
P e w (e1 # e2 # es)"
and ConsCons2: "⋀e1 e2 es. ¬(e1 = (fst e, w) ∧ e2 = (w, snd e)) ∧
e1 = (snd e, w) ∧ e2 = (w, fst e) ⟹ P e w es ⟹
P e w (e1 # e2 # es)"
and ConsCons3: "⋀e1 e2 es.
¬ (e1 = (fst e, w) ∧ e2 = (w, snd e)) ⟹
¬ (e1 = (snd e, w) ∧ e2 = (w, fst e)) ⟹ P e w (e2 # es) ⟹
P e w (e1 # e2 # es)"
shows "P e w p"
proof (induct p rule: length_induct)
case (1 p) then show ?case
proof (cases p rule: list_exhaust_NSC)
case (Cons_Cons e1 e2 es)
then have "P e w es" "P e w (e2 # es)"using 1 by auto
then show ?thesis unfolding Cons_Cons by (blast intro: ConsCons1 ConsCons2 ConsCons3)
qed (auto intro: Nil ConsNil)
qed

lemma co_sd_id:
assumes "(u,w) ∉ set p" "(v,w) ∉ set p"
shows "co_path (u,v) w (sd_path (u,v) w p) = p"
using assms by (induct p) auto

lemma sd_path_id:
assumes "(x,y) ∉ set p" "(y,x) ∉ set p"
shows "sd_path (x,y) w p = p"
using assms by (induct p) auto

lemma (in pair_wf_digraph) pair_wf_digraph_subdivide:
assumes props: "e ∈ parcs G" "w ∉ pverts G"
shows "pair_wf_digraph (subdivide G e w)" (is "pair_wf_digraph ?sG")
proof
obtain u v where [simp]: "e = (u,v)" by (cases e) auto
fix e' assume "e' ∈ parcs ?sG"
then show "fst e' ∈ pverts ?sG" "snd e' ∈ pverts ?sG"
using props by (auto dest: wellformed)
qed

lemma (in pair_sym_digraph) pair_sym_digraph_subdivide:
assumes props: "e ∈ parcs G" "w ∉ pverts G"
shows "pair_sym_digraph (subdivide G e w)" (is "pair_sym_digraph ?sG")
proof -
interpret sdG: pair_wf_digraph "subdivide G e w" using assms by (rule pair_wf_digraph_subdivide)
obtain u v where [simp]: "e = (u,v)" by (cases e) auto
show ?thesis
proof
have "⋀a b. (a, b) ∈ parcs (subdivide G e w) ⟹ (b, a) ∈ parcs (subdivide G e w)"
unfolding ‹e = _› arcs_subdivide
by (elim UnE, rule UnI1, rule_tac  UnI2) (blast intro: arcs_symmetric)+
then show "symmetric ?sG"
unfolding symmetric_def with_proj_simps by (rule symI)
qed
qed

lemma (in pair_loopfree_digraph) pair_loopfree_digraph_subdivide:
assumes props: "e ∈ parcs G" "w ∉ pverts G"
shows "pair_loopfree_digraph (subdivide G e w)" (is "pair_loopfree_digraph ?sG")
proof -
interpret sdG: pair_wf_digraph "subdivide G e w" using assms by (rule pair_wf_digraph_subdivide)
from assms show ?thesis
by unfold_locales (cases e, auto dest: wellformed no_loops)
qed

lemma (in pair_bidirected_digraph) pair_bidirected_digraph_subdivide:
assumes props: "e ∈ parcs G" "w ∉ pverts G"
shows "pair_bidirected_digraph (subdivide G e w)" (is "pair_bidirected_digraph ?sG")
proof -
interpret sdG: pair_sym_digraph "subdivide G e w" using assms by (rule pair_sym_digraph_subdivide)
interpret sdG: pair_loopfree_digraph "subdivide G e w" using assms by (rule pair_loopfree_digraph_subdivide)
show ?thesis by unfold_locales
qed

lemma (in pair_pseudo_graph) pair_pseudo_graph_subdivide:
assumes props: "e ∈ parcs G" "w ∉ pverts G"
shows "pair_pseudo_graph (subdivide G e w)" (is "pair_pseudo_graph ?sG")
proof -
interpret sdG: pair_sym_digraph "subdivide G e w" using assms by (rule pair_sym_digraph_subdivide)
obtain u v where [simp]: "e = (u,v)" by (cases e) auto
show ?thesis by unfold_locales (cases e, auto)
qed

lemma (in pair_graph) pair_graph_subdivide:
assumes "e ∈ parcs G" "w ∉ pverts G"
shows "pair_graph (subdivide G e w)" (is "pair_graph ?sG")
proof -
interpret PPG: pair_pseudo_graph "subdivide G e w"
using assms by (rule pair_pseudo_graph_subdivide)
interpret PPG: pair_loopfree_digraph "subdivide G e w"
using assms by (rule pair_loopfree_digraph_subdivide)
from assms show ?thesis by unfold_locales
qed

lemma arcs_subdivideD:
assumes "x ∈ parcs (subdivide G e w)" "fst x ≠ w" "snd x ≠ w"
shows "x ∈ parcs G"
using assms by (cases e) auto

context pair_sym_digraph begin

lemma
assumes path: "apath u p v"
assumes elems: "e ∈ parcs G" "w ∉ pverts G"
shows apath_sd_path: "pre_digraph.apath (subdivide G e w) u (sd_path e w p) v" (is ?A)
and set_awalk_verts_sd_path: "set (awalk_verts u (sd_path e w p))
⊆ set (awalk_verts u p) ∪ {w}" (is ?B)
proof -
obtain x y where e_conv: "e = (x,y)" by (cases e) auto
define sG where "sG = subdivide G e w"
interpret S: pair_sym_digraph sG
unfolding sG_def using elems by (rule pair_sym_digraph_subdivide)

have ev_sG: "S.awalk_verts = awalk_verts"
by (auto simp: fun_eq_iff pre_digraph.awalk_verts_conv)
have w_sG: "{(x,w), (y,w), (w,x), (w,y)} ⊆ parcs sG"
by (auto simp: sG_def e_conv)

from path have "S.apath u (sd_path (x,y) w p) v"
and "set (S.awalk_verts u (sd_path (x,y) w p)) ⊆ set (awalk_verts u p) ∪ {w}"
proof (induct p arbitrary: u rule: sd_path_induct)
case empty case 1
moreover have "pverts sG = pverts G ∪ {w}" by (simp add: sG_def)
ultimately show ?case by (auto simp: apath_Nil_iff S.apath_Nil_iff)
next
case empty case 2 then show ?case by simp
next
case (pass e' es)
{ case 1
then have "S.apath (snd e') (sd_path (x,y) w es) v" "u ≠ w" "fst e' = u"
"u ∉ set (S.awalk_verts (snd e') (sd_path (x,y) w es))"
using pass elems by (fastforce simp: apath_Cons_iff)+
moreover then have "e' ∈ parcs sG"
using 1 pass by (auto simp: e_conv sG_def S.apath_Cons_iff apath_Cons_iff)
ultimately show ?case using pass by (auto simp: S.apath_Cons_iff) }
note case1 = this
{ case 2 with pass 2 show ?case by (simp add: apath_Cons_iff) blast }
next
{ fix u es a b
assume A: "apath u ((a,b) # es) v"
and ab: "(a,b) = (x,y) ∨ (a,b) = (y,x)"
and hyps: "⋀u. apath u es v ⟹ S.apath u (sd_path (x, y) w es) v"
"⋀u. apath u es v ⟹ set (awalk_verts u (sd_path (x, y) w es)) ⊆ set (awalk_verts u es) ∪ {w}"

from ab A have "(x,y) ∉ set es" "(y,x) ∉ set es"
by (auto simp: apath_Cons_iff dest!: awalkI_apath dest: awalk_verts_arc1 awalk_verts_arc2)
then have ev_sd: "set (S.awalk_verts b (sd_path (x,y) w es)) = set (awalk_verts b es)"

from A ab have [simp]: "x ≠ y"
by (simp add: apath_Cons_iff) (metis awalkI_apath awalk_verts_non_Nil awhd_of_awalk hd_in_set)

from A have "S.apath b (sd_path (x,y) w es) v" "u = a" "u ≠ w"
using ab hyps elems by (auto simp: apath_Cons_iff wellformed')
moreover
then have "S.awalk u (sd_path (x, y) w ((a, b) # es)) v "
using ab w_sG by (auto simp: S.apath_def S.awalk_simps S.wellformed')
then have "u ∉ set (S.awalk_verts w ((w,b) # sd_path (x,y) w es))"
using ab ‹u ≠ w› ev_sd A by (auto simp: apath_Cons_iff S.awalk_def)
moreover
have "w ∉ set (awalk_verts b (sd_path (x, y) w es))"
using ab ev_sd A elems by (auto simp: awalk_Cons_iff apath_def)
ultimately
have path: "S.apath u (sd_path (x, y) w ((a, b) # es)) v "
using ab hyps w_sG ‹u = a› by (auto simp: S.apath_Cons_iff ) }
note path = this
{ case (sd es)
{ case 1 with sd show ?case by (intro path) auto }
{ case 2 show ?case using 2 sd
by (auto simp: apath_Cons_iff) } }
{ case (sdrev es)
{ case 1 with sdrev show ?case by (intro path) auto }
{ case 2 show ?case using 2 sdrev
by (auto simp: apath_Cons_iff) } }
qed
then show ?A ?B unfolding sG_def e_conv .
qed

lemma
assumes elems: "e ∈ parcs G" "w ∉ pverts G" "u ∈ pverts G" "v ∈ pverts G"
assumes path: "pre_digraph.apath (subdivide G e w) u p v"
shows apath_co_path: "apath u (co_path e w p) v" (is ?thesis_path)
and set_awalk_verts_co_path: "set (awalk_verts u (co_path e w p)) = set (awalk_verts u p) - {w}" (is ?thesis_set)
proof -
obtain x y where e_conv: "e = (x,y)" by (cases e) auto
interpret S: pair_sym_digraph "subdivide G e w"
using elems(1,2) by (rule pair_sym_digraph_subdivide)

have e_w: "fst e ≠ w" "snd e ≠ w" using elems by auto

have "S.apath u p v" "u ≠ w" using elems path by auto
then have co_path: "apath u (co_path e w p) v
∧ set (awalk_verts u (co_path e w p)) = set (awalk_verts u p) - {w}"
proof (induction p arbitrary: u rule: co_path_induct)
case empty with elems show ?case
next
case (single e') with elems show ?case
by (auto simp: apath_Cons_iff S.apath_Cons_iff apath_Nil_iff S.apath_Nil_iff
dest: arcs_subdivideD)
next
case (co e1 e2 es)
then have "apath u (co_path e w (e1 # e2 # es)) v" using co e_w elems
by (auto simp: apath_Cons_iff S.apath_Cons_iff)
moreover
have "set (awalk_verts u (co_path e w (e1 # e2 # es))) = set (awalk_verts u (e1 # e2 # es)) - {w}"
using co e_w by (auto simp: apath_Cons_iff S.apath_Cons_iff)
ultimately
show ?case by fast
next
case (corev e1 e2 es)
have "apath u (co_path e w (e1 # e2 # es)) v" using corev(1-3) e_w(1) elems(1)
by (auto simp: apath_Cons_iff S.apath_Cons_iff  intro: arcs_symmetric)
moreover
have "set (awalk_verts u (co_path e w (e1 # e2 # es))) = set (awalk_verts u (e1 # e2 # es)) - {w}"
using corev e_w by (auto simp: apath_Cons_iff S.apath_Cons_iff)
ultimately
show ?case by fast
next
case (pass e1 e2 es)
have "fst e1 ≠ w" using elems pass.prems by (auto simp: S.apath_Cons_iff)
have "snd e1 ≠ w"
proof
assume "snd e1 = w"
then have "e1 ∉ parcs G" using elems by auto
then have "e1 ∈ parcs (subdivide G e w) - parcs G"
using pass by (auto simp: S.apath_Cons_iff)
then have "e1 = (x,w) ∨ e1 = (y,w)"
using ‹fst e1 ≠ w› e_w by (auto simp add: e_conv)
moreover
have "fst e2 = w" using ‹snd e1 = w› pass.prems by (auto simp: S.apath_Cons_iff)
then have "e2 ∉ parcs G" using elems by auto
then have "e2 ∈ parcs (subdivide G e w) - parcs G"
using pass by (auto simp: S.apath_Cons_iff)
then have "e2 = (w,x) ∨ e2 = (w,y)"
using ‹fst e2 = w› e_w by (cases e2) (auto simp add: e_conv)
ultimately
have "e1 = (x,w) ∧ e2 = (w,x) ∨ e1 = (y,w) ∧ e2 = (w,y)"
using pass.hyps[simplified e_conv] by auto
then show False
using pass.prems by (cases es) (auto simp: S.apath_Cons_iff)
qed
then have "e1 ∈ parcs G"
using ‹fst e1 ≠ w› pass.prems by (auto simp: S.apath_Cons_iff dest: arcs_subdivideD)

have ih: "apath (snd e1) (co_path e w (e2 # es)) v ∧ set (awalk_verts (snd e1) (co_path e w (e2 # es))) = set (awalk_verts (snd e1) (e2 # es)) - {w}"
using pass.prems ‹snd e1 ≠ w› by (intro pass.IH) (auto simp: apath_Cons_iff S.apath_Cons_iff)
then have "fst e1 ∉ set (awalk_verts (snd e1) (co_path e w (e2 # es)))" "fst e1 = u"
using pass.prems by (clarsimp simp: S.apath_Cons_iff)+
then have "apath u (co_path e w (e1 # e2 # es)) v"
using ih pass ‹e1 ∈ parcs G› by (auto simp: apath_Cons_iff S.apath_Cons_iff)[]
moreover
have "set (awalk_verts u (co_path e w (e1 # e2 # es))) = set (awalk_verts u (e1 # e2 # es)) - {w}"
using pass.hyps ih ‹fst e1 ≠ w› by auto
ultimately show ?case by fast
qed
then show ?thesis_set ?thesis_path by blast+
qed

end

subsection ‹Bidirected Graphs›

definition (in -) swap_in :: "('a × 'a) set ⇒ 'a × 'a ⇒ 'a × 'a" where
"swap_in S x = (if x ∈ S then prod.swap x else x)"

lemma bidirected_digraph_rev_conv_pair:
assumes "bidirected_digraph (with_proj G) rev_G"
shows "rev_G = swap_in (parcs G)"
proof -
interpret bidirected_digraph G rev_G by fact
have "⋀a b. (a, b) ∈ parcs G ⟹ rev_G (a, b) = (b, a)"
by (metis fst_conv prod.collapse snd_conv)
then show ?thesis by (auto simp: swap_in_def fun_eq_iff arev_eq)
qed

lemma (in pair_bidirected_digraph) bidirected_digraph:
"bidirected_digraph (with_proj G) (swap_in (parcs G))"
using no_loops' arcs_symmetric
by unfold_locales (auto simp: swap_in_def)

lemma pair_bidirected_digraphI_bidirected_digraph:
assumes "bidirected_digraph (with_proj G) (swap_in (parcs G))"
shows "pair_bidirected_digraph G"
proof -
interpret bidirected_digraph "with_proj G" "swap_in (parcs G)" by fact
{
fix a assume "a ∈ parcs G" then have "fst a ≠ snd a"
using arev_neq[of a] bidirected_digraph_rev_conv_pair[OF assms(1)]
by (cases a) (auto simp: swap_in_def)
}
then show ?thesis
using tail_in_verts head_in_verts by unfold_locales auto
qed

end


# Theory Digraph_Component

(* Title:  Digraph_Component.thy
Author: Lars Noschinski, TU München
*)

theory Digraph_Component
imports
Digraph
Arc_Walk
Pair_Digraph
begin

section ‹Components of (Symmetric) Digraphs›

definition compatible :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where
"compatible G H ≡ tail G = tail H ∧ head G = head H"

(* Require @{term "wf_digraph G"}? *)
definition subgraph :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where
"subgraph H G ≡ verts H ⊆ verts G ∧ arcs H ⊆ arcs G ∧ wf_digraph G ∧ wf_digraph H ∧ compatible G H"

definition induced_subgraph :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where
"induced_subgraph H G ≡ subgraph H G ∧ arcs H = {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}"

definition spanning :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where
"spanning H G ≡ subgraph H G ∧ verts G = verts H"

definition strongly_connected :: "('a,'b) pre_digraph ⇒ bool" where
"strongly_connected G ≡ verts G ≠ {} ∧ (∀u ∈ verts G. ∀v ∈ verts G. u →⇧*⇘G⇙ v)"

text ‹
The following function computes underlying symmetric graph of a digraph
and removes parallel arcs.
›

definition mk_symmetric :: "('a,'b) pre_digraph ⇒ 'a pair_pre_digraph" where
"mk_symmetric G ≡ ⦇ pverts = verts G, parcs = ⋃e∈arcs G. {(tail G e, head G e), (head G e, tail G e)}⦈"

definition connected :: "('a,'b) pre_digraph ⇒ bool" where
"connected G ≡ strongly_connected (mk_symmetric G)"

definition forest :: "('a,'b) pre_digraph ⇒ bool" where
"forest G ≡ ¬(∃p. pre_digraph.cycle G p)"

definition tree :: "('a,'b) pre_digraph ⇒ bool" where
"tree G ≡ connected G ∧ forest G"

definition spanning_tree :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where
"spanning_tree H G ≡ tree H ∧ spanning H G"

definition (in pre_digraph)
max_subgraph :: "(('a,'b) pre_digraph ⇒ bool) ⇒ ('a,'b) pre_digraph ⇒  bool"
where
"max_subgraph P H ≡ subgraph H G ∧ P H ∧ (∀H'. H' ≠ H ∧ subgraph H H' ⟶ ¬(subgraph H' G ∧ P H'))"

definition (in pre_digraph) sccs :: "('a,'b) pre_digraph set" where
"sccs ≡ {H. induced_subgraph H G ∧ strongly_connected H ∧ ¬(∃H'. induced_subgraph H' G
∧ strongly_connected H' ∧ verts H ⊂ verts H')}"

definition (in pre_digraph) sccs_verts :: "'a set set" where
"sccs_verts = {S. S ≠ {} ∧ (∀u ∈ S. ∀v ∈ S. u →⇧*⇘G⇙ v) ∧ (∀u ∈ S. ∀v. v ∉ S ⟶ ¬u →⇧*⇘G⇙ v ∨ ¬v →⇧*⇘G⇙ u)}"
(*XXX:  "sccs_verts = verts  sccs" *)

definition (in pre_digraph) scc_of :: "'a ⇒ 'a set" where
"scc_of u ≡ {v. u →⇧* v ∧ v →⇧* u}"

definition union :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph" where
"union G H ≡ ⦇ verts = verts G ∪ verts H, arcs = arcs G ∪ arcs H, tail = tail G, head = head G⦈"

definition (in pre_digraph) Union :: "('a,'b) pre_digraph set ⇒ ('a,'b) pre_digraph" where
"Union gs = ⦇ verts = (⋃G ∈ gs. verts G), arcs = (⋃G ∈ gs. arcs G),

subsection ‹Compatible Graphs›

lemma compatible_tail:
assumes "compatible G H" shows "tail G = tail H"
using assms by (simp add: fun_eq_iff compatible_def)

using assms by (simp add: fun_eq_iff compatible_def)

lemma compatible_cas:
assumes "compatible G H" shows "pre_digraph.cas G = pre_digraph.cas H"
proof (unfold fun_eq_iff, intro allI)
fix u es v show "pre_digraph.cas G u es v = pre_digraph.cas H u es v"
using assms
by (induct es arbitrary: u)
qed

lemma compatible_awalk_verts:
assumes "compatible G H" shows "pre_digraph.awalk_verts G = pre_digraph.awalk_verts H"
proof (unfold fun_eq_iff, intro allI)
fix u es show "pre_digraph.awalk_verts G u es = pre_digraph.awalk_verts H u es"
using assms
by (induct es arbitrary: u)
qed

lemma compatibleI_with_proj[intro]:
shows "compatible (with_proj G) (with_proj H)"
by (auto simp: compatible_def)

subsection ‹Basic lemmas›

lemma (in sym_digraph) graph_symmetric:
shows "(u,v) ∈ arcs_ends G ⟹ (v,u) ∈ arcs_ends G"
using sym_arcs by (auto simp add: symmetric_def sym_def)

lemma strongly_connectedI[intro]:
assumes "verts G ≠ {}" "⋀u v. u ∈ verts G ⟹ v ∈ verts G ⟹ u →⇧*⇘G⇙ v"
shows "strongly_connected G"
using assms by (simp add: strongly_connected_def)

lemma strongly_connectedE[elim]:
assumes "strongly_connected G"
assumes "(⋀u v. u ∈ verts G ∧ v ∈ verts G ⟹ u →⇧*⇘G⇙ v) ⟹ P"
shows "P"
using assms by (auto simp add: strongly_connected_def)

lemma subgraph_imp_subverts:
assumes "subgraph H G"
shows "verts H ⊆ verts G"
using assms by (simp add: subgraph_def)

lemma induced_imp_subgraph:
assumes "induced_subgraph H G"
shows "subgraph H G"
using assms by (simp add: induced_subgraph_def)

lemma (in pre_digraph) in_sccs_imp_induced:
assumes "c ∈ sccs"
shows "induced_subgraph c G"
using assms by (auto simp: sccs_def)

lemma spanning_tree_imp_tree[dest]:
assumes "spanning_tree H G"
shows "tree H"
using assms by (simp add: spanning_tree_def)

lemma tree_imp_connected[dest]:
assumes "tree G"
shows "connected G"
using assms by (simp add: tree_def)

lemma spanning_treeI[intro]:
assumes "spanning H G"
assumes "tree H"
shows "spanning_tree H G"
using assms by (simp add: spanning_tree_def)

lemma spanning_treeE[elim]:
assumes "spanning_tree H G"
assumes "tree H ∧ spanning H G ⟹ P"
shows "P"
using assms by (simp add: spanning_tree_def)

lemma spanningE[elim]:
assumes "spanning H G"
assumes "subgraph H G ∧ verts G = verts H ⟹ P"
shows "P"
using assms by (simp add: spanning_def)

lemma (in pre_digraph) in_sccsI[intro]:
assumes "induced_subgraph c G"
assumes "strongly_connected c"
assumes "¬(∃c'. induced_subgraph c' G ∧ strongly_connected c' ∧
verts c ⊂ verts c')"
shows "c ∈ sccs"
using assms by (auto simp add: sccs_def)

lemma (in pre_digraph) in_sccsE[elim]:
assumes "c ∈ sccs"
assumes "induced_subgraph c G ⟹ strongly_connected c ⟹ ¬ (∃d.
induced_subgraph d G ∧ strongly_connected d ∧ verts c ⊂ verts d) ⟹ P"
shows "P"
using assms by (simp add: sccs_def)

lemma subgraphI:
assumes "verts H ⊆ verts G"
assumes "arcs H ⊆ arcs G"
assumes "compatible G H"
assumes "wf_digraph H"
assumes "wf_digraph G"
shows "subgraph H G"
using assms by (auto simp add: subgraph_def)

lemma subgraphE[elim]:
assumes "subgraph H G"
obtains "verts H ⊆ verts G" "arcs H ⊆ arcs G" "compatible G H" "wf_digraph H" "wf_digraph G"
using assms by (simp add: subgraph_def)

lemma induced_subgraphI[intro]:
assumes "subgraph H G"
assumes "arcs H = {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}"
shows "induced_subgraph H G"
using assms unfolding induced_subgraph_def by safe

lemma induced_subgraphE[elim]:
assumes "induced_subgraph H G"
assumes "⟦subgraph H G; arcs H = {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}⟧ ⟹ P"
shows "P"
using assms by (auto simp add: induced_subgraph_def)

lemma pverts_mk_symmetric[simp]: "pverts (mk_symmetric G) = verts G"
and parcs_mk_symmetric:
"parcs (mk_symmetric G) = (⋃e∈arcs G. {(tail G e, head G e), (head G e, tail G e)})"
by (auto simp: mk_symmetric_def arcs_ends_conv image_UN)

lemma arcs_ends_mono:
assumes "subgraph H G"
shows "arcs_ends H ⊆ arcs_ends G"

lemma (in wf_digraph) subgraph_refl: "subgraph G G"
by (auto simp: subgraph_def compatible_def) unfold_locales

lemma (in wf_digraph) induced_subgraph_refl: "induced_subgraph G G"
by (rule induced_subgraphI) (auto simp: subgraph_refl)

subsection ‹The underlying symmetric graph of a digraph›

lemma (in wf_digraph) wellformed_mk_symmetric[intro]: "pair_wf_digraph (mk_symmetric G)"
by unfold_locales (auto simp: parcs_mk_symmetric)

lemma (in fin_digraph) pair_fin_digraph_mk_symmetric[intro]: "pair_fin_digraph (mk_symmetric G)"
proof -
have "finite ((λ(a,b). (b,a))  arcs_ends G)" (is "finite ?X") by (auto simp: arcs_ends_conv)
also have "?X = {(a, b). (b, a) ∈ arcs_ends G}" by auto
finally have X: "finite ..." .
then show ?thesis
by unfold_locales (auto simp: mk_symmetric_def arcs_ends_conv)
qed

lemma (in digraph) digraph_mk_symmetric[intro]: "pair_digraph (mk_symmetric G)"
proof -
have "finite ((λ(a,b). (b,a))  arcs_ends G)" (is "finite ?X") by (auto simp: arcs_ends_conv)
also have "?X = {(a, b). (b, a) ∈ arcs_ends G}" by auto
finally have "finite ..." .
then show ?thesis
by unfold_locales (auto simp: mk_symmetric_def arc_to_ends_def dest: no_loops)
qed

lemma (in wf_digraph) reachable_mk_symmetricI:
assumes "u →⇧* v" shows "u →⇧*⇘mk_symmetric G⇙ v"
proof -
have "arcs_ends G ⊆ parcs (mk_symmetric G)"
"(u, v) ∈ rtrancl_on (pverts (mk_symmetric G)) (arcs_ends G)"
using assms unfolding reachable_def by (auto simp: parcs_mk_symmetric)
then show ?thesis unfolding reachable_def by (auto intro: rtrancl_on_mono)
qed

"symmetric G ⟹ parcs (mk_symmetric G) = arcs_ends G"
by (auto simp: parcs_mk_symmetric in_arcs_imp_in_arcs_ends arcs_ends_symmetric)

lemma (in wf_digraph) reachable_mk_symmetric_eq:
assumes "symmetric G" shows "u →⇧*⇘mk_symmetric G⇙ v ⟷ u →⇧* v" (is "?L ⟷ ?R")
using adj_mk_symmetric_eq[OF assms] unfolding reachable_def by auto

lemma (in wf_digraph) mk_symmetric_awalk_imp_awalk:
assumes sym: "symmetric G"
assumes walk: "pre_digraph.awalk (mk_symmetric G) u p v"
obtains q where "awalk u q v"
proof -
interpret S: pair_wf_digraph "mk_symmetric G" ..
from walk have "u →⇧*⇘mk_symmetric G⇙ v"
by (simp only: S.reachable_awalk) rule
then have "u →⇧* v" by (simp only: reachable_mk_symmetric_eq[OF sym])
then show ?thesis by (auto simp: reachable_awalk intro: that)
qed

lemma symmetric_mk_symmetric:
"symmetric (mk_symmetric G)"
by (auto simp: symmetric_def parcs_mk_symmetric intro: symI)

subsection ‹Subgraphs and Induced Subgraphs›

lemma subgraph_trans:
assumes "subgraph G H" "subgraph H I" shows "subgraph G I"
using assms by (auto simp: subgraph_def compatible_def)

text ‹
The @{term digraph} and @{term fin_digraph} properties are preserved under
the (inverse) subgraph relation
›
lemma (in fin_digraph) fin_digraph_subgraph:
assumes "subgraph H G" shows "fin_digraph H"
proof (intro_locales)
from assms show "wf_digraph H" by auto

have HG: "arcs H ⊆ arcs G" "verts H ⊆ verts G"
using assms by auto
then have "finite (verts H)" "finite (arcs H)"
using finite_verts finite_arcs by (blast intro: finite_subset)+
then show "fin_digraph_axioms H"
by unfold_locales
qed

lemma (in digraph) digraph_subgraph:
assumes "subgraph H G" shows "digraph H"
proof
fix e assume e: "e ∈ arcs H"
with assms show "tail H e ∈ verts H" "head H e ∈ verts H"
by (auto simp: subgraph_def intro: wf_digraph.wellformed)
from e and assms have "e ∈ arcs H ∩ arcs G" by auto
with assms show "tail H e ≠ head H e"
using no_loops by (auto simp: subgraph_def compatible_def arc_to_ends_def)
next
have "arcs H ⊆ arcs G" "verts H ⊆ verts G" using assms by auto
then show "finite (arcs H)" "finite (verts H)"
using finite_verts finite_arcs by (blast intro: finite_subset)+
next
fix e1 e2 assume "e1 ∈ arcs H" "e2 ∈ arcs H"
and eq: "arc_to_ends H e1 = arc_to_ends H e2"
with assms have "e1 ∈ arcs H ∩ arcs G" "e2 ∈ arcs H ∩ arcs G"
by auto
with eq show "e1 = e2"
using no_multi_arcs assms
by (auto simp: subgraph_def compatible_def arc_to_ends_def)
qed

assumes "u →⇘H⇙ v" "subgraph H G"
shows "u → v"
using assms by (blast dest: arcs_ends_mono)

lemma (in pre_digraph) reachable_mono:
assumes walk: "u →⇧*⇘H⇙ v" and sub: "subgraph H G"
shows "u →⇧* v"
proof -
have "verts H ⊆ verts G" using sub by auto
with assms show ?thesis
unfolding reachable_def by (metis arcs_ends_mono rtrancl_on_mono)
qed

text ‹
Arc walks and paths are preserved under the subgraph relation.
›
lemma (in wf_digraph) subgraph_awalk_imp_awalk:
assumes walk: "pre_digraph.awalk H u p v"
assumes sub: "subgraph H G"
shows "awalk u p v"
using assms by (auto simp: pre_digraph.awalk_def compatible_cas)

lemma (in wf_digraph) subgraph_apath_imp_apath:
assumes path: "pre_digraph.apath H u p v"
assumes sub: "subgraph H G"
shows "apath u p v"
using assms unfolding pre_digraph.apath_def
by (auto intro: subgraph_awalk_imp_awalk simp: compatible_awalk_verts)

lemma subgraph_mk_symmetric:
assumes "subgraph H G"
shows "subgraph (mk_symmetric H) (mk_symmetric G)"
proof (rule subgraphI)
let ?wpms = "λG. mk_symmetric G"
from assms have "compatible G H" by auto
with assms
show "verts (?wpms H)  ⊆ verts (?wpms G)"
and "arcs (?wpms H) ⊆ arcs (?wpms G)"
by (auto simp: parcs_mk_symmetric compatible_head compatible_tail)
show "compatible (?wpms G) (?wpms H)" by rule
interpret H: pair_wf_digraph "mk_symmetric H"
using assms by (auto intro: wf_digraph.wellformed_mk_symmetric)
interpret G: pair_wf_digraph "mk_symmetric G"
using assms by (auto intro: wf_digraph.wellformed_mk_symmetric)
show "wf_digraph (?wpms H)"
by unfold_locales
show "wf_digraph (?wpms G)" by unfold_locales
qed

lemma (in fin_digraph) subgraph_in_degree:
assumes "subgraph H G"
shows "in_degree H v ≤ in_degree G v"
proof -
have "finite (in_arcs G v)" by auto
moreover
have "in_arcs H v ⊆ in_arcs G v"
using assms by (auto simp: subgraph_def in_arcs_def compatible_head compatible_tail)
ultimately
show ?thesis unfolding in_degree_def by (rule card_mono)
qed

lemma (in wf_digraph) subgraph_cycle:
assumes "subgraph H G" "pre_digraph.cycle H p " shows "cycle p"
proof -
from assms have "compatible G H" by auto
with assms show ?thesis
by (auto simp: pre_digraph.cycle_def compatible_awalk_verts intro: subgraph_awalk_imp_awalk)
qed

lemma (in wf_digraph) subgraph_del_vert: "subgraph (del_vert u) G"
by (auto simp: subgraph_def compatible_def del_vert_simps wf_digraph_del_vert) intro_locales

lemma (in wf_digraph) subgraph_del_arc: "subgraph (del_arc a) G"
by (auto simp: subgraph_def compatible_def del_vert_simps wf_digraph_del_vert) intro_locales

subsection ‹Induced subgraphs›

lemma wf_digraphI_induced:
assumes "induced_subgraph H G"
shows "wf_digraph H"
proof -
from assms have "compatible G H" by auto
with assms show ?thesis by unfold_locales (auto simp: compatible_tail compatible_head)
qed

lemma (in digraph) digraphI_induced:
assumes "induced_subgraph H G"
shows "digraph H"
proof -
interpret W: wf_digraph H using assms by (rule wf_digraphI_induced)
from assms have "compatible G H" by auto
from assms have arcs: "arcs H ⊆ arcs G" by blast
show ?thesis
proof
from assms have "verts H ⊆ verts G" by blast
then show "finite (verts H)" using finite_verts by (rule finite_subset)
next
from arcs show "finite (arcs H)" using finite_arcs by (rule finite_subset)
next
fix e assume "e ∈ arcs H"
with arcs ‹compatible G H› show "tail H e ≠ head H e"
by (auto dest: no_loops simp: compatible_tail[symmetric] compatible_head[symmetric])
next
fix e1 e2 assume "e1 ∈ arcs H" "e2 ∈ arcs H" and ate: "arc_to_ends H e1 = arc_to_ends H e2"
with arcs ‹compatible G H› show "e1 = e2" using ate
by (auto intro: no_multi_arcs simp: compatible_tail[symmetric] compatible_head[symmetric] arc_to_ends_def)
qed
qed

text ‹Computes the subgraph of @{term G} induced by @{term vs}›
definition induce_subgraph :: "('a,'b) pre_digraph ⇒ 'a set ⇒ ('a,'b) pre_digraph" (infix "↾" 67) where
"G ↾ vs = ⦇ verts = vs, arcs = {e ∈ arcs G. tail G e ∈ vs ∧ head G e ∈ vs},

lemma induce_subgraph_verts[simp]:
"verts (G ↾ vs) = vs"

lemma induce_subgraph_arcs[simp]:
"arcs (G ↾ vs) = {e ∈ arcs G. tail G e ∈ vs ∧ head G e ∈ vs}"

lemma induce_subgraph_tail[simp]:
"tail (G ↾ vs) = tail G"
by (auto simp: induce_subgraph_def)

by (auto simp: induce_subgraph_def)

lemma compatible_induce_subgraph: "compatible (G ↾ S) G"
by (auto simp: compatible_def)

lemma (in wf_digraph) induced_induce[intro]:
assumes "vs ⊆ verts G"
shows "induced_subgraph (G ↾ vs) G"
using assms
by (intro subgraphI induced_subgraphI)
(auto simp: arc_to_ends_def induce_subgraph_def wf_digraph_def compatible_def)

lemma (in wf_digraph) wellformed_induce_subgraph[intro]:
"wf_digraph (G ↾ vs)"
by unfold_locales auto

lemma induced_graph_imp_symmetric:
assumes "symmetric G"
assumes "induced_subgraph H G"
shows "symmetric H"
proof (unfold symmetric_conv, safe)
from assms have "compatible G H" by auto

fix e1 assume "e1 ∈ arcs H"
then obtain e2 where "tail G e1 = head G e2"  "head G e1 = tail G e2" "e2 ∈ arcs G"
using assms by (auto simp add: symmetric_conv)
moreover
then have "e2 ∈ arcs H"
using assms and ‹e1 ∈ arcs H› by auto
ultimately
show "∃e2∈arcs H. tail H e1 = head H e2 ∧ head H e1 = tail H e2"
using assms ‹e1 ∈ arcs H› ‹compatible G H›
qed

lemma (in sym_digraph) induced_graph_imp_graph:
assumes "induced_subgraph H G"
shows "sym_digraph H"
proof (rule wf_digraph.sym_digraphI)
from assms show "wf_digraph H" by (rule wf_digraphI_induced)
next
show "symmetric H"
using assms sym_arcs by (auto intro: induced_graph_imp_symmetric)
qed

lemma (in wf_digraph) induce_reachable_preserves_paths:
assumes "u →⇧*⇘G⇙ v"
shows "u →⇧*⇘G ↾ {w. u →⇧*⇘G⇙ w}⇙ v"
using assms
proof induct
case base then show ?case by (auto simp: reachable_def)
next
case (step u w)
interpret iG: wf_digraph "G ↾ {w. u →⇧*⇘G⇙ w}"
by (rule wellformed_induce_subgraph)
from ‹u → w› have "u →⇘G ↾ {wa. u →⇧*⇘G⇙ wa}⇙ w"
by (auto simp: arcs_ends_conv reachable_def intro: wellformed rtrancl_on_into_rtrancl_on)
then have "u →⇧*⇘G ↾ {wa. u →⇧*⇘G⇙ wa}⇙ w"
moreover
from step have "{x. w →⇧* x} ⊆ {x. u →⇧* x}"
then have "subgraph (G ↾ {wa. w →⇧* wa}) (G ↾ {wa. u →⇧* wa})"
by (intro subgraphI) (auto simp: arcs_ends_conv compatible_def)
then have "w →⇧*⇘G ↾ {wa. u →⇧* wa}⇙ v"
by (rule iG.reachable_mono[rotated]) fact
ultimately show ?case by (rule iG.reachable_trans)
qed

lemma induce_subgraph_ends[simp]:
"arc_to_ends (G ↾ S) = arc_to_ends G"
by (auto simp: arc_to_ends_def)

lemma dominates_induce_subgraphD:
assumes "u →⇘G ↾ S⇙ v" shows "u →⇘G⇙ v"
using assms by (auto simp: arcs_ends_def intro: rev_image_eqI)

context wf_digraph begin

lemma reachable_induce_subgraphD:
assumes "u →⇧*⇘G ↾ S⇙ v" "S ⊆ verts G" shows "u →⇧*⇘G⇙ v"
proof -
interpret GS: wf_digraph "G ↾ S" by auto
show ?thesis
using assms by induct (auto dest: dominates_induce_subgraphD intro: adj_reachable_trans)
qed

lemma dominates_induce_ss:
assumes "u →⇘G ↾ S⇙ v" "S ⊆ T" shows "u →⇘G ↾ T⇙ v"
using assms by (auto simp: arcs_ends_def)

lemma reachable_induce_ss:
assumes "u →⇧*⇘G ↾ S⇙ v" "S ⊆ T" shows "u →⇧*⇘G ↾ T⇙ v"
using assms unfolding reachable_def
by induct (auto intro: dominates_induce_ss converse_rtrancl_on_into_rtrancl_on)

lemma awalk_verts_induce:
"pre_digraph.awalk_verts (G ↾ S) = awalk_verts"
proof (intro ext)
fix u p show "pre_digraph.awalk_verts (G ↾ S) u p = awalk_verts u p"
by (induct p arbitrary: u) (auto simp: pre_digraph.awalk_verts.simps)
qed

lemma (in -) cas_subset:
assumes "pre_digraph.cas G u p v" "subgraph G H"
shows "pre_digraph.cas H u p v"
using assms
by (induct p arbitrary: u) (auto simp: pre_digraph.cas.simps subgraph_def compatible_def)

lemma cas_induce:
assumes "cas u p v" "set (awalk_verts u p) ⊆ S"
shows "pre_digraph.cas (G ↾ S) u p v"
using assms
proof (induct p arbitrary: u S)
case Nil then show ?case by (auto simp: pre_digraph.cas.simps)
next
case (Cons a as)
have "pre_digraph.cas (G ↾ set (awalk_verts (head G a) as)) (head G a) as v"
using Cons by auto
then have "pre_digraph.cas (G ↾ S) (head G a) as v"
using ‹_ ⊆ S› by (rule_tac cas_subset) (auto simp: subgraph_def compatible_def)
then show ?case using Cons by (auto simp: pre_digraph.cas.simps)
qed

lemma awalk_induce:
assumes "awalk u p v" "set (awalk_verts u p) ⊆ S"
shows "pre_digraph.awalk (G ↾ S) u p v"
proof -
interpret GS: wf_digraph "G ↾ S" by auto
show ?thesis
using assms by (auto simp: pre_digraph.awalk_def cas_induce GS.cas_induce set_awalk_verts)
qed

lemma subgraph_induce_subgraphI:
assumes "V ⊆ verts G" shows "subgraph (G ↾ V) G"
by (metis assms induced_imp_subgraph induced_induce)

end

lemma induced_subgraphI':
assumes subg:"subgraph H G"
assumes max: "⋀H'. subgraph H' G ⟹ (verts H' ≠ verts H ∨ arcs H' ⊆ arcs H)"
shows "induced_subgraph H G"
proof -
interpret H: wf_digraph H using ‹subgraph H G› ..
define H' where "H' = G ↾ verts H"
then have H'_props: "subgraph H' G" "verts H' = verts H"
using subg by (auto intro: wf_digraph.subgraph_induce_subgraphI)
moreover
have "arcs H' = arcs H"
proof
show "arcs H' ⊆ arcs H" using max H'_props by auto
show "arcs H ⊆ arcs H'" using subg by (auto simp: H'_def compatible_def)
qed
then show "induced_subgraph H G" by (auto simp: induced_subgraph_def H'_def subg)
qed

lemma (in pre_digraph) induced_subgraph_altdef:
"induced_subgraph H G ⟷ subgraph H G ∧ (∀H'. subgraph H' G ⟶ (verts H' ≠ verts H ∨ arcs H' ⊆ arcs H))" (is "?L ⟷ ?R")
proof -
{ fix H' :: "('a,'b) pre_digraph"
assume A: "verts H' = verts H" "subgraph H' G"
interpret H': wf_digraph H' using ‹subgraph H' G› ..
from ‹subgraph H' G›
have comp: "tail G = tail H'" "head G = head H'" by (auto simp: compatible_def)
then have "⋀a. a ∈ arcs H' ⟹ tail G a ∈ verts H" "⋀a. a ∈ arcs H' ⟹ tail G a ∈ verts H"
by (auto dest: H'.wellformed simp: A)
then have "arcs H' ⊆ {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}"
using ‹subgraph H' G› by (auto simp: subgraph_def comp A(1)[symmetric])
}
then show ?thesis using induced_subgraphI'[of H G] by (auto simp: induced_subgraph_def)
qed

subsection ‹Unions of Graphs›

lemma
verts_union[simp]: "verts (union G H) = verts G ∪ verts H" and
arcs_union[simp]: "arcs (union G H) = arcs G ∪ arcs H" and
tail_union[simp]: "tail (union G H) = tail G" and
by (auto simp: union_def)

lemma wellformed_union:
assumes "wf_digraph G" "wf_digraph H" "compatible G H"
shows "wf_digraph (union G H)"
using assms
by unfold_locales
(auto simp: union_def compatible_tail compatible_head dest: wf_digraph.wellformed)

lemma subgraph_union_iff:
assumes "wf_digraph H1" "wf_digraph H2" "compatible H1 H2"
shows "subgraph (union H1 H2) G ⟷ subgraph H1 G ∧ subgraph H2 G"
using assms by (fastforce simp: compatible_def intro!: subgraphI wellformed_union)

lemma subgraph_union[intro]:
assumes "subgraph H1 G" "compatible H1 G"
assumes "subgraph H2 G" "compatible H2 G"
shows "subgraph (union H1 H2) G"
proof -
from assms have "wf_digraph (union H1 H2)"
by (auto intro: wellformed_union simp: compatible_def)
with assms show ?thesis
by (auto simp add: subgraph_def union_def arc_to_ends_def compatible_def)
qed

lemma union_fin_digraph:
assumes "fin_digraph G" "fin_digraph H" "compatible G H"
shows "fin_digraph (union G H)"
proof intro_locales
interpret G: fin_digraph G by (rule assms)
interpret H: fin_digraph H by (rule assms)
show "wf_digraph (union G H)" using assms
by (intro wellformed_union) intro_locales
show "fin_digraph_axioms (union G H)"
using assms by unfold_locales (auto simp: union_def)
qed

lemma subgraphs_of_union:
assumes "wf_digraph G" "wf_digraph G'" "compatible G G'"
shows "subgraph G (union G G')"
and "subgraph G' (union G G')"
using assms by (auto intro!: subgraphI wellformed_union simp: compatible_def)

subsection ‹Maximal Subgraphs›

lemma (in pre_digraph) max_subgraph_mp:
assumes "max_subgraph Q x" "⋀x. P x ⟹ Q x" "P x" shows "max_subgraph P x"
using assms by (auto simp: max_subgraph_def)

lemma (in pre_digraph) max_subgraph_prop: "max_subgraph P x ⟹ P x"

lemma (in pre_digraph) max_subgraph_subg_eq:
assumes "max_subgraph P H1" "max_subgraph P H2" "subgraph H1 H2"
shows "H1 = H2"
using assms by (auto simp: max_subgraph_def)

lemma subgraph_induce_subgraphI2:
assumes "subgraph H G" shows "subgraph H (G ↾ verts H)"
using assms by (auto simp: subgraph_def compatible_def wf_digraph.wellformed wf_digraph.wellformed_induce_subgraph)

definition arc_mono :: "(('a,'b) pre_digraph ⇒ bool) ⇒ bool" where
"arc_mono P ≡ (∀H1 H2. P H1 ∧ subgraph H1 H2 ∧ verts H1 = verts H2 ⟶ P H2)"

lemma (in pre_digraph) induced_subgraphI_arc_mono:
assumes "max_subgraph P H"
assumes "arc_mono P"
shows "induced_subgraph H G"
proof -
interpret wf_digraph G using assms by (auto simp: max_subgraph_def)
have "subgraph H (G ↾ verts H)" "subgraph (G ↾ verts H) G" "verts H = verts (G ↾ verts H)" "P H"
using assms by (auto simp: max_subgraph_def subgraph_induce_subgraphI2 subgraph_induce_subgraphI)
moreover
then have "P (G ↾ verts  H)"
using assms by (auto simp: arc_mono_def)
ultimately
have "max_subgraph P (G ↾ verts H)"
using assms by (auto simp: max_subgraph_def) metis
then have "H = G ↾ verts H"
using ‹max_subgraph P H› ‹subgraph H _›
by (intro max_subgraph_subg_eq)
show ?thesis using assms by (subst ‹H = _›) (auto simp: max_subgraph_def)
qed

lemma (in pre_digraph) induced_subgraph_altdef2:
"induced_subgraph H G ⟷ max_subgraph (λH'. verts H' = verts H) H" (is "?L ⟷ ?R")
proof
assume ?L
moreover
{ fix H' assume "induced_subgraph H G" "subgraph H H'" "H ≠ H'"
then have "¬(subgraph H' G ∧ verts H' = verts H)"
by (auto simp: induced_subgraph_altdef compatible_def elim!: allE[where x=H'])
}
ultimately show "max_subgraph (λH'. verts H' = verts H) H" by (auto simp: max_subgraph_def)
next
assume ?R
moreover have "arc_mono (λH'. verts H' = verts H)" by (auto simp: arc_mono_def)
ultimately show ?L by (rule induced_subgraphI_arc_mono)
qed

(*XXX*)
lemma (in pre_digraph) max_subgraphI:
assumes "P x" "subgraph x G" "⋀y. ⟦x ≠ y; subgraph x y; subgraph y G⟧ ⟹ ¬P y"
shows "max_subgraph P x"
using assms by (auto simp: max_subgraph_def)

lemma (in pre_digraph) subgraphI_max_subgraph: "max_subgraph P x ⟹ subgraph x G"

subsection ‹Connected and Strongly Connected Graphs›

context wf_digraph begin

lemma in_sccs_verts_conv_reachable:
"S ∈ sccs_verts ⟷ S ≠ {} ∧ (∀u ∈ S. ∀v ∈ S. u →⇧*⇘G⇙ v) ∧ (∀u ∈ S. ∀v. v ∉ S ⟶ ¬u →⇧*⇘G⇙ v ∨ ¬v →⇧*⇘G⇙ u)"

lemma sccs_verts_disjoint:
assumes "S ∈ sccs_verts" "T ∈ sccs_verts" "S ≠ T" shows "S ∩ T = {}"
using assms unfolding in_sccs_verts_conv_reachable by safe meson+

lemma strongly_connected_spanning_imp_strongly_connected:
assumes "spanning H G"
assumes "strongly_connected H"
shows "strongly_connected G"
proof (unfold strongly_connected_def, intro ballI conjI)
from assms show "verts G ≠ {}" unfolding strongly_connected_def spanning_def by auto
next
fix u v assume "u ∈ verts G" and "v ∈ verts G"
then have "u →⇧*⇘H⇙ v" "subgraph H G"
using assms by (auto simp add: strongly_connected_def)
then show "u →⇧* v" by (rule reachable_mono)
qed

lemma strongly_connected_imp_induce_subgraph_strongly_connected:
assumes subg: "subgraph H G"
assumes sc: "strongly_connected H"
shows "strongly_connected (G ↾ (verts H))"
proof -
let ?is_H = "G ↾ (verts H)"

interpret H: wf_digraph H
using subg by (rule subgraphE)
interpret GrH: wf_digraph "?is_H"
by (rule wellformed_induce_subgraph)

have "verts H ⊆ verts G" using assms by auto

have "subgraph H (G ↾ verts H)"
using subg by (intro subgraphI) (auto simp: compatible_def)
then show ?thesis
using induced_induce[OF ‹verts H ⊆ verts G›]
and sc GrH.strongly_connected_spanning_imp_strongly_connected
unfolding spanning_def by auto
qed

lemma in_sccs_vertsI_sccs:
assumes "S ∈ verts  sccs" shows "S ∈ sccs_verts"
unfolding sccs_verts_def
proof (intro CollectI conjI allI ballI impI)
show "S ≠ {}" using assms by (auto simp: sccs_verts_def sccs_def strongly_connected_def)

from assms have sc: "strongly_connected (G ↾ S)" "S ⊆ verts G"
apply (auto simp: sccs_verts_def sccs_def)
by (metis induced_imp_subgraph subgraphE wf_digraph.strongly_connected_imp_induce_subgraph_strongly_connected)

{
fix u v assume A: "u ∈ S" "v ∈ S"
with sc have "u →⇧*⇘G ↾ S⇙ v" by auto
then show "u →⇧*⇘G⇙ v" using ‹S ⊆ verts G› by (rule reachable_induce_subgraphD)
next
fix u v assume A: "u ∈ S" "v ∉ S"
{ assume B: "u →⇧*⇘G⇙ v" "v →⇧*⇘G⇙ u"
from B obtain p_uv where p_uv: "awalk u p_uv v" by (metis reachable_awalk)
from B obtain p_vu where p_vu: "awalk v p_vu u" by (metis reachable_awalk)
define T where "T = S ∪ set (awalk_verts u p_uv) ∪ set (awalk_verts v p_vu)"
have "S ⊆ T" by (auto simp: T_def)
have "v ∈ T" using p_vu by (auto simp: T_def set_awalk_verts)
then have "T ≠ S" using ‹v ∉ S› by auto

interpret T: wf_digraph "G ↾ T" by auto

from p_uv have T_p_uv: "T.awalk u p_uv v"
by (rule awalk_induce) (auto simp: T_def)
from p_vu have T_p_vu: "T.awalk v p_vu u"
by (rule awalk_induce) (auto simp: T_def)

have uv_reach: "u →⇧*⇘G ↾ T⇙ v" "v →⇧*⇘G ↾ T⇙ u"
using T_p_uv T_p_vu A by (metis T.reachable_awalk)+

{ fix x y assume "x ∈ S" "y ∈ S"
then have "x →⇧*⇘G ↾ S⇙ y" "y →⇧*⇘G ↾ S⇙ x"
using sc by auto
then have "x →⇧*⇘G ↾ T⇙ y" "y →⇧*⇘G ↾ T⇙ x"
using ‹S ⊆ T› by (auto intro: reachable_induce_ss)
} note A1 = this

{ fix x assume "x ∈ T"
moreover
{ assume "x ∈ S" then have "x →⇧*⇘G ↾ T⇙ v"
using uv_reach A1 A by (auto intro: T.reachable_trans[rotated])
} moreover
{ assume "x ∈ set (awalk_verts u p_uv)" then have "x →⇧*⇘G ↾ T⇙ v"
using T_p_uv by (auto simp: awalk_verts_induce intro: T.awalk_verts_reachable_to)
} moreover
{ assume "x ∈ set (awalk_verts v p_vu)" then have "x →⇧*⇘G ↾ T⇙ v"
using T_p_vu by (rule_tac T.reachable_trans)
(auto simp: uv_reach awalk_verts_induce dest: T.awalk_verts_reachable_to)
} ultimately
have "x →⇧*⇘G ↾ T⇙ v" by (auto simp: T_def)
} note xv_reach = this

{ fix x assume "x ∈ T"
moreover
{ assume "x ∈ S" then have "v →⇧*⇘G ↾ T⇙ x"
using uv_reach A1 A by (auto intro: T.reachable_trans)
} moreover
{ assume "x ∈ set (awalk_verts v p_vu)" then have "v →⇧*⇘G ↾ T⇙ x"
using T_p_vu by (auto simp: awalk_verts_induce intro: T.awalk_verts_reachable_from)
} moreover
{ assume "x ∈ set (awalk_verts u p_uv)" then have "v →⇧*⇘G ↾ T⇙ x"
using T_p_uv by (rule_tac T.reachable_trans[rotated])
(auto intro: T.awalk_verts_reachable_from uv_reach simp: awalk_verts_induce)
} ultimately
have "v →⇧*⇘G ↾ T⇙ x" by (auto simp: T_def)
} note vx_reach = this

{ fix x y assume "x ∈ T" "y ∈ T" then have "x →⇧*⇘G ↾ T⇙ y"
using xv_reach vx_reach by (blast intro: T.reachable_trans)
}
then have "strongly_connected (G ↾ T)"
using ‹S ≠ {}› ‹S ⊆ T› by auto
moreover have "induced_subgraph (G ↾ T) G"
using ‹S ⊆ verts G›
by (auto simp: T_def intro: awalk_verts_reachable_from p_uv p_vu reachable_in_verts(2))
ultimately
have "∃T. induced_subgraph (G ↾ T) G ∧ strongly_connected (G ↾ T) ∧ verts (G ↾ S) ⊂ verts (G ↾ T)"
using ‹S ⊆ T› ‹T ≠ S› by auto
then have "G ↾ S ∉ sccs" unfolding sccs_def by blast
then have "S ∉ verts  sccs"
by (metis (erased, hide_lams) ‹S ⊆ T› ‹T ≠ S› ‹induced_subgraph (G ↾ T) G› ‹strongly_connected (G ↾ T)›
dual_order.order_iff_strict image_iff in_sccsE induce_subgraph_verts)
then have False using assms by metis
}
then show "¬u →⇧*⇘G⇙ v ∨ ¬v →⇧*⇘G⇙ u" by metis
}
qed

end

lemma arc_mono_strongly_connected[intro,simp]: "arc_mono strongly_connected"
by (auto simp: arc_mono_def) (metis spanning_def subgraphE wf_digraph.strongly_connected_spanning_imp_strongly_connected)

lemma (in pre_digraph) sccs_altdef2:
"sccs = {H. max_subgraph strongly_connected H}" (is "?L = ?R")
proof -
{ fix H H' :: "('a, 'b) pre_digraph"
assume a1: "strongly_connected H'"
assume a2: "induced_subgraph H' G"
assume a3: "max_subgraph strongly_connected H"
assume a4: "verts H ⊆ verts H'"
have sg: "subgraph H G" and ends_G: "tail G = tail H " "head G = head H"
using a3 by (auto simp: max_subgraph_def compatible_def)
then interpret H: wf_digraph H by blast
have "arcs H ⊆ arcs H'" using a2 a4 sg by (fastforce simp: ends_G)
then have "H = H'"
using a1 a2 a3 a4
by (metis (no_types) compatible_def induced_imp_subgraph max_subgraph_def subgraph_def)
} note X = this

{ fix H
assume a1: "induced_subgraph H G"
assume a2: "strongly_connected H"
assume a3: "∀H'. strongly_connected H' ⟶ induced_subgraph H' G ⟶ ¬ verts H ⊂ verts H'"
interpret G: wf_digraph G using a1 by auto
{ fix y assume "H ≠ y" and subg: "subgraph H y" "subgraph y G"
then have "verts H ⊂ verts y"
using a1 by (auto simp: induced_subgraph_altdef2 max_subgraph_def)
then have "¬strongly_connected y"
using subg a1 a2 a3[THEN spec, of "G ↾ verts y"]
by (auto simp: G.induced_induce G.strongly_connected_imp_induce_subgraph_strongly_connected)
}
then have "max_subgraph strongly_connected H"
using a1 a2 by (auto intro: max_subgraphI)
} note Y = this

show ?thesis unfolding sccs_def
by (auto dest: max_subgraph_prop X intro: induced_subgraphI_arc_mono Y)
qed

locale max_reachable_set = wf_digraph +
fixes S assumes S_in_sv: "S ∈ sccs_verts"
begin

lemma reach_in: "⋀u v. ⟦u ∈ S; v ∈ S⟧ ⟹ u →⇧*⇘G⇙ v"
and not_reach_out: "⋀u v. ⟦u ∈ S; v ∉ S⟧ ⟹ ¬u →⇧*⇘G⇙ v ∨ ¬v →⇧*⇘G⇙ u"
and not_empty: "S ≠ {}"
using S_in_sv by (auto simp: sccs_verts_def)

lemma reachable_induced:
assumes conn: "u ∈ S" "v ∈ S" "u →⇧*⇘G⇙ v"
shows "u →⇧*⇘G ↾ S⇙ v"
proof -
let ?H = "G ↾ S"
have "S ⊆ verts G" using reach_in by (auto dest: reachable_in_verts)
then have "induced_subgraph ?H G"
by (rule induced_induce)
then interpret H: wf_digraph ?H by (rule wf_digraphI_induced)

from conn obtain p where p: "awalk u p v" by (metis reachable_awalk)
show ?thesis
proof (cases "set p ⊆ arcs (G ↾ S)")
case True
with p conn have "H.awalk u p v"
by (auto simp: pre_digraph.awalk_def compatible_cas[OF compatible_induce_subgraph])
then show ?thesis by (metis H.reachable_awalk)
next
case False
then obtain a where "a ∈ set p" "a ∉ arcs (G ↾ S)" by auto
moreover
then have "tail G a ∉ S ∨ head G a ∉ S" using p by auto
ultimately
obtain w where "w ∈ set (awalk_verts u p)" "w ∉ S" using p by (auto simp: set_awalk_verts)
then have "u →⇧*⇘G⇙ w" "w →⇧*⇘G⇙ v"
using p by (auto intro: awalk_verts_reachable_from awalk_verts_reachable_to)
moreover have "v →⇧*⇘G⇙ u" using conn reach_in by auto
ultimately have "u →⇧*⇘G⇙ w" "w →⇧*⇘G⇙ u" by (auto intro: reachable_trans)
with ‹w ∉ S› conn not_reach_out have False by blast
then show ?thesis ..
qed
qed

lemma strongly_connected:
shows "strongly_connected (G ↾ S)"
using not_empty by (intro strongly_connectedI) (auto intro: reachable_induced reach_in)

lemma induced_in_sccs: "G ↾ S ∈ sccs"
proof -
let ?H = "G ↾ S"
have "S ⊆ verts G" using reach_in by (auto dest: reachable_in_verts)
then have "induced_subgraph ?H G"
by (rule induced_induce)
then interpret H: wf_digraph ?H by (rule wf_digraphI_induced)

{ fix T assume "S ⊂ T" "T ⊆ verts G" "strongly_connected (G ↾ T)"
from ‹S ⊂ T› obtain v where "v ∈ T" "v ∉ S" by auto
from not_empty obtain u where "u ∈ S" by auto
then have "u ∈ T" using ‹S ⊂ T› by auto

from ‹u ∈ S› ‹v ∉ S› have "¬u →⇧*⇘G⇙ v ∨ ¬v →⇧*⇘G⇙ u" by (rule not_reach_out)
moreover
from ‹strongly_connected _› have "u →⇧*⇘G ↾ T⇙ v" "v →⇧*⇘G ↾ T⇙ u"
using ‹v ∈ T› ‹u ∈ T› by (auto simp: strongly_connected_def)
then have "u →⇧*⇘G⇙ v" "v →⇧*⇘G⇙ u"
using ‹T ⊆ verts G› by (auto dest: reachable_induce_subgraphD)
ultimately have False by blast
} note psuper_not_sc = this

have "¬ (∃c'. induced_subgraph c' G ∧ strongly_connected c' ∧ verts (G ↾ S) ⊂ verts c')"
by (metis induce_subgraph_verts induced_imp_subgraph psuper_not_sc subgraphE
strongly_connected_imp_induce_subgraph_strongly_connected)
with ‹S ⊆ _› not_empty show "?H ∈ sccs" by (intro in_sccsI induced_induce strongly_connected)
qed
end

context wf_digraph begin

lemma in_verts_sccsD_sccs:
assumes "S ∈ sccs_verts"
shows "G ↾ S ∈ sccs"
proof -
from assms interpret max_reachable_set by unfold_locales
show ?thesis by (auto simp: sccs_verts_def intro: induced_in_sccs)
qed

lemma sccs_verts_conv: "sccs_verts = verts  sccs"
by (auto intro: in_sccs_vertsI_sccs rev_image_eqI dest: in_verts_sccsD_sccs)

lemma induce_eq_iff_induced:
assumes "induced_subgraph H G" shows "G ↾ verts H = H"
using assms by (auto simp: induced_subgraph_def induce_subgraph_def compatible_def)

lemma sccs_conv_sccs_verts: "sccs = induce_subgraph G  sccs_verts"
by (auto intro!: rev_image_eqI in_sccs_vertsI_sccs dest: in_verts_sccsD_sccs
simp: sccs_def induce_eq_iff_induced)

end

lemma connected_conv:
shows "connected G ⟷ verts G ≠ {} ∧ (∀u ∈ verts G. ∀v ∈ verts G. (u,v) ∈ rtrancl_on (verts G) ((arcs_ends G)⇧s))"
proof -
have "symcl (arcs_ends G) = parcs (mk_symmetric G)"
by (auto simp: parcs_mk_symmetric symcl_def arcs_ends_conv)
then show ?thesis by (auto simp: connected_def strongly_connected_def reachable_def)
qed

lemma (in wf_digraph) symmetric_connected_imp_strongly_connected:
assumes "symmetric G" "connected G"
shows "strongly_connected G"
proof
from ‹connected G› show "verts G ≠ {}" unfolding connected_def strongly_connected_def by auto
next
from ‹connected G›
have sc_mks: "strongly_connected (mk_symmetric G)"
unfolding connected_def by simp

fix u v assume "u ∈ verts G" "v ∈ verts G"
with sc_mks have "u →⇧*⇘mk_symmetric G⇙ v"
unfolding strongly_connected_def by auto
then show "u →⇧* v" using assms by (simp only: reachable_mk_symmetric_eq)
qed

lemma (in wf_digraph) connected_spanning_imp_connected:
assumes "spanning H G"
assumes "connected H"
shows "connected G"
proof (unfold connected_def strongly_connected_def, intro conjI ballI)
from assms show "verts (mk_symmetric G )≠ {}"
unfolding spanning_def connected_def strongly_connected_def by auto
next
fix u v
assume "u ∈ verts (mk_symmetric G)" and "v ∈ verts (mk_symmetric G)"
then have "u ∈ pverts (mk_symmetric H)" and "v ∈ pverts (mk_symmetric H)"
using ‹spanning H G› by (auto simp: mk_symmetric_def)
with ‹connected H›
have "u →⇧*⇘with_proj (mk_symmetric H)⇙ v" "subgraph (mk_symmetric H) (mk_symmetric G)"
using ‹spanning H G› unfolding connected_def
by (auto simp: spanning_def dest: subgraph_mk_symmetric)
then show "u →⇧*⇘mk_symmetric G⇙ v" by (rule pre_digraph.reachable_mono)
qed

lemma (in wf_digraph) spanning_tree_imp_connected:
assumes "spanning_tree H G"
shows "connected G"
using assms by (auto intro: connected_spanning_imp_connected)

term "LEAST x. P x"

lemma (in sym_digraph) induce_reachable_is_in_sccs:
assumes "u ∈ verts G"
shows "(G ↾ {v. u →⇧* v}) ∈ sccs"
proof -
let ?c = "(G ↾ {v. u →⇧* v})"
have isub_c: "induced_subgraph ?c G"
by (auto elim: reachable_in_vertsE)
then interpret c: wf_digraph ?c by (rule wf_digraphI_induced)

have sym_c: "symmetric (G ↾ {v. u →⇧* v})"
using sym_arcs isub_c by (rule induced_graph_imp_symmetric)

note ‹induced_subgraph ?c G›
moreover
have "strongly_connected ?c"
proof (rule strongly_connectedI)
show "verts ?c ≠ {}" using assms by auto
next
fix v w assume l_assms: "v ∈ verts ?c" "w ∈ verts ?c"
have "u →⇧*⇘G ↾ {v. u →⇧* v}⇙ v"
using l_assms by (intro induce_reachable_preserves_paths) auto
then have "v →⇧*⇘G ↾ {v. u →⇧* v}⇙ u" by (rule symmetric_reachable[OF sym_c])
also have "u →⇧*⇘G ↾ {v. u →⇧* v}⇙ w"
using l_assms by (intro induce_reachable_preserves_paths) auto
finally show "v →⇧*⇘G ↾ {v. u →⇧* v}⇙ w" .
qed
moreover
have "¬(∃d. induced_subgraph d G ∧ strongly_connected d ∧
verts ?c ⊂ verts d)"
proof
assume "∃d. induced_subgraph d G ∧ strongly_connected d ∧
verts ?c ⊂ verts d"
then obtain d where "induced_subgraph d G" "strongly_connected d"
"verts ?c ⊂ verts d" by auto
then obtain v where "v ∈ verts d" and "v ∉ verts ?c"
by auto

have "u ∈ verts ?c" using ‹u ∈ verts G› by auto
then have "u ∈ verts d" using ‹verts ?c ⊂ verts d› by auto
then have "u →⇧*⇘d⇙ v"
using ‹strongly_connected d› ‹u ∈ verts d› ‹v ∈ verts d› by auto
then have "u →⇧* v"
using ‹induced_subgraph d G›
by (auto intro: pre_digraph.reachable_mono)
then have "v ∈ verts ?c" by (auto simp: reachable_awalk)
then show False using ‹v ∉ verts ?c› by auto
qed
ultimately show ?thesis unfolding sccs_def by auto
qed

lemma induced_eq_verts_imp_eq:
assumes "induced_subgraph G H"
assumes "induced_subgraph G' H"
assumes "verts G = verts G'"
shows "G = G'"
using assms by (auto simp: induced_subgraph_def subgraph_def compatible_def)

lemma (in pre_digraph) in_sccs_subset_imp_eq:
assumes "c ∈ sccs"
assumes "d ∈ sccs"
assumes "verts c ⊆ verts d"
shows "c = d"
using assms by (blast intro: induced_eq_verts_imp_eq)

context wf_digraph begin

lemma connectedI:
assumes "verts G ≠ {}" "⋀u v. u ∈ verts G ⟹ v ∈ verts G ⟹ u →⇧*⇘mk_symmetric G⇙ v"
shows "connected G"
using assms by (auto simp: connected_def)

lemma connected_awalkE:
assumes "connected G" "u ∈ verts G" "v ∈ verts G"
obtains p where "pre_digraph.awalk (mk_symmetric G) u p v"
proof -
interpret sG: pair_wf_digraph "mk_symmetric G" ..
from assms have "u →⇧*⇘mk_symmetric G⇙ v" by (auto simp: connected_def)
then obtain p where "sG.awalk u p v" by (auto simp: sG.reachable_awalk)
then show ?thesis ..
qed

lemma inj_on_verts_sccs: "inj_on verts sccs"
by (rule inj_onI) (metis in_sccs_imp_induced induced_eq_verts_imp_eq)

lemma card_sccs_verts: "card sccs_verts = card sccs"
by (auto simp: sccs_verts_conv intro: inj_on_verts_sccs card_image)

end

lemma strongly_connected_non_disj:
assumes wf: "wf_digraph G" "wf_digraph H" "compatible G H"
assumes sc: "strongly_connected G" "strongly_connected H"
assumes not_disj: "verts G ∩ verts H ≠ {}"
shows "strongly_connected (union G H)"
proof
from sc show "verts (union G H) ≠ {}"
unfolding strongly_connected_def by simp
next
let ?x = "union G H"
fix u v w assume "u ∈ verts ?x" and "v ∈ verts ?x"
obtain w where w_in_both: "w ∈ verts G" "w ∈ verts H"
using not_disj by auto

interpret x: wf_digraph ?x
by (rule wellformed_union) fact+
have subg: "subgraph G ?x" "subgraph H ?x"
by (rule subgraphs_of_union[OF _ _ ], fact+)+
have reach_uw: "u →⇧*⇘?x⇙ w"
using ‹u ∈ verts ?x› subg w_in_both sc
by (auto intro: pre_digraph.reachable_mono)
also have reach_wv: "w →⇧*⇘?x⇙ v"
using ‹v ∈ verts ?x› subg w_in_both sc
by (auto intro: pre_digraph.reachable_mono)
finally (x.reachable_trans) show "u →⇧*⇘?x⇙ v" .
qed

context wf_digraph begin

lemma scc_disj:
assumes scc: "c ∈ sccs" "d ∈ sccs"
assumes "c ≠ d"
shows "verts c ∩ verts d = {}"
proof (rule ccontr)
assume contr: "¬?thesis"

let ?x = "union c d"

have comp1: "compatible G c" "compatible G d"
using scc by (auto simp: sccs_def)
then have comp: "compatible c d" by (auto simp: compatible_def)

have wf: "wf_digraph c" "wf_digraph d"
and sc: "strongly_connected c" "strongly_connected d"
using scc by (auto intro: in_sccs_imp_induced)
have "compatible c d"
using comp by (auto simp: sccs_def compatible_def)
from wf comp sc have union_conn: "strongly_connected ?x"
using contr by (rule strongly_connected_non_disj)

have sg: "subgraph ?x G"
using scc comp1 by (intro subgraph_union) (auto simp: compatible_def)
then have v_cd: "verts c ⊆ verts G"  "verts d ⊆ verts G" by (auto elim!: subgraphE)
have "wf_digraph ?x" by (rule wellformed_union) fact+
with v_cd sg union_conn
have induce_subgraph_conn: "strongly_connected (G ↾ verts ?x)"
"induced_subgraph (G ↾ verts ?x) G"
by - (intro strongly_connected_imp_induce_subgraph_strongly_connected,
auto simp: subgraph_union_iff)

from assms have "¬verts c ⊆ verts d" and "¬ verts d ⊆ verts c"
by (metis in_sccs_subset_imp_eq)+
then have psub: "verts c ⊂ verts ?x"
by (auto simp: union_def)
then show False using induce_subgraph_conn
by (metis ‹c ∈ sccs› in_sccsE induce_subgraph_verts)
qed

lemma in_sccs_verts_conv:
"S ∈ sccs_verts ⟷ G ↾ S ∈ sccs"
by (auto simp: sccs_verts_conv intro: rev_image_eqI)
(metis in_sccs_imp_induced induce_subgraph_verts induced_eq_verts_imp_eq induced_imp_subgraph induced_induce subgraphE)

end

lemma (in wf_digraph) in_scc_of_self: "u ∈ verts G ⟹ u ∈ scc_of u"
by (auto simp: scc_of_def)

lemma (in wf_digraph) scc_of_empty_conv: "scc_of u = {} ⟷ u ∉ verts G"
using in_scc_of_self by (auto simp: scc_of_def reachable_in_verts)

lemma (in wf_digraph) scc_of_in_sccs_verts:
assumes "u ∈ verts G" shows "scc_of u ∈ sccs_verts"
using assms by (auto simp: in_sccs_verts_conv_reachable scc_of_def intro: reachable_trans exI[where x=u])

lemma (in wf_digraph) sccs_verts_subsets: "S ∈ sccs_verts ⟹ S ⊆ verts G"
by (auto simp: sccs_verts_conv)

lemma (in fin_digraph) finite_sccs_verts: "finite sccs_verts"
proof -
have "finite (Pow (verts G))" by auto
moreover with sccs_verts_subsets have "sccs_verts ⊆ Pow (verts G)" by auto
ultimately show ?thesis by (rule rev_finite_subset)
qed

lemma (in wf_digraph) sccs_verts_conv_scc_of:
"sccs_verts = scc_of  verts G" (is "?L = ?R")
proof (intro set_eqI iffI)
fix S assume "S ∈ ?R" then show "S ∈ ?L"
by (auto simp: in_sccs_verts_conv_reachable scc_of_empty_conv) (auto simp: scc_of_def intro: reachable_trans)
next
fix S assume "S ∈ ?L"
moreover
then obtain u where "u ∈ S" by (auto simp: in_sccs_verts_conv_reachable)
moreover
then have "u ∈ verts G" using ‹S ∈ ?L› by (metis sccs_verts_subsets subsetCE)
then have "scc_of u ∈ sccs_verts" "u ∈ scc_of u"
by (auto intro: scc_of_in_sccs_verts in_scc_of_self)
ultimately
have "scc_of u = S" using sccs_verts_disjoint by blast
then show "S ∈ ?R" using ‹scc_of u ∈ _› ‹u ∈ verts G› by auto
qed

lemma (in sym_digraph) scc_ofI_reachable:
assumes "u →⇧* v" shows "u ∈ scc_of v"
using assms by (auto simp: scc_of_def symmetric_reachable[OF sym_arcs])

lemma (in sym_digraph) scc_ofI_reachable':
assumes "v →⇧* u" shows "u ∈ scc_of v"
using assms by (auto simp: scc_of_def symmetric_reachable[OF sym_arcs])

lemma (in sym_digraph) scc_ofI_awalk:
assumes "awalk u p v" shows "u ∈ scc_of v"
using assms by (metis reachable_awalk scc_ofI_reachable)

lemma (in sym_digraph) scc_ofI_apath:
assumes "apath u p v" shows "u ∈ scc_of v"
using assms by (metis reachable_apath scc_ofI_reachable)

lemma (in wf_digraph) scc_of_eq: "u ∈ scc_of v ⟹ scc_of u = scc_of v"
by (auto simp: scc_of_def intro: reachable_trans)

lemma (in wf_digraph) strongly_connected_eq_iff:
"strongly_connected G ⟷ sccs = {G}" (is "?L ⟷ ?R")
proof
assume ?L
then have "G ∈ sccs" by (auto simp: sccs_def induced_subgraph_refl)
moreover
{ fix H assume "H ∈ sccs" "G ≠ H"
with ‹G ∈ sccs› have "verts G ∩ verts H = {}" by (rule scc_disj)
moreover
from ‹H ∈ sccs› have "verts H ⊆ verts G" by auto
ultimately
have "verts H = {}" by auto
with ‹H ∈ sccs› have "False" by (auto simp: sccs_def strongly_connected_def)
} ultimately
show ?R by auto
qed (auto simp: sccs_def)

subsection ‹Components›

lemma (in sym_digraph) exists_scc:
assumes "verts G ≠ {}" shows "∃c. c ∈ sccs"
proof -
from assms obtain u where "u ∈ verts G" by auto
then show ?thesis by (blast dest: induce_reachable_is_in_sccs)
qed

theorem (in sym_digraph) graph_is_union_sccs:
shows "Union sccs = G"
proof -
have "(⋃c ∈ sccs. verts c) = verts G"
by (auto intro: induce_reachable_is_in_sccs)
moreover
have "(⋃c ∈ sccs. arcs c) = arcs G"
proof
show "(⋃c ∈ sccs. arcs c) ⊆ arcs G"
by safe (metis in_sccsE induced_imp_subgraph subgraphE subsetD)
show "arcs G ⊆ (⋃c ∈ sccs. arcs c)"
proof (safe)
fix e assume "e ∈ arcs G"
define a b where [simp]: "a = tail G e" and [simp]: "b = head G e"

have "e ∈ (⋃x ∈ sccs. arcs x)"
proof cases
assume "∃x∈sccs. {a,b } ⊆ verts x"
then obtain c where "c ∈ sccs" and "{a,b} ⊆ verts c"
by auto
then have "e ∈ {e ∈ arcs G. tail G e ∈ verts c
∧ head G e ∈ verts c}" using ‹e ∈ arcs G› by auto
then have "e ∈ arcs c" using ‹c ∈ sccs› by blast
then show ?thesis using ‹c ∈ sccs› by auto
next
assume l_assm: "¬(∃x∈sccs. {a,b} ⊆ verts x)"

have "a →⇧* b" using ‹e ∈ arcs G›
by (metis a_def b_def reachable_adjI in_arcs_imp_in_arcs_ends)
then have "{a,b} ⊆ verts (G ↾ {v. a →⇧* v})" "a ∈ verts G"
by (auto elim: reachable_in_vertsE)
moreover
have "(G ↾ {v. a →⇧* v}) ∈ sccs"
using ‹a ∈ verts G› by (auto intro: induce_reachable_is_in_sccs)
ultimately
have False using l_assm by blast
then show ?thesis by simp
qed
then show "e ∈ (⋃c ∈ sccs. arcs c)" by auto
qed
qed
ultimately show ?thesis
qed

lemma (in sym_digraph) scc_for_vert_ex:
assumes "u ∈ verts G"
shows "∃c. c∈sccs ∧ u ∈ verts c"
using assms by (auto intro: induce_reachable_is_in_sccs)

lemma (in sym_digraph) scc_decomp_unique:
assumes "S ⊆ sccs" "verts (Union S) = verts G" shows "S = sccs"
proof (rule ccontr)
assume "S ≠ sccs"
with assms obtain c where "c ∈ sccs" and "c ∉ S" by auto
with assms have "⋀d. d ∈ S ⟹ verts c ∩ verts d = {}"
by (intro scc_disj) auto
then have "verts c ∩ verts (Union S) = {}"
by (auto simp: Union_def)
with assms have "verts c ∩ verts G = {}" by auto
moreover from ‹c ∈ sccs› obtain u where "u ∈ verts c ∩ verts G"
by (auto simp: sccs_def strongly_connected_def)
ultimately show False by blast
qed

end


# Theory Vertex_Walk

(* Title:  Vertex_Walk.thy
Author: Lars Noschinski, TU München
*)

theory Vertex_Walk
imports Arc_Walk
begin

section ‹Walks Based on Vertices›

text ‹
These definitions are here mainly for historical purposes, as they
do not really work with multigraphs. Consider using Arc Walks
›

type_synonym 'a vwalk = "'a list"

text ‹Computes the list of arcs belonging to a list of nodes›
fun vwalk_arcs :: "'a vwalk ⇒ ('a × 'a) list" where
"vwalk_arcs [] = []"
| "vwalk_arcs [x] = []"
| "vwalk_arcs (x#y#xs) = (x,y) # vwalk_arcs (y#xs)"

definition vwalk_length :: "'a vwalk ⇒ nat" where
"vwalk_length p ≡ length (vwalk_arcs p)"

lemma vwalk_length_simp[simp]:
shows "vwalk_length p = length p - 1"
by (induct p rule: vwalk_arcs.induct) (auto simp: vwalk_length_def)

definition vwalk :: "'a vwalk ⇒ ('a,'b) pre_digraph ⇒ bool" where
"vwalk p G ≡ set p ⊆ verts G ∧ set (vwalk_arcs p) ⊆ arcs_ends G ∧ p ≠ []"

definition vpath :: "'a vwalk ⇒ ('a,'b) pre_digraph ⇒ bool" where
"vpath p G ≡ vwalk p G ∧ distinct p"

text ‹For a given vwalk, compute a vpath with the same tail G and end›
function vwalk_to_vpath :: "'a vwalk ⇒ 'a vwalk" where
"vwalk_to_vpath [] = []"
| "vwalk_to_vpath (x # xs) = (if (x ∈ set xs)
then vwalk_to_vpath (dropWhile (λy. y ≠ x) xs)
else x # vwalk_to_vpath xs)"
by p`