Theory Gabow_SCC.Gabow_GBG
section ‹Lasso Finding Algorithm for Generalized B\"uchi Graphs \label{sec:gbg}›
theory Gabow_GBG
imports
Gabow_Skeleton
CAVA_Automata.Lasso
Find_Path
begin
locale igb_fr_graph =
igb_graph G + fr_graph G
for G :: "('Q,'more) igb_graph_rec_scheme"
lemma igb_fr_graphI:
assumes "igb_graph G"
assumes "finite ((g_E G)⇧* `` g_V0 G)"
shows "igb_fr_graph G"
proof -
interpret igb_graph G by fact
show ?thesis using assms(2) by unfold_locales
qed
text ‹
We implement an algorithm that computes witnesses for the
non-emptiness of Generalized B\"uchi Graphs (GBG).
›
section ‹Specification›
context igb_graph
begin
definition ce_correct
where
"ce_correct Vr Vl ≡ (∃pr pl.
Vr ⊆ E⇧*``V0 ∧ Vl ⊆ E⇧*``V0
∧ set pr⊆Vr ∧ set pl⊆Vl
∧ Vl×Vl ⊆ (E ∩ Vl×Vl)⇧*
∧ Vl×Vl ∩ E ≠ {}
∧ is_lasso_prpl (pr,pl))
"
definition find_ce_spec :: "('Q set × 'Q set) option nres" where
"find_ce_spec ≡ SPEC (λr. case r of
None ⇒ (∀prpl. ¬is_lasso_prpl prpl)
| Some (Vr,Vl) ⇒ ce_correct Vr Vl
)"
definition find_lasso_spec :: "('Q list × 'Q list) option nres" where
"find_lasso_spec ≡ SPEC (λr. case r of
None ⇒ (∀prpl. ¬is_lasso_prpl prpl)
| Some prpl ⇒ is_lasso_prpl prpl
)"
end
section ‹Invariant Extension›
text ‹Extension of the outer invariant:›
context igb_fr_graph
begin
definition no_acc_over
where
"no_acc_over D ≡ ¬(∃v∈D. ∃pl. pl≠[] ∧ path E v pl v ∧
(∀i<num_acc. ∃q∈set pl. i∈acc q))"
definition "fgl_outer_invar_ext ≡ λit (brk,D).
case brk of None ⇒ no_acc_over D | Some (Vr,Vl) ⇒ ce_correct Vr Vl"
definition "fgl_outer_invar ≡ λit (brk,D). case brk of
None ⇒ outer_invar it D ∧ no_acc_over D
| Some (Vr,Vl) ⇒ ce_correct Vr Vl"
end
text ‹Extension of the inner invariant:›
locale fgl_invar_loc =
invar_loc G v0 D0 p D pE
+ igb_graph G
for G :: "('Q, 'more) igb_graph_rec_scheme"
and v0 D0 and brk :: "('Q set × 'Q set) option" and p D pE +
assumes no_acc: "brk=None ⟹ ¬(∃v pl. pl≠[] ∧ path lvE v pl v ∧
(∀i<num_acc. ∃q∈set pl. i∈acc q))"
assumes acc: "brk=Some (Vr,Vl) ⟹ ce_correct Vr Vl"
begin
lemma locale_this: "fgl_invar_loc G v0 D0 brk p D pE"
by unfold_locales
lemma invar_loc_this: "invar_loc G v0 D0 p D pE" by unfold_locales
lemma eas_gba_graph_this: "igb_graph G" by unfold_locales
end
definition (in igb_graph) "fgl_invar v0 D0 ≡
λ(brk, p, D, pE). fgl_invar_loc G v0 D0 brk p D pE"
section ‹Definition of the Lasso-Finding Algorithm›
context igb_fr_graph
begin
definition find_ce :: "('Q set × 'Q set) option nres" where
"find_ce ≡ do {
let D = {};
(brk,_)←FOREACHci fgl_outer_invar V0
(λ(brk,_). brk=None)
(λv0 (brk,D0). do {
if v0∉D0 then do {
let s = (None,initial v0 D0);
(brk,p,D,pE) ← WHILEIT (fgl_invar v0 D0)
(λ(brk,p,D,pE). brk=None ∧ 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 {
let (p,D,pE) = collapse v (p,D,pE);
ASSERT (p≠[]);
if ∀i<num_acc. ∃q∈last p. i∈acc q then
RETURN (Some (⋃(set (butlast p)),last p),p,D,pE)
else
RETURN (None,p,D,pE)
} else if v∉D then do {
RETURN (None,push v (p,D,pE))
} else RETURN (None,p,D,pE)
}
| None ⇒ do {
ASSERT (pE ∩ last p × UNIV = {});
RETURN (None,pop (p,D,pE))
}
}) s;
ASSERT (brk=None ⟶ (p=[] ∧ pE={}));
RETURN (brk,D)
} else
RETURN (brk,D0)
}) (None,D);
RETURN brk
}"
end
section ‹Invariant Preservation›
context igb_fr_graph
begin
definition "fgl_invar_part ≡ λ(brk, p, D, pE).
fgl_invar_loc_axioms G brk p D pE"
lemma fgl_outer_invarI[intro?]:
"⟦
brk=None ⟹ outer_invar it D;
⟦brk=None ⟹ outer_invar it D⟧ ⟹ fgl_outer_invar_ext it (brk,D)⟧
⟹ fgl_outer_invar it (brk,D)"
unfolding outer_invar_def fgl_outer_invar_ext_def fgl_outer_invar_def
apply (auto split: prod.splits option.splits)
done
lemma fgl_invarI[intro?]:
"⟦ invar v0 D0 PDPE;
invar v0 D0 PDPE ⟹ fgl_invar_part (B,PDPE)⟧
⟹ fgl_invar v0 D0 (B,PDPE)"
unfolding invar_def fgl_invar_part_def fgl_invar_def
apply (simp split: prod.split_asm)
apply intro_locales
apply (simp add: invar_loc_def)
apply assumption
done
lemma fgl_invar_initial:
assumes OINV: "fgl_outer_invar it (None,D0)"
assumes A: "v0∈it" "v0∉D0"
shows "fgl_invar_part (None, initial v0 D0)"
proof -
from OINV interpret outer_invar_loc G it D0
by (simp add: fgl_outer_invar_def outer_invar_def)
from OINV have no_acc: "no_acc_over D0"
by (simp add: fgl_outer_invar_def fgl_outer_invar_ext_def)
{
fix v pl
assume "pl ≠ []" and P: "path (vE [{v0}] D0 (E ∩ {v0} × UNIV)) v pl v"
hence 1: "v∈D0"
by (cases pl) (auto simp: path_cons_conv vE_def touched_def)
have 2: "path E v pl v" using path_mono[OF vE_ss_E P] .
note 1 2
} note AUX1=this
show ?thesis
unfolding fgl_invar_part_def
apply (simp split: prod.splits add: initial_def)
apply unfold_locales
using ‹v0∉D0›
using AUX1 no_acc unfolding no_acc_over_def apply blast
by simp
qed
lemma fgl_invar_pop:
assumes INV: "fgl_invar v0 D0 (None,p,D,pE)"
assumes INV': "invar v0 D0 (pop (p,D,pE))"
assumes NE[simp]: "p≠[]"
assumes NO': "pE ∩ last p × UNIV = {}"
shows "fgl_invar_part (None, pop (p,D,pE))"
proof -
from INV interpret fgl_invar_loc G v0 D0 None p D pE
by (simp add: fgl_invar_def)
show ?thesis
apply (unfold fgl_invar_part_def pop_def)
apply (simp split: prod.splits)
apply unfold_locales
unfolding vE_pop[OF NE]
using no_acc apply auto []
apply simp
done
qed
lemma fgl_invar_collapse_ce_aux:
assumes INV: "invar v0 D0 (p, D, pE)"
assumes NE[simp]: "p≠[]"
assumes NONTRIV: "vE p D pE ∩ (last p × last p) ≠ {}"
assumes ACC: "∀i<num_acc. ∃q∈last p. i∈acc q"
shows "fgl_invar_part (Some (⋃(set (butlast p)), last p), p, D, pE)"
proof -
from INV interpret invar_loc G v0 D0 p D pE by (simp add: invar_def)
txt ‹The last collapsed node on the path contains states from all
accepting sets.
As it is strongly connected and reachable, we get a counter-example.
Here, we explicitely construct the lasso.›
let ?Er = "E ∩ (⋃(set (butlast p)) × UNIV)"
txt ‹We choose a node in the last Cnode, that is reachable only using
former Cnodes.›
obtain w where "(v0,w)∈?Er⇧*" "w∈last p"
proof cases
assume "length p = 1"
hence "v0∈last p"
using root_v0
by (cases p) auto
thus thesis by (auto intro: that)
next
assume "length p≠1"
hence "length p > 1" by (cases p) auto
hence "Suc (length p - 2) < length p" by auto
from p_connected'[OF this] obtain u v where
UIP: "u∈p!(length p - 2)" and VIP: "v∈p!(length p - 1)" and "(u,v)∈lvE"
using ‹length p > 1› by auto
from root_v0 have V0IP: "v0∈p!0" by (cases p) auto
from VIP have "v∈last p" by (cases p rule: rev_cases) auto
from pathI[OF V0IP UIP] ‹length p > 1› have
"(v0,u)∈(lvE ∩ ⋃(set (butlast p)) × ⋃(set (butlast p)))⇧*"
(is "_ ∈ …⇧*")
by (simp add: path_seg_butlast)
also have "… ⊆ ?Er" using lvE_ss_E by auto
finally (rtrancl_mono_mp[rotated]) have "(v0,u)∈?Er⇧*" .
also note ‹(u,v)∈lvE› UIP hence "(u,v)∈?Er" using lvE_ss_E ‹length p > 1›
apply (auto simp: Bex_def in_set_conv_nth)
by (metis One_nat_def Suc_lessE ‹Suc (length p - 2) < length p›
diff_Suc_1 length_butlast nth_butlast)
finally show ?thesis by (rule that) fact
qed
then obtain "pr" where
P_REACH: "path E v0 pr w" and
R_SS: "set pr ⊆ ⋃(set (butlast p))"
apply -
apply (erule rtrancl_is_path)
apply (frule path_nodes_edges)
apply (auto
dest!: order_trans[OF _ image_Int_subset]
dest: path_mono[of _ E, rotated])
done
have [simp]: "last p = p!(length p - 1)" by (cases p rule: rev_cases) auto
txt ‹From that node, we construct a lasso by inductively appending a path
for each accepting set›
{
fix na
assume na_def: "na = num_acc"
have "∃pl. pl≠[]
∧ path (lvE ∩ last p×last p) w pl w
∧ (∀i<num_acc. ∃q∈set pl. i∈acc q)"
using ACC
unfolding na_def[symmetric]
proof (induction na)
case 0
from NONTRIV obtain u v
where "(u,v)∈lvE ∩ last p × last p" "u∈last p" "v∈last p"
by auto
from cnode_connectedI ‹w∈last p› ‹u∈last p›
have "(w,u)∈(lvE ∩ last p × last p)⇧*"
by auto
also note ‹(u,v)∈lvE ∩ last p × last p›
also (rtrancl_into_trancl1) from cnode_connectedI ‹v∈last p› ‹w∈last p›
have "(v,w)∈(lvE ∩ last p × last p)⇧*"
by auto
finally obtain pl where "pl≠[]" "path (lvE ∩ last p × last p) w pl w"
by (rule trancl_is_path)
thus ?case by auto
next
case (Suc n)
from Suc.prems have "∀i<n. ∃q∈last p. i∈acc q" by auto
with Suc.IH obtain pl where IH:
"pl≠[]"
"path (lvE ∩ last p × last p) w pl w"
"∀i<n. ∃q∈set pl. i∈acc q"
by blast
from Suc.prems obtain v where "v∈last p" and "n∈acc v" by auto
from cnode_connectedI ‹w∈last p› ‹v∈last p›
have "(w,v)∈(lvE ∩ last p × last p)⇧*" by auto
then obtain pl1 where P1: "path (lvE ∩ last p × last p) w pl1 v"
by (rule rtrancl_is_path)
also from cnode_connectedI ‹w∈last p› ‹v∈last p›
have "(v,w)∈(lvE ∩ last p × last p)⇧*" by auto
then obtain pl2 where P2: "path (lvE ∩ last p × last p) v pl2 w"
by (rule rtrancl_is_path)
also (path_conc) note IH(2)
finally (path_conc) have
P: "path (lvE ∩ last p × last p) w (pl1@pl2@pl) w"
by simp
moreover from IH(1) have "pl1@pl2@pl ≠ []" by simp
moreover have "∀i'<n. ∃q∈set (pl1@pl2@pl). i'∈acc q" using IH(3) by auto
moreover have "v∈set (pl1@pl2@pl)" using P1 P2 P IH(1)
apply (cases pl2, simp_all add: path_cons_conv path_conc_conv)
apply (cases pl, simp_all add: path_cons_conv)
apply (cases pl1, simp_all add: path_cons_conv)
done
with ‹n∈acc v› have "∃q∈set (pl1@pl2@pl). n∈acc q" by auto
ultimately show ?case
apply (intro exI conjI)
apply assumption+
apply (auto elim: less_SucE)
done
qed
}
then obtain pl where pl: "pl≠[]" "path (lvE ∩ last p×last p) w pl w"
"∀i<num_acc. ∃q∈set pl. i∈acc q" by blast
hence "path E w pl w" and L_SS: "set pl ⊆ last p"
apply -
apply (frule path_mono[of _ E, rotated])
using lvE_ss_E
apply auto [2]
apply (drule path_nodes_edges)
apply (drule order_trans[OF _ image_Int_subset])
apply auto []
done
have LASSO: "is_lasso_prpl (pr,pl)"
unfolding is_lasso_prpl_def is_lasso_prpl_pre_def
using ‹path E w pl w› P_REACH pl by auto
from p_sc have "last p × last p ⊆ (lvE ∩ last p × last p)⇧*" by auto
with lvE_ss_E have VL_CLOSED: "last p × last p ⊆ (E ∩ last p × last p)⇧*"
apply (erule_tac order_trans)
apply (rule rtrancl_mono)
by blast
have NONTRIV': "last p × last p ∩ E ≠ {}"
by (metis Int_commute NONTRIV disjoint_mono lvE_ss_E subset_refl)
from order_trans[OF path_touched touched_reachable]
have LP_REACH: "last p ⊆ E⇧*``V0"
and BLP_REACH: "⋃(set (butlast p)) ⊆ E⇧*``V0"
apply -
apply (cases p rule: rev_cases)
apply simp
apply auto []
apply (cases p rule: rev_cases)
apply simp
apply auto []
done
show ?thesis
apply (simp add: fgl_invar_part_def)
apply unfold_locales
apply simp
using LASSO R_SS L_SS VL_CLOSED NONTRIV' LP_REACH BLP_REACH
unfolding ce_correct_def
apply simp
apply blast
done
qed
lemma fgl_invar_collapse_ce:
fixes u v
assumes INV: "fgl_invar v0 D0 (None,p,D,pE)"
defines "pE' ≡ pE - {(u,v)}"
assumes CFMT: "(p',D',pE'') = collapse v (p,D,pE')"
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)"
assumes ACC: "∀i<num_acc. ∃q∈last p'. i∈acc q"
defines i_def: "i ≡ idx_of p v"
shows "fgl_invar_part (
Some (⋃(set (butlast p')), last p'),
collapse v (p,D,pE'))"
proof -
from CFMT have p'_def: "p' = collapse_aux p i" and [simp]: "D'=D" "pE''=pE'"
by (simp_all add: collapse_def i_def)
from INV interpret fgl_invar_loc G v0 D0 None p D pE
by (simp add: fgl_invar_def)
from idx_of_props[OF BACK] have "i<length p" and "v∈p!i"
by (simp_all add: i_def)
have "u∈last p'"
using ‹u∈last p› ‹i<length p›
unfolding p'_def collapse_aux_def
apply (simp add: last_drop last_snoc)
by (metis Misc.last_in_set drop_eq_Nil last_drop not_le)
moreover have "v∈last p'"
using ‹v∈p!i› ‹i<length p›
unfolding p'_def collapse_aux_def
by (metis UnionI append_Nil Cons_nth_drop_Suc in_set_conv_decomp last_snoc)
ultimately have "vE p' D pE' ∩ last p' × last p' ≠ {}"
unfolding p'_def pE'_def by (auto simp: E)
have "p'≠[]" by (simp add: p'_def collapse_aux_def)
have [simp]: "collapse v (p,D,pE') = (p',D,pE')"
unfolding collapse_def p'_def i_def
by simp
show ?thesis
apply simp
apply (rule fgl_invar_collapse_ce_aux)
using INV' apply simp
apply fact+
done
qed
lemma fgl_invar_collapse_nce:
fixes u v
assumes INV: "fgl_invar v0 D0 (None,p,D,pE)"
defines "pE' ≡ pE - {(u,v)}"
assumes CFMT: "(p',D',pE'') = collapse v (p,D,pE')"
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)"
assumes NACC: "j<num_acc" "∀q∈last p'. j∉acc q"
defines "i ≡ idx_of p v"
shows "fgl_invar_part (None, collapse v (p,D,pE'))"
proof -
from CFMT have p'_def: "p' = collapse_aux p i" and [simp]: "D'=D" "pE''=pE'"
by (simp_all add: collapse_def i_def)
have [simp]: "collapse v (p,D,pE') = (p',D,pE')"
by (simp add: collapse_def p'_def i_def)
from INV interpret fgl_invar_loc G v0 D0 None p D pE
by (simp add: fgl_invar_def)
from INV' interpret inv': invar_loc G v0 D0 p' D pE' by (simp add: invar_def)
define vE' where "vE' = vE p' D pE'"
have vE'_alt: "vE' = insert (u,v) lvE"
by (simp add: vE'_def p'_def pE'_def E)
from idx_of_props[OF BACK] have "i<length p" and "v∈p!i"
by (simp_all add: i_def)
have "u∈last p'"
using ‹u∈last p› ‹i<length p›
unfolding p'_def collapse_aux_def
apply (simp add: last_drop last_snoc)
by (metis Misc.last_in_set drop_eq_Nil last_drop leD)
moreover have "v∈last p'"
using ‹v∈p!i› ‹i<length p›
unfolding p'_def collapse_aux_def
by (metis UnionI append_Nil Cons_nth_drop_Suc in_set_conv_decomp last_snoc)
ultimately have "vE' ∩ last p' × last p' ≠ {}"
unfolding vE'_alt by (auto)
have "p'≠[]" by (simp add: p'_def collapse_aux_def)
{
txt ‹
We show that no visited strongly connected component contains states
from all acceptance sets.›
fix w pl
txt ‹For this, we chose a non-trivial loop inside the visited edges›
assume P: "path vE' w pl w" and NT: "pl≠[]"
txt ‹And show that there is one acceptance set disjoint with the nodes
of the loop›
have "∃i<num_acc. ∀q∈set pl. i∉acc q"
proof cases
assume "set pl ∩ last p' = {}"
with path_restrict[OF P] ‹u∈last p'› ‹v∈last p'› have "path lvE w pl w"
apply -
apply (drule path_mono[of _ lvE, rotated])
unfolding vE'_alt
by auto
with no_acc NT show ?thesis by auto
next
assume "set pl ∩ last p' ≠ {}"
txt ‹Then, the loop must be completely inside the last CNode›
from inv'.loop_in_lastnode[folded vE'_def, OF P ‹p'≠[]› this]
have "w∈last p'" "set pl ⊆ last p'" .
with NACC show ?thesis by blast
qed
} note AUX_no_acc = this
show ?thesis
apply (simp add: fgl_invar_part_def)
apply unfold_locales
using AUX_no_acc[unfolded vE'_def] apply auto []
apply simp
done
qed
lemma collapse_ne: "([],D',pE') ≠ collapse v (p,D,pE)"
by (simp add: collapse_def collapse_aux_def Let_def)
lemma fgl_invar_push:
assumes INV: "fgl_invar v0 D0 (None,p,D,pE)"
assumes BRK[simp]: "brk=None"
assumes NE[simp]: "p≠[]"
assumes E: "(u,v)∈pE" and UIL: "u∈last p"
assumes VNE: "v∉⋃(set p)" "v∉D"
assumes INV': "invar v0 D0 (push v (p,D,pE - {(u,v)}))"
shows "fgl_invar_part (None, push v (p,D,pE - {(u,v)}))"
proof -
from INV interpret fgl_invar_loc G v0 D0 None p D pE
by (simp add: fgl_invar_def)
define pE' where "pE' = (pE - {(u,v)} ∪ E∩{v}×UNIV)"
have [simp]: "push v (p,D,pE - {(u,v)}) = (p@[{v}],D,pE')"
by (simp add: push_def pE'_def)
from INV' interpret inv': invar_loc G v0 D0 "(p@[{v}])" D "pE'"
by (simp add: invar_def)
note defs_fold = vE_push[OF E UIL VNE, folded pE'_def]
{
txt ‹We show that there still is no loop that contains all accepting
nodes. For this, we choose some loop.›
fix w pl
assume P: "path (insert (u,v) lvE) w pl w" and [simp]: "pl≠[]"
have "∃i<num_acc. ∀q∈set pl. i∉acc q"
proof cases
assume "v∈set pl"
txt ‹Then the loop is entirely on the last cnode›
with inv'.loop_in_lastnode[unfolded defs_fold, OF P]
have [simp]: "w=v" and SPL: "set pl = {v}" by auto
txt ‹However, we then either have that the last cnode is contained in
the last but one cnode, or that there is a visited edge inside the
last cnode.›
from P SPL have "u=v ∨ (v,v)∈lvE"
apply (cases pl) apply (auto simp: path_cons_conv)
apply (case_tac list)
apply (auto simp: path_cons_conv)
done
txt ‹Both leads to a contradiction›
hence False proof
assume "u=v"
with UIL VNE show False by auto
next
assume "(v,v)∈lvE"
with vE_touched VNE show False unfolding touched_def by auto
qed
thus ?thesis ..
next
assume A: "v∉set pl"
txt ‹Then, the path lays inside the old visited edges›
have "path lvE w pl w"
proof -
have "w∈set pl" using P by (cases pl) (auto simp: path_cons_conv)
with A show ?thesis using path_restrict[OF P]
apply -
apply (drule path_mono[of _ lvE, rotated])
apply (cases pl, auto) []
apply assumption
done
qed
txt ‹And thus, the proposition follows from the invariant on the old
state›
with no_acc show ?thesis
apply simp
using ‹pl≠[]›
by blast
qed
} note AUX_no_acc = this
show ?thesis
unfolding fgl_invar_part_def
apply simp
apply unfold_locales
unfolding defs_fold
using AUX_no_acc apply auto []
apply simp
done
qed
lemma fgl_invar_skip:
assumes INV: "fgl_invar v0 D0 (None,p,D,pE)"
assumes BRK[simp]: "brk=None"
assumes NE[simp]: "p≠[]"
assumes E: "(u,v)∈pE" and UIL: "u∈last p"
assumes VID: "v∈D"
assumes INV': "invar v0 D0 (p, D, (pE - {(u,v)}))"
shows "fgl_invar_part (None, p, D, (pE - {(u,v)}))"
proof -
from INV interpret fgl_invar_loc G v0 D0 None p D pE
by (simp add: fgl_invar_def)
from INV' interpret inv': invar_loc G v0 D0 p D "(pE - {(u,v)})"
by (simp add: invar_def)
{
txt ‹We show that there still is no loop that contains all accepting
nodes. For this, we choose some loop.›
fix w pl
assume P: "path (insert (u,v) lvE) w pl w" and [simp]: "pl≠[]"
from P have "∃i<num_acc. ∀q∈set pl. i∉acc q"
proof (cases rule: path_edge_rev_cases)
case no_use
txt ‹The proposition follows from the invariant for the old state›
with no_acc show ?thesis
apply simp
using ‹pl≠[]›
by blast
next
case (split p1 p2)
txt ‹As done is closed under transitions, the nodes of the edge have
already been visited›
from split(2) D_closed_vE_rtrancl
have WID: "w∈D"
using VID by (auto dest!: path_is_rtrancl)
from split(1) WID D_closed_vE_rtrancl have "u∈D"
apply (cases rule: path_edge_cases)
apply (auto dest!: path_is_rtrancl)
done
txt ‹Which is a contradition to the assumptions›
with UIL p_not_D have False by (cases p rule: rev_cases) auto
thus ?thesis ..
qed
} note AUX_no_acc = this
show ?thesis
apply (simp add: fgl_invar_part_def)
apply unfold_locales
unfolding vE_remove[OF NE E]
using AUX_no_acc apply auto []
apply simp
done
qed
lemma fgl_outer_invar_initial:
"outer_invar V0 {} ⟹ fgl_outer_invar_ext V0 (None, {})"
unfolding fgl_outer_invar_ext_def
apply (simp add: no_acc_over_def)
done
lemma fgl_outer_invar_brk:
assumes INV: "fgl_invar v0 D0 (Some (Vr,Vl),p,D,pE)"
shows "fgl_outer_invar_ext anyIt (Some (Vr,Vl), anyD)"
proof -
from INV interpret fgl_invar_loc G v0 D0 "Some (Vr,Vl)" p D pE
by (simp add: fgl_invar_def)
from acc show ?thesis by (simp add: fgl_outer_invar_ext_def)
qed
lemma fgl_outer_invar_newnode_nobrk:
assumes A: "v0∉D0" "v0∈it"
assumes OINV: "fgl_outer_invar it (None,D0)"
assumes INV: "fgl_invar v0 D0 (None,[],D',pE)"
shows "fgl_outer_invar_ext (it-{v0}) (None,D')"
proof -
from OINV interpret outer_invar_loc G it D0
unfolding fgl_outer_invar_def outer_invar_def by simp
from INV interpret inv: fgl_invar_loc G v0 D0 None "[]" D' pE
unfolding fgl_invar_def by simp
from inv.pE_fin have [simp]: "pE = {}" by simp
{ fix v pl
assume A: "v∈D'" "path E v pl v"
have "path (E ∩ D' × UNIV) v pl v"
apply (rule path_mono[OF _ path_restrict_closed[OF inv.D_closed A]])
by auto
} note AUX1=this
show ?thesis
unfolding fgl_outer_invar_ext_def
apply simp
using inv.no_acc AUX1
apply (auto simp add: vE_def touched_def no_acc_over_def) []
done
qed
lemma fgl_outer_invar_newnode:
assumes A: "v0∉D0" "v0∈it"
assumes OINV: "fgl_outer_invar it (None,D0)"
assumes INV: "fgl_invar v0 D0 (brk,p,D',pE)"
assumes CASES: "(∃Vr Vl. brk = Some (Vr, Vl)) ∨ p = []"
shows "fgl_outer_invar_ext (it-{v0}) (brk,D')"
using CASES
apply (elim disjE1)
using fgl_outer_invar_brk[of v0 D0 _ _ p D' pE] INV
apply -
apply (auto, assumption) []
using fgl_outer_invar_newnode_nobrk[OF A] OINV INV apply auto []
done
lemma fgl_outer_invar_Dnode:
assumes "fgl_outer_invar it (None, D)" "v∈D"
shows "fgl_outer_invar_ext (it - {v}) (None, D)"
using assms
by (auto simp: fgl_outer_invar_def fgl_outer_invar_ext_def)
lemma fgl_fin_no_lasso:
assumes A: "fgl_outer_invar {} (None, D)"
assumes B: "is_lasso_prpl prpl"
shows "False"
proof -
obtain "pr" pl where [simp]: "prpl = (pr,pl)" by (cases prpl)
from A have NA: "no_acc_over D"
by (simp add: fgl_outer_invar_def fgl_outer_invar_ext_def)
from A have "outer_invar {} D" by (simp add: fgl_outer_invar_def)
with fin_outer_D_is_reachable have [simp]: "D=E⇧*``V0" by simp
from NA B show False
apply (simp add: no_acc_over_def is_lasso_prpl_def is_lasso_prpl_pre_def)
apply clarsimp
apply (blast dest: path_is_rtrancl)
done
qed
lemma fgl_fin_lasso:
assumes A: "fgl_outer_invar it (Some (Vr,Vl), D)"
shows "ce_correct Vr Vl"
using A by (simp add: fgl_outer_invar_def fgl_outer_invar_ext_def)
lemmas fgl_invar_preserve =
fgl_invar_initial fgl_invar_push fgl_invar_pop
fgl_invar_collapse_ce fgl_invar_collapse_nce fgl_invar_skip
fgl_outer_invar_newnode fgl_outer_invar_Dnode
invar_initial outer_invar_initial fgl_invar_initial fgl_outer_invar_initial
fgl_fin_no_lasso fgl_fin_lasso
end
section ‹Main Correctness Proof›
context igb_fr_graph
begin
lemma outer_invar_from_fgl_invarI:
"fgl_outer_invar it (None,D) ⟹ outer_invar it D"
unfolding fgl_outer_invar_def outer_invar_def
by (simp split: prod.splits)
lemma invar_from_fgl_invarI: "fgl_invar v0 D0 (B,PDPE) ⟹ invar v0 D0 PDPE"
unfolding fgl_invar_def invar_def
apply (simp split: prod.splits)
unfolding fgl_invar_loc_def by simp
theorem find_ce_correct: "find_ce ≤ find_ce_spec"
proof -
note [simp del] = Union_iff
show ?thesis
unfolding find_ce_def find_ce_spec_def select_edge_def select_def
apply (refine_rcg
WHILEIT_rule[where R="inv_image (abs_wf_rel v0) snd" for v0]
refine_vcg
)
using [[goals_limit = 5]]
apply (vc_solve
rec: fgl_invarI fgl_outer_invarI
intro: invar_from_fgl_invarI outer_invar_from_fgl_invarI
dest!: sym[of "collapse a b" for a b]
simp: collapse_ne
simp: pE_fin'[OF invar_from_fgl_invarI] finite_V0
solve: invar_preserve
solve: asm_rl[of "_ ∩ _ = {}"]
solve: fgl_invar_preserve)
done
qed
end
section "Emptiness Check"
text ‹Using the lasso-finding algorithm, we can define an emptiness check›
context igb_fr_graph
begin
definition "abs_is_empty ≡ do {
ce ← find_ce;
RETURN (ce = None)
}"
theorem abs_is_empty_correct:
"abs_is_empty ≤ SPEC (λres. res ⟷ (∀r. ¬is_acc_run r))"
unfolding abs_is_empty_def
apply (refine_rcg refine_vcg
order_trans[OF find_ce_correct, unfolded find_ce_spec_def])
unfolding ce_correct_def
using lasso_accepted accepted_lasso
apply (clarsimp split: option.splits)
apply (metis is_lasso_prpl_of_lasso surj_pair)
by (metis is_lasso_prpl_conv)
definition "abs_is_empty_ce ≡ do {
ce ← find_ce;
case ce of
None ⇒ RETURN None
| Some (Vr,Vl) ⇒ do {
ASSERT (∃pr pl. set pr ⊆ Vr ∧ set pl ⊆ Vl ∧ Vl × Vl ⊆ (E ∩ Vl×Vl)⇧*
∧ is_lasso_prpl (pr,pl));
(pr,pl) ← SPEC (λ(pr,pl).
set pr ⊆ Vr
∧ set pl ⊆ Vl
∧ Vl × Vl ⊆ (E ∩ Vl×Vl)⇧*
∧ is_lasso_prpl (pr,pl));
RETURN (Some (pr,pl))
}
}"
theorem abs_is_empty_ce_correct: "abs_is_empty_ce ≤ SPEC (λres. case res of
None ⇒ (∀r. ¬is_acc_run r)
| Some (pr,pl) ⇒ is_acc_run (pr⌢pl⇧ω)
)"
unfolding abs_is_empty_ce_def
apply (refine_rcg refine_vcg
order_trans[OF find_ce_correct, unfolded find_ce_spec_def])
apply (clarsimp_all simp: ce_correct_def)
using accepted_lasso finite_reachableE_V0 apply (metis is_lasso_prpl_of_lasso surj_pair)
apply blast
apply (simp add: lasso_prpl_acc_run)
done
end
section ‹Refinement›
text ‹
In this section, we refine the lasso finding algorithm to use efficient
data structures. First, we explicitely keep track of the set of acceptance
classes for every c-node on the path. Second, we use Gabow's data structure
to represent the path.
›
subsection ‹Addition of Explicit Accepting Sets›
text ‹In a first step, we explicitely keep track of the current set of
acceptance classes for every c-node on the path.›
type_synonym 'a abs_gstate = "nat set list × 'a abs_state"
type_synonym 'a ce = "('a set × 'a set) option"
type_synonym 'a abs_gostate = "'a ce × 'a set"
context igb_fr_graph
begin
definition gstate_invar :: "'Q abs_gstate ⇒ bool" where
"gstate_invar ≡ λ(a,p,D,pE). a = map (λV. ⋃(acc`V)) p"
definition "gstate_rel ≡ br snd gstate_invar"
lemma gstate_rel_sv[relator_props,simp,intro!]: "single_valued gstate_rel"
by (simp add: gstate_rel_def)
definition (in -) gcollapse_aux
:: "nat set list ⇒ 'a set list ⇒ nat ⇒ nat set list × 'a set list"
where "gcollapse_aux a p i ≡
(take i a @ [⋃(set (drop i a))],take i p @ [⋃(set (drop i p))])"
definition (in -) gcollapse :: "'a ⇒ 'a abs_gstate ⇒ 'a abs_gstate"
where "gcollapse v APDPE ≡
let
(a,p,D,pE)=APDPE;
i=idx_of p v;
(a,p) = gcollapse_aux a p i
in (a,p,D,pE)"
definition "gpush v s ≡
let
(a,s) = s
in
(a@[acc v],push v s)"
definition "gpop s ≡
let (a,s) = s in (butlast a,pop s)"
definition ginitial :: "'Q ⇒ 'Q abs_gostate ⇒ 'Q abs_gstate"
where "ginitial v0 s0 ≡ ([acc v0], initial v0 (snd s0))"
definition goinitial :: "'Q abs_gostate" where "goinitial ≡ (None,{})"
definition go_is_no_brk :: "'Q abs_gostate ⇒ bool"
where "go_is_no_brk s ≡ fst s = None"
definition goD :: "'Q abs_gostate ⇒ 'Q set" where "goD s ≡ snd s"
definition goBrk :: "'Q abs_gostate ⇒ 'Q ce" where "goBrk s ≡ fst s"
definition gto_outer :: "'Q ce ⇒ 'Q abs_gstate ⇒ 'Q abs_gostate"
where "gto_outer brk s ≡ let (A,p,D,pE)=s in (brk,D)"
definition "gselect_edge s ≡ do {
let (a,s)=s;
(r,s)←select_edge s;
RETURN (r,a,s)
}"
definition gfind_ce :: "('Q set × 'Q set) option nres" where
"gfind_ce ≡ do {
let os = goinitial;
os←FOREACHci fgl_outer_invar V0 (go_is_no_brk) (λv0 s0. do {
if v0∉goD s0 then do {
let s = (None,ginitial v0 s0);
(brk,a,p,D,pE) ← WHILEIT (λ(brk,a,s). fgl_invar v0 (goD s0) (brk,s))
(λ(brk,a,p,D,pE). brk=None ∧ p ≠ []) (λ(_,a,p,D,pE).
do {
(vo,(a,p,D,pE)) ← gselect_edge (a,p,D,pE);
ASSERT (p≠[]);
case vo of
Some v ⇒ do {
if v ∈ ⋃(set p) then do {
let (a,p,D,pE) = gcollapse v (a,p,D,pE);
ASSERT (p≠[]);
ASSERT (a≠[]);
if last a = {0..<num_acc} then
RETURN (Some (⋃(set (butlast p)),last p),a,p,D,pE)
else
RETURN (None,a,p,D,pE)
} else if v∉D then do {
RETURN (None,gpush v (a,p,D,pE))
} else RETURN (None,a,p,D,pE)
}
| None ⇒ do {
ASSERT (pE ∩ last p × UNIV = {});
RETURN (None,gpop (a,p,D,pE))
}
}) s;
ASSERT (brk=None ⟶ (p=[] ∧ pE={}));
RETURN (gto_outer brk (a,p,D,pE))
} else RETURN s0
}) os;
RETURN (goBrk os)
}"
lemma gcollapse_refine:
"⟦(v',v)∈Id; (s',s)∈gstate_rel⟧
⟹ (gcollapse v' s',collapse v s)∈gstate_rel"
unfolding gcollapse_def collapse_def collapse_aux_def gcollapse_aux_def
apply (simp add: gstate_rel_def br_def Let_def)
unfolding gstate_invar_def[abs_def]
apply (auto split: prod.splits simp: take_map drop_map)
done
lemma gpush_refine:
"⟦(v',v)∈Id; (s',s)∈gstate_rel⟧ ⟹ (gpush v' s',push v s)∈gstate_rel"
unfolding gpush_def push_def
apply (simp add: gstate_rel_def br_def)
unfolding gstate_invar_def[abs_def]
apply (auto split: prod.splits)
done
lemma gpop_refine:
"⟦(s',s)∈gstate_rel⟧ ⟹ (gpop s',pop s)∈gstate_rel"
unfolding gpop_def pop_def
apply (simp add: gstate_rel_def br_def)
unfolding gstate_invar_def[abs_def]
apply (auto split: prod.splits simp: map_butlast)
done
lemma ginitial_refine:
"(ginitial x (None, b), initial x b) ∈ gstate_rel"
unfolding ginitial_def gstate_rel_def br_def gstate_invar_def initial_def
by auto
lemma oinitial_b_refine: "((None,{}),(None,{}))∈Id×⇩rId" by simp
lemma gselect_edge_refine: "⟦(s',s)∈gstate_rel⟧ ⟹ gselect_edge s'
≤⇓(⟨Id⟩option_rel ×⇩r gstate_rel) (select_edge s)"
unfolding gselect_edge_def select_edge_def
apply (simp add: pw_le_iff refine_pw_simps prod_rel_sv
split: prod.splits option.splits)
apply (auto simp: gstate_rel_def br_def gstate_invar_def)
done
lemma last_acc_impl:
assumes "p≠[]"
assumes "((a',p',D',pE'),(p,D,pE))∈gstate_rel"
shows "(last a' = {0..<num_acc}) = (∀i<num_acc. ∃q∈last p. i∈acc q)"
using assms acc_bound unfolding gstate_rel_def br_def gstate_invar_def
by (auto simp: last_map)
lemma fglr_aux1:
assumes V: "(v',v)∈Id" and S: "(s',s)∈gstate_rel"
and P: "⋀a' p' D' pE' p D pE. ((a',p',D',pE'),(p,D,pE))∈gstate_rel
⟹ f' a' p' D' pE' ≤⇓R (f p D pE)"
shows "(let (a',p',D',pE') = gcollapse v' s' in f' a' p' D' pE')
≤ ⇓R (let (p,D,pE) = collapse v s in f p D pE)"
apply (auto split: prod.splits)
apply (rule P)
using gcollapse_refine[OF V S]
apply simp
done
lemma gstate_invar_empty:
"gstate_invar (a,[],D,pE) ⟹ a=[]"
"gstate_invar ([],p,D,pE) ⟹ p=[]"
by (auto simp add: gstate_invar_def)
lemma find_ce_refine: "gfind_ce ≤⇓Id find_ce"
unfolding gfind_ce_def find_ce_def
unfolding goinitial_def go_is_no_brk_def[abs_def] goD_def goBrk_def
gto_outer_def
using [[goals_limit = 1]]
apply (refine_rcg
gselect_edge_refine prod_relI[OF IdI gpop_refine]
prod_relI[OF IdI gpush_refine]
fglr_aux1 last_acc_impl oinitial_b_refine
inj_on_id
)
apply refine_dref_type
apply (simp_all add: ginitial_refine)
apply (vc_solve (nopre)
solve: asm_rl
simp: gstate_rel_def br_def gstate_invar_empty)
done
end
subsection ‹Refinement to Gabow's Data Structure›
subsubsection ‹Preliminaries›
definition Un_set_drop_impl :: "nat ⇒ 'a set list ⇒ 'a set nres"
where "Un_set_drop_impl i A ≡
do {
(_,res) ← WHILET (λ(i,res). i < length A) (λ(i,res). do {
ASSERT (i<length A);
let res = A!i ∪ res;
let i = i + 1;
RETURN (i,res)
}) (i,{});
RETURN res
}"
lemma Un_set_drop_impl_correct:
"Un_set_drop_impl i A ≤ SPEC (λr. r=⋃(set (drop i A)))"
unfolding Un_set_drop_impl_def
apply (refine_rcg
WHILET_rule[where I="λ(i',res). res=⋃(set ((drop i (take i' A)))) ∧ i≤i'"
and R="measure (λ(i',_). length A - i')"]
refine_vcg)
apply (auto simp: take_Suc_conv_app_nth)
done
schematic_goal Un_set_drop_code_aux:
assumes [autoref_rules]: "(es_impl,{})∈⟨R⟩Rs"
assumes [autoref_rules]: "(un_impl,(∪))∈⟨R⟩Rs→⟨R⟩Rs→⟨R⟩Rs"
shows "(?c,Un_set_drop_impl)∈nat_rel → ⟨⟨R⟩Rs⟩as_rel → ⟨⟨R⟩Rs⟩nres_rel"
unfolding Un_set_drop_impl_def[abs_def]
apply (autoref (trace, keep_goal))
done
concrete_definition Un_set_drop_code uses Un_set_drop_code_aux
schematic_goal Un_set_drop_tr_aux:
"RETURN ?c ≤ Un_set_drop_code es_impl un_impl i A"
unfolding Un_set_drop_code_def
by refine_transfer
concrete_definition Un_set_drop_tr for es_impl un_impl i A
uses Un_set_drop_tr_aux
lemma Un_set_drop_autoref[autoref_rules]:
assumes "GEN_OP es_impl {} (⟨R⟩Rs)"
assumes "GEN_OP un_impl (∪) (⟨R⟩Rs→⟨R⟩Rs→⟨R⟩Rs)"
shows "(λi A. RETURN (Un_set_drop_tr es_impl un_impl i A),Un_set_drop_impl)
∈nat_rel → ⟨⟨R⟩Rs⟩as_rel → ⟨⟨R⟩Rs⟩nres_rel"
apply (intro fun_relI nres_relI)
apply (rule order_trans[OF Un_set_drop_tr.refine])
using Un_set_drop_code.refine[of es_impl Rs R un_impl,
param_fo, THEN nres_relD]
using assms
by simp
subsubsection ‹Actual Refinement›
type_synonym 'Q gGS = "nat set list × 'Q GS"
type_synonym 'Q goGS = "'Q ce × 'Q oGS"
context igb_graph
begin
definition gGS_invar :: "'Q gGS ⇒ bool"
where "gGS_invar s ≡
let (a,S,B,I,P) = s in
GS_invar (S,B,I,P)
∧ length a = length B
∧ ⋃(set a) ⊆ {0..<num_acc}
"
definition gGS_α :: "'Q gGS ⇒ 'Q abs_gstate"
where "gGS_α s ≡ let (a,s)=s in (a,GS.α s)"
definition "gGS_rel ≡ br gGS_α gGS_invar"
lemma gGS_rel_sv[relator_props,intro!,simp]: "single_valued gGS_rel"
unfolding gGS_rel_def by auto
definition goGS_invar :: "'Q goGS ⇒ bool" where
"goGS_invar s ≡ let (brk,ogs)=s in brk=None ⟶ oGS_invar ogs"
definition "goGS_α s ≡ let (brk,ogs)=s in (brk,oGS_α ogs)"
definition "goGS_rel ≡ br goGS_α goGS_invar"
lemma goGS_rel_sv[relator_props,intro!,simp]: "single_valued goGS_rel"
unfolding goGS_rel_def by auto
end
context igb_fr_graph
begin
lemma gGS_relE:
assumes "(s',(a,p,D,pE))∈gGS_rel"
obtains S' B' I' P' where "s'=(a,S',B',I',P')"
and "((S',B',I',P'),(p,D,pE))∈GS_rel"
and "length a = length B'"
and "⋃(set a) ⊆ {0..<num_acc}"
using assms
apply (cases s')
apply (simp add: gGS_rel_def br_def gGS_α_def GS.α_def)
apply (rule that)
apply (simp only:)
apply (auto simp: GS_rel_def br_def gGS_invar_def GS.α_def)
done
definition goinitial_impl :: "'Q goGS"
where "goinitial_impl ≡ (None,Map.empty)"
lemma goinitial_impl_refine: "(goinitial_impl,goinitial)∈goGS_rel"
by (auto
simp: goinitial_impl_def goinitial_def goGS_rel_def br_def
simp: goGS_α_def goGS_invar_def oGS_α_def oGS_invar_def)
definition gto_outer_impl :: "'Q ce ⇒ 'Q gGS ⇒ 'Q goGS"
where "gto_outer_impl brk s ≡ let (A,S,B,I,P)=s in (brk,I)"
lemma gto_outer_refine:
assumes A: "brk = None ⟶ (p=[] ∧ pE={})"
assumes B: "(s, (A,p, D, pE)) ∈ gGS_rel"
assumes C: "(brk',brk)∈Id"
shows "(gto_outer_impl brk' s,gto_outer brk (A,p,D,pE))∈goGS_rel"
proof (cases s)
fix A S B I P
assume [simp]: "s=(A,S,B,I,P)"
show ?thesis
using C
apply (cases brk)
using assms I_to_outer[of S B I P D]
apply (auto
simp: goGS_rel_def br_def goGS_α_def gto_outer_def
gto_outer_impl_def goGS_invar_def
simp: gGS_rel_def oGS_rel_def GS_rel_def gGS_α_def gGS_invar_def
GS.α_def) []
using B apply (auto
simp: gto_outer_def gto_outer_impl_def
simp: br_def goGS_rel_def goGS_invar_def goGS_α_def oGS_α_def
simp: gGS_rel_def gGS_α_def GS.α_def GS.D_α_def
)
done
qed
definition "gpush_impl v s ≡ let (a,s)=s in (a@[acc v], push_impl v s)"
lemma gpush_impl_refine:
assumes B: "(s',(a,p,D,pE))∈gGS_rel"
assumes A: "(v',v)∈Id"
assumes PRE: "v' ∉ ⋃(set p)" "v' ∉ D"
shows "(gpush_impl v' s', gpush v (a,p,D,pE))∈gGS_rel"
proof -
from B obtain S' B' I' P' where [simp]: "s'=(a,S',B',I',P')"
and OSR: "((S',B',I',P'),(p,D,pE))∈GS_rel" and L: "length a = length B'"
and R: "⋃(set a) ⊆ {0..<num_acc}"
by (rule gGS_relE)
{
fix S B I P S' B' I' P'
assume "push_impl v (S, B, I, P) = (S', B', I', P')"
hence "length B' = Suc (length B)"
by (auto simp add: push_impl_def GS.push_impl_def Let_def)
} note AUX1=this
from push_refine[OF OSR A PRE] A L acc_bound R show ?thesis
unfolding gpush_impl_def gpush_def
gGS_rel_def gGS_invar_def gGS_α_def GS_rel_def br_def
apply (auto dest: AUX1)
done
qed
definition gpop_impl :: "'Q gGS ⇒ 'Q gGS nres"
where "gpop_impl s ≡ do {
let (a,s)=s;
s←pop_impl s;
ASSERT (a≠[]);
let a = butlast a;
RETURN (a,s)
}"
lemma gpop_impl_refine:
assumes A: "(s',(a,p,D,pE))∈gGS_rel"
assumes PRE: "p ≠ []" "pE ∩ last p × UNIV = {}"
shows "gpop_impl s' ≤ ⇓gGS_rel (RETURN (gpop (a,p,D,pE)))"
proof -
from A obtain S' B' I' P' where [simp]: "s'=(a,S',B',I',P')"
and OSR: "((S',B',I',P'),(p,D,pE))∈GS_rel" and L: "length a = length B'"
and R: "⋃(set a) ⊆ {0..<num_acc}"
by (rule gGS_relE)
from PRE OSR have [simp]: "a≠[]" using L
by (auto simp add: GS_rel_def br_def GS.α_def GS.p_α_def)
{
fix S B I P S' B' I' P'
assume "nofail (pop_impl ((S, B, I, P)::'a GS))"
"inres (pop_impl ((S, B, I, P)::'a GS)) (S', B', I', P')"
hence "length B' = length B - Suc 0"
apply (simp add: pop_impl_def GS.pop_impl_def Let_def
refine_pw_simps)
apply auto
done
} note AUX1=this
from A L show ?thesis
unfolding gpop_impl_def gpop_def gGS_rel_def gGS_α_def br_def
apply (simp add: Let_def)
using pop_refine[OF OSR PRE]
apply (simp add: pw_le_iff refine_pw_simps split: prod.splits)
unfolding gGS_rel_def gGS_invar_def gGS_α_def GS_rel_def GS.α_def br_def
apply (auto dest!: AUX1 in_set_butlastD iff: Sup_le_iff)
done
qed
definition gselect_edge_impl :: "'Q gGS ⇒ ('Q option × 'Q gGS) nres"
where "gselect_edge_impl s ≡
do {
let (a,s)=s;
(vo,s)←select_edge_impl s;
RETURN (vo,a,s)
}"
thm select_edge_refine
lemma gselect_edge_impl_refine:
assumes A: "(s', a, p, D, pE) ∈ gGS_rel"
assumes PRE: "p ≠ []"
shows "gselect_edge_impl s' ≤ ⇓(Id ×⇩r gGS_rel) (gselect_edge (a, p, D, pE))"
proof -
from A obtain S' B' I' P' where [simp]: "s'=(a,S',B',I',P')"
and OSR: "((S',B',I',P'),(p,D,pE))∈GS_rel" and L: "length a = length B'"
and R: "⋃(set a) ⊆ {0..<num_acc}"
by (rule gGS_relE)
{
fix S B I P S' B' I' P' vo
assume "nofail (select_edge_impl ((S, B, I, P)::'a GS))"
"inres (select_edge_impl ((S, B, I, P)::'a GS)) (vo, (S', B', I', P'))"
hence "length B' = length B"
apply (simp add: select_edge_impl_def GS.sel_rem_last_def refine_pw_simps
split: if_split_asm prod.splits)
apply auto
done
} note AUX1=this
show ?thesis
using select_edge_refine[OF OSR PRE]
unfolding gselect_edge_impl_def gselect_edge_def
apply (simp add: refine_pw_simps pw_le_iff prod_rel_sv)
unfolding gGS_rel_def br_def gGS_α_def gGS_invar_def GS_rel_def GS.α_def
apply (simp split: prod.splits)
apply clarsimp
using R
apply (auto simp: L dest: AUX1)
done
qed
term GS.idx_of_impl
thm GS_invar.idx_of_correct
definition gcollapse_impl_aux :: "'Q ⇒ 'Q gGS ⇒ 'Q gGS nres" where
"gcollapse_impl_aux v s ≡
do {
let (A,s)=s;
i ← GS.idx_of_impl s v;
s ← collapse_impl v s;
ASSERT (i < length A);
us ← Un_set_drop_impl i A;
let A = take i A @ [us];
RETURN (A,s)
}"
term collapse
lemma gcollapse_alt:
"gcollapse v APDPE = (
let
(a,p,D,pE)=APDPE;
i=idx_of p v;
s=collapse v (p,D,pE);
us=⋃(set (drop i a));
a = take i a @ [us]
in (a,s))"
unfolding gcollapse_def gcollapse_aux_def collapse_def collapse_aux_def
by auto
thm collapse_refine
lemma gcollapse_impl_aux_refine:
assumes A: "(s', a, p, D, pE) ∈ gGS_rel"
assumes B: "(v',v)∈Id"
assumes PRE: "v∈⋃(set p)"
shows "gcollapse_impl_aux v' s'
≤ ⇓ gGS_rel (RETURN (gcollapse v (a, p, D, pE)))"
proof -
note [simp] = Let_def
from A obtain S' B' I' P' where [simp]: "s'=(a,S',B',I',P')"
and OSR: "((S',B',I',P'),(p,D,pE))∈GS_rel" and L: "length a = length B'"
and R: "⋃(set a) ⊆ {0..<num_acc}"
by (rule gGS_relE)
from B have [simp]: "v'=v" by simp
from OSR have [simp]: "GS.p_α (S',B',I',P') = p"
by (simp add: GS_rel_def br_def GS.α_def)
from OSR PRE have PRE': "v ∈ ⋃(set (GS.p_α (S',B',I',P')))"
by (simp add: GS_rel_def br_def GS.α_def)
from OSR have GS_invar: "GS_invar (S',B',I',P')"
by (simp add: GS_rel_def br_def)
term GS.B
{
fix s
assume "collapse v (p, D, pE) = (GS.p_α s, GS.D_α s, GS.pE_α s)"
hence "length (GS.B s) = Suc (idx_of p v)"
unfolding collapse_def collapse_aux_def Let_def
apply (cases s)
apply (auto simp: GS.p_α_def)
apply (drule arg_cong[where f=length])
using GS_invar.p_α_disjoint_sym[OF GS_invar]
and PRE ‹GS.p_α (S', B', I', P') = p› idx_of_props(1)[of p v]
by simp
} note AUX1 = this
show ?thesis
unfolding gcollapse_alt gcollapse_impl_aux_def
apply simp
apply (rule RETURN_as_SPEC_refine)
apply (refine_rcg
order_trans[OF GS_invar.idx_of_correct[OF GS_invar PRE']]
order_trans[OF collapse_refine[OF OSR B PRE, simplified]]
refine_vcg
)
using PRE' apply simp
apply (simp add: L)
using Un_set_drop_impl_correct acc_bound R
apply (simp add: refine_pw_simps pw_le_iff)
unfolding gGS_rel_def GS_rel_def GS.α_def br_def gGS_α_def gGS_invar_def
apply (clarsimp simp: L dest!: AUX1)
apply (auto dest!: AUX1 simp: L)
apply (force dest!: in_set_dropD) []
apply (force dest!: in_set_takeD) []
done
qed
definition gcollapse_impl :: "'Q ⇒ 'Q gGS ⇒ 'Q gGS nres"
where "gcollapse_impl v s ≡
do {
let (A,S,B,I,P)=s;
i ← GS.idx_of_impl (S,B,I,P) v;
ASSERT (i+1 ≤ length B);
let B = take (i+1) B;
ASSERT (i < length A);
us←Un_set_drop_impl i A;
let A = take i A @ [us];
RETURN (A,S,B,I,P)
}"
lemma gcollapse_impl_aux_opt_refine:
"gcollapse_impl v s ≤ gcollapse_impl_aux v s"
unfolding gcollapse_impl_def gcollapse_impl_aux_def collapse_impl_def
GS.collapse_impl_def
apply (simp add: refine_pw_simps pw_le_iff split: prod.splits)
apply blast
done
lemma gcollapse_impl_refine:
assumes A: "(s', a, p, D, pE) ∈ gGS_rel"
assumes B: "(v',v)∈Id"
assumes PRE: "v∈⋃(set p)"
shows "gcollapse_impl v' s'
≤ ⇓ gGS_rel (RETURN (gcollapse v (a, p, D, pE)))"
using order_trans[OF
gcollapse_impl_aux_opt_refine
gcollapse_impl_aux_refine[OF assms]]
.
definition ginitial_impl :: "'Q ⇒ 'Q goGS ⇒ 'Q gGS"
where "ginitial_impl v0 s0 ≡ ([acc v0],initial_impl v0 (snd s0))"
lemma ginitial_impl_refine:
assumes A: "v0∉goD s0" "go_is_no_brk s0"
assumes REL: "(s0i,s0)∈goGS_rel" "(v0i,v0)∈Id"
shows "(ginitial_impl v0i s0i,ginitial v0 s0)∈gGS_rel"
unfolding ginitial_impl_def ginitial_def
using REL initial_refine[OF A(1) _ REL(2), of "snd s0i"] A(2)
apply (auto
simp: gGS_rel_def br_def gGS_α_def gGS_invar_def goGS_rel_def goGS_α_def
simp: go_is_no_brk_def goD_def oGS_rel_def GS_rel_def goGS_invar_def
split: prod.splits
)
using acc_bound
apply (fastforce simp: initial_impl_def GS_initial_impl_def)+
done
definition gpath_is_empty_impl :: "'Q gGS ⇒ bool"
where "gpath_is_empty_impl s = path_is_empty_impl (snd s)"
lemma gpath_is_empty_refine:
"(s,(a,p,D,pE))∈gGS_rel ⟹ gpath_is_empty_impl s ⟷ p=[]"
unfolding gpath_is_empty_impl_def
using path_is_empty_refine
by (fastforce simp: gGS_rel_def br_def gGS_invar_def gGS_α_def GS.α_def)
definition gis_on_stack_impl :: "'Q ⇒ 'Q gGS ⇒ bool"
where "gis_on_stack_impl v s = is_on_stack_impl v (snd s)"
lemma gis_on_stack_refine:
"⟦(s,(a,p,D,pE))∈gGS_rel⟧ ⟹ gis_on_stack_impl v s ⟷ v∈⋃(set p)"
unfolding gis_on_stack_impl_def
using is_on_stack_refine
by (fastforce simp: gGS_rel_def br_def gGS_invar_def gGS_α_def GS.α_def)
definition gis_done_impl :: "'Q ⇒ 'Q gGS ⇒ bool"
where "gis_done_impl v s ≡ is_done_impl v (snd s)"
thm is_done_refine
lemma gis_done_refine: "(s,(a,p,D,pE))∈gGS_rel
⟹ gis_done_impl v s ⟷ (v ∈ D)"
using is_done_refine[of "(snd s)" v]
by (auto
simp: gGS_rel_def br_def gGS_α_def gGS_invar_def GS.α_def
gis_done_impl_def)
definition (in -) "on_stack_less I u v ≡
case I v of
Some (STACK j) ⇒ j<u
| _ ⇒ False"
definition (in -) "on_stack_ge I l v ≡
case I v of
Some (STACK j) ⇒ l≤j
| _ ⇒ False"
lemma (in GS_invar) set_butlast_p_refine:
assumes PRE: "p_α≠[]"
shows "Collect (on_stack_less I (last B)) = ⋃(set (butlast p_α))" (is "?L=?R")
proof (intro equalityI subsetI)
from PRE have [simp]: "B≠[]" by (auto simp: p_α_def)
have [simp]: "S≠[]"
by (simp add: empty_eq)
{
fix v
assume "v∈?L"
then obtain j where [simp]: "I v = Some (STACK j)" and "j<last B"
by (auto simp: on_stack_less_def split: option.splits node_state.splits)
from I_consistent[of v j] have [simp]: "j<length S" "v=S!j" by auto
from B0 have "B!0=0" by simp
from ‹j<last B› have "j<B!(length B - 1)" by (simp add: last_conv_nth)
from find_seg_bounds[OF ‹j<length S›] find_seg_correct[OF ‹j<length S›]
have "v∈seg (find_seg j)" "find_seg j < length B" by auto
moreover with ‹j<B!(length B - 1)› have "find_seg j < length B - 1"
proof -
have f1: "⋀x⇩1 x. ¬ (x⇩1::nat) < x⇩1 - x"
using less_imp_diff_less by blast
have "j ≤ last B"
by (metis ‹j < last B› less_le)
hence f2: "⋀x⇩1. ¬ last B < x⇩1 ∨ ¬ x⇩1 ≤ j"
using f1 by (metis diff_diff_cancel le_trans)
have "⋀x⇩1. seg_end x⇩1 ≤ j ∨ ¬ x⇩1 < find_seg j"
by (metis ‹seg_start (find_seg j) ≤ j› calculation(2)
le_trans seg_end_less_start)
thus "find_seg j < length B - 1"
using f1 f2
by (metis GS.seg_start_def ‹B ≠ []› ‹j < B ! (length B - 1)›
‹seg_start (find_seg j) ≤ j› calculation(2) diff_diff_cancel
last_conv_nth nat_neq_iff seg_start_less_end)
qed
ultimately show "v∈?R"
by (auto simp: p_α_def map_butlast[symmetric] butlast_upt)
}
{
fix v
assume "v∈?R"
then obtain i where "i<length B - 1" and "v∈seg i"
by (auto simp: p_α_def map_butlast[symmetric] butlast_upt)
then obtain j where "j < seg_end i" and "v=S!j"
by (auto simp: seg_def)
hence "j<B!(i+1)" and "i+1 ≤ length B - 1" using ‹i<length B - 1›
by (auto simp: seg_end_def last_conv_nth split: if_split_asm)
with sorted_nth_mono[OF B_sorted ‹i+1 ≤ length B - 1›] have "j<last B"
by (auto simp: last_conv_nth)
moreover from ‹j < seg_end i› have "j<length S"
by (metis GS.seg_end_def add_diff_inverse_nat ‹i + 1 ≤ length B - 1›
add_lessD1 less_imp_diff_less less_le_not_le nat_neq_iff
seg_end_bound)
with I_consistent ‹v=S!j› have "I v = Some (STACK j)" by auto
ultimately show "v∈?L"
by (auto simp: on_stack_less_def)
}
qed
lemma (in GS_invar) set_last_p_refine:
assumes PRE: "p_α≠[]"
shows "Collect (on_stack_ge I (last B)) = last p_α" (is "?L=?R")
proof (intro equalityI subsetI)
from PRE have [simp]: "B≠[]" by (auto simp: p_α_def)
have [simp]: "S≠[]" by (simp add: empty_eq)
{
fix v
assume "v∈?L"
then obtain j where [simp]: "I v = Some (STACK j)" and "j≥last B"
by (auto simp: on_stack_ge_def split: option.splits node_state.splits)
from I_consistent[of v j] have [simp]: "j<length S" "v=S!j" by auto
hence "v∈seg (length B - 1)" using ‹j≥last B›
by (auto simp: seg_def last_conv_nth seg_start_def seg_end_def)
thus "v∈last p_α" by (auto simp: p_α_def last_map)
}
{
fix v
assume "v∈?R"
hence "v∈seg (length B - 1)"
by (auto simp: p_α_def last_map)
then obtain j where "v=S!j" "j≥last B" "j<length S"
by (auto simp: seg_def last_conv_nth seg_start_def seg_end_def)
with I_consistent have "I v = Some (STACK j)" by simp
with ‹j≥last B› show "v∈?L" by (auto simp: on_stack_ge_def)
}
qed
definition ce_impl :: "'Q gGS ⇒ (('Q set × 'Q set) option × 'Q gGS) nres"
where "ce_impl s ≡
do {
let (a,S,B,I,P) = s;
ASSERT (B≠[]);
let bls = Collect (on_stack_less I (last B));
let ls = Collect (on_stack_ge I (last B));
RETURN (Some (bls, ls),a,S,B,I,P)
}"
lemma ce_impl_refine:
assumes A: "(s,(a,p,D,pE))∈gGS_rel"
assumes PRE: "p≠[]"
shows "ce_impl s ≤ ⇓(Id×⇩rgGS_rel)
(RETURN (Some (⋃(set (butlast p)),last p),a,p,D,pE))"
proof -
from A obtain S' B' I' P' where [simp]: "s=(a,S',B',I',P')"
and OSR: "((S',B',I',P'),(p,D,pE))∈GS_rel" and L: "length a = length B'"
by (rule gGS_relE)
from OSR have [simp]: "GS.p_α (S',B',I',P') = p"
by (simp add: GS_rel_def br_def GS.α_def)
from PRE have NE': "GS.p_α (S', B', I', P') ≠ []" by simp
hence BNE[simp]: "B'≠[]" by (simp add: GS.p_α_def)
from OSR have GS_invar: "GS_invar (S',B',I',P')"
by (simp add: GS_rel_def br_def)
show ?thesis
using GS_invar.set_butlast_p_refine[OF GS_invar NE']
using GS_invar.set_last_p_refine[OF GS_invar NE']
unfolding ce_impl_def
using A
by auto
qed
definition "last_is_acc_impl s ≡
do {
let (a,_)=s;
ASSERT (a≠[]);
RETURN (∀i<num_acc. i∈last a)
}"
lemma last_is_acc_impl_refine:
assumes A: "(s,(a,p,D,pE))∈gGS_rel"
assumes PRE: "a≠[]"
shows "last_is_acc_impl s ≤ RETURN (last a = {0..<num_acc})"
proof -
from A PRE have "last a ⊆ {0..<num_acc}"
unfolding gGS_rel_def gGS_invar_def br_def gGS_α_def by auto
hence C: "(∀i<num_acc. i∈last a) ⟷ (last a = {0..<num_acc})"
by auto
from A obtain gs where [simp]: "s=(a,gs)"
by (auto simp: gGS_rel_def gGS_α_def br_def split: prod.splits)
show ?thesis
unfolding last_is_acc_impl_def
by (auto simp: gGS_rel_def br_def gGS_α_def C PRE split: prod.splits)
qed
definition go_is_no_brk_impl :: "'Q goGS ⇒ bool"
where "go_is_no_brk_impl s ≡ fst s = None"
lemma go_is_no_brk_refine:
"(s,s')∈goGS_rel ⟹ go_is_no_brk_impl s ⟷ go_is_no_brk s'"
unfolding go_is_no_brk_def go_is_no_brk_impl_def
by (auto simp: goGS_rel_def br_def goGS_α_def split: prod.splits)
definition goD_impl :: "'Q goGS ⇒ 'Q oGS" where "goD_impl s ≡ snd s"
lemma goD_refine:
"go_is_no_brk s' ⟹ (s,s')∈goGS_rel ⟹ (goD_impl s, goD s')∈oGS_rel"
unfolding goD_impl_def goD_def
by (auto
simp: goGS_rel_def br_def goGS_α_def goGS_invar_def oGS_rel_def
go_is_no_brk_def)
definition go_is_done_impl :: "'Q ⇒ 'Q goGS ⇒ bool"
where "go_is_done_impl v s ≡ is_done_oimpl v (snd s)"
thm is_done_orefine
lemma go_is_done_impl_refine: "⟦go_is_no_brk s'; (s,s')∈goGS_rel; (v,v')∈Id⟧
⟹ go_is_done_impl v s ⟷ (v'∈goD s')"
using is_done_orefine
unfolding go_is_done_impl_def goD_def go_is_no_brk_def
apply (fastforce simp: goGS_rel_def br_def goGS_invar_def goGS_α_def)
done
definition goBrk_impl :: "'Q goGS ⇒ 'Q ce" where "goBrk_impl ≡ fst"
lemma goBrk_refine: "(s,s')∈goGS_rel ⟹ (goBrk_impl s, goBrk s')∈Id"
unfolding goBrk_impl_def goBrk_def
by (auto simp: goGS_rel_def br_def goGS_α_def split: prod.splits)
definition find_ce_impl :: "('Q set × 'Q set) option nres" where
"find_ce_impl ≡ do {
stat_start_nres;
let os=goinitial_impl;
os←FOREACHci (λit os. fgl_outer_invar it (goGS_α os)) V0
(go_is_no_brk_impl) (λv0 s0.
do {
if ¬go_is_done_impl v0 s0 then do {
let s = (None,ginitial_impl v0 s0);
(brk,s)←WHILEIT
(λ(brk,s). fgl_invar v0 (oGS_α (goD_impl s0)) (brk,snd (gGS_α s)))
(λ(brk,s). brk=None ∧ ¬gpath_is_empty_impl s) (λ(l,s).
do {
(vo,s) ← gselect_edge_impl s;
case vo of
Some v ⇒ do {
if gis_on_stack_impl v s then do {
s←gcollapse_impl v s;
b←last_is_acc_impl s;
if b then
ce_impl s
else
RETURN (None,s)
} else if ¬gis_done_impl v s then do {
RETURN (None,gpush_impl v s)
} else do {
RETURN (None,s)
}
}
| None ⇒ do {
s←gpop_impl s;
RETURN (None,s)
}
}) (s);
RETURN (gto_outer_impl brk s)
} else RETURN s0
}) os;
stat_stop_nres;
RETURN (goBrk_impl os)
}"
lemma find_ce_impl_refine: "find_ce_impl ≤ ⇓Id gfind_ce"
proof -
note [refine2] = prod_relI[OF IdI[of None] ginitial_impl_refine]
have [refine]: "⋀s a p D pE. ⟦
(s,(a,p,D,pE))∈gGS_rel;
p ≠ []; pE ∩ last p × UNIV = {}
⟧ ⟹
gpop_impl s ⤜ (λs. RETURN (None, s))
≤ SPEC (λc. (c, None, gpop (a,p,D,pE)) ∈ Id ×⇩r gGS_rel)"
apply (drule (2) gpop_impl_refine)
apply (fastforce simp add: pw_le_iff refine_pw_simps)
done
note [[goals_limit = 1]]
note FOREACHci_refine_rcg'[refine del]
show ?thesis
unfolding find_ce_impl_def gfind_ce_def
apply (refine_rcg
bind_refine'
prod_relI IdI
inj_on_id
gselect_edge_impl_refine gpush_impl_refine
oinitial_refine ginitial_impl_refine
bind_Let_refine2[OF gcollapse_impl_refine]
if_bind_cond_refine[OF last_is_acc_impl_refine]
ce_impl_refine
goinitial_impl_refine
gto_outer_refine
goBrk_refine
FOREACHci_refine_rcg'[where R=goGS_rel, OF inj_on_id]
)
apply refine_dref_type
apply (simp_all add: go_is_no_brk_refine go_is_done_impl_refine)
apply (auto simp: goGS_rel_def br_def) []
apply (auto simp: goGS_rel_def br_def goGS_α_def gGS_α_def gGS_rel_def
goD_def goD_impl_def) []
apply (auto dest: gpath_is_empty_refine ) []
apply (auto dest: gis_on_stack_refine) []
apply (auto dest: gis_done_refine) []
done
qed
end
section ‹Constructing a Lasso from Counterexample›
subsection ‹Lassos in GBAs›
context igb_fr_graph begin
definition reconstruct_reach :: "'Q set ⇒ 'Q set ⇒ ('Q list × 'Q) nres"
where "reconstruct_reach Vr Vl ≡ do {
res ← find_path (E∩Vr×UNIV) V0 (λv. v∈Vl);
ASSERT (res ≠ None);
RETURN (the res)
}"
lemma reconstruct_reach_correct:
assumes CEC: "ce_correct Vr Vl"
shows "reconstruct_reach Vr Vl
≤ SPEC (λ(pr,va). ∃v0∈V0. path E v0 pr va ∧ va∈Vl)"
proof -
have FIN_aux: "finite ((E ∩ Vr × UNIV)⇧* `` V0)"
by (metis finite_reachableE_V0 finite_subset inf_sup_ord(1) inf_sup_ord(2)
inf_top.left_neutral reachable_mono)
{
fix u p v
assume P: "path E u p v" and SS: "set p ⊆ Vr"
have "path (E ∩ Vr×UNIV) u p v"
apply (rule path_mono[OF _ path_restrict[OF P]])
using SS by auto
} note P_CONV=this
from CEC obtain v0 "pr" va where "v0∈V0" "set pr ⊆ Vr" "va∈Vl"
"path (E ∩ Vr×UNIV) v0 pr va"
unfolding ce_correct_def is_lasso_prpl_def is_lasso_prpl_pre_def
by (force simp: neq_Nil_conv path_simps dest: P_CONV)
hence 1: "va ∈ (E ∩ Vr × UNIV)⇧* `` V0"
by (auto dest: path_is_rtrancl)
show ?thesis
using assms unfolding reconstruct_reach_def
apply (refine_rcg refine_vcg order_trans[OF find_path_ex_rule])
apply (clarsimp_all simp: FIN_aux finite_V0)
using ‹va∈Vl› 1 apply auto []
apply (auto dest: path_mono[of "E ∩ Vr × UNIV" E, simplified]) []
done
qed
definition "rec_loop_invar Vl va s ≡ let (v,p,cS) = s in
va ∈ E⇧*``V0 ∧
path E va p v ∧
cS = acc v ∪ (⋃(acc`set p)) ∧
va ∈ Vl ∧ v ∈ Vl ∧ set p ⊆ Vl"
definition reconstruct_lasso :: "'Q set ⇒ 'Q set ⇒ ('Q list × 'Q list) nres"
where "reconstruct_lasso Vr Vl ≡ do {
(pr,va) ← reconstruct_reach Vr Vl;
let cS_full = {0..<num_acc};
let E = E ∩ UNIV×Vl;
(vd,p,_) ← WHILEIT (rec_loop_invar Vl va)
(λ(_,_,cS). cS ≠ cS_full)
(λ(v,p,cS). do {
ASSERT (∃v'. (v,v')∈E⇧* ∧ ¬ (acc v' ⊆ cS));
sr ← find_path E {v} (λv. ¬ (acc v ⊆ cS));
ASSERT (sr ≠ None);
let (p_seg,v) = the sr;
RETURN (v,p@p_seg,cS ∪ acc v)
}) (va,[],acc va);
p_close_r ← (if p=[] then
find_path1 E vd ((=) va)
else
find_path E {vd} ((=) va));
ASSERT (p_close_r ≠ None);
let (p_close,_) = the p_close_r;
RETURN (pr, p@p_close)
}"
lemma (in igb_fr_graph) reconstruct_lasso_correct:
assumes CEC: "ce_correct Vr Vl"
shows "reconstruct_lasso Vr Vl ≤ SPEC (is_lasso_prpl)"
proof -
let ?E = "E ∩ UNIV × Vl"
have E_SS: "E ∩ Vl × Vl ⊆ ?E" by auto
from CEC have
REACH: "Vl ⊆ E⇧*``V0"
and CONN: "Vl×Vl ⊆ (E ∩ Vl×Vl)⇧*"
and NONTRIV: "Vl×Vl ∩ E ≠ {}"
and NES[simp]: "Vl≠{}"
and ALL: "⋃(acc`Vl) = {0..<num_acc}"
unfolding ce_correct_def is_lasso_prpl_def
apply clarsimp_all
apply auto []
apply force
done
define term_rel
where "term_rel = (inv_image (finite_psupset {0..<num_acc}) (λ(_::'Q,_::'Q list,cS). cS))"
hence WF: "wf term_rel" by simp
{ fix va
assume "va ∈ Vl"
hence "rec_loop_invar Vl va (va, [], acc va)"
unfolding rec_loop_invar_def using REACH by auto
} note INVAR_INITIAL = this
{
fix v p cS va
assume "rec_loop_invar Vl va (v, p, cS)"
hence "finite ((?E)⇧* `` {v})"
apply -
apply (rule finite_subset[where B="E⇧*``V0"])
unfolding rec_loop_invar_def
using REACH
apply (clarsimp_all dest!: path_is_rtrancl)
apply (drule rtrancl_mono_mp[where U="?E" and V=E, rotated], (auto) [])
by (metis rev_ImageI rtrancl_trans)
} note FIN1 = this
{
fix va v :: 'Q and p cS
assume INV: "rec_loop_invar Vl va (v,p,cS)"
and NC: "cS ≠ {0..<num_acc}"
from NC INV obtain i where "i<num_acc" "i∉cS"
unfolding rec_loop_invar_def by auto blast
with ALL obtain v' where v': "v'∈Vl" "¬ acc v' ⊆ cS"
by (metis NES atLeastLessThan_iff cSUP_least in_mono zero_le)
with CONN INV have "(v,v')∈(E ∩ Vl × Vl)⇧*"
unfolding rec_loop_invar_def by auto
hence "(v,v')∈?E⇧*" using rtrancl_mono_mp[OF E_SS] by blast
with v' have "∃v'. (v,v')∈(?E)⇧* ∧ ¬ acc v' ⊆ cS" by auto
} note ASSERT1 = this
{
fix va v p cS v' p'
assume "rec_loop_invar Vl va (v, p, cS)"
and "path (?E) v p' v'"
and "¬ (acc v' ⊆ cS)"
and "∀v∈set p'. acc v ⊆ cS"
hence "rec_loop_invar Vl va (v', p@p', cS ∪ acc v')"
unfolding rec_loop_invar_def
apply simp
apply (intro conjI)
apply (auto simp: path_simps dest: path_mono[of "?E" E, simplified]) []
apply (cases p')
apply (auto simp: path_simps) [2]
apply (cases p' rule: rev_cases)
apply (auto simp: path_simps) [2]
apply (erule path_set_induct)
apply auto [2]
done
} note INV_PRES = this
{
fix va v p cS v' p'
assume "rec_loop_invar Vl va (v, p, cS)"
and "path ?E v p' v'"
and "¬ (acc v' ⊆ cS)"
and "∀v∈set p'. acc v ⊆ cS"
hence "((v', p@p', cS ∪ acc v'), (v,p,cS)) ∈ term_rel"
unfolding term_rel_def rec_loop_invar_def
by (auto simp: finite_psupset_def)
} note VAR = this
have CONN1: "Vl × Vl ⊆ (?E)⇧+"
proof clarify
fix a b
assume "a∈Vl" "b∈Vl"
from NONTRIV obtain u v where E: "(u,v)∈(E ∩ Vl×Vl)" by auto
from CONN ‹a∈Vl› E have "(a,u)∈(E∩Vl×Vl)⇧*" by auto
also note E
also (rtrancl_into_trancl1) from CONN ‹b∈Vl› E have "(v,b)∈(E∩Vl×Vl)⇧*"
by auto
finally show "(a,b)∈(?E)⇧+" using trancl_mono[OF _ E_SS] by auto
qed
{
fix va v p cS
assume "rec_loop_invar Vl va (v, p, cS)"
hence "(v,va) ∈ (?E)⇧+"
unfolding rec_loop_invar_def
using CONN1
by auto
} note CLOSE1 = this
{
fix va v p cS
assume "rec_loop_invar Vl va (v, p, cS)"
hence "(v,va) ∈ (?E)⇧*"
unfolding rec_loop_invar_def
using CONN rtrancl_mono[OF E_SS]
by auto
} note CLOSE2 = this
{
fix "pr" vd pl va v0
assume "rec_loop_invar Vl va (vd, [], {0..<num_acc})" "va ∈ Vl" "v0 ∈ V0"
"path E v0 pr va" "pl ≠ []" "path ?E vd pl va"
hence "is_lasso_prpl (pr, pl)"
unfolding is_lasso_prpl_def is_lasso_prpl_pre_def rec_loop_invar_def
by (auto simp: neq_Nil_conv path_simps
dest!: path_mono[of "?E" E, simplified]) []
} note INV_POST1 = this
{
fix va v p p' "pr" v0
assume INV: "rec_loop_invar Vl va (v,p,{0..<num_acc})"
and 1: "p≠[]" "path ?E v p' va"
and PR: "v0∈V0" "path E v0 pr va"
from INV have "∀i<num_acc. ∃q∈insert v (set p). i ∈ acc q"
unfolding rec_loop_invar_def
by auto
moreover from INV 1 have "insert v (set p) ⊆ set p ∪ set p'"
unfolding rec_loop_invar_def
apply (cases p)
apply blast
apply (cases p')
apply (auto simp: path_simps)
done
ultimately have ACC: "∀i<num_acc. ∃q∈set p ∪ set p'. i ∈ acc q" by blast
from INV 1 have PL: "path E va (p @ p') va"
by (auto simp: rec_loop_invar_def path_simps
dest!: path_mono[of "?E" E, simplified]) []
have "is_lasso_prpl (pr,p@p')"
unfolding is_lasso_prpl_def is_lasso_prpl_pre_def
apply (clarsimp simp: ACC)
using PR PL ‹p≠[]› by auto
} note INV_POST2 = this
show ?thesis
unfolding reconstruct_lasso_def
apply (refine_rcg
WF
order_trans[OF reconstruct_reach_correct]
order_trans[OF find_path_ex_rule]
order_trans[OF find_path1_ex_rule]
refine_vcg
)
apply (vc_solve
del: subsetI
solve: ASSERT1 INV_PRES asm_rl VAR CLOSE1 CLOSE2 INV_POST1 INV_POST2
simp: INVAR_INITIAL FIN1 CEC)
done
qed
definition find_lasso where "find_lasso ≡ do {
ce ← find_ce_spec;
case ce of
None ⇒ RETURN None
| Some (Vr,Vl) ⇒ do {
l ← reconstruct_lasso Vr Vl;
RETURN (Some l)
}
}"
lemma (in igb_fr_graph) find_lasso_correct: "find_lasso ≤ find_lasso_spec"
unfolding find_lasso_spec_def find_lasso_def find_ce_spec_def
apply (refine_rcg refine_vcg order_trans[OF reconstruct_lasso_correct])
apply auto
done
end
end