Theory CAVA_Automata.Digraph_Basic

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

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

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


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

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

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

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

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

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

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

lemma path_conc: 
  assumes P1: "path E u la v" 
  assumes P2: "path E v lb w"
  shows "path E u (la@lb) w"
  using P1 P2 apply induct 
  by (auto intro: path.intros)
  
lemma path_append:
  "⟦ path E u l v; (v,w)∈E ⟧ ⟹ path E u (l@[v]) w"
  using path_conc[OF _ path1] .

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

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

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

lemmas path_simps = path_empty_conv path_cons_conv path_conc_conv


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


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

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


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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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


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

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

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


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

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

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



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

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


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


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

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

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

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


lemma ipath_subpath:
  assumes P: "ipath E r"
  assumes LE: "l≤u"
  shows "path E (r l) (map r [l..<u]) (r u)"
  using LE
proof (induction "u-l" arbitrary: u l)
  case (Suc n)
  note IH=Suc.hyps(1)
  from ‹Suc n = u-l› ‹l≤u› obtain u' where [simp]: "u=Suc u'" 
    and A: "n=u'-l" "l ≤ u'" 
    by (cases u) auto
    
  note IH[OF A]
  also from P have "(r u',r u)∈E"
    by (auto simp: ipath_def)
  finally show ?case using ‹l ≤ u'› by (simp add: upt_Suc_append)
qed auto  

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


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

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

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

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

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

subsection ‹Strongly Connected Components›

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

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

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

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

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

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

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

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

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

text ‹‹mconn› is an equivalence relation:›
lemma mconn_refl[simp]: "Id⊆mconn E"
  by (auto simp add: mconn_def)

lemma mconn_sym: "mconn E = (mconn E)¯"
  by (auto simp add: mconn_pointwise)

lemma mconn_trans: "mconn E O mconn E = mconn E"
  by (auto simp add: mconn_def)

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

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

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

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


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

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

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

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

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

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

lemma is_scc_restrict3: 
  assumes SCC: "is_scc E U"
  shows "((E⇧*``((E⇧*``U) - U)) ∩ U = {})"
  apply auto
  by (metis assms is_scc_closed is_scc_connected rtrancl_trans)
  
lemma is_scc_alt_restrict_path:
  "is_scc E U ⟷ U≠{} ∧
    (U×U ⊆ (E∩U×U)⇧*) ∧ ((E⇧*``((E⇧*``U) - U)) ∩ U = {})"
  apply rule
  apply (intro conjI)
  apply simp
  apply (blast dest: is_scc_restrict1)
  apply (blast dest: is_scc_restrict3)
  
  unfolding is_scc_def
  apply rule
  apply clarsimp
  apply (metis (full_types) Int_lower1 in_mono mem_Sigma_iff rtrancl_mono_mp)
  apply blast
  done

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

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

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

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

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

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

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

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

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

end