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 Gv"
  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 *Gv" obtains "u  verts G" "v  verts G"
  using assms unfolding reachable_def by induct auto

lemma symmetric_reachable:
  assumes "symmetric G" "v *Gw" shows "w *Gv"
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 *Gv  (u, v)  (arcs_ends G)*"
  unfolding reachable_def by (rule rtrancl_on_rtranclI)


context wf_digraph begin

lemma adj_in_verts:
  assumes "u Gv" 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 Gv"
  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 Gb" "b *Gc" shows "a *Gc"
  using assms by (auto simp: reachable_def intro: converse_rtrancl_on_into_rtrancl_on adj_in_verts)

lemma reachable_adj_trans[trans]:
  assumes "a *Gb" "b Gc" shows "a *Gc"
  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 *Gv"
    and cases: "u  verts G  P u"
       "x y. u *Gx; x Gy; 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 *Gv"
    and cases: "v  verts G  P v"
       "x y. x Gy; y *Gv; 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 *Gv"
  obtains (base) "u = v" "u  verts G"
    | (step) w where "u Gw" "w *Gv"
  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 *Gw" shows "w *Gv"
  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