Theory Gabow_Skeleton
section ‹Skeleton for Gabow's SCC Algorithm \label{sec:skel}›
theory Gabow_Skeleton
imports CAVA_Automata.Digraph
begin
locale fr_graph =
graph G
for G :: "('v, 'more) graph_rec_scheme"
+
assumes finite_reachableE_V0[simp, intro!]: "finite (E⇧* `` V0)"
text ‹
In this theory, we formalize a skeleton of Gabow's SCC algorithm.
The skeleton serves as a starting point to develop concrete algorithms,
like enumerating the SCCs or checking emptiness of a generalized Büchi automaton.
›
section ‹Statistics Setup›
text ‹
We define some dummy-constants that are included into the generated code,
and may be mapped to side-effecting ML-code that records statistics and debug information
about the execution. In the skeleton algorithm, we count the number of visited nodes,
and include a timing for the whole algorithm.
›
definition stat_newnode :: "unit => unit"
where [code]: "stat_newnode ≡ λ_. ()"
definition stat_start :: "unit => unit"
where [code]: "stat_start ≡ λ_. ()"
definition stat_stop :: "unit => unit"
where [code]: "stat_stop ≡ λ_. ()"
lemma [autoref_rules]:
"(stat_newnode,stat_newnode) ∈ unit_rel → unit_rel"
"(stat_start,stat_start) ∈ unit_rel → unit_rel"
"(stat_stop,stat_stop) ∈ unit_rel → unit_rel"
by auto
abbreviation "stat_newnode_nres ≡ RETURN (stat_newnode ())"
abbreviation "stat_start_nres ≡ RETURN (stat_start ())"
abbreviation "stat_stop_nres ≡ RETURN (stat_stop ())"
lemma discard_stat_refine[refine]:
"m1≤m2 ⟹ stat_newnode_nres ⪢ m1 ≤ m2"
"m1≤m2 ⟹ stat_start_nres ⪢ m1 ≤ m2"
"m1≤m2 ⟹ stat_stop_nres ⪢ m1 ≤ m2"
by simp_all
section ‹Abstract Algorithm›
text ‹
In this section, we formalize an abstract version of a path-based SCC algorithm.
Later, this algorithm will be refined to use Gabow's data structure.
›
subsection ‹Preliminaries›
definition path_seg :: "'a set list ⇒ nat ⇒ nat ⇒ 'a set"
where "path_seg p i j ≡ ⋃{p!k|k. i≤k ∧ k<j}"
lemma path_seg_simps[simp]:
"j≤i ⟹ path_seg p i j = {}"
"path_seg p i (Suc i) = p!i"
unfolding path_seg_def
apply auto []
apply (auto simp: le_less_Suc_eq) []
done
lemma path_seg_drop:
"⋃(set (drop i p)) = path_seg p i (length p)"
unfolding path_seg_def
by (fastforce simp: in_set_drop_conv_nth Bex_def)
lemma path_seg_butlast:
"p≠[] ⟹ path_seg p 0 (length p - Suc 0) = ⋃(set (butlast p))"
apply (cases p rule: rev_cases, simp)
apply (fastforce simp: path_seg_def nth_append in_set_conv_nth)
done
definition idx_of :: "'a set list ⇒ 'a ⇒ nat"
where "idx_of p v ≡ THE i. i<length p ∧ v∈p!i"
lemma idx_of_props:
assumes
p_disjoint_sym: "∀i j v. i<length p ∧ j<length p ∧ v∈p!i ∧ v∈p!j ⟶ i=j"
assumes ON_STACK: "v∈⋃(set p)"
shows
"idx_of p v < length p" and
"v ∈ p ! idx_of p v"
proof -
from ON_STACK obtain i where "i<length p" "v ∈ p ! i"
by (auto simp add: in_set_conv_nth)
moreover hence "∀j<length p. v∈p ! j ⟶ i=j"
using p_disjoint_sym by auto
ultimately show "idx_of p v < length p"
and "v ∈ p ! idx_of p v" unfolding idx_of_def
by (metis (lifting) theI')+
qed
lemma idx_of_uniq:
assumes
p_disjoint_sym: "∀i j v. i<length p ∧ j<length p ∧ v∈p!i ∧ v∈p!j ⟶ i=j"
assumes A: "i<length p" "v∈p!i"
shows "idx_of p v = i"
proof -
from A p_disjoint_sym have "∀j<length p. v∈p ! j ⟶ i=j" by auto
with A show ?thesis
unfolding idx_of_def
by (metis (lifting) the_equality)
qed
subsection ‹Invariants›
text ‹The state of the inner loop consists of the path ‹p› of
collapsed nodes, the set ‹D› of finished (done) nodes, and the set
‹pE› of pending edges.›
type_synonym 'v abs_state = "'v set list × 'v set × ('v×'v) set"
context fr_graph
begin
definition touched :: "'v set list ⇒ 'v set ⇒ 'v set"
where "touched p D ≡ D ∪ ⋃(set p)"
definition vE :: "'v set list ⇒ 'v set ⇒ ('v × 'v) set ⇒ ('v × 'v) set"
where "vE p D pE ≡ (E ∩ (touched p D × UNIV)) - pE"
lemma vE_ss_E: "vE p D pE ⊆ E"
unfolding vE_def by auto
end
locale outer_invar_loc
= fr_graph G for G :: "('v,'more) graph_rec_scheme" +
fixes it :: "'v set"
fixes D :: "'v set"
assumes it_initial: "it⊆V0"
assumes it_done: "V0 - it ⊆ D"
assumes D_reachable: "D⊆E⇧*``V0"
assumes D_closed: "E``D ⊆ D"
begin
lemma locale_this: "outer_invar_loc G it D" by unfold_locales
definition (in fr_graph) "outer_invar ≡ λit D. outer_invar_loc G it D"
lemma outer_invar_this[simp, intro!]: "outer_invar it D"
unfolding outer_invar_def apply simp by unfold_locales
end
locale invar_loc
= fr_graph G
for G :: "('v, 'more) graph_rec_scheme" +
fixes v0 :: "'v"
fixes D0 :: "'v set"
fixes p :: "'v set list"
fixes D :: "'v set"
fixes pE :: "('v×'v) set"
assumes v0_initial[simp, intro!]: "v0∈V0"
assumes D_incr: "D0 ⊆ D"
assumes pE_E_from_p: "pE ⊆ E ∩ (⋃(set p)) × UNIV"
assumes E_from_p_touched: "E ∩ (⋃(set p) × UNIV) ⊆ pE ∪ UNIV × touched p D"
assumes D_reachable: "D⊆E⇧*``V0"
assumes p_connected: "Suc i<length p ⟹ p!i × p!Suc i ∩ (E-pE) ≠ {}"
assumes p_disjoint: "⟦i<j; j<length p⟧ ⟹ p!i ∩ p!j = {}"
assumes p_sc: "U∈set p ⟹ U×U ⊆ (vE p D pE ∩ U×U)⇧*"
assumes root_v0: "p≠[] ⟹ v0∈hd p"
assumes p_empty_v0: "p=[] ⟹ v0∈D"
assumes D_closed: "E``D ⊆ D"
assumes vE_no_back: "⟦i<j; j<length p⟧ ⟹ vE p D pE ∩ p!j × p!i = {}"
assumes p_not_D: "⋃(set p) ∩ D = {}"
begin
abbreviation ltouched where "ltouched ≡ touched p D"
abbreviation lvE where "lvE ≡ vE p D pE"
lemma locale_this: "invar_loc G v0 D0 p D pE" by unfold_locales
definition (in fr_graph)
"invar ≡ λv0 D0 (p,D,pE). invar_loc G v0 D0 p D pE"
lemma invar_this[simp, intro!]: "invar v0 D0 (p,D,pE)"
unfolding invar_def apply simp by unfold_locales
lemma finite_reachableE_v0[simp, intro!]: "finite (E⇧*``{v0})"
apply (rule finite_subset[OF _ finite_reachableE_V0])
using v0_initial by auto
lemma D_vis: "E∩D×UNIV ⊆ lvE"
unfolding vE_def touched_def using pE_E_from_p p_not_D by blast
lemma vE_touched: "lvE ⊆ ltouched × ltouched"
using E_from_p_touched D_closed unfolding vE_def touched_def by blast
lemma lvE_ss_E: "lvE ⊆ E"
unfolding vE_def by auto
lemma path_touched: "⋃(set p) ⊆ ltouched" by (auto simp: touched_def)
lemma D_touched: "D ⊆ ltouched" by (auto simp: touched_def)
lemma pE_by_vE: "pE = (E ∩ ⋃(set p) × UNIV) - lvE"
unfolding vE_def touched_def
using pE_E_from_p
by auto
lemma pick_pending: "p≠[] ⟹ pE ∩ last p × UNIV = (E-lvE) ∩ last p × UNIV"
apply (subst pE_by_vE)
by auto
lemma p_connected':
assumes A: "Suc i<length p"
shows "p!i × p!Suc i ∩ lvE ≠ {}"
proof -
from A p_not_D have "p!i ∈ set p" "p!Suc i ∈ set p" by auto
with p_connected[OF A] show ?thesis unfolding vE_def touched_def
by blast
qed
end
subsubsection ‹Termination›
context fr_graph
begin
text ‹The termination argument is based on unprocessed edges:
Reachable edges from untouched nodes and pending edges.›
definition "unproc_edges v0 p D pE ≡ (E ∩ (E⇧*``{v0} - (D ∪ ⋃(set p))) × UNIV) ∪ pE"
text ‹
In each iteration of the loop, either the number of unprocessed edges
decreases, or the path length decreases.›
definition "abs_wf_rel v0 ≡ inv_image (finite_psubset <*lex*> measure length)
(λ(p,D,pE). (unproc_edges v0 p D pE, p))"
lemma abs_wf_rel_wf[simp, intro!]: "wf (abs_wf_rel v0)"
unfolding abs_wf_rel_def
by auto
end
subsection ‹Abstract Skeleton Algorithm›
context fr_graph
begin
definition (in fr_graph) initial :: "'v ⇒ 'v set ⇒ 'v abs_state"
where "initial v0 D ≡ ([{v0}], D, (E ∩ {v0}×UNIV))"
definition (in -) collapse_aux :: "'a set list ⇒ nat ⇒ 'a set list"
where "collapse_aux p i ≡ take i p @ [⋃(set (drop i p))]"
definition (in -) collapse :: "'a ⇒ 'a abs_state ⇒ 'a abs_state"
where "collapse v PDPE ≡
let
(p,D,pE)=PDPE;
i=idx_of p v;
p = collapse_aux p i
in (p,D,pE)"
definition (in -)
select_edge :: "'a abs_state ⇒ ('a option × 'a abs_state) nres"
where
"select_edge PDPE ≡ do {
let (p,D,pE) = PDPE;
e ← SELECT (λe. e ∈ pE ∩ last p × UNIV);
case e of
None ⇒ RETURN (None,(p,D,pE))
| Some (u,v) ⇒ RETURN (Some v, (p,D,pE - {(u,v)}))
}"
definition (in fr_graph) push :: "'v ⇒ 'v abs_state ⇒ 'v abs_state"
where "push v PDPE ≡
let
(p,D,pE) = PDPE;
p = p@[{v}];
pE = pE ∪ (E∩{v}×UNIV)
in
(p,D,pE)"
definition (in -) pop :: "'v abs_state ⇒ 'v abs_state"
where "pop PDPE ≡ let
(p,D,pE) = PDPE;
(p,V) = (butlast p, last p);
D = V ∪ D
in
(p,D,pE)"
text ‹The following lemmas match the definitions presented in the paper:›
lemma "select_edge (p,D,pE) ≡ do {
e ← SELECT (λe. e ∈ pE ∩ last p × UNIV);
case e of
None ⇒ RETURN (None,(p,D,pE))
| Some (u,v) ⇒ RETURN (Some v, (p,D,pE - {(u,v)}))
}"
unfolding select_edge_def by simp
lemma "collapse v (p,D,pE)
≡ let i=idx_of p v in (take i p @ [⋃(set (drop i p))],D,pE)"
unfolding collapse_def collapse_aux_def by simp
lemma "push v (p, D, pE) ≡ (p @ [{v}], D, pE ∪ E ∩ {v} × UNIV)"
unfolding push_def by simp
lemma "pop (p, D, pE) ≡ (butlast p, last p ∪ D, pE)"
unfolding pop_def by auto
thm pop_def[unfolded Let_def, no_vars]
thm select_edge_def[unfolded Let_def]
definition skeleton :: "'v set nres"
where
"skeleton ≡ do {
let D = {};
r ← FOREACHi outer_invar V0 (λv0 D0. do {
if v0∉D0 then do {
let s = initial v0 D0;
(p,D,pE) ← WHILEIT (invar v0 D0)
(λ(p,D,pE). p ≠ []) (λ(p,D,pE).
do {
(vo,(p,D,pE)) ← select_edge (p,D,pE);
ASSERT (p≠[]);
case vo of
Some v ⇒ do {
if v ∈ ⋃(set p) then do {
RETURN (collapse v (p,D,pE))
} else if v∉D then do {
RETURN (push v (p,D,pE))
} else do {
RETURN (p,D,pE)
}
}
| None ⇒ do {
ASSERT (pE ∩ last p × UNIV = {});
RETURN (pop (p,D,pE))
}
}) s;
ASSERT (p=[] ∧ pE={});
RETURN D
} else
RETURN D0
}) D;
RETURN r
}"
end
subsection ‹Invariant Preservation›
context fr_graph begin
lemma set_collapse_aux[simp]: "⋃(set (collapse_aux p i)) = ⋃(set p)"
apply (subst (2) append_take_drop_id[of _ p,symmetric])
apply (simp del: append_take_drop_id)
unfolding collapse_aux_def by auto
lemma touched_collapse[simp]: "touched (collapse_aux p i) D = touched p D"
unfolding touched_def by simp
lemma vE_collapse_aux[simp]: "vE (collapse_aux p i) D pE = vE p D pE"
unfolding vE_def by simp
lemma touched_push[simp]: "touched (p @ [V]) D = touched p D ∪ V"
unfolding touched_def by auto
end
subsubsection ‹Corollaries of the invariant›
text ‹In this section, we prove some more corollaries of the invariant,
which are helpful to show invariant preservation›
context invar_loc
begin
lemma cnode_connectedI:
"⟦i<length p; u∈p!i; v∈p!i⟧ ⟹ (u,v)∈(lvE ∩ p!i×p!i)⇧*"
using p_sc[of "p!i"] by (auto simp: in_set_conv_nth)
lemma cnode_connectedI': "⟦i<length p; u∈p!i; v∈p!i⟧ ⟹ (u,v)∈(lvE)⇧*"
by (metis inf.cobounded1 rtrancl_mono_mp cnode_connectedI)
lemma p_no_empty: "{} ∉ set p"
proof
assume "{}∈set p"
then obtain i where IDX: "i<length p" "p!i={}"
by (auto simp add: in_set_conv_nth)
show False proof (cases i)
case 0 with root_v0 IDX show False by (cases p) auto
next
case [simp]: (Suc j)
from p_connected'[of j] IDX show False by simp
qed
qed
corollary p_no_empty_idx: "i<length p ⟹ p!i≠{}"
using p_no_empty by (metis nth_mem)
lemma p_disjoint_sym: "⟦i<length p; j<length p; v∈p!i; v∈p!j⟧ ⟹ i=j"
by (metis disjoint_iff_not_equal linorder_neqE_nat p_disjoint)
lemma pi_ss_path_seg_eq[simp]:
assumes A: "i<length p" "u≤length p"
shows "p!i⊆path_seg p l u ⟷ l≤i ∧ i<u"
proof
assume B: "p!i⊆path_seg p l u"
from A obtain x where "x∈p!i" by (blast dest: p_no_empty_idx)
with B obtain i' where C: "x∈p!i'" "l≤i'" "i'<u"
by (auto simp: path_seg_def)
from p_disjoint_sym[OF ‹i<length p› _ ‹x∈p!i› ‹x∈p!i'›] ‹i'<u› ‹u≤length p›
have "i=i'" by simp
with C show "l≤i ∧ i<u" by auto
qed (auto simp: path_seg_def)
lemma path_seg_ss_eq[simp]:
assumes A: "l1<u1" "u1≤length p" "l2<u2" "u2≤length p"
shows "path_seg p l1 u1 ⊆ path_seg p l2 u2 ⟷ l2≤l1 ∧ u1≤u2"
proof
assume S: "path_seg p l1 u1 ⊆ path_seg p l2 u2"
have "p!l1 ⊆ path_seg p l1 u1" using A by simp
also note S finally have 1: "l2≤l1" using A by simp
have "p!(u1 - 1) ⊆ path_seg p l1 u1" using A by simp
also note S finally have 2: "u1≤u2" using A by auto
from 1 2 show "l2≤l1 ∧ u1≤u2" ..
next
assume "l2≤l1 ∧ u1≤u2" thus "path_seg p l1 u1 ⊆ path_seg p l2 u2"
using A
apply (clarsimp simp: path_seg_def) []
apply (metis dual_order.strict_trans1 dual_order.trans)
done
qed
lemma pathI:
assumes "x∈p!i" "y∈p!j"
assumes "i≤j" "j<length p"
defines "seg ≡ path_seg p i (Suc j)"
shows "(x,y)∈(lvE ∩ seg×seg)⇧*"
using assms(3,1,2,4) unfolding seg_def
proof (induction arbitrary: y rule: dec_induct)
case base thus ?case by (auto intro!: cnode_connectedI)
next
case (step j)
let ?seg = "path_seg p i (Suc j)"
let ?seg' = "path_seg p i (Suc (Suc j))"
have SSS: "?seg ⊆ ?seg'"
apply (subst path_seg_ss_eq)
using step.hyps step.prems by auto
from p_connected'[OF ‹Suc j < length p›] obtain u v where
UV: "(u,v)∈lvE" "u∈p!j" "v∈p!Suc j" by auto
have ISS: "p!j ⊆ ?seg'" "p!Suc j ⊆ ?seg'"
using step.hyps step.prems by simp_all
from p_no_empty_idx[of j] ‹Suc j < length p› obtain x' where "x'∈p!j"
by auto
with step.IH[of x'] ‹x∈p!i› ‹Suc j < length p›
have t: "(x,x')∈(lvE∩?seg×?seg)⇧*" by auto
have "(x,x')∈(lvE∩?seg'×?seg')⇧*" using SSS
by (auto intro: rtrancl_mono_mp[OF _ t])
also
from cnode_connectedI[OF _ ‹x'∈p!j› ‹u∈p!j›] ‹Suc j < length p› have
t: "(x', u) ∈ (lvE ∩ p ! j × p ! j)⇧*" by auto
have "(x', u) ∈ (lvE∩?seg'×?seg')⇧*" using ISS
by (auto intro: rtrancl_mono_mp[OF _ t])
also have "(u,v)∈lvE∩?seg'×?seg'" using UV ISS by auto
also from cnode_connectedI[OF ‹Suc j < length p› ‹v∈p!Suc j› ‹y∈p!Suc j›]
have t: "(v, y) ∈ (lvE ∩ p ! Suc j × p ! Suc j)⇧*" by auto
have "(v, y) ∈ (lvE∩?seg'×?seg')⇧*" using ISS
by (auto intro: rtrancl_mono_mp[OF _ t])
finally show "(x,y)∈(lvE∩?seg'×?seg')⇧*" .
qed
lemma p_reachable: "⋃(set p) ⊆ E⇧*``{v0}"
proof
fix v
assume A: "v∈⋃(set p)"
then obtain i where "i<length p" and "v∈p!i"
by (metis UnionE in_set_conv_nth)
moreover from A root_v0 have "v0∈p!0" by (cases p) auto
ultimately have
t: "(v0,v)∈(lvE ∩ path_seg p 0 (Suc i) × path_seg p 0 (Suc i))⇧*"
by (auto intro: pathI)
from lvE_ss_E have "(v0,v)∈E⇧*" by (auto intro: rtrancl_mono_mp[OF _ t])
thus "v∈E⇧*``{v0}" by auto
qed
lemma touched_reachable: "ltouched ⊆ E⇧*``V0"
unfolding touched_def using p_reachable D_reachable by blast
lemma vE_reachable: "lvE ⊆ E⇧*``V0 × E⇧*``V0"
apply (rule order_trans[OF vE_touched])
using touched_reachable by blast
lemma pE_reachable: "pE ⊆ E⇧*``{v0} × E⇧*``{v0}"
proof safe
fix u v
assume E: "(u,v)∈pE"
with pE_E_from_p p_reachable have "(v0,u)∈E⇧*" "(u,v)∈E" by blast+
thus "(v0,u)∈E⇧*" "(v0,v)∈E⇧*" by auto
qed
lemma D_closed_vE_rtrancl: "lvE⇧*``D ⊆ D"
by (metis D_closed Image_closed_trancl eq_iff reachable_mono lvE_ss_E)
lemma D_closed_path: "⟦path E u q w; u∈D⟧ ⟹ set q ⊆ D"
proof -
assume a1: "path E u q w"
assume "u ∈ D"
hence f1: "{u} ⊆ D"
using bot.extremum by force
have "set q ⊆ E⇧* `` {u}"
using a1 by (metis insert_subset path_nodes_reachable)
thus "set q ⊆ D"
using f1 by (metis D_closed rtrancl_reachable_induct subset_trans)
qed
lemma D_closed_path_vE: "⟦path lvE u q w; u∈D⟧ ⟹ set q ⊆ D"
by (metis D_closed_path path_mono lvE_ss_E)
lemma path_in_lastnode:
assumes P: "path lvE u q v"
assumes [simp]: "p≠[]"
assumes ND: "u∈last p" "v∈last p"
shows "set q ⊆ last p"
using P ND
proof (induction)
case (path_prepend u v l w)
from ‹(u,v)∈lvE› vE_touched have "v∈ltouched" by auto
hence "v∈⋃(set p)"
unfolding touched_def
proof
assume "v∈D"
moreover from ‹path lvE v l w› have "(v,w)∈lvE⇧*" by (rule path_is_rtrancl)
ultimately have "w∈D" using D_closed_vE_rtrancl by auto
with ‹w∈last p› p_not_D have False
by (metis IntI Misc.last_in_set Sup_inf_eq_bot_iff assms(2)
bex_empty path_prepend.hyps(2))
thus ?thesis ..
qed
then obtain i where "i<length p" "v∈p!i"
by (metis UnionE in_set_conv_nth)
have "i=length p - 1"
proof (rule ccontr)
assume "i≠length p - 1"
with ‹i<length p› have "i < length p - 1" by simp
with vE_no_back[of i "length p - 1"] ‹i<length p›
have "lvE ∩ last p × p!i = {}"
by (simp add: last_conv_nth)
with ‹(u,v)∈lvE› ‹u∈last p› ‹v∈p!i› show False by auto
qed
with ‹v∈p!i› have "v∈last p" by (simp add: last_conv_nth)
with path_prepend.IH ‹w∈last p› ‹u∈last p› show ?case by auto
qed simp
lemma loop_in_lastnode:
assumes P: "path lvE u q u"
assumes [simp]: "p≠[]"
assumes ND: "set q ∩ last p ≠ {}"
shows "u∈last p" and "set q ⊆ last p"
proof -
from ND obtain v where "v∈set q" "v∈last p" by auto
then obtain q1 q2 where [simp]: "q=q1@v#q2"
by (auto simp: in_set_conv_decomp)
from P have "path lvE v (v#q2@q1) v"
by (auto simp: path_conc_conv path_cons_conv)
from path_in_lastnode[OF this ‹p≠[]› ‹v∈last p› ‹v∈last p›]
show "set q ⊆ last p" by simp
from P show "u∈last p"
apply (cases q, simp)
apply simp
using ‹set q ⊆ last p›
apply (auto simp: path_cons_conv)
done
qed
lemma no_D_p_edges: "E ∩ D × ⋃(set p) = {}"
using D_closed p_not_D by auto
lemma idx_of_props:
assumes ON_STACK: "v∈⋃(set p)"
shows
"idx_of p v < length p" and
"v ∈ p ! idx_of p v"
using idx_of_props[OF _ assms] p_disjoint_sym by blast+
end
subsubsection ‹Auxiliary Lemmas Regarding the Operations›
lemma (in fr_graph) vE_initial[simp]: "vE [{v0}] {} (E ∩ {v0} × UNIV) = {}"
unfolding vE_def touched_def by auto
context invar_loc
begin
lemma vE_push: "⟦ (u,v)∈pE; u∈last p; v∉⋃(set p); v∉D ⟧
⟹ vE (p @ [{v}]) D ((pE - {(u,v)}) ∪ E∩{v}×UNIV) = insert (u,v) lvE"
unfolding vE_def touched_def using pE_E_from_p
by auto
lemma vE_remove[simp]:
"⟦p≠[]; (u,v)∈pE⟧ ⟹ vE p D (pE - {(u,v)}) = insert (u,v) lvE"
unfolding vE_def touched_def using pE_E_from_p by blast
lemma vE_pop[simp]: "p≠[] ⟹ vE (butlast p) (last p ∪ D) pE = lvE"
unfolding vE_def touched_def
by (cases p rule: rev_cases) auto
lemma pE_fin: "p=[] ⟹ pE={}"
using pE_by_vE by auto
lemma (in invar_loc) lastp_un_D_closed:
assumes NE: "p ≠ []"
assumes NO': "pE ∩ (last p × UNIV) = {}"
shows "E``(last p ∪ D) ⊆ (last p ∪ D)"
proof (intro subsetI, elim ImageE)
from NO' have NO: "(E - lvE) ∩ (last p × UNIV) = {}"
by (simp add: pick_pending[OF NE])
let ?i = "length p - 1"
from NE have [simp]: "last p = p!?i" by (metis last_conv_nth)
fix u v
assume E: "(u,v)∈E"
assume UI: "u∈last p ∪ D" hence "u∈p!?i ∪ D" by simp
{
assume "u∈last p" "v∉last p"
moreover from E NO ‹u∈last p› have "(u,v)∈lvE" by auto
ultimately have "v∈D ∨ v∈⋃(set p)"
using vE_touched unfolding touched_def by auto
moreover {
assume "v∈⋃(set p)"
then obtain j where V: "j<length p" "v∈p!j"
by (metis UnionE in_set_conv_nth)
with ‹v∉last p› have "j<?i" by (cases "j=?i") auto
from vE_no_back[OF ‹j<?i› _] ‹(u,v)∈lvE› V ‹u∈last p› have False by auto
} ultimately have "v∈D" by blast
} with E UI D_closed show "v∈last p ∪ D" by auto
qed
end
subsubsection ‹Preservation of Invariant by Operations›
context fr_graph
begin
lemma (in outer_invar_loc) invar_initial_aux:
assumes "v0∈it - D"
shows "invar v0 D (initial v0 D)"
unfolding invar_def initial_def
apply simp
apply unfold_locales
apply simp_all
using assms it_initial apply auto []
using D_reachable it_initial assms apply auto []
using D_closed apply auto []
using assms apply auto []
done
lemma invar_initial:
"⟦outer_invar it D0; v0∈it; v0∉D0⟧ ⟹ invar v0 D0 (initial v0 D0)"
unfolding outer_invar_def
apply (drule outer_invar_loc.invar_initial_aux)
by auto
lemma outer_invar_initial[simp, intro!]: "outer_invar V0 {}"
unfolding outer_invar_def
apply unfold_locales
by auto
lemma invar_pop:
assumes INV: "invar v0 D0 (p,D,pE)"
assumes NE[simp]: "p≠[]"
assumes NO': "pE ∩ (last p × UNIV) = {}"
shows "invar v0 D0 (pop (p,D,pE))"
unfolding invar_def pop_def
apply simp
proof -
from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp
have [simp]: "set p = insert (last p) (set (butlast p))"
using NE by (cases p rule: rev_cases) auto
from p_disjoint have lp_dj_blp: "last p ∩ ⋃(set (butlast p)) = {}"
apply (cases p rule: rev_cases)
apply simp
apply (fastforce simp: in_set_conv_nth nth_append)
done
{
fix i
assume A: "Suc i < length (butlast p)"
hence A': "Suc i < length p" by auto
from nth_butlast[of i p] A have [simp]: "butlast p ! i = p ! i" by auto
from nth_butlast[of "Suc i" p] A
have [simp]: "butlast p ! Suc i = p ! Suc i" by auto
from p_connected[OF A']
have "butlast p ! i × butlast p ! Suc i ∩ (E - pE) ≠ {}"
by simp
} note AUX_p_connected = this
show "invar_loc G v0 D0 (butlast p) (last p ∪ D) pE"
apply unfold_locales
unfolding vE_pop[OF NE]
apply simp
using D_incr apply auto []
using pE_E_from_p NO' apply auto []
using E_from_p_touched apply (auto simp: touched_def) []
using D_reachable p_reachable NE apply auto []
apply (rule AUX_p_connected, assumption+) []
using p_disjoint apply (simp add: nth_butlast)
using p_sc apply simp
using root_v0 apply (cases p rule: rev_cases) apply auto [2]
using root_v0 p_empty_v0 apply (cases p rule: rev_cases) apply auto [2]
apply (rule lastp_un_D_closed, insert NO', auto) []
using vE_no_back apply (auto simp: nth_butlast) []
using p_not_D lp_dj_blp apply auto []
done
qed
thm invar_pop[of v_0 D_0, no_vars]
lemma invar_collapse:
assumes INV: "invar v0 D0 (p,D,pE)"
assumes NE[simp]: "p≠[]"
assumes E: "(u,v)∈pE" and "u∈last p"
assumes BACK: "v∈⋃(set p)"
defines "i ≡ idx_of p v"
defines "p' ≡ collapse_aux p i"
shows "invar v0 D0 (collapse v (p,D,pE - {(u,v)}))"
unfolding invar_def collapse_def
apply simp
unfolding i_def[symmetric] p'_def[symmetric]
proof -
from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp
let ?thesis="invar_loc G v0 D0 p' D (pE - {(u,v)})"
have SETP'[simp]: "⋃(set p') = ⋃(set p)" unfolding p'_def by simp
have IL: "i < length p" and VMEM: "v∈p!i"
using idx_of_props[OF BACK] unfolding i_def by auto
have [simp]: "length p' = Suc i"
unfolding p'_def collapse_aux_def using IL by auto
have P'_IDX_SS: "∀j<Suc i. p!j ⊆ p'!j"
unfolding p'_def collapse_aux_def using IL
by (auto simp add: nth_append path_seg_drop)
from ‹u∈last p› have "u∈p!(length p - 1)" by (auto simp: last_conv_nth)
have defs_fold:
"vE p' D (pE - {(u,v)}) = insert (u,v) lvE"
"touched p' D = ltouched"
by (simp_all add: p'_def E)
{
fix j
assume A: "Suc j < length p'"
hence "Suc j < length p" using IL by simp
from p_connected[OF this] have "p!j × p!Suc j ∩ (E-pE) ≠ {}" .
moreover from P'_IDX_SS A have "p!j⊆p'!j" and "p!Suc j ⊆ p'!Suc j"
by auto
ultimately have "p' ! j × p' ! Suc j ∩ (E - (pE - {(u, v)})) ≠ {}"
by blast
} note AUX_p_connected = this
have P_IDX_EQ[simp]: "∀j. j < i ⟶ p'!j = p!j"
unfolding p'_def collapse_aux_def using IL
by (auto simp: nth_append)
have P'_LAST[simp]: "p'!i = path_seg p i (length p)" (is "_ = ?last_cnode")
unfolding p'_def collapse_aux_def using IL
by (auto simp: nth_append path_seg_drop)
{
fix j k
assume A: "j < k" "k < length p'"
have "p' ! j ∩ p' ! k = {}"
proof (safe, simp)
fix v
assume "v∈p'!j" and "v∈p'!k"
with A have "v∈p!j" by simp
show False proof (cases)
assume "k=i"
with ‹v∈p'!k› obtain k' where "v∈p!k'" "i≤k'" "k'<length p"
by (auto simp: path_seg_def)
hence "p ! j ∩ p ! k' = {}"
using A by (auto intro!: p_disjoint)
with ‹v∈p!j› ‹v∈p!k'› show False by auto
next
assume "k≠i" with A have "k<i" by simp
hence "k<length p" using IL by simp
note p_disjoint[OF ‹j<k› this]
also have "p!j = p'!j" using ‹j<k› ‹k<i› by simp
also have "p!k = p'!k" using ‹k<i› by simp
finally show False using ‹v∈p'!j› ‹v∈p'!k› by auto
qed
qed
} note AUX_p_disjoint = this
{
fix U
assume A: "U∈set p'"
then obtain j where "j<Suc i" and [simp]: "U=p'!j"
by (auto simp: in_set_conv_nth)
hence "U × U ⊆ (insert (u, v) lvE ∩ U × U)⇧*"
proof cases
assume [simp]: "j=i"
show ?thesis proof (clarsimp)
fix x y
assume "x∈path_seg p i (length p)" "y∈path_seg p i (length p)"
then obtain ix iy where
IX: "x∈p!ix" "i≤ix" "ix<length p" and
IY: "y∈p!iy" "i≤iy" "iy<length p"
by (auto simp: path_seg_def)
from IX have SS1: "path_seg p ix (length p) ⊆ ?last_cnode"
by (subst path_seg_ss_eq) auto
from IY have SS2: "path_seg p i (Suc iy) ⊆ ?last_cnode"
by (subst path_seg_ss_eq) auto
let ?rE = "λR. (lvE ∩ R×R)"
let ?E = "(insert (u,v) lvE ∩ ?last_cnode × ?last_cnode)"
from pathI[OF ‹x∈p!ix› ‹u∈p!(length p - 1)›] have
"(x,u)∈(?rE (path_seg p ix (Suc (length p - 1))))⇧*" using IX by auto
hence "(x,u)∈?E⇧*"
apply (rule rtrancl_mono_mp[rotated])
using SS1
by auto
also have "(u,v)∈?E" using ‹i<length p›
apply (clarsimp)
apply (intro conjI)
apply (rule rev_subsetD[OF ‹u∈p!(length p - 1)›])
apply (simp)
apply (rule rev_subsetD[OF VMEM])
apply (simp)
done
also
from pathI[OF ‹v∈p!i› ‹y∈p!iy›] have
"(v,y)∈(?rE (path_seg p i (Suc iy)))⇧*" using IY by auto
hence "(v,y)∈?E⇧*"
apply (rule rtrancl_mono_mp[rotated])
using SS2
by auto
finally show "(x,y)∈?E⇧*" .
qed
next
assume "j≠i"
with ‹j<Suc i› have [simp]: "j<i" by simp
with ‹i<length p› have "p!j∈set p"
by (metis Suc_lessD in_set_conv_nth less_trans_Suc)
thus ?thesis using p_sc[of U] ‹p!j∈set p›
apply (clarsimp)
apply (subgoal_tac "(a,b)∈(lvE ∩ p ! j × p ! j)⇧*")
apply (erule rtrancl_mono_mp[rotated])
apply auto
done
qed
} note AUX_p_sc = this
{ fix j k
assume A: "j<k" "k<length p'"
hence "j<i" by simp
have "insert (u, v) lvE ∩ p' ! k × p' ! j = {}"
proof -
have "{(u,v)} ∩ p' ! k × p' ! j = {}"
apply auto
by (metis IL P_IDX_EQ Suc_lessD VMEM ‹j < i›
less_irrefl_nat less_trans_Suc p_disjoint_sym)
moreover have "lvE ∩ p' ! k × p' ! j = {}"
proof (cases "k<i")
case True thus ?thesis
using vE_no_back[of j k] A ‹i<length p› by auto
next
case False with A have [simp]: "k=i" by simp
show ?thesis proof (rule disjointI, clarsimp simp: ‹j<i›)
fix x y
assume B: "(x,y)∈lvE" "x∈path_seg p i (length p)" "y∈p!j"
then obtain ix where "x∈p!ix" "i≤ix" "ix<length p"
by (auto simp: path_seg_def)
moreover with A have "j<ix" by simp
ultimately show False using vE_no_back[of j ix] B by auto
qed
qed
ultimately show ?thesis by blast
qed
} note AUX_vE_no_back = this
show ?thesis
apply unfold_locales
unfolding defs_fold
apply simp
using D_incr apply auto []
using pE_E_from_p apply auto []
using E_from_p_touched BACK apply (simp add: touched_def) apply blast
apply (rule D_reachable)
apply (rule AUX_p_connected, assumption+) []
apply (rule AUX_p_disjoint, assumption+) []
apply (rule AUX_p_sc, assumption+) []
using root_v0
apply (cases i)
apply (simp add: p'_def collapse_aux_def)
apply (metis NE hd_in_set)
apply (cases p, simp_all add: p'_def collapse_aux_def) []
apply (simp add: p'_def collapse_aux_def)
apply (rule D_closed)
apply (drule (1) AUX_vE_no_back, auto) []
using p_not_D apply simp
done
qed
lemma invar_push:
assumes INV: "invar v0 D0 (p,D,pE)"
assumes NE[simp]: "p≠[]"
assumes E: "(u,v)∈pE" and UIL: "u∈last p"
assumes VNE: "v∉⋃(set p)" "v∉D"
shows "invar v0 D0 (push v (p,D,pE - {(u,v)}))"
unfolding invar_def push_def
apply simp
proof -
from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp
let ?thesis
= "invar_loc G v0 D0 (p @ [{v}]) D (pE - {(u, v)} ∪ E ∩ {v} × UNIV)"
note defs_fold = vE_push[OF E UIL VNE] touched_push
{
fix i
assume SILL: "Suc i < length (p @ [{v}])"
have "(p @ [{v}]) ! i × (p @ [{v}]) ! Suc i
∩ (E - (pE - {(u, v)} ∪ E ∩ {v} × UNIV)) ≠ {}"
proof (cases "i = length p - 1")
case True thus ?thesis using SILL E pE_E_from_p UIL VNE
by (simp add: nth_append last_conv_nth) fast
next
case False
with SILL have SILL': "Suc i < length p" by simp
with SILL' VNE have X1: "v∉p!i" "v∉p!Suc i" by auto
from p_connected[OF SILL'] obtain a b where
"a∈p!i" "b∈p!Suc i" "(a,b)∈E" "(a,b)∉pE"
by auto
with X1 have "a≠v" "b≠v" by auto
with ‹(a,b)∈E› ‹(a,b)∉pE› have "(a,b)∈(E - (pE - {(u, v)} ∪ E ∩ {v} × UNIV))"
by auto
with ‹a∈p!i› ‹b∈p!Suc i›
show ?thesis using SILL'
by (simp add: nth_append; blast)
qed
} note AUX_p_connected = this
{
fix U
assume A: "U ∈ set (p @ [{v}])"
have "U × U ⊆ (insert (u, v) lvE ∩ U × U)⇧*"
proof cases
assume "U∈set p"
with p_sc have "U×U ⊆ (lvE ∩ U×U)⇧*" .
thus ?thesis
by (metis (lifting, no_types) Int_insert_left_if0 Int_insert_left_if1
in_mono insert_subset rtrancl_mono_mp subsetI)
next
assume "U∉set p" with A have "U={v}" by simp
thus ?thesis by auto
qed
} note AUX_p_sc = this
{
fix i j
assume A: "i < j" "j < length (p @ [{v}])"
have "insert (u, v) lvE ∩ (p @ [{v}]) ! j × (p @ [{v}]) ! i = {}"
proof (cases "j=length p")
case False with A have "j<length p" by simp
from vE_no_back ‹i<j› this VNE show ?thesis
by (auto simp add: nth_append)
next
from p_not_D A have PDDJ: "p!i ∩ D = {}"
by (auto simp: Sup_inf_eq_bot_iff)
case True thus ?thesis
using A apply (simp add: nth_append)
apply (rule conjI)
using UIL A p_disjoint_sym
apply (metis Misc.last_in_set NE UnionI VNE(1))
using vE_touched VNE PDDJ apply (auto simp: touched_def) []
done
qed
} note AUX_vE_no_back = this
show ?thesis
apply unfold_locales
unfolding defs_fold
apply simp
using D_incr apply auto []
using pE_E_from_p apply auto []
using E_from_p_touched VNE apply (auto simp: touched_def) []
apply (rule D_reachable)
apply (rule AUX_p_connected, assumption+) []
using p_disjoint ‹v∉⋃(set p)› apply (auto simp: nth_append) []
apply (rule AUX_p_sc, assumption+) []
using root_v0 apply simp
apply simp
apply (rule D_closed)
apply (rule AUX_vE_no_back, assumption+) []
using p_not_D VNE apply auto []
done
qed
lemma invar_skip:
assumes INV: "invar v0 D0 (p,D,pE)"
assumes NE[simp]: "p≠[]"
assumes E: "(u,v)∈pE" and UIL: "u∈last p"
assumes VNP: "v∉⋃(set p)" and VD: "v∈D"
shows "invar v0 D0 (p,D,pE - {(u, v)})"
unfolding invar_def
apply simp
proof -
from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp
let ?thesis = "invar_loc G v0 D0 p D (pE - {(u, v)})"
note defs_fold = vE_remove[OF NE E]
show ?thesis
apply unfold_locales
unfolding defs_fold
apply simp
using D_incr apply auto []
using pE_E_from_p apply auto []
using E_from_p_touched VD apply (auto simp: touched_def) []
apply (rule D_reachable)
using p_connected apply auto []
apply (rule p_disjoint, assumption+) []
apply (drule p_sc)
apply (erule order_trans)
apply (rule rtrancl_mono)
apply blast []
apply (rule root_v0, assumption+) []
apply (rule p_empty_v0, assumption+) []
apply (rule D_closed)
using vE_no_back VD p_not_D
apply clarsimp
apply (metis Suc_lessD UnionI VNP less_trans_Suc nth_mem)
apply (rule p_not_D)
done
qed
lemma fin_D_is_reachable:
assumes INV: "invar v0 D0 ([], D, pE)"
shows "D ⊇ E⇧*``{v0}"
proof -
from INV interpret invar_loc G v0 D0 "[]" D pE unfolding invar_def by auto
from p_empty_v0 rtrancl_reachable_induct[OF order_refl D_closed] D_reachable
show ?thesis by auto
qed
lemma fin_reachable_path:
assumes INV: "invar v0 D0 ([], D, pE)"
assumes UR: "u∈E⇧*``{v0}"
shows "path (vE [] D pE) u q v ⟷ path E u q v"
proof -
from INV interpret invar_loc G v0 D0 "[]" D pE unfolding invar_def by auto
show ?thesis
proof
assume "path lvE u q v"
thus "path E u q v" using path_mono[OF lvE_ss_E] by blast
next
assume "path E u q v"
thus "path lvE u q v" using UR
proof induction
case (path_prepend u v p w)
with fin_D_is_reachable[OF INV] have "u∈D" by auto
with D_closed ‹(u,v)∈E› have "v∈D" by auto
from path_prepend.prems path_prepend.hyps have "v∈E⇧*``{v0}" by auto
with path_prepend.IH fin_D_is_reachable[OF INV] have "path lvE v p w"
by simp
moreover from ‹u∈D› ‹v∈D› ‹(u,v)∈E› D_vis have "(u,v)∈lvE" by auto
ultimately show ?case by (auto simp: path_cons_conv)
qed simp
qed
qed
lemma invar_outer_newnode:
assumes A: "v0∉D0" "v0∈it"
assumes OINV: "outer_invar it D0"
assumes INV: "invar v0 D0 ([],D',pE)"
shows "outer_invar (it-{v0}) D'"
proof -
from OINV interpret outer_invar_loc G it D0 unfolding outer_invar_def .
from INV interpret inv: invar_loc G v0 D0 "[]" D' pE
unfolding invar_def by simp
from fin_D_is_reachable[OF INV] have [simp]: "v0∈D'" by auto
show ?thesis
unfolding outer_invar_def
apply unfold_locales
using it_initial apply auto []
using it_done inv.D_incr apply auto []
using inv.D_reachable apply assumption
using inv.D_closed apply assumption
done
qed
lemma invar_outer_Dnode:
assumes A: "v0∈D0" "v0∈it"
assumes OINV: "outer_invar it D0"
shows "outer_invar (it-{v0}) D0"
proof -
from OINV interpret outer_invar_loc G it D0 unfolding outer_invar_def .
show ?thesis
unfolding outer_invar_def
apply unfold_locales
using it_initial apply auto []
using it_done A apply auto []
using D_reachable apply assumption
using D_closed apply assumption
done
qed
lemma pE_fin': "invar x σ ([], D, pE) ⟹ pE={}"
unfolding invar_def by (simp add: invar_loc.pE_fin)
end
subsubsection ‹Termination›
context invar_loc
begin
lemma unproc_finite[simp, intro!]: "finite (unproc_edges v0 p D pE)"
proof -
have "unproc_edges v0 p D pE ⊆ E⇧*``{v0} × E⇧*``{v0}"
unfolding unproc_edges_def
using pE_reachable
by auto
thus ?thesis
by (rule finite_subset) simp
qed
lemma unproc_decreasing:
assumes [simp]: "p≠[]" and A: "(u,v)∈pE" "u∈last p"
shows "unproc_edges v0 p D (pE-{(u,v)}) ⊂ unproc_edges v0 p D pE"
using A unfolding unproc_edges_def
by fastforce
end
context fr_graph
begin
lemma abs_wf_pop:
assumes INV: "invar v0 D0 (p,D,pE)"
assumes NE[simp]: "p≠[]"
assumes NO: "pE ∩ last aba × UNIV = {}"
shows "(pop (p,D,pE), (p, D, pE)) ∈ abs_wf_rel v0"
unfolding pop_def
apply simp
proof -
from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp
let ?thesis = "((butlast p, last p ∪ D, pE), p, D, pE) ∈ abs_wf_rel v0"
have "unproc_edges v0 (butlast p) (last p ∪ D) pE = unproc_edges v0 p D pE"
unfolding unproc_edges_def
apply (cases p rule: rev_cases, simp)
apply auto
done
thus ?thesis
by (auto simp: abs_wf_rel_def)
qed
lemma abs_wf_collapse:
assumes INV: "invar v0 D0 (p,D,pE)"
assumes NE[simp]: "p≠[]"
assumes E: "(u,v)∈pE" "u∈last p"
shows "(collapse v (p,D,pE-{(u,v)}), (p, D, pE))∈ abs_wf_rel v0"
unfolding collapse_def
apply simp
proof -
from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp
define i where "i = idx_of p v"
let ?thesis
= "((collapse_aux p i, D, pE-{(u,v)}), (p, D, pE)) ∈ abs_wf_rel v0"
have "unproc_edges v0 (collapse_aux p i) D (pE-{(u,v)})
= unproc_edges v0 p D (pE-{(u,v)})"
unfolding unproc_edges_def by (auto)
also note unproc_decreasing[OF NE E]
finally show ?thesis
by (auto simp: abs_wf_rel_def)
qed
lemma abs_wf_push:
assumes INV: "invar v0 D0 (p,D,pE)"
assumes NE[simp]: "p≠[]"
assumes E: "(u,v)∈pE" "u∈last p" and A: "v∉D" "v∉⋃(set p)"
shows "(push v (p,D,pE-{(u,v)}), (p, D, pE)) ∈ abs_wf_rel v0"
unfolding push_def
apply simp
proof -
from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp
let ?thesis
= "((p@[{v}], D, pE-{(u,v)} ∪ E∩{v}×UNIV), (p, D, pE)) ∈ abs_wf_rel v0"
have "unproc_edges v0 (p@[{v}]) D (pE-{(u,v)} ∪ E∩{v}×UNIV)
= unproc_edges v0 p D (pE-{(u,v)})"
unfolding unproc_edges_def
using E A pE_reachable
by auto
also note unproc_decreasing[OF NE E]
finally show ?thesis
by (auto simp: abs_wf_rel_def)
qed
lemma abs_wf_skip:
assumes INV: "invar v0 D0 (p,D,pE)"
assumes NE[simp]: "p≠[]"
assumes E: "(u,v)∈pE" "u∈last p"
shows "((p, D, pE-{(u,v)}), (p, D, pE)) ∈ abs_wf_rel v0"
proof -
from INV interpret invar_loc G v0 D0 p D pE unfolding invar_def by simp
from unproc_decreasing[OF NE E] show ?thesis
by (auto simp: abs_wf_rel_def)
qed
end
subsubsection ‹Main Correctness Theorem›
context fr_graph
begin
lemmas invar_preserve =
invar_initial
invar_pop invar_push invar_skip invar_collapse
abs_wf_pop abs_wf_collapse abs_wf_push abs_wf_skip
outer_invar_initial invar_outer_newnode invar_outer_Dnode
text ‹The main correctness theorem for the dummy-algorithm just states that
it satisfies the invariant when finished, and the path is empty.
›
theorem skeleton_spec: "skeleton ≤ SPEC (λD. outer_invar {} D)"
proof -
note [simp del] = Union_iff
note [[goals_limit = 4]]
show ?thesis
unfolding skeleton_def select_edge_def select_def
apply (refine_vcg WHILEIT_rule[OF abs_wf_rel_wf])
apply (vc_solve solve: invar_preserve simp: pE_fin' finite_V0)
apply auto
done
qed
text ‹Short proof, as presented in the paper›
context
notes [refine] = refine_vcg
begin
theorem "skeleton ≤ SPEC (λD. outer_invar {} D)"
unfolding skeleton_def select_edge_def select_def
by (refine_vcg WHILEIT_rule[OF abs_wf_rel_wf])
(auto intro: invar_preserve simp: pE_fin' finite_V0)
end
end
subsection "Consequences of Invariant when Finished"
context fr_graph
begin
lemma fin_outer_D_is_reachable:
assumes INV: "outer_invar {} D"
shows "D = E⇧*``V0"
proof -
from INV interpret outer_invar_loc G "{}" D unfolding outer_invar_def by auto
from it_done rtrancl_reachable_induct[OF order_refl D_closed] D_reachable
show ?thesis by auto
qed
end
section ‹Refinement to Gabow's Data Structure›text_raw‹\label{sec:algo-ds}›
text ‹
The implementation due to Gabow \<^cite>‹"Gabow00"› represents a path as
a stack ‹S› of single nodes, and a stack ‹B› that contains the
boundaries of the collapsed segments. Moreover, a map ‹I› maps nodes
to their stack indices.
As we use a tail-recursive formulation, we use another stack
‹P :: (nat × 'v set) list› to represent the pending edges. The
entries in ‹P› are sorted by ascending first component,
and ‹P› only contains entries with non-empty second component.
An entry ‹(i,l)› means that the edges from the node at
‹S[i]› to the nodes stored in ‹l› are pending.
›
subsection ‹Preliminaries›
primrec find_max_nat :: "nat ⇒ (nat⇒bool) ⇒ nat"
where
"find_max_nat 0 _ = 0"
| "find_max_nat (Suc n) P = (if (P n) then n else find_max_nat n P)"
lemma find_max_nat_correct:
"⟦P 0; 0<u⟧ ⟹ find_max_nat u P = Max {i. i<u ∧ P i}"
apply (induction u)
apply auto
apply (rule Max_eqI[THEN sym])
apply auto [3]
apply (case_tac u)
apply simp
apply clarsimp
by (metis less_SucI less_antisym)
lemma find_max_nat_param[param]:
assumes "(n,n')∈nat_rel"
assumes "⋀j j'. ⟦(j,j')∈nat_rel; j'<n'⟧ ⟹ (P j,P' j')∈bool_rel"
shows "(find_max_nat n P,find_max_nat n' P') ∈ nat_rel"
using assms
by (induction n arbitrary: n') auto
context begin interpretation autoref_syn .
lemma find_max_nat_autoref[autoref_rules]:
assumes "(n,n')∈nat_rel"
assumes "⋀j j'. ⟦(j,j')∈nat_rel; j'<n'⟧ ⟹ (P j,P'$j')∈bool_rel"
shows "(find_max_nat n P,
(OP find_max_nat ::: nat_rel → (nat_rel→bool_rel) → nat_rel) $n'$P'
) ∈ nat_rel"
using find_max_nat_param[OF assms]
by simp
end
subsection ‹Gabow's Datastructure›
subsubsection ‹Definition and Invariant›
datatype node_state = STACK nat | DONE
type_synonym 'v oGS = "'v ⇀ node_state"
definition oGS_α :: "'v oGS ⇒ 'v set" where "oGS_α I ≡ {v. I v = Some DONE}"
locale oGS_invar =
fixes I :: "'v oGS"
assumes I_no_stack: "I v ≠ Some (STACK j)"
type_synonym 'a GS
= "'a list × nat list × ('a ⇀ node_state) × (nat × 'a set) list"
locale GS =
fixes SBIP :: "'a GS"
begin
definition "S ≡ (λ(S,B,I,P). S) SBIP"
definition "B ≡ (λ(S,B,I,P). B) SBIP"
definition "I ≡ (λ(S,B,I,P). I) SBIP"
definition "P ≡ (λ(S,B,I,P). P) SBIP"
definition seg_start :: "nat ⇒ nat"
where "seg_start i ≡ B!i"
definition seg_end :: "nat ⇒ nat"
where "seg_end i ≡ if i+1 = length B then length S else B!(i+1)"
definition seg :: "nat ⇒ 'a set"
where "seg i ≡ {S!j | j. seg_start i ≤ j ∧ j < seg_end i }"
definition "p_α ≡ map seg [0..<length B]"
definition "D_α ≡ {v. I v = Some DONE}"
definition "pE_α ≡ { (u,v) . ∃j I. (j,I)∈set P ∧ u = S!j ∧ v∈I }"
definition "α ≡ (p_α,D_α,pE_α)"
end
lemma GS_sel_simps[simp]:
"GS.S (S,B,I,P) = S"
"GS.B (S,B,I,P) = B"
"GS.I (S,B,I,P) = I"
"GS.P (S,B,I,P) = P"
unfolding GS.S_def GS.B_def GS.I_def GS.P_def
by auto
context GS begin
lemma seg_start_indep[simp]: "GS.seg_start (S',B,I',P') = seg_start"
unfolding GS.seg_start_def[abs_def] by (auto)
lemma seg_end_indep[simp]: "GS.seg_end (S,B,I',P') = seg_end"
unfolding GS.seg_end_def[abs_def] by auto
lemma seg_indep[simp]: "GS.seg (S,B,I',P') = seg"
unfolding GS.seg_def[abs_def] by auto
lemma p_α_indep[simp]: "GS.p_α (S,B,I',P') = p_α"
unfolding GS.p_α_def by auto
lemma D_α_indep[simp]: "GS.D_α (S',B',I,P') = D_α"
unfolding GS.D_α_def by auto
lemma pE_α_indep[simp]: "GS.pE_α (S,B',I',P) = pE_α"
unfolding GS.pE_α_def by auto
definition find_seg
where "find_seg j ≡ Max {i. i<length B ∧ B!i≤j}"
definition S_idx_of
where "S_idx_of v ≡ case I v of Some (STACK i) ⇒ i"
end
locale GS_invar = GS +
assumes B_in_bound: "set B ⊆ {0..<length S}"
assumes B_sorted: "sorted B"
assumes B_distinct: "distinct B"
assumes B0: "S≠[] ⟹ B≠[] ∧ B!0=0"
assumes S_distinct: "distinct S"
assumes I_consistent: "(I v = Some (STACK j)) ⟷ (j<length S ∧ v = S!j)"
assumes P_sorted: "sorted (map fst P)"
assumes P_distinct: "distinct (map fst P)"
assumes P_bound: "set P ⊆ {0..<length S}×Collect ((≠) {})"
begin
lemma locale_this: "GS_invar SBIP" by unfold_locales
end
definition "oGS_rel ≡ br oGS_α oGS_invar"
lemma oGS_rel_sv[intro!,simp,relator_props]: "single_valued oGS_rel"
unfolding oGS_rel_def by auto
definition "GS_rel ≡ br GS.α GS_invar"
lemma GS_rel_sv[intro!,simp,relator_props]: "single_valued GS_rel"
unfolding GS_rel_def by auto
context GS_invar
begin
lemma empty_eq: "S=[] ⟷ B=[]"
using B_in_bound B0 by auto
lemma B_in_bound': "i<length B ⟹ B!i < length S"
using B_in_bound nth_mem by fastforce
lemma seg_start_bound:
assumes A: "i<length B" shows "seg_start i < length S"
using B_in_bound nth_mem[OF A] unfolding seg_start_def by auto
lemma seg_end_bound:
assumes A: "i<length B" shows "seg_end i ≤ length S"
proof (cases "i+1=length B")
case True thus ?thesis by (simp add: seg_end_def)
next
case False with A have "i+1<length B" by simp
from nth_mem[OF this] B_in_bound have " B ! (i + 1) < length S" by auto
thus ?thesis using False by (simp add: seg_end_def)
qed
lemma seg_start_less_end: "i<length B ⟹ seg_start i < seg_end i"
unfolding seg_start_def seg_end_def
using B_in_bound' distinct_sorted_mono[OF B_sorted B_distinct]
by auto
lemma seg_end_less_start: "⟦i<j; j<length B⟧ ⟹ seg_end i ≤ seg_start j"
unfolding seg_start_def seg_end_def
by (auto simp: distinct_sorted_mono_iff[OF B_distinct B_sorted])
lemma find_seg_bounds:
assumes A: "j<length S"
shows "seg_start (find_seg j) ≤ j"
and "j < seg_end (find_seg j)"
and "find_seg j < length B"
proof -
let ?M = "{i. i<length B ∧ B!i≤j}"
from A have [simp]: "B≠[]" using empty_eq by (cases S) auto
have NE: "?M≠{}" using A B0 by (cases B) auto
have F: "finite ?M" by auto
from Max_in[OF F NE]
have LEN: "find_seg j < length B" and LB: "B!find_seg j ≤ j"
unfolding find_seg_def
by auto
thus "find_seg j < length B" by -
from LB show LB': "seg_start (find_seg j) ≤ j"
unfolding seg_start_def by simp
moreover show UB': "j < seg_end (find_seg j)"
unfolding seg_end_def
proof (split if_split, intro impI conjI)
show "j<length S" using A .
assume "find_seg j + 1 ≠ length B"
with LEN have P1: "find_seg j + 1 < length B" by simp
show "j < B ! (find_seg j + 1)"
proof (rule ccontr, simp only: linorder_not_less)
assume P2: "B ! (find_seg j + 1) ≤ j"
with P1 Max_ge[OF F, of "find_seg j + 1", folded find_seg_def]
show False by simp
qed
qed
qed
lemma find_seg_correct:
assumes A: "j<length S"
shows "S!j ∈ seg (find_seg j)" and "find_seg j < length B"
using find_seg_bounds[OF A]
unfolding seg_def by auto
lemma set_p_α_is_set_S:
"⋃(set p_α) = set S"
apply rule
unfolding p_α_def seg_def[abs_def]
using seg_end_bound apply fastforce []
apply (auto simp: in_set_conv_nth)
using find_seg_bounds
apply (fastforce simp: in_set_conv_nth)
done
lemma S_idx_uniq:
"⟦i<length S; j<length S⟧ ⟹ S!i=S!j ⟷ i=j"
using S_distinct
by (simp add: nth_eq_iff_index_eq)
lemma S_idx_of_correct:
assumes A: "v∈⋃(set p_α)"
shows "S_idx_of v < length S" and "S!S_idx_of v = v"
proof -
from A have "v∈set S" by (simp add: set_p_α_is_set_S)
then obtain j where G1: "j<length S" "v=S!j" by (auto simp: in_set_conv_nth)
with I_consistent have "I v = Some (STACK j)" by simp
hence "S_idx_of v = j" by (simp add: S_idx_of_def)
with G1 show "S_idx_of v < length S" and "S!S_idx_of v = v" by simp_all
qed
lemma p_α_disjoint_sym:
shows "∀i j v. i<length p_α ∧ j<length p_α ∧ v∈p_α!i ∧ v∈p_α!j ⟶ i=j"
proof (intro allI impI, elim conjE)
fix i j v
assume A: "i < length p_α" "j < length p_α" "v ∈ p_α ! i" "v ∈ p_α ! j"
from A have LI: "i<length B" and LJ: "j<length B" by (simp_all add: p_α_def)
from A have B1: "seg_start j < seg_end i" and B2: "seg_start i < seg_end j"
unfolding p_α_def seg_def[abs_def]
apply clarsimp_all
apply (subst (asm) S_idx_uniq)
apply (metis dual_order.strict_trans1 seg_end_bound)
apply (metis dual_order.strict_trans1 seg_end_bound)
apply simp
apply (subst (asm) S_idx_uniq)
apply (metis dual_order.strict_trans1 seg_end_bound)
apply (metis dual_order.strict_trans1 seg_end_bound)
apply simp
done
from B1 have B1: "(B!j < B!Suc i ∧ Suc i < length B) ∨ i=length B - 1"
using LI unfolding seg_start_def seg_end_def by (auto split: if_split_asm)
from B2 have B2: "(B!i < B!Suc j ∧ Suc j < length B) ∨ j=length B - 1"
using LJ unfolding seg_start_def seg_end_def by (auto split: if_split_asm)
from B1 have B1: "j<Suc i ∨ i=length B - 1"
using LI LJ distinct_sorted_strict_mono_iff[OF B_distinct B_sorted]
by auto
from B2 have B2: "i<Suc j ∨ j=length B - 1"
using LI LJ distinct_sorted_strict_mono_iff[OF B_distinct B_sorted]
by auto
from B1 B2 show "i=j"
using LI LJ
by auto
qed
end
subsection ‹Refinement of the Operations›
definition GS_initial_impl :: "'a oGS ⇒ 'a ⇒ 'a set ⇒ 'a GS" where
"GS_initial_impl I v0 succs ≡ (
[v0],
[0],
I(v0↦(STACK 0)),
if succs={} then [] else [(0,succs)])"
context GS
begin
definition "push_impl v succs ≡
let
_ = stat_newnode ();
j = length S;
S = S@[v];
B = B@[j];
I = I(v ↦ STACK j);
P = if succs={} then P else P@[(j,succs)]
in
(S,B,I,P)"
definition mark_as_done
where "⋀l u I. mark_as_done l u I ≡ do {
(_,I)←WHILET
(λ(l,I). l<u)
(λ(l,I). do { ASSERT (l<length S); RETURN (Suc l,I(S!l ↦ DONE))})
(l,I);
RETURN I
}"
definition mark_as_done_abs where
"⋀l u I. mark_as_done_abs l u I
≡ (λv. if v∈{S!j | j. l≤j ∧ j<u} then Some DONE else