section ‹Basic Invariant Library› theory DFS_Invars_Basic imports "../Param_DFS" begin text ‹We provide more basic invariants of the DFS algorithm› subsection ‹Basic Timing Invariants› (* Timing *) abbreviation "the_discovered s v ≡ the (discovered s v)" abbreviation "the_finished s v ≡ the (finished s v)" locale timing_syntax begin (* Timing related syntax shortcuts *) notation the_discovered (‹δ›) notation the_finished (‹φ›) end context param_DFS begin context begin interpretation timing_syntax . definition "timing_common_inv s ≡ ― ‹‹δ s v < φ s v›› (∀v ∈ dom (finished s). δ s v < φ s v) ― ‹‹v ≠ w ⟶ δ s v ≠ δ s w ∧ φ s v ≠ φ s w›› ― ‹Can't use ‹card dom = card ran› as the maps may be infinite ...› ∧ (∀v ∈ dom (discovered s). ∀w ∈ dom (discovered s). v ≠ w ⟶ δ s v ≠ δ s w) ∧ (∀v ∈ dom (finished s). ∀w ∈ dom (finished s). v ≠ w ⟶ φ s v ≠ φ s w) ― ‹‹δ s v < counter ∧ φ s v < counter›› ∧ (∀v ∈ dom (discovered s). δ s v < counter s) ∧ (∀v ∈ dom (finished s). φ s v < counter s) ∧ (∀v ∈ dom (finished s). ∀w ∈ succ v. δ s w < φ s v)" lemma timing_common_inv: "is_invar timing_common_inv" proof (induction rule: is_invarI) case (finish s s') then interpret DFS_invar where s=s by simp from finish have NE: "stack s ≠ []" by (simp add: cond_alt) have *: "hd (stack s) ∉ dom (finished s)" "hd (stack s) ∈ dom (discovered s)" using stack_not_finished stack_discovered hd_in_set[OF NE] by blast+ from discovered_closed have "(E - pending s) `` {hd (stack s)} ⊆ dom (discovered s)" using hd_in_set[OF NE] by (auto simp add: discovered_closed_def) hence succ_hd: "pending s `` {hd (stack s)} = {} ⟹ succ (hd (stack s)) ⊆ dom (discovered s)" by blast from finish show ?case apply (simp add: timing_common_inv_def) apply (intro conjI) using * apply simp using * apply simp apply (metis less_irrefl) apply (metis less_irrefl) apply (metis less_SucI) apply (metis less_SucI) apply (blast dest!: succ_hd) using * apply simp done next case (discover s) then interpret DFS_invar where s=s by simp from discover show ?case apply (simp add: timing_common_inv_def) apply (intro conjI) using finished_discovered apply fastforce apply (metis less_irrefl) apply (metis less_irrefl) apply (metis less_SucI) apply (metis less_SucI) using finished_imp_succ_discovered apply fastforce done next case (new_root s s' v0) then interpret DFS_invar where s=s by simp from new_root show ?case apply (simp add: timing_common_inv_def) apply (intro conjI) using finished_discovered apply fastforce apply (metis less_irrefl) apply (metis less_irrefl) apply (metis less_SucI) apply (metis less_SucI) using finished_imp_succ_discovered apply fastforce done qed (simp_all add: timing_common_inv_def) end end context DFS_invar begin context begin interpretation timing_syntax . lemmas s_timing_common_inv = timing_common_inv[THEN make_invar_thm] lemma timing_less_counter: "v ∈ dom (discovered s) ⟹ δ s v < counter s" "v ∈ dom (finished s) ⟹ φ s v < counter s" using s_timing_common_inv by (auto simp add: timing_common_inv_def) lemma disc_lt_fin: "v ∈ dom (finished s) ⟹ δ s v < φ s v" using s_timing_common_inv by (auto simp add: timing_common_inv_def) lemma disc_unequal: assumes "v ∈ dom (discovered s)" "w ∈ dom (discovered s)" and "v ≠ w" shows "δ s v ≠ δ s w" using s_timing_common_inv assms by (auto simp add: timing_common_inv_def) lemma fin_unequal: assumes "v ∈ dom (finished s)" "w ∈ dom (finished s)" and "v ≠ w" shows "φ s v ≠ φ s w" using s_timing_common_inv assms by (auto simp add: timing_common_inv_def) lemma finished_succ_fin: assumes "v ∈ dom (finished s)" and "w ∈ succ v" shows "δ s w < φ s v" using assms s_timing_common_inv by (simp add: timing_common_inv_def) end end context param_DFS begin context begin interpretation timing_syntax . lemma i_prev_stack_discover_all: "is_invar (λs. ∀ n < length (stack s). ∀ v ∈ set (drop (Suc n) (stack s)). δ s (stack s ! n) > δ s v)" proof (induct rule: is_invarI) case (finish s) thus ?case by (cases "stack s") auto next case (discover s s' u v) hence EQ[simp]: "discovered s' = (discovered s)(v ↦ counter s)" "stack s' = v#stack s" by simp_all from discover interpret DFS_invar where s=s by simp from discover stack_discovered have v_ni: "v ∉ set (stack s)" by auto from stack_discovered timing_less_counter have "⋀w. w ∈ set (stack s) ⟹ δ s w < counter s" by blast with v_ni have "⋀w. w ∈ set (stack s) ⟹ δ s' w < δ s' v" by auto hence "⋀w. w ∈ set (drop (Suc 0) (stack s')) ⟹ δ s' w < δ s' (stack s' ! 0)" by auto moreover from v_ni have "⋀n. ⟦n < (length (stack s')); n > 0⟧ ⟹ δ s' (stack s' ! n) = δ s (stack s' ! n)" by auto with discover(1) v_ni have "⋀n. ⟦n < (length (stack s')) - 1; n > 0⟧ ⟹ ∀ w ∈ set (drop (Suc n) (stack s')). δ s' (stack s' ! n) > δ s' w" by (auto dest: in_set_dropD) ultimately show ?case by (metis drop_Suc_Cons length_drop length_pos_if_in_set length_tl list.sel(3) neq0_conv nth_Cons_0 EQ(2) zero_less_diff) qed simp_all end end context DFS_invar begin context begin interpretation timing_syntax . lemmas prev_stack_discover_all = i_prev_stack_discover_all[THEN make_invar_thm] lemma prev_stack_discover: "⟦n < length (stack s); v ∈ set (drop (Suc n) (stack s)) ⟧ ⟹ δ s (stack s ! n) > δ s v" by (metis prev_stack_discover_all) lemma Suc_stack_discover: assumes n: "n < (length (stack s)) - 1" shows "δ s (stack s ! n) > δ s (stack s ! Suc n)" proof - from prev_stack_discover assms have "⋀ v. v ∈ set (drop (Suc n) (stack s)) ⟹ δ s (stack s ! n) > δ s v" by fastforce moreover from n have "stack s ! Suc n ∈ set (drop (Suc n) (stack s))" using in_set_conv_nth by fastforce ultimately show ?thesis . qed lemma tl_lt_stack_hd_discover: assumes notempty: "stack s ≠ []" and "x ∈ set (tl (stack s))" shows "δ s x < δ s (hd (stack s))" proof - from notempty obtain y ys where "stack s = y#ys" by (metis list.exhaust) with assms show ?thesis using prev_stack_discover by (cases ys) force+ qed lemma stack_nth_order: assumes l: "i < length (stack s)" "j < length (stack s)" shows "δ s (stack s ! i) < δ s (stack s ! j) ⟷ i > j" (is "δ s ?i < δ s ?j ⟷ _") proof assume δ: "δ s ?i < δ s ?j" from l stack_set_def have disc: "?i ∈ dom (discovered s)" "?j ∈ dom (discovered s)" by auto with disc_unequal[OF disc] δ have "i ≠ j" by auto moreover { assume "i < j" with l have "stack s ! j ∈ set (drop (Suc i) (stack s))" using in_set_drop_conv_nth[of "stack s ! j" "Suc i" "stack s"] by fastforce with prev_stack_discover l have "δ s (stack s ! j) < δ s (stack s ! i)" by simp with δ have "False" by simp } ultimately show "i > j" by force next assume "i > j" with l have "stack s ! i ∈ set (drop (Suc j) (stack s))" using in_set_drop_conv_nth[of "stack s ! i" "Suc j" "stack s"] by fastforce with prev_stack_discover l show "δ s ?i < δ s ?j" by simp qed end end subsection ‹Paranthesis Theorem› (* Parenthesis Thm *) context param_DFS begin context begin interpretation timing_syntax . definition "parenthesis s ≡ ∀v ∈ dom (discovered s). ∀w ∈ dom (discovered s). δ s v < δ s w ∧ v ∈ dom (finished s) ⟶ ( φ s v < δ s w ― ‹disjoint› ∨ (φ s v > δ s w ∧ w ∈ dom (finished s) ∧ φ s w < φ s v))" lemma i_parenthesis: "is_invar parenthesis" proof (induct rule: is_invarI) case (finish s s') hence EQ[simp]: "discovered s' = discovered s" "counter s' = Suc (counter s)" "finished s' = (finished s)(hd (stack s) ↦ counter s)" by simp_all from finish interpret DFS_invar where s=s by simp from finish have NE[simp]: "stack s ≠ []" by (simp add: cond_alt) { fix x y assume dom: "x ∈ dom (discovered s')" "y ∈ dom (discovered s')" and δ: "δ s' x < δ s' y" and f: "x ∈ dom (finished s')" hence neq: "x ≠ y" by force note assms = dom δ f EQ let ?DISJ = "φ s' x < δ s' y" let ?IN = "δ s' y < φ s' x ∧ y ∈ dom (finished s') ∧ φ s' y < φ s' x" have "?DISJ ∨ ?IN" proof (cases "x = hd (stack s)") case True note x_is_hd = this hence φx: "φ s' x = counter s" by simp from x_is_hd neq have y_not_hd: "y ≠ hd (stack s)" by simp have "δ s y < φ s' x ∧ y ∈ dom (finished s) ∧ φ s y < φ s' x" proof (cases "y ∈ set (stack s)") ― ‹y on stack is not possible: According to @{thm [display] δ} it is discovered after @{text "x (= hd (stack s))"}› case True with y_not_hd have "y ∈ set (tl (stack s))" by (cases "stack s") simp_all with tl_lt_stack_hd_discover[OF NE] δ x_is_hd have "δ s y < δ s x" by simp with δ have False by simp thus ?thesis .. next case False ― ‹y must be a successor of @{text "x (= (hd (stack s)))"}› from dom have "y ∈ dom (discovered s)" by simp with False discovered_not_stack_imp_finished have *: "y ∈ dom (finished s)" by simp moreover with timing_less_counter φx have "φ s y < φ s' x" by simp moreover with * disc_lt_fin φx have "δ s y < φ s' x" by (metis less_trans) ultimately show ?thesis by simp qed with y_not_hd show ?thesis by simp next case False note [simp] = this show ?thesis proof (cases "y = hd (stack s)") case False with finish assms show ?thesis by (simp add: parenthesis_def) next case True with stack_not_finished have "y ∉ dom (finished s)" using hd_in_set[OF NE] by auto with finish assms have "φ s x < δ s y" unfolding parenthesis_def by auto hence ?DISJ by simp thus ?thesis .. qed qed } thus ?case by (simp add: parenthesis_def) next case (discover s s' u v) hence EQ[simp]: "discovered s' = (discovered s)(v ↦ counter s)" "finished s' = finished s" "counter s' = Suc (counter s)" by simp_all from discover interpret DFS_invar where s=s by simp from discover finished_discovered have V': "v ∉ dom (discovered s)" "v ∉ dom (finished s)" by auto { fix x y assume dom: "x ∈ dom (discovered s')" "y ∈ dom (discovered s')" and δ: "δ s' x < δ s' y" and f: "x ∈ dom (finished s')" let ?DISJ = "φ s' x < δ s' y" let ?IN = "δ s' y < φ s' x ∧ y ∈ dom (finished s') ∧ φ s' y < φ s' x" from dom V' f have x: "x ∈ dom (discovered s)""x ≠ v" by auto have "?DISJ ∨ ?IN" proof (cases "y = v") case True hence "δ s' y = counter s" by simp moreover from timing_less_counter x f have "φ s' x < counter s" by auto ultimately have "?DISJ" by simp thus ?thesis .. next case False with dom have "y ∈ dom (discovered s)" by simp with discover False δ f x show ?thesis by (simp add: parenthesis_def) qed } thus ?case by (simp add: parenthesis_def) next case (new_root s s' v0) then interpret DFS_invar where s=s by simp from finished_discovered new_root have "v0 ∉ dom (finished s')" by auto with new_root timing_less_counter show ?case by (simp add: parenthesis_def) qed (simp_all add: parenthesis_def) end end context DFS_invar begin context begin interpretation timing_syntax . lemma parenthesis: assumes "v ∈ dom (finished s)" "w ∈ dom (discovered s)" and "δ s v < δ s w" shows "φ s v < δ s w ― ‹disjoint› ∨ (φ s v > δ s w ∧ w ∈ dom (finished s) ∧ φ s w < φ s v)" using assms using i_parenthesis[THEN make_invar_thm] using finished_discovered unfolding parenthesis_def by blast lemma parenthesis_contained: assumes "v ∈ dom (finished s)" "w ∈ dom (discovered s)" and "δ s v < δ s w" "φ s v > δ s w" shows "w ∈ dom (finished s) ∧ φ s w < φ s v" using parenthesis assms by force lemma parenthesis_disjoint: assumes "v ∈ dom (finished s)" "w ∈ dom (discovered s)" and "δ s v < δ s w" "φ s w > φ s v" shows "φ s v < δ s w" using parenthesis assms by force lemma finished_succ_contained: assumes "v ∈ dom (finished s)" and "w ∈ succ v" and "δ s v < δ s w" shows "w ∈ dom (finished s) ∧ φ s w < φ s v" using finished_succ_fin finished_imp_succ_discovered parenthesis_contained using assms by metis end end subsection ‹Edge Types› context param_DFS begin abbreviation "edges s ≡ tree_edges s ∪ cross_edges s ∪ back_edges s" (* Demo for simple invariant proof *) lemma "is_invar (λs. finite (edges s))" by (induction rule: establish_invarI) auto text ‹Sometimes it's useful to just chose between tree-edges and non-tree.› lemma edgesE_CB: assumes "x ∈ edges s" and "x ∈ tree_edges s ⟹ P" and "x ∈ cross_edges s ∪ back_edges s ⟹ P" shows "P" using assms by auto definition "edges_basic s ≡ Field (back_edges s) ⊆ dom (discovered s) ∧ back_edges s ⊆ E - pending s ∧ Field (cross_edges s) ⊆ dom (discovered s) ∧ cross_edges s ⊆ E - pending s ∧ Field (tree_edges s) ⊆ dom (discovered s) ∧ tree_edges s ⊆ E - pending s ∧ back_edges s ∩ cross_edges s = {} ∧ back_edges s ∩ tree_edges s = {} ∧ cross_edges s ∩ tree_edges s = {} " lemma i_edges_basic: "is_invar edges_basic" unfolding edges_basic_def[abs_def] proof (induct rule: is_invarI_full) case (back_edge s) then interpret DFS_invar where s=s by simp from back_edge show ?case by (auto dest: pendingD) next case (cross_edge s) then interpret DFS_invar where s=s by simp from cross_edge show ?case by (auto dest: pendingD) next case (discover s) then interpret DFS_invar where s=s by simp from discover show ?case (* Speed optimized proof, using only auto takes too long *) apply (simp add: Field_def Range_def Domain_def) apply (drule pendingD) apply simp by (blast) next case (new_root s) thus ?case by (simp add: Field_def) blast qed auto lemmas (in DFS_invar) edges_basic = i_edges_basic[THEN make_invar_thm] lemma i_edges_covered: "is_invar (λs. (E ∩ dom (discovered s) × UNIV) - pending s = edges s)" proof (induction rule: is_invarI_full) case (new_root s s' v0) interpret DFS_invar G param s by fact from new_root empty_stack_imp_empty_pending have [simp]: "pending s = {}" by simp from ‹v0 ∉ dom (discovered s)› have [simp]: "E ∩ insert v0 (dom (discovered s)) × UNIV - {v0} × succ v0 = E ∩ dom (discovered s) × UNIV" by auto from new_root show ?case by simp next case (cross_edge s s' u v) interpret DFS_invar G param s by fact from cross_edge stack_discovered have "u ∈ dom (discovered s)" by (cases "stack s") auto with cross_edge(2-) pending_ssE have "E ∩ dom (discovered s) × UNIV - (pending s - {(hd (stack s), v)}) = insert (hd (stack s), v) (E ∩ dom (discovered s) × UNIV - pending s)" by auto thus ?case using cross_edge by simp next case (back_edge s s' u v) interpret DFS_invar G param s by fact from back_edge stack_discovered have "u ∈ dom (discovered s)" by (cases "stack s") auto with back_edge(2-) pending_ssE have "E ∩ dom (discovered s) × UNIV - (pending s - {(hd (stack s), v)}) = insert (hd (stack s), v) (E ∩ dom (discovered s) × UNIV - pending s)" by auto thus ?case using back_edge by simp next case (discover s s' u v) interpret DFS_invar G param s by fact from discover stack_discovered have "u ∈ dom (discovered s)" by (cases "stack s") auto with discover(2-) pending_ssE have "E ∩ insert v (dom (discovered s)) × UNIV - (pending s - {(hd (stack s), v)} ∪ {v} × succ v) = insert (hd (stack s), v) (E ∩ dom (discovered s) × UNIV - pending s)" by auto thus ?case using discover by simp qed simp_all end context DFS_invar begin lemmas edges_covered = i_edges_covered[THEN make_invar_thm] lemma edges_ss_reachable_edges: "edges s ⊆ E ∩ reachable × UNIV" using edges_covered discovered_reachable by (fast intro: rtrancl_image_advance_rtrancl) lemma nc_edges_covered: assumes "¬cond s" "¬is_break param s" shows "E ∩ reachable × UNIV = edges s" proof - from assms have [simp]: "stack s = []" unfolding cond_def by (auto simp: pred_defs) hence [simp]: "pending s = {}" by (rule empty_stack_imp_empty_pending) from edges_covered nc_discovered_eq_reachable[OF assms] show ?thesis by simp qed lemma tree_edges_ssE: "tree_edges s ⊆ E" and tree_edges_not_pending: "tree_edges s ⊆ - pending s" and tree_edge_is_succ: "(v,w) ∈ tree_edges s ⟹ w ∈ succ v" and tree_edges_discovered: "Field (tree_edges s) ⊆ dom (discovered s)" and cross_edges_ssE: "cross_edges s ⊆ E" and cross_edges_not_pending: "cross_edges s ⊆ - pending s" and cross_edge_is_succ: "(v,w) ∈ cross_edges s ⟹ w ∈ succ v" and cross_edges_discovered: "Field (cross_edges s) ⊆ dom (discovered s)" and back_edges_ssE: "back_edges s ⊆ E" and back_edges_not_pending: "back_edges s ⊆ - pending s" and back_edge_is_succ: "(v,w) ∈ back_edges s ⟹ w ∈ succ v" and back_edges_discovered: "Field (back_edges s) ⊆ dom (discovered s)" using edges_basic unfolding edges_basic_def by auto lemma edges_disjoint: "back_edges s ∩ cross_edges s = {}" "back_edges s ∩ tree_edges s = {}" "cross_edges s ∩ tree_edges s = {}" using edges_basic unfolding edges_basic_def by auto lemma tree_edge_imp_discovered: "(v,w) ∈ tree_edges s ⟹ v ∈ dom (discovered s)" "(v,w) ∈ tree_edges s ⟹ w ∈ dom (discovered s)" using tree_edges_discovered by (auto simp add: Field_def) lemma back_edge_imp_discovered: "(v,w) ∈ back_edges s ⟹ v ∈ dom (discovered s)" "(v,w) ∈ back_edges s ⟹ w ∈ dom (discovered s)" using back_edges_discovered by (auto simp add: Field_def) lemma cross_edge_imp_discovered: "(v,w) ∈ cross_edges s ⟹ v ∈ dom (discovered s)" "(v,w) ∈ cross_edges s ⟹ w ∈ dom (discovered s)" using cross_edges_discovered by (auto simp add: Field_def) lemma edge_imp_discovered: "(v,w) ∈ edges s ⟹ v ∈ dom (discovered s)" "(v,w) ∈ edges s ⟹ w ∈ dom (discovered s)" using tree_edge_imp_discovered cross_edge_imp_discovered back_edge_imp_discovered by blast+ lemma tree_edges_finite[simp, intro!]: "finite (tree_edges s)" using finite_subset[OF tree_edges_discovered discovered_finite] by simp lemma cross_edges_finite[simp, intro!]: "finite (cross_edges s)" using finite_subset[OF cross_edges_discovered discovered_finite] by simp lemma back_edges_finite[simp, intro!]: "finite (back_edges s)" using finite_subset[OF back_edges_discovered discovered_finite] by simp lemma edges_finite: "finite (edges s)" by auto end subsubsection ‹Properties of the DFS Tree› (* Tree *) context DFS_invar begin context begin interpretation timing_syntax . lemma tree_edge_disc_lt_fin: "(v,w) ∈ tree_edges s ⟹ v ∈ dom (finished s) ⟹ δ s w < φ s v" by (metis finished_succ_fin tree_edge_is_succ) lemma back_edge_disc_lt_fin: "(v,w) ∈ back_edges s ⟹ v ∈ dom (finished s) ⟹ δ s w < φ s v" by (metis finished_succ_fin back_edge_is_succ) lemma cross_edge_disc_lt_fin: "(v,w) ∈ cross_edges s ⟹ v ∈ dom (finished s) ⟹ δ s w < φ s v" by (metis finished_succ_fin cross_edge_is_succ) end end (* Stack & Tree *) context param_DFS begin lemma i_stack_is_tree_path: "is_invar (λs. stack s ≠ [] ⟶ (∃v0 ∈ V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))))" proof (induct rule: is_invarI) case (discover s s' u v) hence EQ[simp]: "stack s' = v # stack s" "tree_edges s' = insert (hd (stack s), v) (tree_edges s)" by simp_all from discover have NE[simp]: "stack s ≠ []" by simp from discover obtain v0 where "v0 ∈ V0" "path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))" by blast with path_mono[OF _ this(2)] EQ have "path (tree_edges s') v0 (rev (tl (stack s))) (hd (stack s))" by blast with ‹v0 ∈ V0› show ?case by (cases "stack s") (auto simp: path_simps) next case (finish s s') hence EQ[simp]: "stack s' = tl (stack s)" "tree_edges s' = tree_edges s" by simp_all from finish obtain v0 where "v0 ∈ V0" "path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))" by blast hence P: "path (tree_edges s') v0 (rev (stack s')) (hd (stack s))" by simp show ?case proof assume A: "stack s' ≠ []" with P have "(hd (stack s'), hd (stack s)) ∈ tree_edges s'" by (auto simp: neq_Nil_conv path_simps) moreover from P A have "path (tree_edges s') v0 (rev (tl (stack s')) @ [hd (stack s')]) (hd (stack s))" by (simp) moreover note ‹v0 ∈ V0› ultimately show "∃v0∈V0. path (tree_edges s') v0 (rev (tl (stack s'))) (hd (stack s'))" by (auto simp add: path_append_conv) qed qed simp_all end context DFS_invar begin lemmas stack_is_tree_path = i_stack_is_tree_path[THEN make_invar_thm, rule_format] lemma stack_is_path: "stack s ≠ [] ⟹ ∃v0∈V0. path E v0 (rev (tl (stack s))) (hd (stack s))" using stack_is_tree_path path_mono[OF tree_edges_ssE] by blast lemma hd_succ_stack_is_path: assumes ne: "stack s ≠ []" and succ: "v ∈ succ (hd (stack s))" shows "∃v0∈V0. path E v0 (rev (stack s)) v" proof - from stack_is_path[OF ne] succ obtain v0 where "v0 ∈ V0" "path E v0 (rev (tl (stack s)) @ [hd (stack s)]) v" by (auto simp add: path_append_conv) thus ?thesis using ne by (cases "stack s") auto qed lemma tl_stack_hd_tree_path: assumes "stack s ≠ []" and "v ∈ set (tl (stack s))" shows "(v, hd (stack s)) ∈ (tree_edges s)⇧^{+}" proof - from stack_is_tree_path assms obtain v0 where "path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))" by auto from assms path_member_reach_end[OF this] show ?thesis by simp qed end context param_DFS begin definition "tree_discovered_inv s ≡ (tree_edges s = {} ⟶ dom (discovered s) ⊆ V0 ∧ (stack s = [] ∨ (∃v0∈V0. stack s = [v0]))) ∧ (tree_edges s ≠ {} ⟶ (tree_edges s)⇧^{+}`` V0 ∪ V0 = dom (discovered s) ∪ V0)" lemma i_tree_discovered_inv: "is_invar tree_discovered_inv" proof (induct rule: is_invarI) case (discover s s' u v) hence EQ[simp]: "stack s' = v # stack s" "tree_edges s' = insert (hd (stack s), v) (tree_edges s)" "discovered s' = (discovered s)(v ↦ counter s)" by simp_all from discover interpret DFS_invar where s=s by simp from discover have NE[simp]: "stack s ≠ []" by simp note TDI = ‹tree_discovered_inv s›[unfolded tree_discovered_inv_def] have "tree_edges s' = {} ⟶ dom (discovered s') ⊆ V0 ∧ (stack s' = [] ∨ (∃v0∈V0. stack s' = [v0]))" by simp ― ‹@{text "tree_edges s' ≠ {}"}› moreover { fix x assume A: "x ∈ (tree_edges s')⇧^{+}`` V0 ∪ V0" "x ∉ V0" then obtain y where y: "(y,x) ∈ (tree_edges s')⇧^{+}" "y ∈ V0" by auto have "x ∈ dom (discovered s') ∪ V0" proof (cases "tree_edges s = {}") case True with discover A have "(tree_edges s')⇧^{+}= {(hd (stack s), v)}" by (simp add: trancl_single) with A show ?thesis by auto next case False note t_ne = this show ?thesis proof (cases "x = v") case True thus ?thesis by simp next case False with y have "(y,x) ∈ (tree_edges s)⇧^{+}" proof (induct rule: trancl_induct) case (step a b) hence "(a,b) ∈ tree_edges s" by simp with tree_edge_imp_discovered have "a ∈ dom (discovered s)" by simp with discover have "a ≠ v" by blast with step show ?case by auto qed simp with ‹y ∈ V0› have "x ∈ (tree_edges s)⇧^{+}`` V0" by auto with t_ne TDI show ?thesis by auto qed qed } note t_d = this { fix x assume "x ∈ dom (discovered s') ∪ V0" "x ∉ V0" hence A: "x ∈ dom (discovered s')" by simp have "x ∈ (tree_edges s')⇧^{+}`` V0 ∪ V0" proof (cases "tree_edges s = {}") case True with trancl_single have "(tree_edges s')⇧^{+}= {(hd (stack s), v)}" by simp moreover from True TDI have "hd (stack s) ∈ V0" "dom (discovered s) ⊆ V0" by auto ultimately show ?thesis using A ‹x∉V0› by auto next case False note t_ne = this show ?thesis proof (cases "x=v") case False with A have "x ∈ dom (discovered s)" by simp with TDI t_ne ‹x ∉ V0› have "x ∈ (tree_edges s)⇧^{+}`` V0" by auto with trancl_sub_insert_trancl show ?thesis by simp blast next case True from t_ne TDI have "dom (discovered s) ∪ V0 = (tree_edges s)⇧^{+}`` V0 ∪ V0" by simp moreover from stack_is_tree_path[OF NE] obtain v0 where "v0 ∈ V0" and "(v0, hd (stack s)) ∈ (tree_edges s)⇧^{*}" by (blast intro!: path_is_rtrancl) with EQ have "(v0, hd (stack s)) ∈ (tree_edges s')⇧^{*}" by (auto intro: rtrancl_mono_mp) ultimately show ?thesis using ‹v0 ∈ V0› True by (auto elim: rtrancl_into_trancl1) qed qed } with t_d have "(tree_edges s')⇧^{+}`` V0 ∪ V0 = dom (discovered s') ∪ V0" by blast ultimately show ?case by (simp add: tree_discovered_inv_def) qed (auto simp add: tree_discovered_inv_def) lemmas (in DFS_invar) tree_discovered_inv = i_tree_discovered_inv[THEN make_invar_thm] lemma (in DFS_invar) discovered_iff_tree_path: "v ∉ V0 ⟹ v ∈ dom (discovered s) ⟷ (∃v0∈V0. (v0,v) ∈ (tree_edges s)⇧^{+})" using tree_discovered_inv by (auto simp add: tree_discovered_inv_def) lemma i_tree_one_predecessor: "is_invar (λs. ∀(v,v') ∈ tree_edges s. ∀y. y ≠ v ⟶ (y,v') ∉ tree_edges s)" proof (induct rule: is_invarI) case (discover s s' u v) hence EQ[simp]: "tree_edges s' = insert (hd (stack s),v) (tree_edges s)" by simp from discover interpret DFS_invar where s=s by simp from discover have NE[simp]: "stack s ≠ []" by (simp add: cond_alt) { fix w w' y assume *: "(w,w') ∈ tree_edges s'" and "y ≠ w" from discover stack_discovered have v_hd: "hd (stack s) ≠ v" using hd_in_set[OF NE] by blast from discover tree_edges_discovered have v_notin_tree: "∀(x,x') ∈ tree_edges s. x ≠ v ∧ x' ≠ v" by (blast intro!: Field_not_elem) have "(y,w') ∉ tree_edges s'" proof (cases "w = hd (stack s)") case True have "(y,v) ∉ tree_edges s'" proof (rule notI) assume "(y,v) ∈ tree_edges s'" with True ‹y≠w› have "(y,v) ∈ tree_edges s" by simp with v_notin_tree show False by auto qed with True * ‹y≠w› v_hd show ?thesis apply (cases "w = v") apply simp using discover apply simp apply blast done next case False with v_notin_tree * ‹y≠w› v_hd show ?thesis apply (cases "w' = v") apply simp apply blast using discover apply simp apply blast done qed } thus ?case by blast qed simp_all lemma (in DFS_invar) tree_one_predecessor: assumes "(v,w) ∈ tree_edges s" and "a ≠ v" shows "(a,w) ∉ tree_edges s" using assms make_invar_thm[OF i_tree_one_predecessor] by blast lemma (in DFS_invar) tree_eq_rule: "⟦(v,w) ∈ tree_edges s; (u,w) ∈ tree_edges s⟧ ⟹ v=u" using tree_one_predecessor by blast context begin interpretation timing_syntax . lemma i_tree_edge_disc: "is_invar (λs. ∀(v,v') ∈ tree_edges s. δ s v < δ s v')" proof (induct rule: is_invarI) case (discover s s' u v) hence EQ[simp]: "tree_edges s' = insert (hd (stack s), v) (tree_edges s)" "discovered s' = (discovered s)(v ↦ counter s)" by simp_all from discover interpret DFS_invar where s=s by simp from discover have NE[simp]: "stack s ≠ []" by (simp add: cond_alt) from discover tree_edges_discovered have v_notin_tree: "∀(x,x') ∈ tree_edges s. x ≠ v ∧ x' ≠ v" by (blast intro!: Field_not_elem) from discover stack_discovered have v_hd: "hd (stack s) ≠ v" using hd_in_set[OF NE] by blast { fix a b assume T: "(a,b) ∈ tree_edges s'" have "δ s' a < δ s' b" proof (cases "b = v") case True with T v_notin_tree have [simp]: "a = hd (stack s)" by auto with stack_discovered have "a ∈ dom (discovered s)" by (metis hd_in_set NE subsetD) with v_hd True timing_less_counter show ?thesis by simp next case False with v_notin_tree T have "(a,b) ∈ tree_edges s" "a ≠ v" by auto with discover have "δ s a < δ s b" by auto with False ‹a≠v› show ?thesis by simp qed } thus ?case by blast next case (new_root s s' v0) then interpret DFS_invar where s=s by simp from new_root have "tree_edges s' = tree_edges s" by simp moreover from tree_edge_imp_discovered new_root have "∀(v,v') ∈ tree_edges s. v ≠ v0 ∧ v' ≠ v0" by blast ultimately show ?case using new_root by auto qed simp_all end end context DFS_invar begin context begin interpretation timing_syntax . lemma tree_edge_disc: "(v,w) ∈ tree_edges s ⟹ δ s v < δ s w" using i_tree_edge_disc[THEN make_invar_thm] by blast lemma tree_path_disc: "(v,w) ∈ (tree_edges s)⇧^{+}⟹ δ s v < δ s w" by (auto elim!: trancl_induct dest: tree_edge_disc) lemma no_loop_in_tree: "(v,v) ∉ (tree_edges s)⇧^{+}" using tree_path_disc by auto lemma tree_acyclic: "acyclic (tree_edges s)" by (metis acyclicI no_loop_in_tree) lemma no_self_loop_in_tree: "(v,v) ∉ tree_edges s" using tree_edge_disc by auto lemma tree_edge_unequal: "(v,w) ∈ tree_edges s ⟹ v ≠ w" by (metis no_self_loop_in_tree) lemma tree_path_unequal: "(v,w) ∈ (tree_edges s)⇧^{+}⟹ v ≠ w" by (metis no_loop_in_tree) lemma tree_subpath': assumes x: "(x,v) ∈ (tree_edges s)⇧^{+}" and y: "(y,v) ∈ (tree_edges s)⇧^{+}" and "x ≠ y" shows "(x,y) ∈ (tree_edges s)⇧^{+}∨ (y,x) ∈ (tree_edges s)⇧^{+}" proof - from x obtain px where px: "path (tree_edges s) x px v" and "px ≠ []" using trancl_is_path by metis from y obtain py where py: "path (tree_edges s) y py v" and "py ≠ []" using trancl_is_path by metis from ‹px ≠ []› ‹py ≠ []› px py show ?thesis proof (induction arbitrary: v rule: rev_nonempty_induct2') case (single) hence "(x,v) ∈ tree_edges s" "(y,v) ∈ tree_edges s" by (simp_all add: path_simps) with tree_eq_rule have "x=y" by simp with ‹x≠y› show ?case by contradiction next case (snocl a as) hence "(y,v) ∈ tree_edges s" by (simp add: path_simps) moreover from snocl have "path (tree_edges s) x as a" "(a,v) ∈ tree_edges s" by (simp_all add: path_simps) ultimately have "path (tree_edges s) x as y" using tree_eq_rule by auto with path_is_trancl ‹as ≠ []› show ?case by metis next case (snocr _ a as) hence "(x,v) ∈ tree_edges s" by (simp add: path_simps) moreover from snocr have "path (tree_edges s) y as a" "(a,v) ∈ tree_edges s" by (simp_all add: path_simps) ultimately have "path (tree_edges s) y as x" using tree_eq_rule by auto with path_is_trancl ‹as ≠ []› show ?case by metis next case (snoclr a as b bs) hence "path (tree_edges s) x as a" "(a,v) ∈ tree_edges s" "path (tree_edges s) y bs b" "(b,v) ∈ tree_edges s" by (simp_all add: path_simps) moreover hence "a=b" using tree_eq_rule by simp ultimately show ?thesis using snoclr.IH by metis qed qed lemma tree_subpath: assumes "(x,v) ∈ (tree_edges s)⇧^{+}" and "(y,v) ∈ (tree_edges s)⇧^{+}" and δ: "δ s x < δ s y" shows "(x,y) ∈ (tree_edges s)⇧^{+}" proof - from δ have "x ≠ y" by auto with assms tree_subpath' have "(x,y) ∈ (tree_edges s)⇧^{+}∨ (y,x) ∈ (tree_edges s)⇧^{+}" by simp moreover from δ tree_path_disc have "(y,x) ∉ (tree_edges s)⇧^{+}" by force ultimately show ?thesis by simp qed lemma on_stack_is_tree_path: assumes x: "x ∈ set (stack s)" and y: "y ∈ set (stack s)" and δ: "δ s x < δ s y" shows "(x,y) ∈ (tree_edges s)⇧^{+}" proof - from x obtain i where i: "stack s ! i = x" "i < length (stack s)" by (metis in_set_conv_nth) from y obtain j where j: "stack s ! j = y" "j < length (stack s)" by (metis in_set_conv_nth) with i δ stack_nth_order have "j < i" by force from x have ne[simp]: "stack s ≠ []" by auto from ‹j<i› have "x ∈ set (tl (stack s))" using nth_mem nth_tl[OF ne, of "i - 1"] i by auto with tl_stack_hd_tree_path have x_path: "(x, hd (stack s)) ∈ (tree_edges s)⇧^{+}" by simp then show ?thesis proof (cases "j=0") case True with j have "hd (stack s) = y" by (metis hd_conv_nth ne) with x_path show ?thesis by simp next case False hence "y ∈ set (tl (stack s))" using nth_mem nth_tl[OF ne, of "j - 1"] j by auto with tl_stack_hd_tree_path have "(y, hd (stack s)) ∈ (tree_edges s)⇧^{+}" by simp with x_path δ show ?thesis using tree_subpath by metis qed qed lemma hd_stack_tree_path_finished: assumes "stack s ≠ []" assumes "(hd (stack s), v) ∈ (tree_edges s)⇧^{+}" shows "v ∈ dom (finished s)" proof (cases "v ∈ set (stack s)") case True from assms no_loop_in_tree have "hd (stack s) ≠ v" by auto with True have "v ∈ set (tl (stack s))" by (cases "stack s") auto with tl_stack_hd_tree_path assms have "(hd (stack s), hd (stack s)) ∈ (tree_edges s)⇧^{+}" by (metis trancl_trans) with no_loop_in_tree show ?thesis by contradiction next case False from assms obtain x where "(x,v) ∈ tree_edges s" by (metis tranclE) with tree_edge_imp_discovered have "v ∈ dom (discovered s)" by blast with False show ?thesis by (simp add: stack_set_def) qed lemma tree_edge_impl_parenthesis: assumes t: "(v,w) ∈ tree_edges s" and f: "v ∈ dom (finished s)" shows "w ∈ dom (finished s) ∧ δ s v < δ s w ∧ φ s w < φ s v " proof - from tree_edge_disc_lt_fin assms have "δ s w < φ s v" by simp with f tree_edge_imp_discovered[OF t] tree_edge_disc[OF t] show ?thesis using parenthesis_contained by metis qed lemma tree_path_impl_parenthesis: assumes "(v,w) ∈ (tree_edges s)⇧^{+}" and "v ∈ dom (finished s)" shows "w ∈ dom (finished s) ∧ δ s v < δ s w ∧ φ s w < φ s v " using assms by (auto elim!: trancl_induct dest: tree_edge_impl_parenthesis) lemma nc_reachable_v0_parenthesis: assumes C: "¬ cond s" "¬ is_break param s" and v: "v ∈ reachable" "v ∉ V0" obtains v0 where "v0 ∈ V0" and "δ s v0 < δ s v ∧ φ s v < φ s v0 " proof - from nc_discovered_eq_reachable[OF C] discovered_iff_tree_path v obtain v0 where "v0 ∈ V0" and "(v0,v) ∈ (tree_edges s)⇧^{+}" by auto moreover with nc_V0_finished[OF C] have "v0 ∈ dom (finished s)" by auto ultimately show ?thesis using tree_path_impl_parenthesis that[OF ‹v0 ∈ V0›] by simp qed end end context param_DFS begin context begin interpretation timing_syntax . definition paren_imp_tree_reach where "paren_imp_tree_reach s ≡ ∀v ∈ dom (discovered s). ∀w ∈ dom (finished s). δ s v < δ s w ∧ (v ∉ dom (finished s) ∨ φ s v > φ s w) ⟶ (v,w) ∈ (tree_edges s)⇧^{+}" lemma paren_imp_tree_reach: "is_invar paren_imp_tree_reach" unfolding paren_imp_tree_reach_def[abs_def] proof (induct rule: is_invarI) case (discover s s' u v) hence EQ[simp]: "tree_edges s' = insert (hd (stack s), v) (tree_edges s)" "finished s' = finished s" "discovered s' = (discovered s)(v ↦ counter s)" by simp_all from discover interpret DFS_invar where s=s by simp from discover have NE[simp]: "stack s ≠ []" by (simp add: cond_alt) show ?case proof (intro ballI impI) fix a b assume F:"a ∈ dom (discovered s')" "b ∈ dom (finished s')" and D: "δ s' a < δ s' b ∧ (a ∉ dom (finished s') ∨ φ s' a > φ s' b)" from F finished_discovered discover have "b ≠ v" by auto show "(a,b) ∈ (tree_edges s')⇧^{+}" proof (cases "a = v") case True with D ‹b≠v› have "counter s < δ s b" by simp also from F have "b ∈ dom (discovered s)" using finished_discovered by auto with timing_less_counter have "δ s b < counter s" by simp finally have False . thus ?thesis .. next case False with ‹b≠v› F D discover have "(a,b) ∈ (tree_edges s)⇧^{+}" by simp thus ?thesis by (auto intro: trancl_mono_mp) qed qed next case (finish s s' u) hence EQ[simp]: "tree_edges s' = tree_edges s" "finished s' = (finished s)(hd (stack s) ↦ counter s)" "discovered s' = discovered s" "stack s' = tl (stack s)" by simp_all from finish interpret DFS_invar where s=s by simp from finish have NE[simp]: "stack s ≠ []" by (simp add: cond_alt) show ?case proof (intro ballI impI) fix a b assume F: "a ∈ dom (discovered s')" "b ∈ dom (finished s')" and paren: "δ s' a < δ s' b ∧ (a ∉ dom (finished s') ∨ φ s' a > φ s' b)" hence "a ≠ b" by auto show "(a,b) ∈ (tree_edges s')⇧^{+}" proof (cases "b = hd (stack s)") case True hence φb: "φ s' b = counter s" by simp have "a ∈ set (stack s)" unfolding stack_set_def proof from F show "a ∈ dom (discovered s)" by simp from True ‹a≠b› φb paren have "a ∈ dom (finished s) ⟶ φ s a > counter s" by simp with timing_less_counter show "a ∉ dom (finished s)" by force qed with paren True on_stack_is_tree_path have "(a,b) ∈ (tree_edges s)⇧^{+}" by auto thus ?thesis by (auto intro: trancl_mono_mp) next case False note b_not_hd = this show ?thesis proof (cases "a = hd (stack s)") case False with b_not_hd F paren finish show ?thesis by simp next case True with paren b_not_hd F have "a ∈ dom (discovered s)" "b ∈ dom (finished s)" "δ s a < δ s b" by simp_all moreover from True stack_not_finished have "a ∉ dom (finished s)" by simp ultimately show ?thesis by (simp add: finish) qed qed qed next case (new_root s s' v0) then interpret DFS_invar where s=s by simp from new_root finished_discovered have "v0 ∉ dom (finished s)" by auto moreover note timing_less_counter finished_discovered ultimately show ?case using new_root by clarsimp force qed simp_all end end context DFS_invar begin context begin interpretation timing_syntax . lemmas s_paren_imp_tree_reach = paren_imp_tree_reach[THEN make_invar_thm] lemma parenthesis_impl_tree_path_not_finished: assumes "v ∈ dom (discovered s)" and "w ∈ dom (finished s)" and "δ s v < δ s w" and "v ∉ dom (finished s)" shows "(v,w) ∈ (tree_edges s)⇧^{+}" using s_paren_imp_tree_reach assms by (auto simp add: paren_imp_tree_reach_def) lemma parenthesis_impl_tree_path: assumes "v ∈ dom (finished s)" "w ∈ dom (finished s)" and "δ s v < δ s w" "φ s v > φ s w" shows "(v,w) ∈ (tree_edges s)⇧^{+}" proof - from assms(1) have "v ∈ dom (discovered s)" using finished_discovered by blast with assms show ?thesis using s_paren_imp_tree_reach assms by (auto simp add: paren_imp_tree_reach_def) qed lemma tree_path_iff_parenthesis: assumes "v ∈ dom (finished s)" "w ∈ dom (finished s)" shows "(v,w) ∈ (tree_edges s)⇧^{+}⟷ δ s v < δ s w ∧ φ s v > φ s w" using assms by (metis parenthesis_impl_tree_path tree_path_impl_parenthesis) lemma no_pending_succ_impl_path_in_tree: assumes v: "v ∈ dom (discovered s)" "pending s `` {v} = {}" and w: "w ∈ succ v" and δ: "δ s v < δ s w" shows "(v,w) ∈ (tree_edges s)⇧^{+}" proof (cases "v ∈ dom (finished s)") case True with assms assms have "δ s w < φ s v" "w ∈ dom (discovered s)" using finished_succ_fin finished_imp_succ_discovered by simp_all with True δ show ?thesis using parenthesis_contained parenthesis_impl_tree_path by blast next case False show ?thesis proof (cases "w ∈ dom (finished s)") case True with False v δ show ?thesis by (simp add: parenthesis_impl_tree_path_not_finished) next case False with ‹v ∉ dom (finished s)› no_pending_imp_succ_discovered v w have "v ∈ set (stack s)" "w ∈ set (stack s)" by (simp_all add: stack_set_def) with on_stack_is_tree_path δ show ?thesis by simp qed qed lemma finished_succ_impl_path_in_tree: assumes f: "v ∈ dom (finished s)" and s: "w ∈ succ v" and δ: "δ s v < δ s w" shows "(v,w) ∈ (tree_edges s)⇧^{+}" using no_pending_succ_impl_path_in_tree finished_no_pending finished_discovered using assms by blast end end subsubsection ‹Properties of Cross Edges› (* Cross Edges *) context param_DFS begin context begin interpretation timing_syntax . lemma i_cross_edges_finished: "is_invar (λs. ∀(u,v)∈cross_edges s. v ∈ dom (finished s) ∧ (u ∈ dom (finished s) ⟶ φ s v < φ s u))" proof (induction rule: is_invarI_full) case (finish s s' u e) interpret DFS_invar G param s by fact from finish stack_not_finished have "u ∉ dom (finished s)" by auto with finish show ?case by (auto intro: timing_less_counter) next case (cross_edge s s' u v e) interpret DFS_invar G param s by fact from cross_edge stack_not_finished have "u ∉ dom (finished s)" by auto with cross_edge show ?case by (auto intro: timing_less_counter) qed simp_all end end context DFS_invar begin context begin interpretation timing_syntax . lemmas cross_edges_finished = i_cross_edges_finished[THEN make_invar_thm] lemma cross_edges_target_finished: "(u,v)∈cross_edges s ⟹ v ∈ dom (finished s)" using cross_edges_finished by auto lemma cross_edges_finished_decr: "⟦(u,v)∈cross_edges s; u∈dom (finished s)⟧ ⟹ φ s v < φ s u" using cross_edges_finished by auto lemma cross_edge_unequal: assumes cross: "(v,w) ∈ cross_edges s" shows "v ≠ w" proof - from cross_edges_target_finished[OF cross] have w_fin: "w ∈ dom (finished s)" . show ?thesis proof (cases "v ∈ dom (finished s)") case True with cross_edges_finished_decr[OF cross] show ?thesis by force next case False with w_fin show ?thesis by force qed qed end end subsubsection ‹Properties of Back Edges› (* Back Edges *) context param_DFS begin context begin interpretation timing_syntax . lemma i_back_edge_impl_tree_path: "is_invar (λs. ∀(v,w) ∈ back_edges s. (w,v) ∈ (tree_edges s)⇧^{+}∨ w = v)" proof (induct rule: is_invarI_full) case (back_edge s s' u v) then interpret DFS_invar where s=s by simp from back_edge have st: "v ∈ set (stack s)" "u ∈ set (stack s)" using stack_set_def by auto have "(v,u) ∈ (tree_edges s)⇧^{+}∨ u = v" proof (rule disjCI) assume "u ≠ v" with st back_edge have "v ∈ set (tl (stack s))" by (metis not_hd_in_tl) with tl_lt_stack_hd_discover st back_edge have "δ s v < δ s u" by simp with on_stack_is_tree_path st show "(v,u) ∈ (tree_edges s)⇧^{+}" by simp qed with back_edge show ?case by auto next case discover thus ?case using trancl_sub_insert_trancl by force qed simp_all end end context DFS_invar begin context begin interpretation timing_syntax . lemma back_edge_impl_tree_path: "⟦(v,w) ∈ back_edges s; v ≠ w⟧ ⟹ (w,v) ∈ (tree_edges s)⇧^{+}" using i_back_edge_impl_tree_path[THEN make_invar_thm] by blast lemma back_edge_disc: assumes "(v,w) ∈ back_edges s" shows "δ s w ≤ δ s v" proof cases assume "v≠w" with assms back_edge_impl_tree_path have "(w,v) ∈ (tree_edges s)⇧^{+}" by simp with tree_path_disc show ?thesis by force qed simp lemma back_edges_tree_disjoint: "back_edges s ∩ tree_edges s = {}" using back_edge_disc tree_edge_disc by force lemma back_edges_tree_pathes_disjoint: "back_edges s ∩ (tree_edges s)⇧^{+}= {}" using back_edge_disc tree_path_disc by force lemma back_edge_finished: assumes "(v,w) ∈ back_edges s" and "w ∈ dom (finished s)" shows "v ∈ dom (finished s) ∧ φ s v ≤ φ s w" proof (cases "v=w") case True with assms show ?thesis by simp next case False with back_edge_impl_tree_path assms have "(w,v) ∈ (tree_edges s)⇧^{+}" by simp with tree_path_impl_parenthesis assms show ?thesis by fastforce qed end end context param_DFS begin context begin interpretation timing_syntax . (* The lemma should probably replaced by: is_invar (λs. ∀(v,w) ∈ (tree_edges s)⇧^{+}. v ∈ succ w ⟶ (w,v) ∈ back_edges s ∨ (w,v) ∈ pending s) *) lemma i_disc_imp_back_edge_or_pending: "is_invar (λs. ∀(v,w) ∈ E. v ∈ dom (discovered s) ∧ w ∈ dom (discovered s) ∧ δ s v ≥ δ s w ∧ (w ∈ dom (finished s) ⟶ v ∈ dom (finished s) ∧ φ s w ≥ φ s v) ⟶ (v,w) ∈ back_edges s ∨ (v,w) ∈ pending s)" proof (induct rule: is_invarI_full) case (cross_edge s s' u v) then interpret DFS_invar where s=s by simp from cross_edge stack_not_finished[of u] have "u ∉ dom (finished s)" using hd_in_set by (auto simp add: cond_alt) with cross_edge show ?case by auto next case (finish s s' u v) then interpret DFS_invar where s=s by simp from finish have IH: "⋀v w. ⟦w ∈ succ v; v ∈ dom (discovered s); w ∈ dom (discovered s); δ s w ≤ δ s v; (w ∈ dom (finished s) ⟹ v ∈ dom (finished s) ∧ φ s v ≤ φ s w)⟧ ⟹ (v, w) ∈ back_edges s ∨ (v, w) ∈ pending s" by blast from finish have ne[simp]: "stack s ≠ []" and p[simp]: "pending s `` {hd (stack s)} = {}" by (simp_all) from hd_in_set[OF ne] have disc: "hd (stack s) ∈ dom (discovered s)" and not_fin: "hd (stack s) ∉ dom (finished s)" using stack_discovered stack_not_finished by blast+ { fix w assume w: "w ∈ succ (hd (stack s))" "w ≠ hd (stack s)" "w ∈ dom (discovered s)" and f: "w ∈ dom (finished s) ⟶ counter s ≤ φ s w" and δ: "δ s w ≤ δ s (hd (stack s))" with timing_less_counter have "w ∉ dom (finished s)" by force with finish w δ disc have "(hd (stack s), w) ∈ back_edges s" by blast } moreover { fix w assume "hd (stack s) ∈ succ w" "w ≠ hd (stack s)" and "w ∈ dom (finished s)" "δ s (hd (stack s)) ≤ δ s w" with IH[of "hd (stack s)" w] disc not_fin have "(w, hd (stack s)) ∈ back_edges s" using finished_discovered finished_no_pending[of w] by blast } ultimately show ?case using finish by clarsimp auto next case (discover s s' u v) then interpret DFS_invar where s=s by simp from discover show ?case using timing_less_counter by clarsimp fastforce next case (new_root s s' v0) then interpret DFS_invar where s=s by simp from new_root empty_stack_imp_empty_pending have "pending s = {}" by simp with new_root show ?case using timing_less_counter by clarsimp fastforce qed auto end end context DFS_invar begin context begin interpretation timing_syntax . lemma disc_imp_back_edge_or_pending: "⟦w ∈ succ v; v ∈ dom (discovered s); w ∈ dom (discovered s); δ s w ≤ δ s v; (w ∈ dom (finished s) ⟹ v ∈ dom (finished s) ∧ φ s v ≤ φ s w)⟧ ⟹ (v, w) ∈ back_edges s ∨ (v, w) ∈ pending s" using i_disc_imp_back_edge_or_pending[THEN make_invar_thm] by blast lemma finished_imp_back_edge: "⟦w ∈ succ v; v ∈ dom (finished s); w ∈ dom (finished s); δ s w ≤ δ s v; φ s v ≤ φ s w⟧ ⟹ (v, w) ∈ back_edges s" using disc_imp_back_edge_or_pending finished_discovered finished_no_pending by fast lemma finished_not_finished_imp_back_edge: "⟦w ∈ succ v; v ∈ dom (finished s); w ∈ dom (discovered s); w ∉ dom (finished s); δ s w ≤ δ s v⟧ ⟹ (v, w) ∈ back_edges s" using disc_imp_back_edge_or_pending finished_discovered finished_no_pending by fast lemma finished_self_loop_in_back_edges: assumes "v ∈ dom (finished s)" and "(v,v) ∈ E" shows "(v,v) ∈ back_edges s" using assms using finished_imp_back_edge by blast end end (* Back edges and Cycles *) context DFS_invar begin context begin interpretation timing_syntax . (* Cross and tree_edges edges are always acyclic *) lemma tree_cross_acyclic: "acyclic (tree_edges s ∪ cross_edges s)" (is "acyclic ?E") proof (rule ccontr) { fix u v assume *: "u ∈ dom (finished s)" and "(u,v) ∈ ?E⇧^{+}" from this(2) have "φ s v < φ s u ∧ v ∈ dom (finished s)" proof induct case base thus ?case by (metis Un_iff * cross_edges_finished_decr cross_edges_target_finished tree_edge_impl_parenthesis) next case (step v w) hence "φ s w < φ s v ∧ w ∈ dom (finished s)" by (metis Un_iff cross_edges_finished_decr cross_edges_target_finished tree_edge_impl_parenthesis) with step show ?case by auto qed } note aux = this assume "¬ acyclic ?E" then obtain u where path: "(u,u) ∈ ?E⇧^{+}" by (auto simp add: acyclic_def) show False proof cases assume "u ∈ dom (finished s)" with aux path show False by blast next assume *: "u ∉ dom (finished s)" moreover from no_loop_in_tree have "(u,u) ∉ (tree_edges s)⇧^{+}" . with trancl_union_outside[OF path] obtain x y where "(u,x) ∈ ?E⇧^{*}" "(x,y) ∈ cross_edges s" "(y,u) ∈ ?E⇧^{*}" by auto with cross_edges_target_finished have "y ∈ dom (finished s)" by simp moreover with * ‹(y,u) ∈ ?E⇧^{*}› have "(y,u) ∈ ?E⇧^{+}" by (auto simp add: rtrancl_eq_or_trancl) ultimately show False by (metis aux) qed qed end lemma cycle_contains_back_edge: assumes cycle: "(u,u) ∈ (edges s)⇧^{+}" shows "∃v w. (u,v) ∈ (edges s)⇧^{*}∧ (v,w) ∈ back_edges s ∧ (w,u) ∈ (edges s)⇧^{*}" proof - from tree_cross_acyclic have "(u,u) ∉ (tree_edges s ∪ cross_edges s)⇧^{+}" by (simp add: acyclic_def) with trancl_union_outside[OF cycle] show ?thesis . qed lemma cycle_needs_back_edge: assumes "back_edges s = {}" shows "acyclic (edges s)" proof (rule ccontr) assume "¬ acyclic (edges s)" then obtain u where "(u,u) ∈ (edges s)⇧^{+}" by (auto simp: acyclic_def) with assms have "(u,u) ∈ (tree_edges s ∪ cross_edges s)⇧^{+}" by auto with tree_cross_acyclic show False by (simp add: acyclic_def) qed lemma back_edge_closes_cycle: assumes "back_edges s ≠ {}" shows "¬ acyclic (edges s)" proof - from assms obtain v w where be: "(v,w) ∈ back_edges s" by auto hence "(w,w) ∈ (edges s)⇧^{+}" proof (cases "v=w") case False with be back_edge_impl_tree_path have "(w,v) ∈ (tree_edges s)⇧^{+}" by simp hence "(w,v) ∈ (edges s)⇧^{+}" by (blast intro: trancl_mono_mp) also from be have "(v,w) ∈ edges s" by simp finally show ?thesis . qed auto thus ?thesis by (auto simp add: acyclic_def) qed lemma back_edge_closes_reachable_cycle: "back_edges s ≠ {} ⟹ ¬ acyclic (E ∩ reachable × UNIV)" by (metis back_edge_closes_cycle edges_ss_reachable_edges cyclic_subset) lemma cycle_iff_back_edges: "acyclic (edges s) ⟷ back_edges s = {}" by (metis back_edge_closes_cycle cycle_needs_back_edge) end subsection ‹White Path Theorem› context DFS begin context begin interpretation timing_syntax . definition white_path where "white_path s x y ≡ x≠y ⟶ (∃p. path E x p y ∧ (δ s x < δ s y ∧ (∀ v ∈ set (tl p). δ s x < δ s v)))" lemma white_path: "it_dfs ≤ SPEC(λs. ∀x ∈ reachable. ∀y ∈ reachable. ¬ is_break param s ⟶ white_path s x y ⟷ (x,y) ∈ (tree_edges s)⇧^{*})" proof (rule it_dfs_SPEC, intro ballI impI) fix s x y assume DI: "DFS_invar G param s" and C: "¬ cond s" "¬ is_break param s" and reach: "x ∈ reachable" "y ∈ reachable" from DI interpret DFS_invar where s=s . note fin_eq_reach = nc_finished_eq_reachable[OF C] show "white_path s x y ⟷ (x,y) ∈ (tree_edges s)⇧^{*}" proof (cases "x=y") case True thus ?thesis by (simp add: white_path_def) next case False show ?thesis proof assume "(x,y) ∈ (tree_edges s)⇧^{*}" with ‹x≠y› have T: "(x,y) ∈ (tree_edges s)⇧^{+}" by (metis rtranclD) then obtain p where P: "path (tree_edges s) x p y" by (metis trancl_is_path) with tree_edges_ssE have "path E x p y" using path_mono[where E="tree_edges s"] by simp moreover from P have "δ s x < δ s y ∧ (∀ v ∈ set (tl p). δ s x < δ s v)" using ‹x≠y› proof (induct rule: path_tl_induct) case (single u) thus ?case by (fact tree_edge_disc) next case (step u v) note ‹δ s x < δ s u› also from step have "δ s u < δ s v" by (metis tree_edge_disc) finally show ?case . qed ultimately show "white_path s x y" by (auto simp add: ‹x≠y› white_path_def) next assume "white_path s x y" with ‹x≠y› obtain p where P:"path E x p y" and white: "δ s x < δ s y ∧ (∀ v ∈ set (tl p). δ s x < δ s v)" unfolding white_path_def by blast hence "p ≠ []" by auto thus "(x,y) ∈ (tree_edges s)⇧^{*}" using P white reach(2) proof (induction p arbitrary: y rule: rev_nonempty_induct) case single hence "y ∈ succ x" by (simp add: path_cons_conv) with reach single show ?case using fin_eq_reach finished_succ_impl_path_in_tree[of x y] by simp next case (snoc u us) hence "path E x us u" by (simp add: path_append_conv) moreover hence "(x,u) ∈ E⇧^{*}" by (simp add: path_is_rtrancl) with reach have ureach: "u ∈ reachable" by (metis rtrancl_image_advance_rtrancl) moreover from snoc have "δ s x < δ s u" "(∀v∈set (tl us). δ s x < δ s v)" by simp_all ultimately have x_u: "(x,u) ∈ (tree_edges s)⇧^{*}" by (metis snoc.IH) from snoc have "y ∈ succ u" by (simp add: path_append_conv) from snoc(5) fin_eq_reach finished_discovered have y_f_d: "y ∈ dom (finished s)" "y ∈ dom (discovered s)" by auto from ‹y ∈ succ u› ureach fin_eq_reach have "δ s y < φ s u" using finished_succ_fin by simp also from ‹δ s x < δ s u› have "x ≠ u" by auto with x_u have "