Theory Nested_DFS
section ‹\isaheader{Nested DFS (HPY improvement)}›
theory Nested_DFS
imports
Collections.Refine_Dflt
Succ_Graph
Collections.Code_Target_ICF
CAVA_Automata.Digraph_Basic
begin
text ‹
Implementation of a nested DFS algorithm for accepting cycle detection
using the refinement framework. The algorithm uses the improvement of
[HPY96], i.e., it reports a cycle if the inner DFS finds a path back to
the stack of the outer DFS.
The algorithm returns a witness in case that an accepting cycle is detected.
›
subsection "Tools for DFS Algorithms"
subsubsection "Invariants"
definition "gen_dfs_pre E U S V u0 ≡
E``U ⊆ U
∧ finite U
∧ V ⊆ U
∧ u0 ∈ U
∧ E``(V-S) ⊆ V
∧ u0∉V
∧ S ⊆ V
∧ (∀v∈S. (v,u0)∈(E∩S×UNIV)⇧*)
"
definition "gen_dfs_var U ≡ finite_psupset U"
definition "gen_dfs_fe_inv E U S V0 u0 it V brk ≡
(¬brk ⟶ E``(V-S) ⊆ V)
∧ E``{u0} - it ⊆ V
∧ V0 ⊆ V
∧ V ⊆ V0 ∪ (E - UNIV×S)⇧* `` (E``{u0} - it - S)
"
definition "gen_dfs_post E U S V0 u0 V brk ≡
(¬brk ⟶ E``(V-S) ⊆ V)
∧ u0 ∈ V
∧ V0 ⊆ V
∧ V ⊆ V0 ∪ (E - UNIV×S)⇧* `` {u0}
"
subsubsection "Invariant Preservation"
lemma gen_dfs_pre_initial:
assumes "finite (E⇧*``{v0})"
assumes "v0∈U"
shows "gen_dfs_pre E (E⇧*``{v0}) {} {} v0"
using assms unfolding gen_dfs_pre_def
apply auto
done
lemma gen_dfs_pre_imp_wf:
assumes "gen_dfs_pre E U S V u0"
shows "wf (gen_dfs_var U)"
using assms unfolding gen_dfs_pre_def gen_dfs_var_def by auto
lemma gen_dfs_pre_imp_fin:
assumes "gen_dfs_pre E U S V u0"
shows "finite (E `` {u0})"
apply (rule finite_subset[where B="U"])
using assms unfolding gen_dfs_pre_def
by auto
text ‹Inserted ‹u0› on stack and to visited set›
lemma gen_dfs_pre_imp_fe:
assumes "gen_dfs_pre E U S V u0"
shows "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0
(E``{u0}) (insert u0 V) False"
using assms unfolding gen_dfs_pre_def gen_dfs_fe_inv_def
apply auto
done
lemma gen_dfs_fe_inv_pres_visited:
assumes "gen_dfs_pre E U S V u0"
assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
assumes "t∈it" "it⊆E``{u0}" "t∈V'"
shows "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (it-{t}) V' False"
using assms unfolding gen_dfs_fe_inv_def
apply auto
done
lemma gen_dfs_upper_aux:
assumes "(x,y)∈E'⇧*"
assumes "(u0,x)∈E"
assumes "u0∈U"
assumes "E'⊆E"
assumes "E``U ⊆ U"
shows "y∈U"
using assms
by induct auto
lemma gen_dfs_fe_inv_imp_var:
assumes "gen_dfs_pre E U S V u0"
assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
assumes "t∈it" "it⊆E``{u0}" "t∉V'"
shows "(V',V) ∈ gen_dfs_var U"
using assms unfolding gen_dfs_fe_inv_def gen_dfs_pre_def gen_dfs_var_def
apply (clarsimp simp add: finite_psupset_def)
apply (blast dest: gen_dfs_upper_aux)
done
lemma gen_dfs_fe_inv_imp_pre:
assumes "gen_dfs_pre E U S V u0"
assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
assumes "t∈it" "it⊆E``{u0}" "t∉V'"
shows "gen_dfs_pre E U (insert u0 S) V' t"
using assms unfolding gen_dfs_fe_inv_def gen_dfs_pre_def
apply clarsimp
apply (intro conjI)
apply (blast dest: gen_dfs_upper_aux)
apply blast
apply blast
apply blast
apply clarsimp
apply (rule rtrancl_into_rtrancl[where b=u0])
apply (auto intro: rev_subsetD[OF _ rtrancl_mono[where r="E ∩ S × UNIV"]]) []
apply blast
done
lemma gen_dfs_post_imp_fe_inv:
assumes "gen_dfs_pre E U S V u0"
assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
assumes "t∈it" "it⊆E``{u0}" "t∉V'"
assumes "gen_dfs_post E U (insert u0 S) V' t V'' cyc"
shows "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (it-{t}) V'' cyc"
using assms unfolding gen_dfs_fe_inv_def gen_dfs_post_def gen_dfs_pre_def
apply clarsimp
apply (intro conjI)
apply blast
apply blast
apply blast
apply (erule order_trans)
apply simp
apply (rule conjI)
apply (erule order_trans[
where y="insert u0 (V ∪ (E - UNIV × insert u0 S)⇧*
`` (E `` {u0} - it - insert u0 S))"])
apply blast
apply (cases cyc)
apply simp
apply blast
apply simp
apply blast
done
lemma gen_dfs_post_aux:
assumes 1: "(u0,x)∈E"
assumes 2: "(x,y)∈(E - UNIV × insert u0 S)⇧*"
assumes 3: "S⊆V" "x∉V"
shows "(u0, y) ∈ (E - UNIV × S)⇧*"
proof -
from 1 3 have "(u0,x)∈(E - UNIV × S)" by blast
also have "(x,y)∈(E - UNIV × S)⇧*"
apply (rule_tac rev_subsetD[OF 2 rtrancl_mono])
by auto
finally show ?thesis .
qed
lemma gen_dfs_fe_imp_post_brk:
assumes "gen_dfs_pre E U S V u0"
assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' True"
assumes "it⊆E``{u0}"
shows "gen_dfs_post E U S V u0 V' True"
using assms unfolding gen_dfs_pre_def gen_dfs_fe_inv_def gen_dfs_post_def
apply clarify
apply (intro conjI)
apply simp
apply simp
apply simp
apply clarsimp
apply (blast intro: gen_dfs_post_aux)
done
lemma gen_dfs_fe_inv_imp_post:
assumes "gen_dfs_pre E U S V u0"
assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 {} V' cyc"
assumes "cyc⟶cyc'"
shows "gen_dfs_post E U S V u0 V' cyc'"
using assms unfolding gen_dfs_pre_def gen_dfs_fe_inv_def gen_dfs_post_def
apply clarsimp
apply (intro conjI)
apply blast
apply (auto intro: gen_dfs_post_aux) []
done
lemma gen_dfs_pre_imp_post_brk:
assumes "gen_dfs_pre E U S V u0"
shows "gen_dfs_post E U S V u0 (insert u0 V) True"
using assms unfolding gen_dfs_pre_def gen_dfs_post_def
apply auto
done
subsubsection "Consequences of Postcondition"
lemma gen_dfs_post_imp_reachable:
assumes "gen_dfs_pre E U S V0 u0"
assumes "gen_dfs_post E U S V0 u0 V brk"
shows "V ⊆ V0 ∪ E⇧*``{u0}"
using assms unfolding gen_dfs_post_def gen_dfs_pre_def
apply clarsimp
apply (blast intro: rev_subsetD[OF _ rtrancl_mono])
done
lemma gen_dfs_post_imp_complete:
assumes "gen_dfs_pre E U {} V0 u0"
assumes "gen_dfs_post E U {} V0 u0 V False"
shows "V0 ∪ E⇧*``{u0} ⊆ V"
using assms unfolding gen_dfs_post_def gen_dfs_pre_def
apply clarsimp
apply (blast dest: Image_closed_trancl)
done
lemma gen_dfs_post_imp_eq:
assumes "gen_dfs_pre E U {} V0 u0"
assumes "gen_dfs_post E U {} V0 u0 V False"
shows "V = V0 ∪ E⇧*``{u0}"
using gen_dfs_post_imp_reachable[OF assms] gen_dfs_post_imp_complete[OF assms]
by blast
lemma gen_dfs_post_imp_below_U:
assumes "gen_dfs_pre E U S V0 u0"
assumes "gen_dfs_post E U S V0 u0 V False"
shows "V ⊆ U"
using assms unfolding gen_dfs_pre_def gen_dfs_post_def
apply clarsimp
apply (blast intro: rev_subsetD[OF _ rtrancl_mono] dest: Image_closed_trancl)
done
subsection "Abstract Algorithm"
subsubsection ‹Inner (red) DFS›
text ‹A witness of the red algorithm is a node on the stack and a path
to this node›
type_synonym 'v red_witness = "('v list × 'v) option"
text ‹Prepend node to red witness›
fun prep_wit_red :: "'v ⇒ 'v red_witness ⇒ 'v red_witness" where
"prep_wit_red v None = None"
| "prep_wit_red v (Some (p,u)) = Some (v#p,u)"
text ‹
Initial witness for node ‹u› with onstack successor ‹v›
›
definition red_init_witness :: "'v ⇒ 'v ⇒ 'v red_witness" where
"red_init_witness u v = Some ([u],v)"
definition red_dfs where
"red_dfs E onstack V u ≡
REC⇩T (λD (V,u). do {
let V=insert u V;
brk ← FOREACH⇩C (E``{u}) (λbrk. brk=None)
(λt _. if t∈onstack then RETURN (red_init_witness u t) else RETURN None)
None;
case brk of
None ⇒
FOREACH⇩C (E``{u}) (λ(V,brk). brk=None)
(λt (V,_).
if t∉V then do {
(V,brk) ← D (V,t);
RETURN (V,prep_wit_red u brk)
} else RETURN (V,None))
(V,None)
| _ ⇒ RETURN (V,brk)
}) (V,u)
"
text ‹
A witness of the blue DFS may be in two different phases, the ‹REACH›
phase is before the node on the stack has actually been popped, and the
‹CIRC› phase is after the node on the stack has been popped.
‹REACH v p u p'›: \begin{description}
\item[‹v›] accepting node
\item[‹p›] path from ‹v› to ‹u›
\item[‹u›] node on stack
\item[‹p'›] path from current node to ‹v›
\end{description}
‹CIRC v pc pr›: \begin{description}
\item[‹v›] accepting node
\item[‹pc›] path from ‹v› to ‹v›
\item[‹pr›] path from current node to ‹v›
\end{description}
›