section‹Lasso Finding Algorithm for Generalized B\"uchi Graphs \label{sec:gbg}› theory Gabow_GBG imports
Gabow_Skeleton
CAVA_Automata.Lasso
Find_Path begin
(* TODO: convenience locale, consider merging this with invariants *) 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
― ‹Specifies a correct counter-example› where "ce_correct Vr Vl ≡ (∃pr pl. Vr ⊆ E*``V0 ∧ Vl ⊆ E*``V0 ― ‹Only reachable nodes are covered› ∧ set pr⊆Vr ∧ set pl⊆Vl ― ‹The paths are inside the specified sets› ∧ Vl×Vl ⊆ (E ∩ Vl×Vl)* ― ‹‹Vl› is mutually connected› ∧ Vl×Vl ∩ E ≠ {} ― ‹‹Vl› is non-trivial› ∧ is_lasso_prpl (pr,pl)) ― ‹Paths form a lasso› "
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
― ‹Specifies that there is no accepting cycle touching a set of nodes› 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))" ― ‹No accepting cycle over
visited edges› 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 { ― ‹Select edge from end of path› (vo,(p,D,pE)) ← select_edge (p,D,pE);
ASSERT (p≠[]); case vo of Some v ==> do { if v ∈∪(set p) then do { ― ‹Collapse› 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 { ― ‹Edge to new node. Append to path› RETURN (None,push v (p,D,pE)) } else RETURN (None,p,D,pE) } | None ==> do { ― ‹No more outgoing edges from current node on path› 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_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) alsohave"…⊆ ?Er"using lvE_ss_E by auto finally (rtrancl_mono_mp[rotated]) have"(v0,u)∈?Er*" . alsonote‹(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) finallyshow ?thesis by (rule that) fact qed thenobtain"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) case0
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 alsonote‹(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 finallyobtain pl where"pl≠[]""path (lvE ∩ last p × last p) w pl w" by (rule trancl_is_path) thus ?caseby 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 thenobtain pl1 where P1: "path (lvE ∩ last p × last p) w pl1 v" by (rule rtrancl_is_path) alsofrom cnode_connectedI ‹w∈last p›‹v∈last p› have"(v,w)∈(lvE ∩ last p × last p)*"by auto thenobtain 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 moreoverfrom IH(1) have"pl1@pl2@pl ≠ []"by simp moreoverhave"∀i'<n. ∃q∈set (pl1@pl2@pl). i'∈acc q"using IH(3) by auto moreoverhave"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 ultimatelyshow ?case apply (intro exI conjI) apply assumption+ apply (auto elim: less_SucE) done qed
} thenobtain 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]
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
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" assumesBACK: "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) moreoverhave"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) ultimatelyhave"vE p' D pE' ∩ last p' × last p' ≠ {}" unfolding p'_def pE'_defby (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" assumesBACK: "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) moreoverhave"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) ultimatelyhave"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' = {}"
― ‹Case: The loop is outside the last Cnode› 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' ≠ {}"
― ‹Case: The loop touches the last Cnode› 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" ― ‹Case: The newly pushed last cnode is on the loop› 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" ― ‹This is impossible, as @{text "u"} was on the
original path, but @{text "v"} was not› with UIL VNE show False by auto next assume"(v,v)∈lvE" ― ‹This is impossible, as all visited edges are
from touched nodes, but @{text "v"} was untouched› with vE_touched VNE show False unfolding touched_def by auto qed thus ?thesis .. next assume A: "v∉set pl"
― ‹Case: The newly pushed last cnode is not on the loop› 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 ― ‹Case: The loop does not use the new edge› 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) ― ‹Case: The loop uses the new edge› 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]
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)
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)
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"
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 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 { ― ‹Select edge from end of path› (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 { ― ‹Collapse› 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 { ― ‹Edge to new node. Append to path› RETURN (None,gpush v (a,p,D,pE)) } else RETURN (None,a,p,D,pE) } | None ==> do { ― ‹No more outgoing edges from current node on path› 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 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 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
subsubsection‹Preliminaries› definition Un_set_drop_impl :: "nat ==> 'a set list ==> 'a set nres"
― ‹Executable version of @{text "∪set (drop i A)"}, using indexing to
access @{text "A"}› 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_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 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" assumesPRE: "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" assumesPRE: "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)
fromPRE 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" assumesPRE: "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; 🍋‹ASSERT (v∈∪set (GS.p_α 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
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 PREhavePRE': "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] andPRE‹GS.p_α (S', B', I', P') = p› idx_of_props(1)[of p v] by simp
} note AUX1 = this
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" assumesPRE: "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]]
.
{ fix v assume"v∈?L" thenobtain 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 moreoverwith‹j<B!(length B - 1)›have"find_seg j < length B - 1" (* What follows is an unreadable, auto-generated structured proof thatreplacesthefollowingsmt-call:
by (smt GS.seg_start_def `seg_start (find_seg j) \<le> j`)*) proof - have f1: "∧x1 x. ¬ (x1::nat) < x1 - x" using less_imp_diff_less by blast have"j ≤ last B" by (metis ‹j < last B› less_le) hence f2: "∧x1. ¬ last B < x1∨¬ x1≤ j" using f1 by (metis diff_diff_cancel le_trans) have"∧x1. seg_end x1≤ j ∨¬ x1 < 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 ultimatelyshow"v∈?R" by (auto simp: p_α_def map_butlast[symmetric] butlast_upt)
}
{ fix v assume"v∈?R" thenobtain i where"i<length B - 1"and"v∈seg i" by (auto simp: p_α_def map_butlast[symmetric] butlast_upt) thenobtain 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) moreoverfrom‹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) (*by (smt `i < length B - 1` seg_end_bound)*) with I_consistent ‹v=S!j›have"I v = Some (STACK j)"by auto ultimatelyshow"v∈?L" by (auto simp: on_stack_less_def)
} qed
lemma (in GS_invar) set_last_p_refine: assumesPRE: "p_α≠[]" shows"Collect (on_stack_ge I (last B)) = last p_α" (is"?L=?R") proof (intro equalityI subsetI) fromPREhave [simp]: "B≠[]"by (auto simp: p_α_def)
have [simp]: "S≠[]"by (simp add: empty_eq)
{ fix v assume"v∈?L" thenobtain 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) thenobtain 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" assumesPRE: "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 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" assumesPRE: "a≠[]" shows"last_is_acc_impl s ≤ RETURN (last a = {0..<num_acc})" proof - from A PREhave"last a ⊆ {0..<num_acc}" unfolding gGS_rel_def gGS_invar_def br_def gGS_α_defby 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 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 { ― ‹Select edge from end of path› (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 { ― ‹Edge to new node. Append to path› RETURN (None,gpush_impl v s) } else do { ― ‹Edge to done node. Skip› RETURN (None,s) } } | None ==> do { ― ‹No more outgoing edges from current node on path› 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) }"
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
definition reconstruct_reach :: "'Q set ==> 'Q set ==> ('Q list × 'Q) nres"
― ‹Reconstruct the reaching path of a lasso› where"reconstruct_reach Vr Vl ≡ do { res ← find_path (E∩Vr×UNIV) V0 (λv. v∈Vl); ASSERT (res ≠ None); RETURN (the res) }"
{ 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) hence1: "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›1apply 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"
― ‹Reconstruct lasso› 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;
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
{ 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' 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 alsonote E also (rtrancl_into_trancl1) from CONN ‹b∈Vl› E have"(v,b)∈(E∩Vl×Vl)*" by auto finallyshow"(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})" and1: "p≠[]""path ?E v p' va" andPR: "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 moreoverfrom INV 1have"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 ultimatelyhave ACC: "∀i<num_acc. ∃q∈set p ∪ set p'. i ∈ acc q"by blast
from INV 1have 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) usingPR PL ‹p≠[]›by auto
} note INV_POST2 = this
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
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
