section ‹Invariants for Tarjan's Algorithm› theory Tarjan_LowLink imports "../DFS_Framework" "../Invars/DFS_Invars_SCC" begin context param_DFS_defs begin definition "lowlink_path s v p w ≡ path E v p w ∧ p ≠ [] ∧ (last p, w) ∈ cross_edges s ∪ back_edges s ∧ (length p > 1 ⟶ p!1 ∈ dom (finished s) ∧ (∀k < length p - 1. (p!k, p!Suc k) ∈ tree_edges s))" definition "lowlink_set s v ≡ {w ∈ dom (discovered s). v = w ∨ (v,w) ∈ E⇧^{+}∧ (w,v) ∈ E⇧^{+}∧ (∃p. lowlink_path s v p w)}" context begin interpretation timing_syntax . abbreviation LowLink where "LowLink s v ≡ Min (δ s ` lowlink_set s v)" end end context DFS_invar begin lemma lowlink_setI: assumes "lowlink_path s v p w" and "w ∈ dom (discovered s)" and "(v,w) ∈ E⇧^{*}" "(w,v) ∈ E⇧^{*}" shows "w ∈ lowlink_set s v" proof (cases "v = w") case True thus ?thesis by (simp add: lowlink_set_def assms) next case False with assms have "(v,w) ∈ E⇧^{+}" "(w,v) ∈ E⇧^{+}" by (metis rtrancl_eq_or_trancl)+ with assms show ?thesis by (auto simp add: lowlink_set_def) qed lemma lowlink_set_discovered: "lowlink_set s v ⊆ dom (discovered s)" unfolding lowlink_set_def by blast lemma lowlink_set_finite[simp, intro!]: "finite (lowlink_set s v)" using lowlink_set_discovered discovered_finite by (metis finite_subset) lemma lowlink_set_not_empty: assumes "v ∈ dom (discovered s)" shows "lowlink_set s v ≠ {}" unfolding lowlink_set_def using assms by auto lemma lowlink_path_single: assumes "(v,w) ∈ cross_edges s ∪ back_edges s" shows "lowlink_path s v [v] w" unfolding lowlink_path_def using assms cross_edges_ssE back_edges_ssE by (auto simp add: path_simps) lemma lowlink_path_Cons: assumes "lowlink_path s v (x#xs) w" and "xs ≠ []" shows "∃u. lowlink_path s u xs w" proof - from assms have path: "path E v (x#xs) w" and cb: "(last xs, w) ∈ cross_edges s ∪ back_edges s" and f: "(x#xs)!1 ∈ dom (finished s)" and t: "(∀k < length xs. ((x#xs)!k, (x#xs)!Suc k) ∈ tree_edges s)" unfolding lowlink_path_def by auto from path obtain u where "path E u xs w" by (auto simp add: path_simps) moreover note cb ‹xs ≠ []› moreover { fix k define k' where "k' = Suc k" assume "k < length xs - 1" with k'_def have "k' < length xs" by simp with t have "((x#xs)!k', (x#xs)!Suc k') ∈ tree_edges s" by simp hence "(xs!k,xs!Suc k) ∈ tree_edges s" by (simp add: k'_def nth_Cons') } note t' = this moreover { assume *: "length xs > 1" from f have "xs!0 ∈ dom (finished s)" by auto moreover from t'[of 0] * have "(xs!0,xs!1) ∈ tree_edges s" by simp ultimately have "xs!1 ∈ dom (finished s)" using tree_edge_impl_parenthesis by metis } ultimately have "lowlink_path s u xs w" by (auto simp add: lowlink_path_def) thus ?thesis .. qed lemma lowlink_path_in_tree: assumes p: "lowlink_path s v p w" and j: "j < length p" and k: "k < j" shows "(p!k, p!j) ∈ (tree_edges s)⇧^{+}" proof - from p have "p ≠ []" by (auto simp add: lowlink_path_def) thus ?thesis using p j k proof (induction arbitrary: v j k rule: list_nonempty_induct) case single thus ?case by auto next case (cons x xs) define j' where "j' = j - 1" with cons have j'_le: "j' < length xs" and "k ≤ j'" and j: "j = Suc j'" by auto from cons lowlink_path_Cons obtain u where p: "lowlink_path s u xs w" by blast show ?case proof (cases "k=0") case True from cons have "⋀k. k < length (x#xs) - 1 ⟹ ((x#xs)!k,(x#xs)!Suc k) ∈ tree_edges s" unfolding lowlink_path_def by auto moreover from True cons have "k < length (x#xs) - 1" by auto ultimately have *: "((x#xs)!k,(x#xs)!Suc k) ∈ tree_edges s" by metis show ?thesis proof (cases "j' = 0") case True with * j ‹k=0› show ?thesis by simp next case False with True have "j' > k" by simp with cons.IH[OF p j'_le] have "(xs!k, xs!j') ∈ (tree_edges s)⇧^{+}" . with j have "((x#xs)!Suc k, (x#xs)!j) ∈ (tree_edges s)⇧^{+}" by simp with * show ?thesis by (metis trancl_into_trancl2) qed next case False define k' where "k' = k - 1" with False ‹k ≤ j'› have "k' < j'" and k: "k = Suc k'" by simp_all with cons.IH[OF p j'_le] have "(xs!k', xs!j') ∈ (tree_edges s)⇧^{+}" by metis hence "((x#xs)!Suc k', (x#xs)!Suc j') ∈ (tree_edges s)⇧^{+}" by simp with k j show ?thesis by simp qed qed qed lemma lowlink_path_finished: assumes p: "lowlink_path s v p w" and j: "j < length p" "j > 0" shows "p!j ∈ dom (finished s)" proof - from j have "length p > 1" by simp with p have f: "p!1 ∈ dom (finished s)" by (simp add: lowlink_path_def) thus ?thesis proof (cases "j=1") case False with j have "j > 1" by simp with assms lowlink_path_in_tree[where k=1] have "(p!1,p!j) ∈ (tree_edges s)⇧^{+}" by simp with f tree_path_impl_parenthesis show ?thesis by simp qed simp qed lemma lowlink_path_tree_prepend: assumes p: "lowlink_path s v p w" and tree_edges: "(u,v) ∈ (tree_edges s)⇧^{+}" and fin: "u ∈ dom (finished s) ∨ (stack s ≠ [] ∧ u = hd (stack s))" shows "∃p. lowlink_path s u p w" proof - note lowlink_path_def[simp] from tree_edges trancl_is_path obtain tp where tp: "path (tree_edges s) u tp v" "tp ≠ []" by metis from tree_path_impl_parenthesis assms hd_stack_tree_path_finished have v_fin: "v ∈ dom (finished s)" by blast from p have "p!0 = hd p" by (simp add: hd_conv_nth) with p have p_0: "p!0 = v" by (auto simp add: path_hd) let ?p = "tp @ p" { from tp path_mono[OF tree_edges_ssE] have "path E u tp v" by simp also from p have "path E v p w" by simp finally have "path E u ?p w" . } moreover from p have "?p ≠ []" by simp moreover from p have "(last ?p, w) ∈ cross_edges s ∪ back_edges s" by simp moreover { assume "length ?p > 1" have "?p ! 1 ∈ dom (finished s)" proof (cases "length tp > 1") case True hence tp1: "?p ! 1 = tp ! 1" by (simp add: nth_append) from tp True have "(tp ! 0, tp ! 1) ∈ (tree_edges s)⇧^{+}" by (auto simp add: path_nth_conv nth_append elim: allE[where x=0]) also from True have "tp ! 0 = hd tp" by (simp add: hd_conv_nth) also from tp have "hd tp = u" by (simp add: path_hd) finally have "tp ! 1 ∈ dom (finished s)" using tree_path_impl_parenthesis fin hd_stack_tree_path_finished by blast thus ?thesis by (subst tp1) next case False with tp have "length tp = 1" by (cases tp) auto with p_0 have "?p ! 1 = v" by (simp add: nth_append) thus ?thesis by (simp add: v_fin) qed also have "∀k < length ?p - 1. (?p!k, ?p!Suc k) ∈ tree_edges s" proof (safe) fix k assume A: "k < length ?p - 1" show "(?p!k, ?p!Suc k) ∈ tree_edges s" proof (cases "k < length tp") case True hence k: "?p ! k = tp ! k" by (simp add: nth_append) show ?thesis proof (cases "Suc k < length tp") case True hence "?p ! Suc k = tp ! Suc k" by (simp add: nth_append) moreover from True tp have "(tp ! k, tp ! Suc k) ∈ tree_edges s" by (auto simp add: path_nth_conv nth_append elim: allE[where x=k]) ultimately show ?thesis using k by simp next case False with True have *: "Suc k = length tp" by simp with tp True have "(tp ! k, v) ∈ tree_edges s" by (auto simp add: path_nth_conv nth_append elim: allE[where x=k]) also from * p_0 have "v = ?p ! Suc k" by (simp add: nth_append) finally show ?thesis by (simp add: k) qed next case False hence *: "Suc k - length tp = Suc (k - length tp)" by simp define k' where "k' = k - length tp" with False * have k': "?p ! k = p ! k'" "?p ! Suc k = p ! Suc k'" by (simp_all add: nth_append) from k'_def False A have "k' < length p - 1" by simp with p have "(p!k', p!Suc k') ∈ tree_edges s" by simp (* p is lowlink_path *) with k' show ?thesis by simp qed qed also (conjI) note calculation } ultimately have "lowlink_path s u ?p w" by simp thus ?thesis .. qed lemma lowlink_path_complex: assumes "(u,v) ∈ (tree_edges s)⇧^{+}" and "u ∈ dom (finished s) ∨ (stack s ≠ [] ∧ u = hd (stack s))" and "(v,w) ∈ cross_edges s ∪ back_edges s" shows "∃p. lowlink_path s u p w" proof - from assms lowlink_path_single have "lowlink_path s v [v] w" by simp with assms lowlink_path_tree_prepend show ?thesis by simp qed lemma no_path_imp_no_lowlink_path: assumes "edges s `` {v} = {}" shows "¬lowlink_path s v p w" proof assume p: "lowlink_path s v p w" hence [simp]: "p≠[]" by (simp add: lowlink_path_def) from p have "hd p = v" by (auto simp add: lowlink_path_def path_hd) with hd_conv_nth[OF ‹p≠[]›] have v: "p!0 = v" by simp show False proof (cases "length p > 1") case True with p have "(p!0,p!1) ∈ tree_edges s" by (simp add: lowlink_path_def) with v assms show False by auto next case False with ‹p≠[]› have "length p = 1" by (cases p) auto hence "last p = v" by (simp add: last_conv_nth v) with p have "(v,w) ∈ edges s" by (simp add: lowlink_path_def) with assms show False by auto qed qed context begin interpretation timing_syntax . lemma LowLink_le_disc: assumes "v ∈ dom (discovered s)" shows "LowLink s v ≤ δ s v" using assms unfolding lowlink_set_def by clarsimp lemma LowLink_lessE: assumes "LowLink s v < x" and "v ∈ dom (discovered s)" obtains w where "δ s w < x" "w ∈ lowlink_set s v" proof - let ?L = "δ s ` lowlink_set s v" note assms moreover from lowlink_set_finite have "finite ?L" by auto moreover from lowlink_set_not_empty assms have "?L ≠ {}" by auto ultimately show ?thesis using that by (auto simp: Min_less_iff) qed lemma LowLink_lessI: assumes "y ∈ lowlink_set s v" and "δ s y < δ s v" shows "LowLink s v < δ s v" proof - let ?L = "δ s ` lowlink_set s v" from assms have "δ s y ∈ ?L" by simp moreover hence "?L ≠ {}" by auto moreover from lowlink_set_finite have "finite ?L" by auto ultimately show ?thesis by (metis Min_less_iff assms(2)) qed lemma LowLink_eqI: assumes "DFS_invar G param s'" assumes sub_m: "discovered s ⊆⇩_{m}discovered s'" assumes sub: "lowlink_set s w ⊆ lowlink_set s' w" and rev_sub: "lowlink_set s' w ⊆ lowlink_set s w ∪ X" and w_disc: "w ∈ dom (discovered s)" and X: "⋀x. ⟦x ∈ X; x ∈ lowlink_set s' w⟧ ⟹ δ s' x ≥ LowLink s w" shows "LowLink s w = LowLink s' w" proof (rule ccontr) interpret s': DFS_invar where s=s' by fact assume A: "LowLink s w ≠ LowLink s' w" from lowlink_set_discovered sub sub_m w_disc have sub': "δ s ` lowlink_set s w ⊆ δ s' ` lowlink_set s' w" and w_disc': "w ∈ dom (discovered s')" and eq: "⋀ll. ll ∈ lowlink_set s w ⟹ δ s' ll = δ s ll" by (force simp: map_le_def)+ from lowlink_set_not_empty[OF w_disc] A Min_antimono[OF sub'] s'.lowlink_set_finite have "LowLink s' w < LowLink s w" by fastforce then obtain ll where ll: "ll ∈ lowlink_set s' w" and ll_le: "δ s' ll < LowLink s w" by (metis s'.LowLink_lessE w_disc') with rev_sub have "ll ∈ lowlink_set s w ∨ ll ∈ X" by auto hence "LowLink s w ≤ δ s' ll" proof assume "ll ∈ lowlink_set s w" with lowlink_set_finite eq show ?thesis by force next assume "ll ∈ X" with ll show ?thesis by (metis X) qed with ll_le show False by simp qed lemma LowLink_eq_disc_iff_scc_root: assumes "v ∈ dom (finished s) ∨ (stack s ≠ [] ∧ v = hd (stack s) ∧ pending s `` {v} = {})" shows "LowLink s v = δ s v ⟷ scc_root s v (scc_of E v)" proof let ?scc = "scc_of E v" assume scc: "scc_root s v ?scc" show "LowLink s v = δ s v" proof (rule ccontr) assume A: "LowLink s v ≠ δ s v" from assms finished_discovered stack_discovered hd_in_set have disc: "v ∈ dom (discovered s)" by blast with assms LowLink_le_disc A have "LowLink s v < δ s v" by force with disc obtain w where w: "δ s w < δ s v" "w ∈ lowlink_set s v" by (metis LowLink_lessE) with lowlink_set_discovered have wdisc: "w ∈ dom (discovered s)" by auto from w have "(v,w) ∈ E⇧^{*}" "(w,v) ∈ E⇧^{*}" by (auto simp add: lowlink_set_def) moreover have "is_scc E ?scc" "v ∈ ?scc" by simp_all ultimately have "w ∈ ?scc" by (metis is_scc_closed) with wdisc scc_root_disc_le[OF scc] have "δ s v ≤ δ s w" by simp with w show False by auto qed next assume LL: "LowLink s v = δ s v" from assms finished_discovered stack_discovered hd_in_set have v_disc: "v ∈ dom (discovered s)" by blast from assms finished_no_pending have v_no_p: "pending s `` {v} = {}" by blast let ?scc = "scc_of E v" have is_scc: "is_scc E ?scc" by simp { fix r assume "r ≠ v" and "r ∈ ?scc" "r ∈ dom (discovered s)" have "v ∈ ?scc" by simp with ‹r ∈ ?scc› is_scc have "(v,r) ∈ (Restr E ?scc)⇧^{*}" by (simp add: is_scc_connected') hence "(v,r) ∈ (tree_edges s)⇧^{+}" using ‹r≠v› proof (induction rule: rtrancl_induct) case (step y z) hence "(v,z) ∈ (Restr E ?scc)⇧^{*}" by (metis rtrancl_into_rtrancl) hence "(v,z) ∈ E⇧^{*}" by (metis Restr_rtrancl_mono) from step have "(z,v) ∈ E⇧^{*}" by (simp add: is_scc_connected[OF is_scc]) { assume z_disc: "z ∈ dom (discovered s)" and "∃p. lowlink_path s v p z" with ‹(z,v)∈E⇧^{*}› ‹(v,z)∈E⇧^{*}› have ll: "z ∈ lowlink_set s v" by (metis lowlink_setI) have "δ s v < δ s z" proof (rule ccontr) presume "δ s v ≥ δ s z" with ‹z≠v› v_disc z_disc disc_unequal have "δ s z < δ s v" by fastforce with ll have "LowLink s v < δ s v" by (metis LowLink_lessI) with LL show False by simp qed simp } note δz = this show ?case proof (cases "y=v") case True note [simp] = this with step v_no_p v_disc no_pending_imp_succ_discovered have z_disc: "z ∈ dom (discovered s)" by blast from step edges_covered v_no_p v_disc have "(v,z) ∈ edges s" by auto thus ?thesis proof (rule edgesE_CB) assume "(v,z) ∈ tree_edges s" thus ?thesis .. next assume CB: "(v,z) ∈ cross_edges s ∪ back_edges s" hence "lowlink_path s v [v] z" by (simp add: lowlink_path_single) with δz[OF z_disc] no_pending_succ_impl_path_in_tree v_disc v_no_p step show ?thesis by auto qed next case False with step.IH have T: "(v,y) ∈ (tree_edges s)⇧^{+}" . with tree_path_impl_parenthesis assms hd_stack_tree_path_finished tree_path_disc have y_fin: "y ∈ dom (finished s)" and y_δ : "δ s v < δ s y" by blast+ with step have z_disc: "z ∈ dom (discovered s)" using finished_imp_succ_discovered by auto from step edges_covered finished_no_pending[of y] y_fin finished_discovered have "(y,z) ∈ edges s" by fast thus ?thesis proof (rule edgesE_CB) assume "(y,z) ∈ tree_edges s" with T show ?thesis .. next assume CB: "(y,z) ∈ cross_edges s ∪ back_edges s" with lowlink_path_complex[OF T] assms have "∃p. lowlink_path s v p z" by blast with δz z_disc have δz: "δ s v < δ s z" by simp show ?thesis proof (cases "v ∈ dom (finished s)") case True with tree_path_impl_parenthesis T have y_f: "φ s y < φ s v" by blast from CB show ?thesis proof assume C: "(y,z) ∈ cross_edges s" with cross_edges_finished_decr y_fin y_f have "φ s z < φ s v" by force moreover note δz moreover from C cross_edges_target_finished have "z ∈ dom (finished s)" by simp ultimately show ?thesis using parenthesis_impl_tree_path[OF True] by metis next assume B: "(y,z) ∈ back_edges s" with back_edge_disc_lt_fin y_fin y_f have "δ s z < φ s v" by force moreover note δz z_disc ultimately have "z ∈ dom (finished s)" "φ s z < φ s v" using parenthesis_contained[OF True] by simp_all with δz show ?thesis using parenthesis_impl_tree_path[OF True] by metis qed next case False ― ‹‹v ∉ dom (finished s)›› with assms have st: "stack s ≠ []" "v = hd (stack s)" "pending s `` {v} = {}" by blast+ have "z ∈ dom (finished s)" proof (rule ccontr) assume "z ∉ dom (finished s)" with z_disc have "z ∈ set (stack s)" by (simp add: stack_set_def) with ‹z≠v› st have "z ∈ set (tl (stack s))" by (cases "stack s") auto with st tl_lt_stack_hd_discover δz show False by force qed with δz parenthesis_impl_tree_path_not_finished v_disc False show ?thesis by simp qed qed qed qed simp hence "r ∈ (tree_edges s)⇧^{*}`` {v}" by auto } hence "?scc ∩ dom (discovered s) ⊆ (tree_edges s)⇧^{*}`` {v}" by fastforce thus "scc_root s v ?scc" by (auto intro!: scc_rootI v_disc) qed end end end