Theory NDFS_SI
section ‹Nested DFS using Standard Invariants Approach›
theory NDFS_SI
imports
CAVA_Automata.Automata_Impl
CAVA_Automata.Lasso
NDFS_SI_Statistics
CAVA_Base.CAVA_Code_Target
begin
text ‹
Implementation of a nested DFS algorithm for accepting cycle detection
using the refinement framework. The algorithm uses the improvement of
Holzmann et al.~\<^cite>‹"HPY97"›, i.e., it reports a cycle if the inner
DFS finds a path back to
the stack of the outer DFS. Moreover, an early cycle detection optimization is
implemented~\<^cite>‹"SE05"›, i.e., the outer DFS may already report a cycle on
a back-edge involving an accepting node.
The algorithm returns a witness in case that an accepting cycle is detected.
The design approach to this algorithm is to first establish invariants of a
generic DFS-Algorithm, which are then used to instantiate the concrete
nested DFS-algorithm for B\"uchi emptiness check. This formalization can be
seen as a predecessor of the formalization of
Gabow's algorithm~\<^cite>‹"La14_ITP"›, where this technique has been
further developed.
›
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}
"
definition "gen_dfs_outer E U V0 it V brk ≡
V0 ⊆ U
∧ E``U ⊆ U
∧ finite U
∧ V ⊆ U
∧ (¬brk ⟶ E``V ⊆ V)
∧ (V0 - it ⊆ V) "
subsubsection "Invariant Preservation"
lemma gen_dfs_outer_initial:
assumes "finite (E⇧*``V0)"
shows "gen_dfs_outer E (E⇧*``V0) V0 V0 {} brk"
using assms unfolding gen_dfs_outer_def
by (auto intro: rev_ImageI)
lemma gen_dfs_pre_initial:
assumes "gen_dfs_outer E U V0 it V False"
assumes "v0∈U - V"
shows "gen_dfs_pre E U {} V v0"
using assms unfolding gen_dfs_pre_def gen_dfs_outer_def
apply auto
done
lemma fin_U_imp_wf:
assumes "finite U"
shows "wf (gen_dfs_var U)"
using assms unfolding gen_dfs_var_def by auto
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
lemma gen_dfs_post_imp_outer:
assumes "gen_dfs_outer E U V0 it Vis0 False"
assumes "gen_dfs_post E U {} Vis0 v0 Vis False"
assumes "v0 ∈ it" "it ⊆ V0" "v0 ∉ Vis0"
shows "gen_dfs_outer E U V0 (it - {v0}) Vis False"
proof -
{
assume "v0 ∈ it" "it ⊆ V0" "V0 ⊆ U" "E `` U ⊆ U"
hence "E⇧* `` {v0} ⊆ U"
by (metis (full_types) empty_subsetI insert_subset rtrancl_reachable_induct subset_trans)
} note AUX=this
show ?thesis
using assms
unfolding gen_dfs_outer_def gen_dfs_post_def
using AUX
by auto
qed
lemma gen_dfs_outer_already_vis:
assumes "v0 ∈ it" "it ⊆ V0" "v0 ∈ V"
assumes "gen_dfs_outer E U V0 it V False"
shows "gen_dfs_outer E U V0 (it - {v0}) V False"
using assms
unfolding gen_dfs_outer_def
by auto
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;
NDFS_SI_Statistics.vis_red_nres;
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)
"