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