Theory Graph_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"
  head :: "'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

lemmas wellformed = tail_in_verts head_in_verts

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,
  see also \<^cite>‹"harary1974nullgraph"›.
›
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)

lemma (in loopfree_digraph) adj_not_same:
  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

lemma adj_in_verts:
  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

lemma adj_reachable_trans[trans]:
  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)

lemma reachable_adj_trans[trans]:
  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"
  by (auto intro: adj_reachable_trans adj_in_verts)

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"
  using assms by induct (simp_all add: adj_in_verts)

lemma reachable1_in_verts:
  assumes "u →⇧+ v" shows "u ∈ verts G" "v ∈ verts G"
  using assms
  by induct (simp_all add: adj_in_verts)

lemma reachable1_reachable[intro]:
  "v →⇧+ w ⟹ v →⇧* w"
  unfolding reachable_def
  by (rule rtrancl_consistent_rtrancl_on) (simp_all add: reachable1_in_verts adj_in_verts)

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
  verts_add_arc_conv: "verts (add_arc a) = verts G ∪ {tail G a, head G a}" and
  arcs_add_arc: "arcs (add_arc a) = insert a (arcs G)" and
  tail_add_arc: "tail (add_arc a) = tail G" and
  head_add_arc: "head (add_arc a) = head G"
  by (auto simp: add_arc_def)

lemmas add_arc_simps[simp] = verts_add_arc arcs_add_arc tail_add_arc head_add_arc

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
  head_del_arc: "head (del_arc a) = head G"
  by (auto simp: del_arc_def)

lemmas del_arc_simps[simp] = verts_del_arc arcs_del_arc tail_del_arc head_del_arc

lemma
    verts_add_vert: "verts (pre_digraph.add_vert G u) = insert u (verts G)" and
    arcs_add_vert: "arcs (pre_digraph.add_vert G u) = arcs G" and
    tail_add_vert: "tail (pre_digraph.add_vert G u) = tail G" and
    head_add_vert: "head (pre_digraph.add_vert G u) = head G"
  by (auto simp: pre_digraph.add_vert_def)

lemmas add_vert_simps = verts_add_vert arcs_add_vert tail_add_vert head_add_vert

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
    head_del_vert: "head (pre_digraph.del_vert G u) = head 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

lemma add_add_arc_collapse[simp]: "pre_digraph.add_arc (add_arc a) a = add_arc a"
  by (auto simp: pre_digraph.add_arc_def)

lemma add_del_arc_collapse[simp]: "pre_digraph.add_arc (del_arc a) a = add_arc a"
  by (auto simp: pre_digraph.verts_add_arc_conv pre_digraph.add_arc_simps)

lemma del_add_arc_collapse[simp]:
  "⟦ tail G a ∈ verts G; head G a ∈ verts G ⟧ ⟹ pre_digraph.del_arc (add_arc a) a = del_arc a"
  by (auto simp: pre_digraph.add_arc_simps pre_digraph.del_arc_simps)

lemma del_del_arc_collapse[simp]: "pre_digraph.del_arc (del_arc a) a = del_arc a"
  by (auto simp: pre_digraph.add_arc_simps pre_digraph.del_arc_simps)

lemma add_arc_commute: "pre_digraph.add_arc (add_arc b) a = pre_digraph.add_arc (add_arc a) b"
  by (auto simp: pre_digraph.add_arc_def)

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)

lemma in_arcs_add_arc_iff:
  "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

lemma out_arcs_add_arc_iff:
  "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_add_arc[intro]:
  "wf_digraph (add_arc a)" by unfold_locales (auto simp: verts_add_arc_conv)

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)

lemma wf_digraph_add_vert: "wf_digraph (add_vert u)"
  by standard (auto simp: add_vert_simps)

lemma del_vert_add_vert:
  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

lemma in_degree_add_arc_iff:
  "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

lemma out_degree_add_arc_iff:
  "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