Theory DFS
theory DFS
imports Pair_Graph_Specs Set2_Addons Set_Addons
begin
section‹Depth-Frist Search›
subsection ‹The program state›
datatype return = Reachable | NotReachable
record ('ver, 'vset) DFS_state = stack:: "'ver list" seen:: "'vset" return:: return
subsection ‹Setup for automation›
named_theorems call_cond_elims
named_theorems call_cond_intros
named_theorems ret_holds_intros
named_theorems invar_props_intros
named_theorems invar_props_elims
named_theorems invar_holds_intros
named_theorems state_rel_intros
named_theorems state_rel_holds_intros
subsection ‹A \emph{locale} for fixing data structures and their implemenations›
locale DFS =
Graph: Pair_Graph_Specs
where lookup = lookup +
set_ops: Set2 vset_empty vset_delete _ t_set vset_inv insert
for lookup :: "'adjmap⇒ 'v ⇒ 'vset option" +
fixes G::"'adjmap" and s::"'v" and t::"'v"
begin
definition "DFS_axioms = ( Graph.graph_inv G ∧ Graph.finite_graph G ∧ Graph.finite_vsets
∧ s ∈ dVs (Graph.digraph_abs G))"
abbreviation "neighb' v == Graph.neighb G v"
notation "neighb'" ("𝒩⇩G _" 100)
subsection ‹Defining the Algorithm›
function (domintros) DFS::"('v, 'vset) DFS_state ⇒ ('v, 'vset) DFS_state" where
"DFS dfs_state =
(case (stack dfs_state) of (v # stack_tl) ⇒
(if v = t then
(dfs_state ⦇return := Reachable⦈)
else ((if (𝒩⇩G v -⇩G (seen dfs_state)) ≠ ∅⇩V then
let u = (sel ((𝒩⇩G v) -⇩G (seen dfs_state)));
stack' = u# (stack dfs_state);
seen' = insert u (seen dfs_state)
in
(DFS (dfs_state ⦇stack := stack',
seen := seen' ⦈))
else
let stack' = stack_tl in
DFS (dfs_state ⦇stack := stack'⦈))
)
)
| _ ⇒ (dfs_state ⦇return := NotReachable⦈)
)"
by pat_completeness auto
subsection ‹Setup for Reasoning About the Algorithm›
definition initial_state::"('v,'vset) DFS_state" where
"initial_state = ⦇stack = [s], seen = insert s ∅⇩V, return = NotReachable⦈"
definition "DFS_call_1_conds dfs_state =
(case stack dfs_state of (v # stack_tl) ⇒
(if v = t then
False
else ((if ((𝒩⇩G v) -⇩G (seen dfs_state)) ≠ (∅⇩V) then
True
else False)
)
)
| _ ⇒ False
)"
lemma DFS_call_1_conds[call_cond_elims]:
"DFS_call_1_conds dfs_state ⟹
⟦⟦∃v stack_tl. stack dfs_state = v # stack_tl;
hd (stack dfs_state) ≠ t;
(𝒩⇩G (hd (stack dfs_state))) -⇩G (seen dfs_state) ≠ (∅⇩V)⟧ ⟹ P⟧ ⟹
P"
by(auto simp: DFS_call_1_conds_def split: list.splits option.splits if_splits)
definition "DFS_upd1 dfs_state = (
let
N = (𝒩⇩G (hd (stack dfs_state)));
u = (sel ((N -⇩G (seen dfs_state))));
stack' = u # (stack dfs_state);
seen' = insert u (seen dfs_state)
in
dfs_state ⦇stack := stack', seen := seen'⦈)"
definition DFS_call_2_conds::"('v, 'vset) DFS_state ⇒ bool" where
"DFS_call_2_conds dfs_state =
(case stack dfs_state of (v # stack_tl) ⇒
(if v = t then
False
else (
(if ((𝒩⇩G v) -⇩G (seen dfs_state)) ≠ (∅⇩V) then
False
else True)
)
)
| _ ⇒ False
)"
lemma DFS_call_2_condsE[call_cond_elims]:
"DFS_call_2_conds dfs_state ⟹
⟦⟦∃v stack_tl. stack dfs_state = v # stack_tl;
hd (stack dfs_state) ≠ t;
(𝒩⇩G (hd (stack dfs_state))) -⇩G (seen dfs_state) = (∅⇩V)⟧ ⟹ P⟧ ⟹
P"
by(auto simp: DFS_call_2_conds_def split: list.splits option.splits if_splits)
definition "DFS_upd2 dfs_state =
((dfs_state ⦇stack := tl (stack dfs_state)⦈))"
definition "DFS_ret_1_conds dfs_state =
(case stack dfs_state of (v # stack_tl) ⇒
(if v = t then
False
else (
(if ((𝒩⇩G v) -⇩G (seen dfs_state)) ≠ ∅⇩V then
False
else False)
)
)
| _ ⇒ True
)"
lemma DFS_ret_1_conds[call_cond_elims]:
"DFS_ret_1_conds dfs_state ⟹
⟦⟦stack dfs_state = []⟧ ⟹ P⟧ ⟹
P"
by(auto simp: DFS_ret_1_conds_def split: list.splits option.splits if_splits)
lemma DFS_call_4_condsI[call_cond_intros]:
"⟦stack dfs_state = []⟧ ⟹ DFS_ret_1_conds dfs_state"
by(auto simp: DFS_ret_1_conds_def split: list.splits option.splits if_splits)
definition "DFS_ret1 dfs_state = (dfs_state ⦇return := NotReachable⦈)"
definition "DFS_ret_2_conds dfs_state =
(case stack dfs_state of (v # stack_tl) ⇒
(if v = t then
True
else (
(if (𝒩⇩G v -⇩G (seen dfs_state)) ≠ ∅⇩V then
False
else False)
)
)
| _ ⇒ False
)"
lemma DFS_ret_2_conds[call_cond_elims]:
"DFS_ret_2_conds dfs_state ⟹
⟦⋀v stack_tl. ⟦stack dfs_state = v # stack_tl;
(hd (stack dfs_state)) = t⟧ ⟹ P⟧ ⟹
P"
by(auto simp: DFS_ret_2_conds_def split: list.splits option.splits if_splits)
lemma DFS_ret_2_condsI[call_cond_intros]:
"⋀v stack_tl. ⟦stack dfs_state = v # stack_tl; (hd (stack dfs_state)) = t⟧ ⟹ DFS_ret_2_conds dfs_state"
by(auto simp: DFS_ret_2_conds_def split: list.splits option.splits if_splits)
definition "DFS_ret2 dfs_state = (dfs_state ⦇return := Reachable⦈)"
lemma DFS_cases:
assumes "DFS_call_1_conds dfs_state ⟹ P"
"DFS_call_2_conds dfs_state ⟹ P"
"DFS_ret_1_conds dfs_state ⟹ P"
"DFS_ret_2_conds dfs_state ⟹ P"
shows "P"
proof-
have "DFS_call_1_conds dfs_state ∨ DFS_call_2_conds dfs_state ∨
DFS_ret_1_conds dfs_state ∨ DFS_ret_2_conds dfs_state"
by (auto simp add: DFS_call_1_conds_def DFS_call_2_conds_def
DFS_ret_1_conds_def DFS_ret_2_conds_def
split: list.split_asm option.split_asm if_splits)
then show ?thesis
using assms
by auto
qed
lemma DFS_simps:
assumes "DFS_dom dfs_state"
shows"DFS_call_1_conds dfs_state ⟹ DFS dfs_state = DFS (DFS_upd1 dfs_state)"
"DFS_call_2_conds dfs_state ⟹ DFS dfs_state = DFS (DFS_upd2 dfs_state)"
"DFS_ret_1_conds dfs_state ⟹ DFS dfs_state = DFS_ret1 dfs_state"
"DFS_ret_2_conds dfs_state ⟹ DFS dfs_state = DFS_ret2 dfs_state"
by (auto simp add: DFS.psimps[OF assms] Let_def
DFS_call_1_conds_def DFS_upd1_def DFS_call_2_conds_def DFS_upd2_def
DFS_ret_1_conds_def DFS_ret1_def
DFS_ret_2_conds_def DFS_ret2_def
split: list.splits option.splits if_splits )
lemma DFS_induct:
assumes "DFS_dom dfs_state"
assumes "⋀dfs_state. ⟦DFS_dom dfs_state;
DFS_call_1_conds dfs_state ⟹ P (DFS_upd1 dfs_state);
DFS_call_2_conds dfs_state ⟹ P (DFS_upd2 dfs_state)⟧ ⟹ P dfs_state"
shows "P dfs_state"
apply(rule DFS.pinduct[OF assms(1)])
apply(rule assms(2)[simplified DFS_call_1_conds_def DFS_upd1_def DFS_call_2_conds_def DFS_upd2_def])
by (auto simp: Let_def split: list.splits option.splits if_splits)
lemma DFS_domintros:
assumes "DFS_call_1_conds dfs_state ⟹ DFS_dom (DFS_upd1 dfs_state)"
assumes "DFS_call_2_conds dfs_state ⟹ DFS_dom (DFS_upd2 dfs_state)"
shows "DFS_dom dfs_state"
proof(rule DFS.domintros, goal_cases)
case (1 x21 x22)
then show ?case
using assms(1)[simplified DFS_call_1_conds_def DFS_upd1_def]
by (force simp: Let_def split: list.splits option.splits if_splits)
next
case (2 x21 x22)
then show ?case
using assms(2)[simplified DFS_call_2_conds_def DFS_upd2_def]
by (force split: list.splits option.splits if_splits)
qed
subsection ‹Loop Invariants›
definition invar_well_formed::"('v,'vset) DFS_state ⇒ bool" where
"invar_well_formed dfs_state = vset_inv (seen dfs_state)"
definition invar_stack_walk::"('v,'vset) DFS_state ⇒ bool" where
"invar_stack_walk dfs_state = (Vwalk.vwalk (Graph.digraph_abs G) (rev (stack dfs_state)))"
definition invar_seen_stack::"('v,'vset) DFS_state ⇒ bool" where
"invar_seen_stack dfs_state ⟷
distinct (stack dfs_state)
∧ set (stack dfs_state) ⊆ t_set (seen dfs_state)
∧ t_set (seen dfs_state) ⊆ dVs (Graph.digraph_abs G)"
definition invar_s_in_stack::"('v,'vset) DFS_state ⇒ bool" where
"invar_s_in_stack dfs_state ⟷
(stack (dfs_state) ≠ [] ⟶ last (stack dfs_state) = s)"
definition invar_visited_through_seen::"('v,'vset) DFS_state ⇒ bool" where
"invar_visited_through_seen dfs_state =
(∀v ∈ t_set (seen dfs_state).
(∀p. Vwalk.vwalk_bet (Graph.digraph_abs G) v p t ∧ distinct p ⟶ (set p ∩ set (stack dfs_state) ≠ {})))"
definition call_1_measure::"('v,'vset) DFS_state ⇒ nat" where
"call_1_measure dfs_state = card (dVs (Graph.digraph_abs G) - t_set (seen dfs_state))"
definition call_2_measure::"('v,'vset) DFS_state ⇒ nat" where
"call_2_measure dfs_state = card (set (stack dfs_state))"
definition DFS_term_rel::"(('v,'vset) DFS_state × ('v,'vset) DFS_state) set" where
"DFS_term_rel = (call_1_measure) <*mlex*> (call_2_measure) <*mlex*> {}"
end
locale DFS_thms = DFS +
assumes DFS_axioms: DFS_axioms
begin
context
includes set_ops.automation and Graph.adjmap.automation and Graph.vset.set.automation
begin
lemma graph_inv[simp,intro]:
"Graph.graph_inv G"
"Graph.finite_graph G"
"Graph.finite_vsets"
using DFS_axioms
by (auto simp: DFS_axioms_def)
lemma s_in_G[simp,intro]: "s ∈ dVs (Graph.digraph_abs G)"
using DFS_axioms
by (auto simp: DFS_axioms_def)
lemma finite_neighbourhoods[simp]:
"finite (t_set N)"
using graph_inv(3)
by fastforce
lemmas simps[simp] = Graph.neighbourhood_abs[OF graph_inv(1)] Graph.are_connected_abs[OF graph_inv(1)]
lemma invar_well_formed_props[invar_props_elims]:
"invar_well_formed dfs_state ⟹
(⟦vset_inv (seen dfs_state)⟧ ⟹ P) ⟹
P"
by (auto simp: invar_well_formed_def)
lemma invar_well_formed_intro[invar_props_intros]: "⟦vset_inv (seen dfs_state)⟧
⟹ invar_well_formed dfs_state"
by (auto simp: invar_well_formed_def)
lemma invar_well_formed_holds_1[invar_holds_intros]:
"⟦DFS_call_1_conds dfs_state; invar_well_formed dfs_state⟧ ⟹
invar_well_formed (DFS_upd1 dfs_state)"
by (auto simp: Let_def DFS_upd1_def elim!: invar_props_elims intro!: invar_props_intros)
lemma invar_well_formed_holds_2[invar_holds_intros]: "⟦DFS_call_2_conds dfs_state; invar_well_formed dfs_state⟧ ⟹ invar_well_formed (DFS_upd2 dfs_state)"
by (auto simp: DFS_upd2_def elim!: invar_props_elims intro: invar_props_intros)
lemma invar_well_formed_holds_4[invar_holds_intros]: "⟦DFS_ret_1_conds dfs_state; invar_well_formed dfs_state⟧ ⟹ invar_well_formed (DFS_ret1 dfs_state)"
by (auto elim!: invar_props_elims intro: invar_props_intros simp: DFS_ret1_def)
lemma invar_well_formed_holds_5[invar_holds_intros]: "⟦DFS_ret_2_conds dfs_state; invar_well_formed dfs_state⟧ ⟹ invar_well_formed (DFS_ret2 dfs_state)"
by (auto elim!: invar_props_elims intro: invar_props_intros simp: DFS_ret2_def)
lemma invar_well_formed_holds[invar_holds_intros]:
assumes "DFS_dom dfs_state" "invar_well_formed dfs_state"
shows "invar_well_formed (DFS dfs_state)"
using assms(2)
proof(induction rule: DFS_induct[OF assms(1)])
case IH: (1 dfs_state)
show ?case
apply(rule DFS_cases[where dfs_state = dfs_state])
by (auto intro!: IH(2-4) invar_holds_intros simp: DFS_simps[OF IH(1)])
qed
lemma invar_stack_walk_props[invar_props_elims]:
"invar_stack_walk dfs_state ⟹
((Vwalk.vwalk (Graph.digraph_abs G) (rev (stack dfs_state))) ⟹ P) ⟹ P"
by (auto simp: invar_stack_walk_def)
lemma invar_stack_walk_intro[invar_props_intros]: "Vwalk.vwalk (Graph.digraph_abs G) (rev (stack dfs_state)) ⟹ invar_stack_walk dfs_state"
by (auto simp: invar_stack_walk_def)
lemma invar_stack_walk_holds_1[invar_holds_intros]:
assumes "DFS_call_1_conds dfs_state" "invar_well_formed dfs_state" "invar_stack_walk dfs_state"
shows "invar_stack_walk (DFS_upd1 dfs_state)"
using assms graph_inv
by (force simp: Let_def DFS_upd1_def elim!: call_cond_elims elim!: invar_props_elims
intro!: Vwalk.vwalk_append2 neighbourhoodI invar_props_intros)
lemma invar_stack_walk_holds_2[invar_holds_intros]: "⟦DFS_call_2_conds dfs_state; invar_stack_walk dfs_state⟧ ⟹ invar_stack_walk (DFS_upd2 dfs_state)"
by (auto simp: DFS_upd2_def dest!: append_vwalk_pref elim!: invar_props_elims intro!: invar_props_intros elim: call_cond_elims)
lemma invar_stack_walk_holds_4[invar_holds_intros]: "⟦DFS_ret_1_conds dfs_state; invar_stack_walk dfs_state⟧ ⟹ invar_stack_walk (DFS_ret1 dfs_state)"
by (auto elim!: invar_props_elims intro: invar_props_intros simp: DFS_ret1_def)
lemma invar_2_holds_5[invar_holds_intros]: "⟦DFS_ret_2_conds dfs_state; invar_stack_walk dfs_state⟧ ⟹ invar_stack_walk (DFS_ret2 dfs_state)"
by (auto elim!: invar_props_elims intro: invar_props_intros simp: DFS_ret2_def)
lemma invar_2_holds[invar_holds_intros]:
assumes "DFS_dom dfs_state" "invar_well_formed dfs_state" "invar_stack_walk dfs_state"
shows "invar_stack_walk (DFS dfs_state)"
using assms(2-3)
proof(induction rule: DFS_induct[OF assms(1)])
case IH: (1 dfs_state)
show ?case
apply(rule DFS_cases[where dfs_state = dfs_state])
by (auto intro!: IH(2-5) invar_holds_intros simp: DFS_simps[OF IH(1)])
qed
lemma invar_seen_stack_props[invar_props_elims]:
"invar_seen_stack dfs_state ⟹
(⟦distinct (stack dfs_state); set (stack dfs_state) ⊆ t_set (seen dfs_state);
t_set (seen dfs_state) ⊆ dVs (Graph.digraph_abs G)⟧ ⟹ P) ⟹ P "
by (auto simp: invar_seen_stack_def)
lemma invar_seen_stack_intro[invar_props_intros]:
"⟦distinct (stack dfs_state); set (stack dfs_state) ⊆ t_set (seen dfs_state); t_set (seen dfs_state) ⊆ dVs (Graph.digraph_abs G)⟧ ⟹ invar_seen_stack dfs_state"
by (auto simp: invar_seen_stack_def)
lemma invar_seen_stack_holds_1[invar_holds_intros]:
"⟦DFS_call_1_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state⟧ ⟹ invar_seen_stack (DFS_upd1 dfs_state)"
by (force simp: Let_def DFS_upd1_def dest!: append_vwalk_pref elim!: call_cond_elims
elim!: invar_props_elims intro!: invar_props_intros)
lemma invar_seen_stack_holds_2[invar_holds_intros]:
"⟦DFS_call_2_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state⟧ ⟹
invar_seen_stack (DFS_upd2 dfs_state)"
by (auto elim!: call_cond_elims simp: DFS_upd2_def elim: vwalk_betE
elim!: invar_props_elims dest!: Graph.vset.emptyD append_vwalk_pref intro!: invar_props_intros)
lemma invar_seen_stack_holds_4[invar_holds_intros]:
"⟦DFS_ret_1_conds dfs_state; invar_seen_stack dfs_state⟧ ⟹
invar_seen_stack (DFS_ret1 dfs_state)"
by (auto elim!: invar_props_elims intro!: invar_props_intros simp: DFS_ret1_def)
lemma invar_seen_stack_holds_5[invar_holds_intros]: "⟦DFS_ret_2_conds dfs_state; invar_seen_stack dfs_state⟧ ⟹ invar_seen_stack (DFS_ret2 dfs_state)"
by (auto elim!: invar_props_elims intro!: invar_props_intros simp: DFS_ret2_def)
lemma invar_seen_stack_holds[invar_holds_intros]:
assumes "DFS_dom dfs_state" "invar_well_formed dfs_state" "invar_seen_stack dfs_state"
shows "invar_seen_stack (DFS dfs_state)"
using assms(2-)
proof(induction rule: DFS_induct[OF assms(1)])
case IH: (1 dfs_state)
show ?case
apply(rule DFS_cases[where dfs_state = dfs_state])
by (auto intro!: IH(2-5) invar_holds_intros simp: DFS_simps[OF IH(1)])
qed
lemma invar_s_in_stack_props[invar_props_elims]:
"invar_s_in_stack dfs_state ⟹
(⟦(stack (dfs_state) ≠ [] ⟹ last (stack dfs_state) = s)⟧ ⟹ P) ⟹ P "
by (auto simp: invar_s_in_stack_def)
lemma invar_s_in_stack_intro[invar_props_intros]:
"⟦(stack (dfs_state) ≠ [] ⟹ last (stack dfs_state) = s)⟧ ⟹ invar_s_in_stack dfs_state"
by (auto simp: invar_s_in_stack_def)
lemma invar_s_in_stack_holds_1[invar_holds_intros]:
"⟦DFS_call_1_conds dfs_state; invar_well_formed dfs_state; invar_s_in_stack dfs_state⟧ ⟹ invar_s_in_stack (DFS_upd1 dfs_state)"
by (force simp: Let_def DFS_upd1_def dest!: append_vwalk_pref elim!: call_cond_elims
elim!: invar_props_elims intro!: invar_props_intros)
lemma invar_s_in_stack_holds_2[invar_holds_intros]:
"⟦DFS_call_2_conds dfs_state; invar_well_formed dfs_state; invar_s_in_stack dfs_state⟧ ⟹
invar_s_in_stack (DFS_upd2 dfs_state)"
by (auto elim!: call_cond_elims simp: DFS_upd2_def elim: vwalk_betE
elim!: invar_props_elims dest!: Graph.vset.emptyD append_vwalk_pref intro!: invar_props_intros)
lemma invar_s_in_stack_holds_4[invar_holds_intros]:
"⟦DFS_ret_1_conds dfs_state; invar_s_in_stack dfs_state⟧ ⟹
invar_s_in_stack (DFS_ret1 dfs_state)"
by (auto elim!: invar_props_elims intro!: invar_props_intros simp: DFS_ret1_def)
lemma invar_s_in_stack_holds_5[invar_holds_intros]: "⟦DFS_ret_2_conds dfs_state; invar_s_in_stack dfs_state⟧ ⟹ invar_s_in_stack (DFS_ret2 dfs_state)"
by (auto elim!: invar_props_elims intro!: invar_props_intros simp: DFS_ret2_def)
lemma invar_s_in_stack_holds[invar_holds_intros]:
assumes "DFS_dom dfs_state" "invar_well_formed dfs_state" "invar_s_in_stack dfs_state"
shows "invar_s_in_stack (DFS dfs_state)"
using assms(2-)
proof(induction rule: DFS_induct[OF assms(1)])
case IH: (1 dfs_state)
show ?case
apply(rule DFS_cases[where dfs_state = dfs_state])
by (auto intro!: IH(2-5) invar_holds_intros simp: DFS_simps[OF IH(1)])
qed
lemma invar_visited_through_seen_props[elim!]:
"invar_visited_through_seen dfs_state ⟹
(⟦⋀v p. ⟦v ∈ t_set (seen dfs_state);
(Vwalk.vwalk_bet (Graph.digraph_abs G) v p t); distinct p ⟧ ⟹
set p ∩ set (stack dfs_state) ≠ {}⟧ ⟹ P) ⟹ P "
by (auto simp: invar_visited_through_seen_def)
lemma invar_visited_through_seen_intro[invar_props_intros]:
"⟦⋀v p. ⟦v ∈ t_set (seen dfs_state);
(Vwalk.vwalk_bet (Graph.digraph_abs G) v p t); distinct p⟧ ⟹
set p ∩ set (stack dfs_state) ≠ {}⟧ ⟹ invar_visited_through_seen dfs_state"
by (auto simp: invar_visited_through_seen_def)
subsection ‹Proofs that the Invariants Hold›
lemma invar_visited_through_seen_holds_1[invar_holds_intros]:
"⟦DFS_call_1_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state;
invar_visited_through_seen dfs_state⟧
⟹ invar_visited_through_seen (DFS_upd1 dfs_state)"
by(fastforce simp: Let_def DFS_upd1_def dest: append_vwalk_pref hd_of_vwalk_bet''
elim!: invar_props_elims intro!: invar_props_intros)
lemma invar_visited_through_seen_holds_2[invar_holds_intros]:
"⟦DFS_call_2_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state;
invar_visited_through_seen dfs_state⟧ ⟹ invar_visited_through_seen (DFS_upd2 dfs_state)"
proof(rule invar_props_intros, elim invar_visited_through_seen_props call_cond_elims exE, goal_cases)
case (1 v1 p v2 stack_tl)
text ‹We know one thing: a path starting at @{term v1} and ending at @{term t} intersects with the
old stack @{term "v2 # stack_tl"}.
We have two cases:›
hence "set p ∩ set (stack dfs_state) ≠ {}"
by (auto simp: DFS_upd2_def)
then obtain u where "u ∈ set p ∩ set (stack dfs_state)"
by auto
show ?case
proof(cases "u ∈ set stack_tl")
case True
text ‹
Case 1: If the point of intersection of the path is in @{term stack_tl}, then we are done.›
thus ?thesis
using 1 ‹u ∈ set p ∩ set (stack dfs_state)›
by (auto simp: DFS_upd2_def)
next
case False
hence "u = v2"
using 1 ‹u ∈ set p ∩ set (stack dfs_state)›
by auto
text ‹
Case 2: If it intersects the old stack at @{term v2}, which is the more interesting case as
@{term v2} will not be in the new stack.›
then obtain p1 p2 where [simp]: "p = p1 @ [v2] @ p2"
using ‹u ∈ set p ∩ set (stack dfs_state)›
by (auto simp: in_set_conv_decomp)
text ‹
Let @{term "p = p1 @ [v2] @ p2"}.›
hence "set (v2 # p2) ∩ set (stack dfs_state) ≠ {}"
using 1
by (auto simp: DFS_upd2_def)
text ‹
Since the invariant holds for the old state, then @{term "[v2] @ p2"}
intersects the old stack @{term "v2 # stack_tl"}.›
show ?thesis
proof(cases "p2 = []")
case True
text ‹
There are two cases we need to consider
here:
Case a: @{term "p2 = []"} This cannot be the case, since it would imply that @{term "v2 = t"}, which
violates the assumption of us being in this execution branch.›
thus ?thesis
using 1
by (auto simp: vwalk_bet_snoc)
next
case False
text ‹
Case b: @{term "p2 ≠ []"} From the current branch's assumptions, we know that @{term "hd p2"}, who
is a neighbour of @{term v2}, is in @{term "seen dfs_state"}. This means that, from the
invariant at @{term dfs_state}, we can conclude that @{term "v2#p2"} intersects with the
old stack. However, since it is distinct, that means that @{term p2}
cannot contain @{term v2}. This means that it intersects @{term stack_tl},
which implies that @{term p} with @{term stack_tl}. This finishes our proof.›
hence "hd p2 ∈ t_set (𝒩⇩G v2)"
using ‹vwalk_bet (Graph.digraph_abs G) v1 p t›
by (auto dest!: split_vwalk simp: neq_Nil_conv)
hence "hd p2 ∈ t_set (seen dfs_state)"
using 1
by (fastforce elim!: invar_props_elims simp del: ‹p = p1 @ [v2] @ p2›)
hence "set p2 ∩ set (stack dfs_state) ≠ {}"
using 1 False
by (fastforce simp: DFS_upd2_def neq_Nil_conv dest!: split_vwalk)
moreover have "v2 ∉ set p2"
using ‹distinct p›
by auto
ultimately have "set p2 ∩ set (stack (DFS_upd2 dfs_state)) ≠ {}"
using 1
by (auto simp: DFS_upd2_def)
thus ?thesis
by auto
qed
qed
qed
lemma invar_visited_through_seen_holds_4[invar_holds_intros]: "⟦DFS_ret_1_conds dfs_state; invar_visited_through_seen dfs_state⟧ ⟹ invar_visited_through_seen (DFS_ret1 dfs_state)"
by (auto simp: intro: invar_props_intros simp: DFS_ret1_def)
lemma invar_visited_through_seen_holds_5[invar_holds_intros]: "⟦DFS_ret_2_conds dfs_state; invar_visited_through_seen dfs_state⟧ ⟹ invar_visited_through_seen (DFS_ret2 dfs_state)"
by (auto simp: intro: invar_props_intros simp: DFS_ret2_def)
lemma invar_visited_through_seen_holds[invar_holds_intros]:
assumes "DFS_dom dfs_state" "invar_well_formed dfs_state" "invar_seen_stack dfs_state"
"invar_visited_through_seen dfs_state"
shows "invar_visited_through_seen (DFS dfs_state)"
using assms(2-)
proof(induction rule: DFS_induct[OF assms(1)])
case IH: (1 dfs_state)
show ?case
apply(rule DFS_cases[where dfs_state = dfs_state])
by (auto intro!: IH(2-6) invar_holds_intros simp: DFS_simps[OF IH(1)])
qed
definition "state_rel_1 dfs_state_1 dfs_state_2
= ( t_set (seen dfs_state_1) ⊆ t_set (seen dfs_state_2))"
lemma state_rel_1_props[elim!]: "state_rel_1 dfs_state_1 dfs_state_2 ⟹
(t_set (seen dfs_state_1) ⊆ t_set (seen dfs_state_2) ⟹ P) ⟹ P "
by (auto simp: state_rel_1_def)
lemma state_rel_1_intro[state_rel_intros]:
"⟦t_set (seen dfs_state_1) ⊆ t_set (seen dfs_state_2)⟧ ⟹ state_rel_1 dfs_state_1 dfs_state_2"
by (auto simp: state_rel_1_def)
lemma state_rel_1_trans:
"⟦state_rel_1 dfs_state_1 dfs_state_2; state_rel_1 dfs_state_2 dfs_state_3⟧ ⟹
state_rel_1 dfs_state_1 dfs_state_3"
by (auto intro!: state_rel_intros)
lemma state_rel_1_holds_1[state_rel_holds_intros]:
"⟦DFS_call_1_conds dfs_state; invar_well_formed dfs_state⟧ ⟹ state_rel_1 dfs_state (DFS_upd1 dfs_state)"
by (auto simp: Let_def DFS_upd1_def elim!: invar_props_elims intro!: state_rel_intros)
lemma state_rel_1_holds_2[state_rel_holds_intros]:
"⟦DFS_call_2_conds dfs_state; invar_well_formed dfs_state⟧ ⟹ state_rel_1 dfs_state (DFS_upd2 dfs_state)"
by (auto simp: DFS_upd2_def intro!: state_rel_intros elim: call_cond_elims)
lemma state_rel_1_holds_4[state_rel_holds_intros]:
"⟦DFS_ret_1_conds dfs_state⟧ ⟹ state_rel_1 dfs_state (DFS_ret1 dfs_state)"
by (auto simp: intro!: state_rel_intros simp: DFS_ret1_def)
lemma state_rel_1_holds_5[state_rel_holds_intros]:
"⟦DFS_ret_2_conds dfs_state⟧ ⟹ state_rel_1 dfs_state (DFS_ret2 dfs_state)"
by (auto simp: intro!: state_rel_intros simp: DFS_ret2_def)
lemma state_rel_1_holds[state_rel_holds_intros]:
assumes "DFS_dom dfs_state" "invar_well_formed dfs_state"
shows "state_rel_1 dfs_state (DFS dfs_state)"
using assms(2-)
proof(induction rule: DFS_induct[OF assms(1)])
case IH: (1 dfs_state)
show ?case
apply(rule DFS_cases[where dfs_state = dfs_state])
by (auto intro: state_rel_1_trans invar_holds_intros state_rel_holds_intros intro!: IH(2-) simp: DFS_simps[OF IH(1)])
qed
lemma DFS_ret_1[ret_holds_intros]: "DFS_ret_1_conds (dfs_state) ⟹ DFS_ret_1_conds (DFS_ret1 dfs_state)"
by (auto simp: elim!: call_cond_elims intro!: call_cond_intros simp: DFS_ret1_def)
lemma ret1_holds[ret_holds_intros]:
assumes "DFS_dom dfs_state" "return (DFS dfs_state) = NotReachable"
shows "DFS_ret_1_conds (DFS dfs_state)"
using assms(2-)
proof(induction rule: DFS_induct[OF assms(1)])
case IH: (1 dfs_state)
show ?case
apply(rule DFS_cases[where dfs_state = dfs_state])
using IH(4)
by (auto intro: ret_holds_intros intro!: IH(2-) simp: DFS_simps[OF IH(1)] DFS_ret2_def)
qed
lemma DFS_correct_ret_1:
"⟦invar_visited_through_seen dfs_state; DFS_ret_1_conds dfs_state; u ∈ t_set (seen dfs_state)⟧
⟹ ∄p. distinct p ∧ vwalk_bet (Graph.digraph_abs G) u p t"
by (auto elim!: call_cond_elims invar_props_elims)
lemma DFS_ret_2[ret_holds_intros]: "DFS_ret_2_conds (dfs_state) ⟹ DFS_ret_2_conds (DFS_ret2 dfs_state)"
by (auto simp: elim!: call_cond_elims intro!: call_cond_intros simp: DFS_ret2_def)
lemma ret2_holds[ret_holds_intros]:
assumes "DFS_dom dfs_state" "return (DFS dfs_state) = Reachable"
shows "DFS_ret_2_conds (DFS dfs_state)"
using assms(2-)
proof(induction rule: DFS_induct[OF assms(1)])
case IH: (1 dfs_state)
show ?case
apply(rule DFS_cases[where dfs_state = dfs_state])
using IH(4)
by (auto intro: ret_holds_intros intro!: IH(2-) simp: DFS_simps[OF IH(1)] DFS_ret1_def)
qed
lemma DFS_correct_ret_2:
"⟦invar_stack_walk dfs_state; DFS_ret_2_conds dfs_state⟧
⟹ vwalk_bet (Graph.digraph_abs G) (last (stack dfs_state)) (rev (stack dfs_state)) t"
by (auto elim!: call_cond_elims invar_props_elims simp: hd_rev vwalk_bet_def)
subsection ‹Termination›
named_theorems termination_intros
declare termination_intros
lemma in_prod_relI[intro!,termination_intros]:
"⟦f1 a = f1 a'; (a, a') ∈ f2 <*mlex*> r⟧ ⟹ (a,a') ∈ (f1 <*mlex*> f2 <*mlex*> r)"
by (simp add: mlex_iff)+
definition "less_rel = {(x::nat, y::nat). x < y}"
lemma wf_less_rel[intro!]: "wf less_rel"
by(auto simp: less_rel_def wf_less)
lemma call_1_measure_nonsym[simp]: "(call_1_measure dfs_state, call_1_measure dfs_state) ∉ less_rel"
by (auto simp: less_rel_def)
lemma call_1_terminates[termination_intros]:
"⟦DFS_call_1_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state⟧ ⟹
(DFS_upd1 dfs_state, dfs_state) ∈ call_1_measure <*mlex*> r"
by(fastforce elim!: invar_props_elims call_cond_elims
simp add: DFS_upd1_def call_1_measure_def Let_def
intro!: mlex_less psubset_card_mono
dest!: Graph.vset.choose')
lemma call_2_measure_nonsym[simp]: "(call_2_measure dfs_state, call_2_measure dfs_state) ∉ less_rel"
by (auto simp: less_rel_def)
lemma call_2_measure_1[termination_intros]:
"⟦DFS_call_2_conds dfs_state; invar_well_formed dfs_state⟧ ⟹
call_1_measure dfs_state = call_1_measure (DFS_upd2 dfs_state)"
by(auto simp add: DFS_upd2_def call_1_measure_def Let_def
intro!: psubset_card_mono)
lemma call_2_terminates[termination_intros]:
"⟦DFS_call_2_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state⟧ ⟹
(DFS_upd2 dfs_state, dfs_state) ∈ call_2_measure <*mlex*> r"
by(auto elim!: invar_props_elims elim!: call_cond_elims
simp add: DFS_upd2_def call_2_measure_def
intro!: mlex_less)
lemma wf_term_rel: "wf DFS_term_rel"
by(auto simp: wf_mlex DFS_term_rel_def)
lemma in_DFS_term_rel[termination_intros]:
"⟦DFS_call_1_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state⟧ ⟹
(DFS_upd1 dfs_state, dfs_state) ∈ DFS_term_rel"
"⟦DFS_call_2_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state⟧ ⟹
(DFS_upd2 dfs_state, dfs_state) ∈ DFS_term_rel"
by (simp add: DFS_term_rel_def termination_intros)+
lemma DFS_terminates[termination_intros]:
assumes "invar_well_formed dfs_state" "invar_seen_stack dfs_state"
shows "DFS_dom dfs_state"
using wf_term_rel assms
proof(induction rule: wf_induct_rule)
case (less x)
show ?case
by (rule DFS_domintros) (auto intro!: invar_holds_intros less in_DFS_term_rel)
qed
subsection ‹Final Correctness Theorems›
lemma initial_state_props[invar_holds_intros, termination_intros]:
"invar_well_formed (initial_state)" "invar_stack_walk (initial_state)" "invar_seen_stack (initial_state)"
"invar_visited_through_seen (initial_state)" "invar_s_in_stack initial_state"
"DFS_dom initial_state"
by (auto simp: initial_state_def
hd_of_vwalk_bet''
elim: vwalk_betE
intro!: termination_intros invar_props_intros)
lemma DFS_correct_1:
assumes "return (DFS initial_state) = NotReachable"
shows "∄p. distinct p ∧ vwalk_bet (Graph.digraph_abs G) s p t"
proof-
have "s ∈ t_set (seen (DFS initial_state))"
by(auto intro!: invar_holds_intros ret_holds_intros state_rel_holds_intros
intro: state_rel_1_props[where ?dfs_state_1.0 = initial_state]
simp add: initial_state_def)
thus ?thesis
using assms
by(intro DFS_correct_ret_1[where dfs_state = "DFS initial_state"])
(auto intro!: invar_holds_intros ret_holds_intros state_rel_holds_intros)
qed
lemma DFS_correct_2:
assumes "return (DFS initial_state) = Reachable"
shows "vwalk_bet (Graph.digraph_abs G) s (rev (stack (DFS initial_state))) t"
proof-
have "vwalk_bet
(Graph.digraph_abs G)
(last (stack (DFS initial_state)))
(rev (stack (DFS initial_state))) t"
using assms
by(auto intro!: invar_holds_intros ret_holds_intros state_rel_holds_intros
DFS_correct_ret_2[where dfs_state = "DFS initial_state"])
moreover hence "(last (stack (DFS initial_state))) = s"
by(fastforce intro!: invar_holds_intros
intro: invar_s_in_stack_props[where dfs_state = "DFS initial_state"])+
ultimately show ?thesis
by auto
qed
end
end
end