Theory Gabow_SCC
section ‹Enumerating the SCCs of a Graph \label{sec:scc}›
theory Gabow_SCC
imports Gabow_Skeleton
begin
text ‹
We implement an algorithm that computes a list of SCCs
of a graph, in topological order. This is the standard variant described by
Gabow~\cite{Gabow2000}.
›
subsection ‹General lemmas›
lemma insert_Suc_elem: "{P j |j. j < Suc n} = insert (P n) {P j |j. j < n}"
apply auto
by (metis less_SucE)
lemma insert_Suc_elem_image: "n ≤ i ⟹ A ` {n..<Suc i} = insert (A i) (A ` {n..<i})"
apply(induction i)
apply auto
by (metis atLeastLessThan_iff imageI less_SucE)
lemma cond_set_eq: "⟦⋀x. P x ⟹ f x = g x⟧ ⟹ {f x |x. P x} = {g x |x. P x}"
by metis
lemma cond_set_eq_image: "⟦⋀i. i∈I ⟹ P i = Q i⟧ ⟹ P ` I = Q ` I"
by simp
lemma fin_nonempty_card_gt_1:
"finite A ⟹ A ≠ {} ⟹ card A ≥ 1"
apply(cases "card A = 0")
apply simp
by linarith
lemma fin_disj_union_card:
assumes "finite I" and "∀i∈I. finite (A i)"
and "∀i∈I. ∀j∈I. i ≠ j ⟶ A i ∩ A j = {}"
and "∀i ∈ I. A i ≠ {}"
shows "card I ≤ card (⋃ (A ` I))"
proof -
have "∀i∈I. card (A i) ≥ 1"
using fin_nonempty_card_gt_1 assms(2) assms(4) by fast
hence "∀i∈I.(∑x∈A i. Suc 0) ≥ Suc 0"
by(simp add: card_eq_sum sum.UNION_disjoint del: sum_constant)
hence "(∑x∈I. Suc 0) ≤ (∑x∈I. ∑x∈A x. Suc 0)"
by (meson sum_mono)
moreover have "(∑i∈I. card (A i)) = (∑i∈I. ∑x∈A i. 1)"
by simp
ultimately show ?thesis using assms
by(simp add: card_eq_sum sum.UNION_disjoint del: sum_constant)
qed
lemma card_UN_disjoint:
assumes "finite I" and "∀i∈I. finite (A i)"
and "∀i∈I. ∀j∈I. i ≠ j ⟶ A i ∩ A j = {}"
shows "card (⋃(A ` I)) = (∑i∈I. card(A i))"
proof -
have "(∑i∈I. card (A i)) = (∑i∈I. ∑x∈A i. 1)"
by simp
with assms show ?thesis
by (simp add: card_eq_sum sum.UNION_disjoint del: sum_constant)
qed
subsection ‹Specification›
context fr_graph
begin
text ‹We specify a distinct list that covers all reachable nodes and
contains SCCs in topological order›
definition "scc_set = {scc. is_scc E scc ∧ scc ⊆ E⇧* `` V0}"
lemma scc_set_mem: "s ∈ scc_set ⟷ is_scc E s ∧ s ⊆ E⇧* `` V0"
unfolding scc_set_def by simp
lemma scc_set_of_scc: "scc_set ⊆ Collect (is_scc E)"
unfolding scc_set_def
by blast
lemma scc_set_covers_state_space: "⋃ scc_set = E⇧* `` V0"
proof(safe)
fix x SCC
assume "x ∈ SCC" "SCC ∈ scc_set"
then show "x ∈ E⇧* `` V0"
unfolding scc_set_def
by blast
next
fix u v
assume "(u,v) ∈ E⇧*" "u ∈ V0"
hence A: "v ∈ E⇧* `` V0" by blast
obtain SCC where B: "v ∈ SCC" "is_scc E SCC"
by (meson is_scc_ex)
hence "SCC ⊆ E⇧* `` V0"
using A is_scc_connected rtrancl_trans by fast
with B show "v ∈ ⋃ scc_set"
unfolding scc_set_def by blast
qed
lemma scc_set_disj: "SCC1 ∈ scc_set ⟹ SCC2 ∈ scc_set ⟹ SCC1 ≠ SCC2 ⟹ SCC1 ∩ SCC2 = {}"
unfolding scc_set_def
using scc_disj_or_eq by auto
lemma finite_scc_set: "finite scc_set"
using finite_reachableE_V0 unfolding scc_set_def by auto
lemma scc_set_alt_def: "scc_set = scc_of E ` (E⇧* `` V0)"
proof -
{
fix S
assume "S ∈ scc_set"
hence "is_scc E S" and "S ⊆ E⇧* `` V0" unfolding scc_set_def by auto
moreover then obtain v where "v ∈ S" and "S = scc_of E v"
by (metis is_scc_unique node_in_scc_of_node scc_non_empty' scc_of_is_scc subset_empty subset_emptyI)
ultimately have "S ∈ scc_of E ` E⇧* `` V0" by fast
} note AUX1 = this
{
fix S
assume "S ∈ scc_of E ` E⇧* `` V0"
then obtain v where VREACH: "v ∈ E⇧* `` V0" and "S = scc_of E v" and SCC: "is_scc E S" and VMEM: "v ∈ S"
by(auto simp: image_iff)
have "S ⊆ E⇧* `` V0"
proof safe
fix x
assume "x ∈ S"
with SCC VMEM have "(v,x) ∈ E⇧*"
unfolding is_scc_def
by blast
with VREACH show "x ∈ E⇧* `` V0"
using rtrancl_image_advance_rtrancl
by fast
qed
hence "S ∈ scc_set"
unfolding scc_set_def
using SCC
by simp
} note AUX2 = this
from AUX1 AUX2 show ?thesis by blast
qed
definition "compute_SCC_spec ≡ SPEC (λ l. set l = scc_set ∧ (∀i j. i < j ⟶ j < length l ⟶ l!i × l!j ∩ E⇧* = {}))"
end
subsection ‹Extended Invariant›
locale cscc_invar_ext = fr_graph E V0 for E :: "'v digraph" and V0 :: "'v set" +
fixes l :: "'v set list" and D :: "'v set"
assumes scc_is_D: "⋃ (set l) = D"
assumes is_scc_set: "set l ⊆ scc_set"
assumes scc_nforward: "⋀ i j. i < j ⟹ j < length l ⟹l!i × l!j ∩ E⇧* = {}"
begin
definition "SCC = set l"
lemma reachable_scc: assumes "U ∈ SCC" shows "is_scc E U" and "U ⊆ E⇧* `` V0"
using assms is_scc_set SCC_def
apply(auto simp: scc_set_def)
done
lemma scc_no_empty: "{}∉SCC" using reachable_scc SCC_def by fastforce
lemma scc_disjoint: "⋀ S1 S2. ⟦ S1 ∈ SCC; S2 ∈ SCC; S1 ≠ S2 ⟧ ⟹ S1 ∩ S2 = {}"
using scc_disj_or_eq reachable_scc
by blast
lemma finite_SCC: "finite SCC"
unfolding SCC_def
using finite_subset[OF is_scc_set finite_scc_set] .
lemma "card SCC ≤ card scc_set"
unfolding SCC_def
using card_mono[OF finite_scc_set is_scc_set] .
lemma scc_nforward_append:
assumes NBACK_IN_NEW: "(⋀ k1 k2. k1 < k2 ⟹ k2 < length nl ⟹ nl!k1 × nl!k2 ∩ E⇧* = {})"
assumes NBACK_TO_NEW: "(⋀ k1 k2. k1 < length l ⟹ k2 < length nl ⟹ l!k1 × nl!k2 ∩ E⇧* = {})"
assumes JLEN_LT: "j < length l + length nl"
assumes IJ_LT: "i < j"
shows "(l @ nl)!i × (l @ nl)!j ∩ E⇧* = {}"
apply(cases "j < length l")
subgoal using IJ_LT by (simp add: scc_nforward)
subgoal apply(cases "i < length l")
subgoal
apply(simp add: nth_append)
apply(rule NBACK_TO_NEW)
using JLEN_LT by auto
subgoal
apply(simp add: nth_append)
apply(rule NBACK_IN_NEW)
using JLEN_LT IJ_LT by auto
done
done
lemma scc_done: "i < length l ⟹ l!i ⊆ D"
using scc_is_D by force
end
locale cscc_outer_invar_loc = outer_invar_loc E V0 it D + cscc_invar_ext E V0 l D
for E :: "'v digraph" and V0 :: "'v set" and it l D
begin
lemma locale_this: "cscc_outer_invar_loc E V0 it l D" by unfold_locales
lemma abs_outer_this: "outer_invar_loc E V0 it D" by unfold_locales
end
locale cscc_invar_loc = invar_loc E V0 v0 D0 p D pE vE + cscc_invar_ext E V0 l D
for E :: "'v digraph" and V0 :: "'v set" and v0 D0 and l :: "'v set list"
and p D pE vE
begin
lemma locale_this: "cscc_invar_loc E V0 v0 D0 l p D pE vE" by unfold_locales
lemma invar_this: "invar_loc E V0 v0 D0 p D pE vE" by unfold_locales
end
context fr_graph
begin
definition "cscc_outer_invar ≡ λit (SCC,D). cscc_outer_invar_loc E V0 it SCC D"
definition "cscc_invar ≡ λv0 D0 (SCC,p,D,pE,vE). cscc_invar_loc E V0 v0 D0 SCC p D pE vE"
end
subsection ‹Definition of the SCC-Algorithm›
context fr_graph
begin
definition "build_scc = (λ (l,p,D,pE,vE).
do{
let l = l @ [last p];
let (p,D,pE,vE) = pop (p,D,pE,vE);
(l,p,D,pE,vE)
})"
lemma invar_build_scc:
assumes INV: "invar v0 D0 (p,D,pE,vE)"
assumes NE[simp]: "p≠[]"
assumes NO': "(set_mset pE) ∩ (last p × UNIV) = {}"
shows "invar v0 D0 (snd (build_scc (l,p,D,pE,vE)))"
unfolding build_scc_def
using invar_pop[OF assms]
by force
lemma abs_wf_build_scc:
assumes NE: "p≠[]"
shows "(snd (build_scc (SCC,p,D,pE,vE)), (p, D, pE, vE)) ∈ abs_wf_rel v0"
unfolding build_scc_def
using abs_wf_pop[OF NE]
by force
definition "initial_S l v0 D0 ≡ do {
s ← initial v0 D0;
RETURN (l,s)
}"
definition "push_S v ≡ (λ (l,p,D,pE,vE). do {
(p,D,pE,vE) ← push v (p,D,pE,vE);
RETURN (l,p,D,pE,vE)
})"
definition "select_edge_S ≡ λ(l,PDPE). do { (r,PDPE)←select_edge PDPE; RETURN (r,(l,PDPE)) }"
definition compute_SCC :: "'v set list nres" where
"compute_SCC ≡ do {
let so = ([],{});
(l,D) ← FOREACHi cscc_outer_invar V0 (λv0 (l0,D0). do {
if v0∉D0 then do {
ASSERT(v0 ∈ E⇧*``V0);
s ← initial_S l0 v0 D0;
(l,p,D,pE,vE) ←
WHILEIT (cscc_invar v0 D0)
(λ(l,p,D,pE,vE). p ≠ []) (λ(l,p,D,pE,vE).
do {
(vo,(l,p,D,pE,vE)) ← select_edge_S (l,p,D,pE,vE);
ASSERT (p≠[]);
case vo of
Some v ⇒ do {
ASSERT (v ∈ E⇧* `` V0);
if v ∈ ⋃(set p) then do {
RETURN (l,collapse v (p,D,pE,vE))
} else if v∉D then do {
push_S v (l,p,D,pE,vE)
} else RETURN (l,p,D,pE,vE)
}
| None ⇒ do {
ASSERT ((set_mset pE) ∩ last p × UNIV = {});
RETURN (build_scc (l,p,D,pE,vE))
}
}) s;
ASSERT (p=[] ∧ pE={#});
RETURN (l,D)
} else
RETURN (l0,D0)
}) so;
RETURN l
}"
end
context fr_graph
begin
definition "cscc_invar_part ≡ λ(SCC,p,D,pE). cscc_invar_ext E V0 SCC D"
lemma cscc_invarI:
assumes "invar v0 D0 PDPE"
assumes "invar v0 D0 PDPE ⟹ cscc_invar_part (SCC,PDPE)"
shows "cscc_invar v0 D0 (SCC,PDPE)"
using assms
unfolding cscc_invar_def invar_def
apply (simp split: prod.split_asm)
apply intro_locales
apply (simp add: invar_loc_def)
apply (simp add: cscc_invar_part_def cscc_invar_ext_def)
done
lemma cscc_outer_invarI[intro?]:
assumes "outer_invar it D"
assumes "outer_invar it D ⟹ cscc_invar_ext E V0 SCC D"
shows "cscc_outer_invar it (SCC,D)"
using assms
unfolding cscc_outer_invar_def outer_invar_def
apply (simp split: prod.split_asm)
apply intro_locales
apply (simp add: outer_invar_loc_def)
apply (simp add: cscc_invar_ext_def)
done
lemma cscc_invar_initial:
assumes A: "v0∈it" "v0∉D0"
assumes INV: "cscc_outer_invar it (SCC,D0)"
shows "initial v0 D0 ≤ SPEC (λ (p,D,pE,vE). cscc_invar_part (SCC,p,D,pE,vE))"
unfolding initial_def out_edges_def
apply refine_vcg
apply clarsimp
proof -
fix pE'
assume "set_mset pE' = E ∩ {v0} × UNIV"
from INV interpret cscc_outer_invar_loc E V0 it SCC D0
unfolding cscc_outer_invar_def by simp
show "cscc_invar_part (SCC, [{v0}], D0, pE', E ∩ D0 × UNIV)"
unfolding cscc_invar_part_def initial_def
apply simp
by unfold_locales
qed
lemma cscc_invar_pop_aux:
assumes INV: "cscc_invar v0 D0 (l,p,D,pE,vE)"
assumes NE[simp]: "p≠[]"
assumes NO': "(set_mset pE) ∩ (last p × UNIV) = {}"
shows "cscc_invar_part (l @ [last p], pop (p,D,pE,vE))"
proof -
from INV interpret cscc_invar_loc E V0 v0 D0 l p D pE
unfolding cscc_invar_def by simp
have AUX_l_scc: "is_scc E (last p)"
unfolding is_scc_pointwise
proof safe
{
assume "last p = {}" thus False
using p_no_empty by (cases p rule: rev_cases) auto
}
fix u v
assume "u∈last p" "v∈last p"
with p_sc[of "last p"] have "(u,v) ∈ (vE ∩ last p × last p)⇧*" by auto
with vE_ss_E show "(u,v)∈(E ∩ last p × last p)⇧*"
by (metis Int_mono equalityE rtrancl_mono_mp)
fix u'
assume "u'∉last p" "(u,u')∈E⇧*" "(u',v)∈E⇧*"
from ‹u'∉last p› ‹u∈last p› ‹(u,u')∈E⇧*›
and rtrancl_reachable_induct[OF order_refl lastp_un_D_closed[OF NE NO']]
have "u'∈D" by auto
with ‹(u',v)∈E⇧*› and rtrancl_reachable_induct[OF order_refl D_closed]
have "v∈D" by auto
with ‹v∈last p› p_not_D show False by (cases p rule: rev_cases) auto
qed
have scc_no_back: "i < length l ⟹ l ! i × last p ∩ E⇧* = {}" for i
proof(rule ccontr)
assume A: "i < length l" and B: "l ! i × last p ∩ E⇧* ≠ {}"
then obtain u v where UMEM: "u ∈ l ! i" and VMEM: "v ∈ last p" and UVE: "(u,v) ∈ E⇧*" by blast
moreover have "u ∈ D" using scc_done[OF A] UMEM by blast
ultimately have "v ∈ D" using D_image_closed by blast
then show False using p_not_D VMEM by fastforce
qed
have "last p ⊆ E⇧* `` V0" using p_elem_reachable
by force
thus ?thesis
unfolding cscc_invar_part_def pop_def apply simp
apply unfold_locales
subgoal using scc_is_D by simp
subgoal using is_scc_set AUX_l_scc by(simp add: scc_set_mem)
subgoal for i j
apply(rule scc_nforward_append)
by (auto intro!: scc_no_back)
done
qed
lemma cscc_invar_build_scc:
assumes CINV: "cscc_invar v0 D0 (l,p,D,pE,vE)"
assumes NE[simp]: "p≠[]"
assumes NO': "(set_mset pE) ∩ (last p × UNIV) = {}"
shows "cscc_invar v0 D0 (build_scc (l,p,D,pE,vE))"
proof -
from CINV have INV: "invar v0 D0 (p, D, pE, vE)"
unfolding cscc_invar_def invar_def
using cscc_invar_loc.invar_this
by fast
have INV_BUILD: "invar v0 D0 (snd (build_scc (l, p, D, pE, vE)))"
using invar_build_scc[OF INV NE NO']
by blast
have build_scc_decomp: "(l @ [last p], snd (build_scc (l, p, D, pE, vE))) = build_scc (l, p, D, pE, vE)"
unfolding build_scc_def by auto
have "cscc_invar_part (build_scc (l, p, D, pE, vE))"
using cscc_invar_pop_aux[OF assms]
unfolding build_scc_def
by force
thus ?thesis using cscc_invarI[OF INV_BUILD, of "l @ [last p]"]
unfolding build_scc_decomp by simp
qed
lemma cscc_invar_unchanged:
assumes INV: "cscc_invar v0 D0 (l,p,D,pE,vE)"
shows "cscc_invar_part (l,p',D,pE',vE')"
using INV unfolding cscc_invar_def cscc_invar_part_def cscc_invar_loc_def
by simp
corollary cscc_invar_collapse:
assumes INV: "cscc_invar v0 D0 (l,p,D,pE,vE)"
shows "cscc_invar_part (l,collapse v (p',D,pE',vE'))"
unfolding collapse_def
by (simp add: cscc_invar_unchanged[OF INV])
corollary cscc_invar_push:
assumes INV: "cscc_invar v0 D0 (l,p,D,pE,vE)"
shows "push v (p',D,pE',vE') ≤ SPEC (λ (p,D,pE,vE). cscc_invar_part (l,p,D,pE,vE))"
unfolding push_def out_edges_def
apply refine_vcg
by (simp add: cscc_invar_unchanged[OF INV])
lemma cscc_outer_invar_initial: "cscc_invar_ext E V0 [] {}"
by unfold_locales auto
lemma cscc_invar_outer_newnode:
assumes A: "v0∉D0" "v0∈it"
assumes OINV: "cscc_outer_invar it (l,D0)"
assumes INV: "cscc_invar v0 D0 (l',[],D',pE,vE)"
shows "cscc_invar_ext E V0 l' D'"
proof -
from OINV interpret cscc_outer_invar_loc E V0 it l D0
unfolding cscc_outer_invar_def by simp
from INV interpret inv: cscc_invar_loc E V0 v0 D0 l' "[]" D' pE vE
unfolding cscc_invar_def by simp
show ?thesis
by unfold_locales
qed
lemma cscc_invar_outer_Dnode:
assumes "cscc_outer_invar it (SCC, D)"
shows "cscc_invar_ext E V0 SCC D"
using assms
by (simp add: cscc_outer_invar_def cscc_outer_invar_loc_def)
lemmas cscc_invar_preserve = invar_preserve
abs_wf_build_scc cscc_invar_build_scc
cscc_invar_collapse cscc_invar_push cscc_invar_unchanged
cscc_outer_invar_initial cscc_invar_outer_newnode cscc_invar_outer_Dnode
text ‹On termination, the invariant implies the specification›
lemma cscc_finI:
assumes INV: "cscc_outer_invar {} (l,D)"
shows fin_SCC_is_scc: "⟦U∈set l⟧ ⟹ is_scc E U"
and fin_SCC_is_reachable: "⋃ (set l) = E⇧* `` V0"
and fin_reach_scc_in_SCC: "is_scc E U ⟹ U ⊆ E⇧* `` V0⟹ U ∈ set l"
proof -
from INV interpret cscc_outer_invar_loc E V0 "{}" l D
unfolding cscc_outer_invar_def by simp
show "⟦U∈set l⟧ ⟹ is_scc E U" using reachable_scc(1) unfolding SCC_def .
show A: "⋃ (set l) = E⇧* `` V0"
using fin_outer_D_is_reachable[OF outer_invar_this] scc_is_D
unfolding SCC_def
by auto
show "is_scc E U ⟹ U ⊆ E⇧* `` V0 ⟹ U ∈ set l"
proof (rule ccontr)
assume U_SCC: "is_scc E U" and U_REACH: "U ⊆ E⇧* `` V0" and U_NOT_SCC: "U ∉ set l"
from U_NOT_SCC have "⋀ U2. U2 ∈ set l ⟹ U2 ∩ U = {}"
using scc_disj_or_eq[OF U_SCC] reachable_scc(1) unfolding SCC_def by blast
with A have "E⇧* `` V0 ∩ U = {}" by blast
hence "¬U ⊆ E⇧* `` V0" using scc_non_empty'[OF U_SCC] by blast
thus False using U_REACH by simp
qed
qed
end
subsection ‹Main Correctness Proof›
context fr_graph
begin
lemma invar_from_cscc_invarI: "cscc_invar v0 D0 (L,PDPE) ⟹ invar v0 D0 PDPE"
unfolding cscc_invar_def invar_def
apply (simp split: prod.splits)
unfolding cscc_invar_loc_def by simp
lemma outer_invar_from_cscc_invarI:
"cscc_outer_invar it (L,D) ⟹outer_invar it D"
unfolding cscc_outer_invar_def outer_invar_def
apply (simp split: prod.splits)
unfolding cscc_outer_invar_loc_def by simp
text ‹With the extended invariant and the auxiliary lemmas, the actual
correctness proof is straightforward:›
lemmas [refine_vcg del] = invar_initial
theorem compute_SCC_correct: "compute_SCC ≤ compute_SCC_spec"
proof -
note [[goals_limit = 54]]
note [simp del] = Union_iff
note [refine_vcg del] = WHILEIT_rule
show ?thesis
unfolding compute_SCC_def compute_SCC_spec_def select_edge_def select_def initial_S_def push_S_def select_edge_S_def
apply (refine_vcg SPEC_rule_conjI[OF invar_initial cscc_invar_initial])
apply (vc_solve
rec: cscc_outer_invarI
solve: cscc_invar_preserve
intro!: outer_invar_from_cscc_invarI
)
apply (auto simp: cscc_outer_invar_initial intro!: outer_invar_from_cscc_invarI)
apply (refine_vcg
WHILEIT_rule[where R="inv_image (abs_wf_rel v0) snd" for v0]
refine_vcg
)
apply (vc_solve
rec: cscc_invarI cscc_outer_invarI
solve: cscc_invar_preserve
intro!: invar_from_cscc_invarI outer_invar_from_cscc_invarI
simp: pE_fin'[OF invar_from_cscc_invarI] finite_V0
)
apply(auto intro!: invar_from_cscc_invarI invar_pE_is_node)[3]
apply(refine_vcg SPEC_rule_conjI[OF cscc_invar_push invar_rel_push])
apply (auto intro!: invar_from_cscc_invarI)[3]
apply (auto intro!: cscc_invarI) [3]
using cscc_invar_ext.is_scc_set cscc_invar_outer_Dnode apply blast
apply (simp add: fin_reach_scc_in_SCC scc_set_def)
unfolding cscc_outer_invar_def cscc_outer_invar_loc_def cscc_invar_ext_def cscc_invar_ext_axioms_def
by blast
qed
end
subsection ‹Refinement to Gabow's Data Structure›
context GS begin
definition "seg_set_impl l u ≡ do {
(_,res) ← WHILET
(λ(l,_). l<u)
(λ(l,res). do {
ASSERT (l<length S);
let x = S!l;
ASSERT (x∉res);
RETURN (Suc l,insert x res)
})
(l,{});
RETURN res
}"
lemma seg_set_impl_aux:
fixes l u
shows "⟦l<u; u≤length S; distinct S⟧ ⟹ seg_set_impl l u
≤ SPEC (λr. r = {S!j | j. l≤j ∧ j<u})"
unfolding seg_set_impl_def
apply (refine_rcg
WHILET_rule[where
I="λ(l',res). res = {S!j | j. l≤j ∧ j<l'} ∧ l≤l' ∧ l'≤u"
and R="measure (λ(l',_). u-l')"
]
refine_vcg)
apply (auto simp: less_Suc_eq nth_eq_iff_index_eq)
done
lemma (in GS_invar) seg_set_impl_correct:
assumes "i<length B"
shows "seg_set_impl (seg_start i) (seg_end i) ≤ SPEC (λr. r=p_α!i)"
apply (refine_rcg order_trans[OF seg_set_impl_aux] refine_vcg)
using assms
apply (simp_all add: seg_start_less_end seg_end_bound S_distinct) [3]
apply (auto simp: p_α_def assms seg_def) []
done
definition "last_seg_impl
≡ do {
ASSERT (length B - 1 < length B);
seg_set_impl (seg_start (length B - 1)) (seg_end (length B - 1))
}"
lemma (in GS_invar) last_seg_impl_correct:
assumes "p_α ≠ []"
shows "last_seg_impl ≤ SPEC (λr. r=last p_α)"
unfolding last_seg_impl_def
apply (refine_rcg order_trans[OF seg_set_impl_correct] refine_vcg)
using assms apply (auto simp add: p_α_def last_conv_nth)
done
end
definition "SCC_at I i = {v. I v = Some (DONE i)}"
definition SCC_α :: "'v oGS ⇒ nat ⇒ 'v set list" where "SCC_α I i ≡ map (SCC_at I) [0..<i]"
lemma set_SCC_α_alt: "set (SCC_α I i) = (SCC_at I ` {0..<i})"
by (simp add: SCC_α_def)
lemma SCC_at_extend_neq: "⟦⋀v. I v = Some (DONE j) ⟹ ¬Q v; j ≠ i⟧ ⟹ SCC_at (λv. if Q v then Some (DONE i) else I v) j = SCC_at I j"
unfolding SCC_at_def
apply auto
done
lemma SCC_at_extend: "SCC_at (λv. if Q v then Some (DONE i) else I v) i = Collect Q ∪ SCC_at I i"
unfolding SCC_at_def
apply auto
done
definition oGSS_α :: "'v oGS ⇒ nat ⇒ ('v set list × 'v set)" where "oGSS_α I i ≡ (SCC_α I i, oGS_α I)"
locale GSS_invar_ext = fr_graph E V0 for E and V0 :: "'v set" +
fixes I :: "'v oGS"
fixes i :: "nat"
assumes non_empty_scc: "j < i ⟹ SCC_at I j ≠ {}"
assumes empty_not_scc: "j ≥ i ⟹ SCC_at I j = {}"
assumes finite_scc: "finite (SCC_at I j)"
assumes I_reachable: "I v ≠ None ⟶ v ∈ E⇧*``V0"
begin
lemma I_reachable': "I v = None ∨ v ∈ E⇧*``V0"
using I_reachable
by blast
lemma SCC_at_disj: "j ≠ k ⟹ SCC_at I j ∩ SCC_at I k = {}"
unfolding SCC_at_def by fastforce
lemma non_eq_scc: "j < i ⟹ k ≠ j ⟹ SCC_at I j ≠ SCC_at I k"
using SCC_at_disj non_empty_scc by fast
lemma card_scc_j: "j ≤ i ⟹ length (SCC_α I j) = j"
unfolding SCC_α_def
proof (induction j)
case 0
then show ?case by simp
next
case (Suc j)
have "card (SCC_at I ` {0..<Suc j}) = card (insert (SCC_at I j) (SCC_at I ` {0..<j}))"
unfolding insert_Suc_elem_image[of 0, simplified] by blast
moreover have "SCC_at I j ∉ (SCC_at I ` {0..<j})"
using non_eq_scc[OF Suc_le_lessD[OF Suc.prems]]
by fastforce
moreover have "finite (SCC_at I ` {0..<j})" by simp
ultimately show ?case using card_insert_disjoint Suc
by simp
qed
lemma card_scc_i: "length (SCC_α I i) = i"
using card_scc_j
by simp
lemma "j < i ⟹ ∃ v. I v = Some (DONE j)"
using non_empty_scc
unfolding SCC_at_def
by blast
lemma "j ≥ i ⟹ ∀ v. I v ≠ Some (DONE j)"
using empty_not_scc
unfolding SCC_at_def
by blast
lemma DONE_j_less_i: "I v = Some (DONE j) ⟹ j < i"
apply (rule ccontr)
apply (drule leI)
apply (drule empty_not_scc)
unfolding SCC_at_def
by blast
lemma j_less_i_DONE: "j < i ⟷ (∃ v. I v = Some (DONE j))"
using non_empty_scc empty_not_scc
unfolding SCC_at_def
by fastforce
lemma invar_card_D_bound: "outer_invar_loc E V0 it D ⟹ card D ≤ card (E⇧*``V0)"
apply (rule card_mono)
apply (auto simp: outer_invar_loc_def outer_invar_loc_axioms_def)
done
lemma oGS_α_alt_def: "oGS_α I = ⋃ (set (SCC_α I i))"
by (auto simp: oGS_α_def SCC_α_def SCC_at_def dest: DONE_j_less_i)
lemma i_bound_SCC: "i ≤ card (⋃ (set (SCC_α I i)))"
apply (rewrite at "⌑≤ card (⋃ (set (SCC_α I i)))" diff_zero[of i, symmetric, unfolded card_atLeastLessThan[symmetric]])
unfolding set_SCC_α_alt
apply (rule fin_disj_union_card)
using finite_scc SCC_at_disj non_empty_scc
by auto
lemma i_bound: "outer_invar_loc E V0 it (oGS_α I) ⟹ i ≤ card (E⇧*``V0)"
apply (drule invar_card_D_bound)
unfolding oGS_α_alt_def
using i_bound_SCC
by linarith
end
locale oGSS_invar = oGS_invar + GSS_invar_ext
context fr_graph
begin
definition "SCC_rel = br (λ (i, I). SCC_α I i) (λ (i, I). oGSS_invar E V0 I i)"
definition "oGSS_rel = br (λ (i, I). oGSS_α I i) (λ (i, I). oGSS_invar E V0 I i)"
lemma oGSS_to_SCC_rel:"((i, I), (SCC, D0)) ∈ oGSS_rel ⟹ ((i, I), SCC) ∈ SCC_rel"
apply(auto simp: oGSS_rel_def SCC_rel_def in_br_conv oGSS_α_def)
done
lemma oGSS_to_oGS: "((i, I), (SCC, D0)) ∈ oGSS_rel ⟹ (I, D0) ∈ oGS_rel"
unfolding oGSS_rel_def
apply(auto simp: in_br_conv oGS_rel_def oGSS_α_def oGSS_invar_def)
done
lemma oGSS_relI: "GSS_invar_ext E V0 I i ⟹ SCC = SCC_α I i ⟹ (I, D0) ∈ oGS_rel ⟹ ((i, I), (SCC, D0)) ∈ oGSS_rel"
unfolding oGSS_rel_def oGSS_α_def oGS_rel_def oGSS_invar_def
apply(auto simp: in_br_conv)
done
end
locale GSS_defs = GS_defs E V0 SBIP for E and V0 :: "'a set" and SBIP +
fixes i :: "nat"
begin
definition "s_α = (SCC_α I i, α)"
definition "build_scc_impl =
do {
ASSERT (i < card (E⇧*``V0));
s←pop_impl i;
RETURN (i+1, s)
}"
end
locale GSS = GSS_defs + fr_graph
locale GSS_invar = GSS E V0 SBIP i + GS_invar E V0 SBIP + GSS_invar_ext E V0 I i for E and V0 :: "'a set" and SBIP and i
context fr_graph
begin
definition "initial_S_impl i0 v0 I0 = do{
s ← initial_impl v0 I0;
RETURN (i0,s)
}"
definition "push_S_impl v ≡ (λ (i,S,B,I,P). do{
s ← push_impl_fr v (S,B,I,P);
RETURN (i, s)
})"
definition "GSS_rel ≡ { (c,SCC,p,D,pE,vE) . (c,SCC,p,D,pE) ∈ br (λ (i,SBIP). GSS_defs.s_α SBIP i) (λ (i,SBIP). GSS_invar E V0 SBIP i) }"
definition "GSS_rel_I_eq I ≡ { (c,SCC,p,D,pE,vE) . (c,SCC,p,D,pE) ∈ br (λ (i,SBIP). GSS_defs.s_α SBIP i) (λ (i,SBIP). GSS_invar E V0 SBIP i ∧ GS_defs.I SBIP = I) }"
definition "GSS_rel_I_upd I v j ≡ { (c,SCC,p,D,pE,vE) . (c,SCC,p,D,pE) ∈ br (λ (i,SBIP). GSS_defs.s_α SBIP i) (λ (i,SBIP). GSS_invar E V0 SBIP i ∧ GS_defs.I SBIP = I(v↦STACK j)) }"
lemma GSS_rel_I_eqD: "s ∈ GSS_rel_I_eq I ⟹ s ∈ GSS_rel"
unfolding GSS_rel_I_eq_def GSS_rel_def
by (auto simp: in_br_conv)
lemma GSS_rel_I_updD: "s ∈ GSS_rel_I_upd I v j ⟹ s ∈ GSS_rel"
unfolding GSS_rel_I_upd_def GSS_rel_def
by (auto simp: in_br_conv)
lemma GSS_rel_I_eqI: "((i,SBIP),s) ∈ GSS_rel ⟹ GS_defs.I (SBIP) = I ⟹ ((i,SBIP),s) ∈ GSS_rel_I_eq I"
unfolding GSS_rel_I_eq_def GSS_rel_def
by (auto simp: in_br_conv)
lemma GSS_rel_I_updI: "((i,SBIP),s) ∈ GSS_rel ⟹ GS_defs.I (SBIP) = I(v↦STACK j) ⟹ ((i,SBIP),s) ∈ GSS_rel_I_upd I v j"
unfolding GSS_rel_I_upd_def GSS_rel_def
by (auto simp: in_br_conv)
lemma "I v ≠ Some (STACK j) ⟹ GSS_rel_I_eq I ∩ GSS_rel_I_upd I v j = {}"
unfolding GSS_rel_I_upd_def GSS_rel_I_eq_def GSS_rel_def
apply(cases "I v")
by (auto simp: in_br_conv dest!: fun_cong[of I "I(v ↦ STACK j)" v])
lemma GSS_rel_GS_eq: "((i,S,B,I,P), (SCC, p, D, pE)) ∈ GSS_rel ⟷ SCC = SCC_α I i ∧ GSS_invar_ext E V0 I i ∧ ((S,B,I,P), (p, D, pE)) ∈ GS_rel"
unfolding GSS_rel_def
apply(auto simp: in_br_conv GSS_defs.s_α_def GS_rel_def GSS_invar_def GSS_def GSS_invar_ext_def)
done
lemma GSS_relI: "SCC = SCC_α I i ⟹ GSS_invar_ext E V0 I i ⟹ ((S,B,I,P), (p, D, pE, vE)) ∈ GS_rel ⟹ ((i,S,B,I,P), (SCC, p, D, pE, vE)) ∈ GSS_rel"
unfolding GSS_rel_def
apply(auto simp: in_br_conv GSS_defs.s_α_def GS_rel_def GSS_invar_def GSS_def GSS_invar_ext_def)
done
lemma GSS_relD: "((i,S,B,I,P), (SCC, p, D, pE)) ∈ GSS_rel ⟹ SCC = SCC_α I i ∧ GSS_invar_ext E V0 I i ∧ ((S,B,I,P), (p, D, pE)) ∈ GS_rel"
unfolding GSS_rel_def
apply(auto simp: in_br_conv GSS_defs.s_α_def GS_rel_def GSS_invar_def)
done
lemma GSS_to_GS: "((i,SBIP), (SCC, p, D, pE)) ∈ GSS_rel ⟹ (SBIP, (p, D, pE)) ∈ GS_rel"
unfolding GSS_rel_def GSS_defs.s_α_def GS_rel_def GSS_invar_def SCC_rel_def
apply(auto simp: in_br_conv)
done
lemma oinitial_S_refine: "((0, Map.empty), [], {}) ∈ oGSS_rel"
apply (auto simp: oGSS_rel_def in_br_conv oGSS_α_def SCC_α_def oGS_α_def)
apply unfold_locales
apply (auto simp: SCC_at_def)
done
lemma I_Stack_GS: "GS_defs.I (GS_initial_impl I v succs) = I(v ↦ (STACK 0))"
unfolding GS_initial_impl_def GS_defs.I_def
by force
lemma I_Stack: "initial_impl v I ≤ SPEC (λ (_,_,I',_). I' = I(v ↦ (STACK 0)))"
unfolding initial_impl_def successors_def
apply(refine_vcg)
apply(auto simp: GS_initial_impl_def)
done
lemma v0_not_done_None:
assumes REL: "((i,I),(SCC,D0))∈oGSS_rel"
and V0D: "v0 ∉ D0"
shows "I v0 = None"
proof (rule ccontr)
assume "I v0 ≠ None"
then obtain a where ALT: "I v0 = Some a" by blast
show False
proof (cases a)
case (STACK x1)
with REL ALT show ?thesis
by(auto simp: oGSS_rel_def in_br_conv oGSS_invar_def oGS_invar_def oGS_invar_axioms_def)
next
case (DONE x2)
with REL ALT V0D show ?thesis
by(auto simp: oGSS_rel_def in_br_conv oGSS_α_def oGS_α_def)
qed
qed
lemma initial_preserve_scc_at: "I v = None ⟹ SCC_at (I(v ↦ (STACK j))) i = SCC_at I i"
unfolding SCC_at_def
by auto
lemma initial_preserve_scc: "I v = None ⟹ SCC_α (I(v ↦ (STACK j))) i = SCC_α I i"
unfolding SCC_α_def SCC_at_def
by auto
lemma initial_preserve_SCC: "I0 v0 = None ⟹ SCC_at (GS_defs.I (GS_initial_impl I0 v0 succs)) i = SCC_at I0 i"
unfolding initial_impl_def GS_initial_impl_def SCC_at_def
apply auto
done
lemma initial_preserve_SCC_α:
assumes "I0 v0 = None"
shows "SCC_α (GS_defs.I (GS_initial_impl I0 v0 succs)) i = SCC_α I0 i"
unfolding SCC_α_def
using initial_preserve_SCC[of I0 v0, OF assms]
by presburger
lemma push_core_preserve_I: "GS_defs.I (GS_defs.push_impl_core (S0,B0,I0,P0) v0 succs) = I0(v0 ↦ STACK (length S0))"
unfolding GS_defs.push_impl_core_def GS_defs.I_def Let_def
by simp
lemma push_preserve_I: "length S0 < card (E⇧* `` V0) ⟹ length B0 < card (E⇧* `` V0) ⟹ length P0 < card (E⇧* `` V0)
⟹ push_impl_fr v0 (S0,B0,I0,P0) ≤ SPEC (λ (S,B,I,P). I = I0(v0 ↦ STACK (length S0)))"
unfolding push_impl_fr_def successors_def GS_defs.push_impl_def
apply refine_vcg
using push_core_preserve_I
apply (auto dest!: GS_selI(3))
by fast
lemma push_preserve_SCC: "I0 v0 = None ⟹ SCC_at (GS_defs.I (GS_defs.push_impl_core (S0,B0,I0,P0) v0 succs)) i = SCC_at I0 i"
unfolding GS_defs.push_impl_core_def SCC_at_def
apply simp
unfolding fun_upd_apply let_distrib GS_sel_simps
by auto
lemma push_preserve_SCC_α:
assumes NN: "I0 v0 = None"
shows "SCC_α (GS_defs.I (GS_defs.push_impl_core (S0,B0,I0,P0) v0 succs)) i = SCC_α I0 i"
unfolding SCC_α_def push_preserve_SCC[of I0 v0, OF NN]
by simp
lemma oGS_ndone_maps_None: "¬is_done_oimpl v0 I ⟹ oGS_invar E V0 I ⟹ I v0 = None"
unfolding is_done_oimpl_def oGS_invar_def
apply(auto split: option.splits node_state.splits simp: oGS_invar_axioms_def)
done
lemma initial_GSS_ext_invar:
assumes V0I: "v0 ∈ V0"
and V0NNONE: "I v0 = None"
and INV: "GSS_invar_ext E V0 I i"
shows "GSS_invar_ext E V0 (GS_defs.I (GS_initial_impl I v0 succs)) i"
proof -
interpret GSS_invar_ext E V0 I i using INV by simp
show ?thesis
apply(unfold_locales)
unfolding I_Stack_GS
subgoal
using V0NNONE
apply(clarsimp dest!: non_empty_scc simp: SCC_at_def )[]
by force
subgoal
by(auto dest!: empty_not_scc simp: SCC_at_def)
subgoal
using finite_scc
by (auto simp: SCC_at_def)
subgoal
using I_reachable V0I
by auto
done
qed
lemma GSS_initial_invar:
assumes NDONE: "¬is_done_oimpl v0 I"
assumes REL: "((i,I),(SCC,D0))∈oGSS_rel"
assumes A: "v0∉D0"
assumes REACH: "v0 ∈ V0"
shows "GSS_invar E V0 (GS_initial_impl I v0 succs) i"
unfolding GSS_invar_def
using GS_initial_correct[OF oGSS_to_oGS[OF REL] A REACH] REL
using initial_GSS_ext_invar[of v0 I i succs,OF REACH oGS_ndone_maps_None[OF NDONE] ]
apply (auto simp: oGSS_rel_def in_br_conv oGSS_invar_def GSS_def GSS_invar_ext_def)
done
lemma initial_S_refine:
assumes "¬is_done_oimpl v0 I"
and VV0: "v0∈V0"
and VD0: "v0∉D0"
and OGSS: "((i,I),(SCC,D0))∈oGSS_rel"
and ID: "(v0i,v0)∈Id"
and INV: "cscc_outer_invar it (SCC,D0)"
shows "initial_S_impl i v0i I ≤ ⇓ GSS_rel (initial_S SCC v0 D0)"
proof -
interpret oGSS_invar E V0 I i using OGSS
by(auto simp: oGSS_rel_def in_br_conv)
have OGS: "(I,D0) ∈ oGS_rel"
using OGSS by(auto intro!: oGSS_to_oGS)
have LE: "initial_impl v0i I ≤ ⇓ {((S',B',I',P'),s). ((S',B',I',P'),s) ∈ GS_rel ∧ I' = I(v0 ↦ STACK 0)} (initial v0 D0)"
using I_Stack initial_refine[OF VV0 VD0 OGS ID]
apply (clarsimp simp: pw_le_iff refine_pw_simps)
using ID
by fast
have INIT_NSTACK: "oGSS_invar E V0 I i ⟹ ∀j. I v0 ≠ Some (STACK j)"
unfolding oGSS_invar_def
by(auto dest!: oGS_invar.I_no_stack[where ?v=v0])
note V0NONE = v0_not_done_None[OF OGSS VD0]
show ?thesis
unfolding initial_S_impl_def initial_S_def
apply(refine_vcg LE)
using OGSS
apply(auto intro!: GSS_relI GSS_rel_I_updI
simp: oGSS_rel_def oGSS_α_def in_br_conv initial_preserve_scc[of I v0, OF V0NONE] GS_rel_def)
apply(unfold_locales)
unfolding initial_preserve_scc_at[of I v0, OF V0NONE]
subgoal using non_empty_scc by assumption
subgoal using empty_not_scc by assumption
subgoal using finite_scc by assumption
subgoal using I_reachable VV0 by auto
done
qed
definition "last_seg_impl s ≡ GS.last_seg_impl s"
lemmas last_seg_impl_def_opt =
last_seg_impl_def[abs_def, THEN opt_GSdef,
unfolded GS.last_seg_impl_def GS.seg_set_impl_def
GS_defs.seg_start_def GS_defs.seg_end_def GS_sel_simps]
lemma last_seg_impl_refine:
assumes A: "(s,(p,D,pE,vE))∈GS_rel"
assumes NE: "p≠[]"
shows "last_seg_impl s ≤ ⇓Id (RETURN (last p))"
proof -
from A have
[simp]: "p=GS_defs.p_α s ∧ D=GS_defs.D_α s ∧ pE=GS_defs.pE_α s"
and INV: "GS_invar E V0 s"
by (auto simp add: GS_rel_def br_def GS_α_split)
show ?thesis
unfolding last_seg_impl_def[abs_def]
apply (rule order_trans[OF GS_invar.last_seg_impl_correct])
using INV NE
apply (simp_all)
done
qed
lemma push_S_refine:
assumes A: "((i,s),(SCC,p,D,pE,vE))∈GSS_rel"
assumes B: "(v,v')∈Id"
assumes C: "v∉⋃(set p)" "v∉D"
assumes NSTACK: "¬is_on_stack_impl v s"
assumes NDONE: "¬is_done_impl v s"
assumes REACH: "v ∈ E⇧* `` V0"
shows "push_S_impl v (i,s) ≤ ⇓GSS_rel (push_S v' (SCC,p,D,pE,vE))"
proof -
from A B have XF[simp]: "p=GS_defs.p_α s" "D=GS_defs.D_α s" "pE=GS_defs.pE_α s" "v'=v" and SCCD: "SCC = SCC_α (GS_defs.I s) i"
and INV: "GSS_invar E V0 s i"
by (auto simp add: GSS_rel_def GSS_defs.s_α_def GS_rel_def br_def GS_α_split)
have IVNONE: "(GS_defs.I s) v = None" using NDONE NSTACK
unfolding is_done_impl_def is_on_stack_impl_def GS_defs.is_done_impl_def GS_defs.is_on_stack_impl_def
apply (auto split: option.splits node_state.splits)
done
interpret GSS_invar E V0 s i by fact
note GS = GSS_to_GS[OF A]
note CC = push_impl_core_correct[OF C[unfolded XF] REACH]
have VNS: "v∉set (GS_defs.S s)"
using XF(1) assms(3) set_p_α_is_set_S by blast
hence LS: "length (GS_defs.S s) < card (E⇧* `` V0)"
by (metis REACH S_distinct S_length_nodes S_subset_nodes card_subset_eq distinct_card finite_reachableE_V0 le_neq_implies_less)
hence LB: "length (GS_defs.B s) < card (E⇧* `` V0)"
by (metis B_distinct B_in_bound' B_length_nodes B_sorted order_le_imp_less_or_eq order_le_less_trans order_less_imp_not_eq2 sorted_wrt_less_idx strict_sorted_iff)
have LP: "length (GS_defs.P s) < card (E⇧* `` V0)"
proof -
have "v∉set (map fst (GS_defs.P s))"
using P_bound VNS by auto
hence "set (map fst (GS_defs.P s)) ⊆ E⇧* `` V0 - {v}" using P_bound S_subset_nodes by fastforce
hence "card (set (map fst (GS_defs.P s))) ≤ card (E⇧* `` V0 - {v})"
by (auto intro: card_mono)
moreover have "card (set (map fst (GS_defs.P s))) = length (GS_defs.P s)"
by (metis P_distinct distinct_card length_map)
moreover have "card (E⇧* `` V0 - {v}) = card (E⇧* `` V0) - 1"
by (simp add: REACH)
moreover have "card (E⇧* `` V0) ≠ 0"
using REACH by auto
ultimately show ?thesis by linarith
qed
have INVPRES: "GSS_invar E V0 (push_impl_core v succs) i" for succs
apply (auto simp add: GSS_invar_def GS_rel_def in_br_conv CC push_def GSS_invar_ext_def GSS_invar_ext_axioms_def fr_graph_axioms)
unfolding push_preserve_SCC[of I v S B P _, OF IVNONE, unfolded GS_sel_id[symmetric], simplified]
apply (auto simp: non_empty_scc empty_not_scc finite_scc)
using I_reachable
unfolding push_core_preserve_I[of S B I P v, unfolded GS_sel_id[symmetric]]
using GSS_invar_axioms apply(auto simp: REACH GSS_invar_def split: if_splits)
done
have LE: "push_impl_fr v s ≤ ⇓ {((S',B',I',P'),s). ((S',B',I',P'),s) ∈ GS_rel ∧ I' = I(v ↦ STACK (length S))} (push v (p,D,pE,vE))"
using push_preserve_I[OF LS LB LP, of v I, folded GS_sel_id[of s]] push_refine[OF GS B C REACH]
by (fastforce simp: pw_le_iff refine_pw_simps push_def out_edges_def)
show ?thesis
unfolding push_S_impl_def push_S_def
apply simp
apply (refine_vcg)
using LE apply simp
apply (auto intro!: GSS_relI simp: SCCD initial_preserve_scc[of I v, OF IVNONE])
apply(unfold_locales)
unfolding initial_preserve_scc_at[of I v, OF IVNONE]
subgoal using non_empty_scc by assumption
subgoal using empty_not_scc by assumption
subgoal using finite_scc by assumption
subgoal using I_reachable REACH by auto
done
qed
lemma (in GSS_invar) collapse_S_correct:
assumes A: "v∈⋃(set (p_α))"
shows "do{x ← collapse_impl v; RETURN (i,x)} ≤ ⇓GSS_rel (RETURN (SCC_α I i, collapse v (p_α, D_α, pE_α, vE)))"
proof -
{
fix i
assume "i<length p_α"
hence ILEN: "i<length B" by (simp add: p_α_def)
let ?SBIP' = "(S, take (Suc i) B, I, P)"
{
have [simp]: "GS_defs.seg_start ?SBIP' i = seg_start i"
by (simp add: GS_defs.seg_start_def)
have [simp]: "GS_defs.seg_end ?SBIP' i = seg_end (length B - 1)"
using ILEN by (simp add: GS_defs.seg_end_def min_absorb2)
{
fix j
assume B: "seg_start i ≤ j" "j < seg_end (length B - Suc 0)"
hence "j<length S" using ILEN seg_end_bound
proof -
note B(2)
also from ‹i<length B› have "(length B - Suc 0) < length B" by auto
from seg_end_bound[OF this]
have "seg_end (length B - Suc 0) ≤ length S" .
finally show ?thesis .
qed
have "i ≤ find_seg j ∧ find_seg j < length B
∧ seg_start (find_seg j) ≤ j ∧ j < seg_end (find_seg j)"
proof (intro conjI)
show "i≤find_seg j"
by (metis le_trans not_less B(1) find_seg_bounds(2)
seg_end_less_start ILEN ‹j < length S›)
qed (simp_all add: find_seg_bounds[OF ‹j<length S›])
} note AUX1 = this
{
fix Q and j::nat
assume "Q j"
hence "∃i. S!j = S!i ∧ Q i"
by blast
} note AUX_ex_conj_SeqSI = this
have "GS_defs.seg ?SBIP' i = ⋃ (seg ` {i..<length B})"
unfolding GS_defs.seg_def[abs_def]
apply simp
apply (rule)
apply (auto dest!: AUX1) []
apply (auto
simp: seg_start_def seg_end_def
split: if_split_asm
intro!: AUX_ex_conj_SeqSI
)
apply (metis diff_diff_cancel le_diff_conv le_eq_less_or_eq
lessI trans_le_add1
distinct_sorted_mono[OF B_sorted B_distinct, of i])
apply (metis diff_diff_cancel le_diff_conv le_eq_less_or_eq
trans_le_add1 distinct_sorted_mono[OF B_sorted B_distinct, of i])
apply (metis (opaque_lifting, no_types) Suc_lessD Suc_lessI less_trans_Suc
B_in_bound')
done
} note AUX2 = this
from ILEN have "GS_defs.p_α (S, take (Suc i) B, I, P) = collapse_aux p_α i"
unfolding GS_defs.p_α_def collapse_aux_def
apply (simp add: min_absorb2 drop_map)
apply (rule conjI)
apply (auto
simp: GS_defs.seg_def[abs_def] GS_defs.seg_start_def GS_defs.seg_end_def take_map) []
apply (simp add: AUX2)
done
} note AUX1 = this
from A obtain j where [simp]: "I v = Some (STACK j)"
using I_consistent set_p_α_is_set_S
by (auto simp: in_set_conv_nth)
{
have "(SCC_α I i, collapse_aux p_α (idx_of p_α v), D_α, pE_α) =
GSS_defs.s_α (S, take (Suc (idx_of p_α v)) B, I, P) i"
apply(auto simp: GSS_defs.s_α_def)
unfolding GS_defs.α_def
using idx_of_props[OF p_α_disjoint_sym A]
by (simp add: AUX1)
} note ABS=this
{
have "GSS_invar E V0 (S, take (Suc (idx_of p_α v)) B, I, P) i"
apply unfold_locales
apply simp_all
using B_in_bound B_sorted B_distinct
apply (auto simp: sorted_take dest: in_set_takeD) [3]
using B0 S_distinct apply auto [2]
using I_consistent apply simp
using P_sorted P_distinct P_bound apply auto[3]
using S_subset_nodes apply auto
using non_empty_scc empty_not_scc finite_scc I_reachable apply auto
done
} note INV=this
show ?thesis
unfolding collapse_impl_fr_def collapse_impl_def
apply (refine_rcg SPEC_refine refine_vcg order_trans[OF idx_of_correct])
apply fact
apply (metis discrete)
apply (simp add: collapse_def α_def GSS_rel_def GS_rel_def in_br_conv)
unfolding GSS_rel_def GS_rel_def
apply (rule conjI)
apply (rule ABS)
apply (rule INV)
done
qed
lemma collapse_S_refine:
assumes A: "((i,s),(SCC,p,D,pE,vE))∈GSS_rel" "(v,v')∈Id"
assumes B: "v'∈⋃(set p)"
assumes STACK: "is_on_stack_impl v s"
shows "do{x ← collapse_impl_fr v s; RETURN (i,x)} ≤ ⇓GSS_rel (RETURN (SCC, collapse v' (p,D,pE,vE)))"
proof -
from A have [simp]: "p=GS_defs.p_α s ∧ D=GS_defs.D_α s ∧ pE=GS_defs.pE_α s" "v'=v" "SCC = SCC_α (GS_defs.I s) i"
and INV: "GSS_invar E V0 s i"
by (auto simp add: GSS_rel_def GS_rel_def br_def GS_α_split GSS_defs.s_α_def)
show ?thesis
unfolding collapse_impl_fr_def
apply (rule order_trans[OF GSS_invar.collapse_S_correct])
using INV B
by (auto simp add: GS_defs.α_def GSS_rel_def in_br_conv)
qed
lemma (in GSS_invar) SCC_at_mark_as_done_eq:
assumes "p_α ≠ []"
shows "SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) i = last p_α"
unfolding mark_as_done_abs_def SCC_at_extend[of "(λ v. v ∈ {S ! j |j. seg_start (length B - 1) ≤ j ∧ j < seg_end (length B - 1)})"]
unfolding seg_start_def seg_end_def
using empty_not_scc[of i, simplified] last_p_α_alt_def[OF assms] assms[unfolded p_α_B_empty]
unfolding last_conv_nth[of B, unfolded p_α_B_empty[symmetric], OF assms]
by force
lemma (in GSS_invar) SCC_α_mark_as_done:
assumes "p_α ≠ []"
shows "SCC_α (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) (Suc i) = (SCC_α I i) @ [last p_α]"
proof -
{
fix v j
assume "I v = Some (DONE j)"
hence "∀i. ¬(i < length S ∧ v = S ! i)"
using I_consistent
by (metis node_state.distinct(1) option.inject)
hence AUX1: "∀ i < length S. S!i ≠ v"
by blast
} note AUX1=this
have AUX2: "map (SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i)) [0..<i] = map (SCC_at I) [0..<i]"
apply(rule list.map_cong0)
unfolding mark_as_done_abs_def
apply (rule SCC_at_extend_neq[of _ _ "(λ v. v ∈ {S ! j |j. seg_start (length B - 1) ≤ j ∧ j < seg_end (length B - 1)})"])
using AUX1 seg_end_last[OF assms[unfolded p_α_B_empty]]
by auto
have "map (SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i)) [0..<Suc i]
= map (SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i)) [0..<i] @ [(SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) i)]"
by simp
also have "...= map(SCC_at I) [0..<i] @ [last p_α]"
unfolding SCC_at_mark_as_done_eq[OF assms] AUX2
by blast
finally show ?thesis
unfolding SCC_α_def
by blast
qed
lemma (in GSS_invar) GSS_invar_mark_as_done:
assumes NE: "p_α≠[]"
shows "GSS_invar_ext E V0 (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) (Suc i)"
proof -
from NE have BNE: "B ≠ []" unfolding p_α_def by simp
{
fix j
assume A: "j < i"
have "SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) j ≠ {}"
unfolding SCC_at_def mark_as_done_abs_def
using non_empty_scc[OF A, unfolded SCC_at_def] seg_start_less_end[of "length B - 1", simplified, OF BNE]
apply (auto simp:)
subgoal for x
apply (rule exI[where x=x])
apply (auto simp: A)
by (metis BNE I_consistent One_nat_def node_state.distinct(1) option.inject seg_end_last)
done
} note AUX1 = this
{
have "SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) i ≠ {}"
unfolding SCC_at_def mark_as_done_abs_def seg_start_def seg_end_def
using empty_not_scc[unfolded SCC_at_def, of i, simplified]
by (auto simp: BNE B_in_bound')
} note AUX2 = this
{
fix j
assume A: "j ≥ Suc i"
then have "SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) j = {}"
unfolding SCC_at_def mark_as_done_abs_def
using empty_not_scc[OF Suc_leD[OF A], unfolded SCC_at_def]
by auto
} note AUX3 = this
{
fix j
assume A: "j < i"
have "I v = Some (DONE j) ⟹ v ∉ {S ! j |j. seg_start (length B - 1) ≤ j ∧ j < seg_end (length B - 1)}" for v
using I_consistent
apply auto
by (metis BNE One_nat_def node_state.distinct(1) option.inject seg_end_last)
hence "SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) j = SCC_at I j"
using SCC_at_extend_neq[of I j "λ v. v ∈ {S ! j |j. seg_start (length B - 1) ≤ j ∧ j < seg_end (length B - 1)}" i] A
unfolding mark_as_done_abs_def
by blast
hence "finite (SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) j)"
using finite_scc
by presburger
} note AUX4 = this
{
fix j
assume A: "j > i"
hence "I v ≠ Some (DONE j)" for v using empty_not_scc[of j] unfolding SCC_at_def by simp
hence "SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) j = SCC_at I j"
using SCC_at_extend_neq[of I j "λ v. v ∈ {S ! j |j. seg_start (length B - 1) ≤ j ∧ j < seg_end (length B - 1)}" i] A
unfolding mark_as_done_abs_def
by blast
hence "finite (SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) j)"
using finite_scc
by presburger
} note AUX5 = this
{
have "finite (SCC_at I i)" using empty_not_scc[of i, simplified]
by auto
moreover have "finite {v. v ∈ {S ! j |j. seg_start (length B - 1) ≤ j ∧ j < seg_end (length B - 1)}}"
by fastforce
ultimately have "finite (SCC_at (mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i) i)"
unfolding mark_as_done_abs_def SCC_at_extend[of "λ v. v ∈ {S ! j |j. seg_start (length B - 1) ≤ j ∧ j < seg_end (length B - 1)}" i I]
by blast
} note AUX6 = this
have BNE: "B ≠ []" using NE unfolding p_α_def by force
show ?thesis
apply (unfold_locales)
apply (simp add: fr_graph_def fr_graph_axioms)
apply (metis One_nat_def less_SucE AUX1 AUX2)
using AUX3 apply blast
apply (metis AUX4 AUX5 AUX6 linorder_neqE_nat)
unfolding mark_as_done_abs_def
using S_subset_nodes I_reachable
by (auto split: if_splits simp: seg_end_last[OF BNE, simplified])
qed
lemma (in GSS_invar) pop_S_correct:
assumes NE: "p_α≠[]" and NS: "(set_mset pE_α) ∩ last p_α × UNIV = {}"
shows "pop_impl i
≤ SPEC (λs. (s, (butlast p_α, D_α ∪ last p_α, pE_α, vE)) ∈ GS_rel
∧ (GS_defs.I s = mark_as_done_abs (seg_start (length B - 1)) (seg_end (length B - 1)) I i))"
proof -
from NE have BNE: "B ≠ []" by (auto simp: p_α_def)
show ?thesis
apply (rule SPEC_rule_conjI)
using pop_correct[OF NE NS]
apply (auto simp: pw_le_iff refine_pw_simps)[]
unfolding pop_impl_def
apply(refine_vcg order_trans[OF mark_as_done_aux])
apply (auto simp: BNE intro!: seg_start_less_end seg_end_bound)
using B_in_bound
by (metis BNE B_in_bound' Misc.last_in_set in_set_conv_nth order.strict_implies_order)
qed
lemma (in GS_invar) t1:
"D_α ∩ ⋃ (set p_α) = {}"
unfolding D_α_def p_α_def seg_def
using I_consistent seg_end_bound apply auto
by (metis dual_order.strict_trans1 node_state.distinct(1) option.inject)
lemma (in GS_invar) t2:
"⋃ (set p_α) ⊆ E⇧*``V0"
by (simp add: S_subset_nodes set_p_α_is_set_S)
lemma (in GS_invar) t3:
"p_α ≠ [] ⟹ ⋃ (set p_α) ≠ {}"
by (simp add: empty_eq p_α_B_empty set_p_α_is_set_S)
lemma (in GS_invar) t4:
assumes B: "p_α ≠ []" and INV: "outer_invar_loc E V0 it D_α"
shows "D_α ⊂ E⇧*``V0"
using outer_invar_loc.D_reachable[OF INV] t1 t2 t3[OF B]
by fast
lemma (in GSS_invar) build_scc_impl_correct:
assumes B: "p_α ≠ []" "(set_mset pE_α) ∩ last (p_α) × UNIV = {}"
shows "build_scc_impl ≤ ⇓GSS_rel (RETURN (build_scc (SCC_α I i, p_α, D_α, pE_α, vE)))"
proof-
{
have "D_α ∩ ⋃ (set p_α) = {}"
unfolding D_α_def p_α_def seg_def
using I_consistent seg_end_bound apply auto
by (metis dual_order.strict_trans1 node_state.distinct(1) option.inject)
moreover have "⋃ (set p_α) ⊆ E⇧*``V0"
by (simp add: S_subset_nodes set_p_α_is_set_S)
moreover have "⋃ (set p_α) ≠ {}"
using B by (simp add: empty_eq p_α_B_empty set_p_α_is_set_S)
moreover have "D_α ⊆ E⇧*``V0"
using I_reachable unfolding D_α_def by blast
ultimately have "D_α ⊂ E⇧*``V0"
using D_α_alt_def
by fast
hence A: "⋃ (set (SCC_α I i)) ⊂ E⇧*``V0" unfolding oGS_α_alt_def D_α_alt_def .
have "i < card (E⇧* `` V0)" using psubset_card_mono[OF finite_reachableE_V0 A] i_bound_SCC
by linarith
} note AUX1 = this
show ?thesis unfolding build_scc_impl_def build_scc_def pop_impl_fr_def
apply (refine_rcg refine_vcg order_trans[OF GSS_invar.pop_S_correct])
using B GSS_invar_axioms apply auto
using AUX1 apply argo
apply (auto simp: GS_rel_def br_def conc_fun_def pop_def intro!: GSS_relI)
apply(simp add: SCC_α_mark_as_done[simplified] s_α_def α_def)
apply (auto simp: GSS_invar_mark_as_done[simplified])
apply (auto simp: s_α_def GS_defs.α_def)
done
qed
lemma select_edge_refine_aux:
assumes A: "(s,(p,D,pE,vE))∈GS_rel"
assumes NE: "p ≠ []"
shows "select_edge_impl s ≤
SPEC (λ (i,S,B,I,P). I = GS_defs.I s)"
proof -
from A have "GS_invar E V0 s"
by(auto simp: GS_rel_def in_br_conv)
interpret GS_invar E V0 s by fact
{
fix x1 x2
assume "GS_defs.P s ≠ []" and "last P = (x1, x2)"
hence "x1 ∈ set S"
using P_bound
by fastforce
hence "∃ j. (j < length S ∧ x1 = S ! j)"
by (metis in_set_conv_nth)
hence "∃ j. I x1 = Some (STACK j)"
using I_consistent
by blast
} note AUX1 = this
{
assume "P ≠ []"
hence "S ≠ []"
using P_bound
by force
hence "B ≠ []"
using B0
by blast
} note AUX2 = this
show ?thesis
unfolding select_edge_impl_def GS_defs.sel_rem_last_def
apply(refine_vcg)
apply auto
using AUX1 AUX2 P_bound
by auto
qed
lemma select_edge_S_refine_aux:
assumes A: "(s,(p,D,pE,vE))∈GS_rel"
assumes NE: "p ≠ []"
shows "select_edge_impl s ≤
SPEC (λ r. RETURN r ≤ ⇓(Id ×⇩r GS_rel) (select_edge (p,D,pE,vE)) ∧ (case r of (i,S,B,I,P) ⇒ I = GS_defs.I s))"
apply (rule SPEC_rule_conjI)
apply (rule order_trans[OF select_edge_refine])
using A NE apply auto[2]
apply (auto simp: pw_le_iff refine_pw_simps select_edge_def split: option.splits)[]
using select_edge_refine_aux[OF A NE] by blast
definition "select_edge_S_impl ≡ λ(i,s). do { (r,s')←select_edge_impl s; RETURN (r,(i,s')) }"
lemma (in GS_defs) sel_rem_last_pres_I: "sel_rem_last ≤⇩n SPEC (λ(_,(_,_,I',_)). I'=I)"
unfolding sel_rem_last_def
apply refine_vcg
by auto
lemma select_edge_impl_presI: "select_edge_impl (S,B,I,P) ≤⇩n SPEC (λ(_,(_,_,I',_)). I'=I)"
unfolding select_edge_impl_def
using GS_defs.sel_rem_last_pres_I[of "(S,B,I,P)"]
by simp
lemma select_edge_S_refine:
assumes A: "(s,(SCC,p,D,pE,vE))∈GSS_rel"
assumes NE: "p ≠ []"
shows "select_edge_S_impl s ≤ ⇓(Id ×⇩r GSS_rel) (select_edge_S (SCC,p,D,pE,vE))"
using assms
unfolding select_edge_S_impl_def select_edge_S_def
using select_edge_impl_presI select_edge_refine
by (clarsimp simp: pw_le_iff pw_leof_iff refine_pw_simps GSS_rel_GS_eq split: prod.splits; blast)
lemma i_I_to_outer:
assumes "((i, (S, B, I, P)), (SCC, ([], D, {#}, vE))) ∈ GSS_rel"
shows "((i,I),(SCC,D))∈oGSS_rel"
using assms
unfolding GSS_rel_def GS_rel_def GSS_defs.s_α_def oGSS_rel_def oGS_rel_def br_def oGS_α_def GS_defs.α_def GS_defs.D_α_def GSS_invar_def GS_invar_def GS_invar_axioms_def oGSS_invar_def oGS_invar_def oGSS_α_def
apply (auto simp: GS_defs.p_α_def GS_defs.pE_α_def SCC_α_def SCC_at_def fr_graph_axioms oGS_invar_axioms_def)
done
interpretation GSSX: GSS E V0 SBIP i for i SBIP by unfold_locales
definition "build_scc_impl_fr s i = GSSX.build_scc_impl s i"
lemma build_scc_impl_refine:
assumes REL: "((i,s), (SCC,p,D,pE,vE)) ∈ GSS_rel"
and B: "p ≠ []" "(set_mset pE) ∩ last p × UNIV = {}"
shows "build_scc_impl_fr s i ≤ ⇓GSS_rel (RETURN (build_scc (SCC,p,D,pE,vE)))"
proof -
from REL have [simp]: "p=GS_defs.p_α s ∧ D=GS_defs.D_α s ∧ pE=GS_defs.pE_α s" "SCC = SCC_α (GS_defs.I s) i"
and INV: "GSS_invar E V0 s i"
by (auto simp add: GSS_rel_def GS_rel_def br_def GS_α_split GSS_defs.s_α_def)
show ?thesis
unfolding build_scc_impl_fr_def
apply auto
apply (rule order_trans[OF GSS_invar.build_scc_impl_correct])
using INV B
by (auto simp: GSS_defs.s_α_def GS_defs.α_def GSS_rel_def in_br_conv)
qed
definition "compute_SCC_inner_while_body = (λ (i, s).
do {
(vo,(i,s)) ← select_edge_S_impl (i,s);
case vo of
Some v ⇒ do {
ASSERT (v ∈ E⇧*``V0);
if is_on_stack_impl v s then do {
s← collapse_impl_fr v s;
RETURN (i, s)
} else if ¬is_done_impl v s then do {
push_S_impl v (i, s)
} else do {
RETURN (i, s)
}
}
| None ⇒ do {
build_scc_impl_fr s i
}
})"
definition "compute_SCC_impl ≡ do {
let so = (0,Map.empty);
(i,D) ← FOREACHi (λit (i0,I0). cscc_outer_invar it (oGSS_α I0 i0)) V0 (λv0 (i0, I0). do {
ASSERT (v0 ∈ E⇧*``V0);
if ¬is_done_oimpl v0 I0 then do {
s ← initial_S_impl i0 v0 I0;
(i,(S,B,I,P))← WHILEIT (λ (i,s). (λ (SCC,p,D,pE). ∃vE. cscc_invar v0 (oGS_α I0) (SCC,p,D,pE,vE)) (GSS_defs.s_α s i))
(λ (_, s). ¬path_is_empty_impl s)
compute_SCC_inner_while_body
s;
RETURN (i, I)
} else
RETURN (i0, I0)
}) so;
RETURN (i, D)
}"
lemma compute_SCC_impl_refine: "compute_SCC_impl ≤ ⇓SCC_rel compute_SCC"
proof -
note [[goals_limit = 3]]
show ?thesis
unfolding compute_SCC_impl_def compute_SCC_def compute_SCC_inner_while_body_def
apply (refine_rcg
bind_refine'
select_edge_S_refine
initial_S_refine
oinitial_S_refine
build_scc_impl_refine
push_S_refine
collapse_S_refine
IdI
inj_on_id
)
apply refine_dref_type
apply (vc_solve (nopre) solve: asm_rl i_I_to_outer
simp: GS_rel_def br_def GS_defs.α_def oGS_rel_def oGS_α_def
oGSS_α_def oGSS_rel_def in_br_conv oGSS_invar_def GSS_defs.s_α_def
is_on_stack_refine path_is_empty_refine is_done_refine is_done_orefine
intro: oGSS_to_SCC_rel
dest!: GSS_relD
)
done
qed
end
end