Theory CFGExit
theory CFGExit imports CFG begin
subsection ‹Adds an exit node to the abstract CFG›
locale CFGExit = CFG sourcenode targetnode kind valid_edge Entry
get_proc get_return_edges procs Main
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind"
and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" (‹'('_Entry'_')›) and get_proc :: "'node ⇒ 'pname"
and get_return_edges :: "'edge ⇒ 'edge set"
and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname" +
fixes Exit::"'node" (‹'('_Exit'_')›)
assumes Exit_source [dest]: "⟦valid_edge a; sourcenode a = (_Exit_)⟧ ⟹ False"
and get_proc_Exit:"get_proc (_Exit_) = Main"
and Exit_no_return_target:
"⟦valid_edge a; kind a = Q↩⇘p⇙f; targetnode a = (_Exit_)⟧ ⟹ False"
and Entry_Exit_edge: "∃a. valid_edge a ∧ sourcenode a = (_Entry_) ∧
targetnode a = (_Exit_) ∧ kind a = (λs. False)⇩√"
begin
lemma Entry_noteq_Exit [dest]:
assumes eq:"(_Entry_) = (_Exit_)" shows "False"
proof -
from Entry_Exit_edge obtain a where "sourcenode a = (_Entry_)"
and "valid_edge a" by blast
with eq show False by simp(erule Exit_source)
qed
lemma Exit_noteq_Entry [dest]:"(_Exit_) = (_Entry_) ⟹ False"
by(rule Entry_noteq_Exit[OF sym],simp)
lemma [simp]: "valid_node (_Entry_)"
proof -
from Entry_Exit_edge obtain a where "sourcenode a = (_Entry_)"
and "valid_edge a" by blast
thus ?thesis by(fastforce simp:valid_node_def)
qed
lemma [simp]: "valid_node (_Exit_)"
proof -
from Entry_Exit_edge obtain a where "targetnode a = (_Exit_)"
and "valid_edge a" by blast
thus ?thesis by(fastforce simp:valid_node_def)
qed
subsubsection ‹Definition of ‹method_exit››
definition method_exit :: "'node ⇒ bool"
where "method_exit n ≡ n = (_Exit_) ∨
(∃a Q p f. n = sourcenode a ∧ valid_edge a ∧ kind a = Q↩⇘p⇙f)"
lemma method_exit_cases:
"⟦method_exit n; n = (_Exit_) ⟹ P;
⋀a Q f p. ⟦n = sourcenode a; valid_edge a; kind a = Q↩⇘p⇙f⟧ ⟹ P⟧ ⟹ P"
by(fastforce simp:method_exit_def)
lemma method_exit_inner_path:
assumes "method_exit n" and "n -as→⇩ι* n'" shows "as = []"
using ‹method_exit n›
proof(rule method_exit_cases)
assume "n = (_Exit_)"
show ?thesis
proof(cases as)
case (Cons a' as')
with ‹n -as→⇩ι* n'› have "n = sourcenode a'" and "valid_edge a'"
by(auto elim:path_split_Cons simp:intra_path_def)
with ‹n = (_Exit_)› have "sourcenode a' = (_Exit_)" by simp
with ‹valid_edge a'› have False by(rule Exit_source)
thus ?thesis by simp
qed simp
next
fix a Q f p
assume "n = sourcenode a" and "valid_edge a" and "kind a = Q↩⇘p⇙f"
show ?thesis
proof(cases as)
case (Cons a' as')
with ‹n -as→⇩ι* n'› have "n = sourcenode a'" and "valid_edge a'"
and "intra_kind (kind a')"
by(auto elim:path_split_Cons simp:intra_path_def)
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› ‹valid_edge a'› ‹n = sourcenode a›
‹n = sourcenode a'› ‹intra_kind (kind a')›
have False by(fastforce dest:return_edges_only simp:intra_kind_def)
thus ?thesis by simp
qed simp
qed
subsubsection ‹Definition of ‹inner_node››
definition inner_node :: "'node ⇒ bool"
where inner_node_def:
"inner_node n ≡ valid_node n ∧ n ≠ (_Entry_) ∧ n ≠ (_Exit_)"
lemma inner_is_valid:
"inner_node n ⟹ valid_node n"
by(simp add:inner_node_def valid_node_def)
lemma [dest]:
"inner_node (_Entry_) ⟹ False"
by(simp add:inner_node_def)
lemma [dest]:
"inner_node (_Exit_) ⟹ False"
by(simp add:inner_node_def)
lemma [simp]:"⟦valid_edge a; targetnode a ≠ (_Exit_)⟧
⟹ inner_node (targetnode a)"
by(simp add:inner_node_def,rule ccontr,simp,erule Entry_target)
lemma [simp]:"⟦valid_edge a; sourcenode a ≠ (_Entry_)⟧
⟹ inner_node (sourcenode a)"
by(simp add:inner_node_def,rule ccontr,simp,erule Exit_source)
lemma valid_node_cases [consumes 1, case_names "Entry" "Exit" "inner"]:
"⟦valid_node n; n = (_Entry_) ⟹ Q; n = (_Exit_) ⟹ Q;
inner_node n ⟹ Q⟧ ⟹ Q"
apply(auto simp:valid_node_def)
apply(case_tac "sourcenode a = (_Entry_)") apply auto
apply(case_tac "targetnode a = (_Exit_)") apply auto
done
subsubsection ‹Lemmas on paths with ‹(_Exit_)››
lemma path_Exit_source:
"⟦n -as→* n'; n = (_Exit_)⟧ ⟹ n' = (_Exit_) ∧ as = []"
proof(induct rule:path.induct)
case (Cons_path n'' as n' a n)
from ‹n = (_Exit_)› ‹sourcenode a = n› ‹valid_edge a› have False
by -(rule Exit_source,simp_all)
thus ?case by simp
qed simp
lemma [dest]:"(_Exit_) -as→* n' ⟹ n' = (_Exit_) ∧ as = []"
by(fastforce elim!:path_Exit_source)
lemma Exit_no_sourcenode[dest]:
assumes isin:"(_Exit_) ∈ set (sourcenodes as)" and path:"n -as→* n'"
shows False
proof -
from isin obtain ns' ns'' where "sourcenodes as = ns'@(_Exit_)#ns''"
by(auto dest:split_list simp:sourcenodes_def)
then obtain as' as'' a where "as = as'@a#as''"
and source:"sourcenode a = (_Exit_)"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
with path have "valid_edge a" by(fastforce dest:path_split)
with source show ?thesis by -(erule Exit_source)
qed
lemma vpa_no_slpa:
"⟦valid_path_aux cs as; n -as→* n'; valid_call_list cs n; cs ≠ [];
∀xs ys. as = xs@ys ⟶ (¬ same_level_path_aux cs xs ∨ upd_cs cs xs ≠ [])⟧
⟹ ∃a Q r fs. valid_edge a ∧ kind a = Q:r↪⇘get_proc n'⇙fs"
proof(induct arbitrary:n rule:vpa_induct)
case (vpa_empty cs)
from ‹valid_call_list cs n› ‹cs ≠ []› obtain Q r fs where "valid_edge (hd cs)"
and "kind (hd cs) = Q:r↪⇘get_proc n⇙fs"
apply(unfold valid_call_list_def)
apply(drule hd_Cons_tl[THEN sym])
apply(erule_tac x="[]" in allE)
apply(erule_tac x="hd cs" in allE)
by auto
from ‹n -[]→* n'› have "n = n'" by fastforce
with ‹valid_edge (hd cs)› ‹kind (hd cs) = Q:r↪⇘get_proc n⇙fs› show ?case by blast
next
case (vpa_intra cs a as)
note IH = ‹⋀n. ⟦n -as→* n'; valid_call_list cs n; cs ≠ [];
∀xs ys. as = xs@ys ⟶ ¬ same_level_path_aux cs xs ∨ upd_cs cs xs ≠ []⟧
⟹ ∃a' Q' r' fs'. valid_edge a' ∧ kind a' = Q':r'↪⇘get_proc n'⇙fs'›
note all = ‹∀xs ys. a#as = xs@ys
⟶ ¬ same_level_path_aux cs xs ∨ upd_cs cs xs ≠ []›
from ‹n -a#as→* n'› have "sourcenode a = n" and "valid_edge a"
and "targetnode a -as→* n'"
by(auto intro:path_split_Cons)
from ‹valid_call_list cs n› ‹cs ≠ []› obtain Q r fs where "valid_edge (hd cs)"
and "kind (hd cs) = Q:r↪⇘get_proc n⇙fs"
apply(unfold valid_call_list_def)
apply(drule hd_Cons_tl[THEN sym])
apply(erule_tac x="[]" in allE)
apply(erule_tac x="hd cs" in allE)
by auto
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
with ‹kind (hd cs) = Q:r↪⇘get_proc n⇙fs› ‹sourcenode a = n›
have "kind (hd cs) = Q:r↪⇘get_proc (targetnode a)⇙fs" by simp
from ‹valid_call_list cs n› ‹sourcenode a = n›
‹get_proc (sourcenode a) = get_proc (targetnode a)›
have "valid_call_list cs (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(erule_tac x="cs'" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split)
from all ‹intra_kind (kind a)›
have "∀xs ys. as = xs@ys ⟶ ¬ same_level_path_aux cs xs ∨ upd_cs cs xs ≠ []"
apply clarsimp apply(erule_tac x="a#xs" in allE)
by(auto simp:intra_kind_def)
from IH[OF ‹targetnode a -as→* n'› ‹valid_call_list cs (targetnode a)›
‹cs ≠ []› this] show ?case .
next
case (vpa_Call cs a as Q r p fs)
note IH = ‹⋀n. ⟦n -as→* n'; valid_call_list (a#cs) n; a#cs ≠ [];
∀xs ys. as = xs@ys ⟶ ¬ same_level_path_aux (a#cs) xs ∨ upd_cs (a#cs) xs ≠ []⟧
⟹ ∃a' Q' r' fs'. valid_edge a' ∧ kind a' = Q':r'↪⇘get_proc n'⇙fs'›
note all = ‹∀xs ys.
a#as = xs@ys ⟶ ¬ same_level_path_aux cs xs ∨ upd_cs cs xs ≠ []›
from ‹n -a#as→* n'› have "sourcenode a = n" and "valid_edge a"
and "targetnode a -as→* n'"
by(auto intro:path_split_Cons)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
by(rule get_proc_call)
with ‹kind a = Q:r↪⇘p⇙fs› have "kind a = Q:r↪⇘get_proc (targetnode a)⇙fs" by simp
with ‹valid_call_list cs n› ‹valid_edge a› ‹sourcenode a = n›
have "valid_call_list (a#cs) (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split simp:sourcenodes_def)
from all ‹kind a = Q:r↪⇘p⇙fs›
have "∀xs ys. as = xs@ys
⟶ ¬ same_level_path_aux (a#cs) xs ∨ upd_cs (a#cs) xs ≠ []"
apply clarsimp apply(erule_tac x="a#xs" in allE)
by auto
from IH[OF ‹targetnode a -as→* n'› ‹valid_call_list (a#cs) (targetnode a)›
_ this] show ?case by simp
next
case (vpa_ReturnEmpty cs a as Q p fx)
from ‹cs ≠ []› ‹cs = []› have False by simp
thus ?case by simp
next
case (vpa_ReturnCons cs a as Q p f c' cs')
note IH = ‹⋀n. ⟦n -as→* n'; valid_call_list cs' n; cs' ≠ [];
∀xs ys. as = xs@ys ⟶ ¬ same_level_path_aux cs' xs ∨ upd_cs cs' xs ≠ []⟧
⟹ ∃a' Q' r' fs'. valid_edge a' ∧ kind a' = Q':r'↪⇘get_proc n'⇙fs'›
note all = ‹∀xs ys. a#as = xs@ys
⟶ ¬ same_level_path_aux cs xs ∨ upd_cs cs xs ≠ []›
from ‹n -a#as→* n'› have "sourcenode a = n" and "valid_edge a"
and "targetnode a -as→* n'"
by(auto intro:path_split_Cons)
from ‹valid_call_list cs n› ‹cs = c'#cs'› have "valid_edge c'"
apply(clarsimp simp:valid_call_list_def)
apply(erule_tac x="[]" in allE)
by auto
show ?case
proof(cases "cs' = []")
case True
with all ‹cs = c'#cs'› ‹kind a = Q↩⇘p⇙f› ‹a ∈ get_return_edges c'› have False
by(erule_tac x="[a]" in allE,fastforce)
thus ?thesis by simp
next
case False
with ‹valid_call_list cs n› ‹cs = c'#cs'›
have "valid_call_list cs' (sourcenode c')"
apply(clarsimp simp:valid_call_list_def)
apply(hypsubst_thin)
apply(erule_tac x="c'#cs'" in allE)
apply(auto simp:sourcenodes_def)
apply(case_tac cs') apply auto
apply(case_tac list) apply(auto simp:sourcenodes_def)
done
from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
have "get_proc (sourcenode c') = get_proc (targetnode a)"
by(rule get_proc_get_return_edge)
with ‹valid_call_list cs' (sourcenode c')›
have "valid_call_list cs' (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(hypsubst_thin)
apply(erule_tac x="cs'" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split)
from all ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹a ∈ get_return_edges c'›
have "∀xs ys. as = xs@ys ⟶ ¬ same_level_path_aux cs' xs ∨ upd_cs cs' xs ≠ []"
apply clarsimp apply(erule_tac x="a#xs" in allE)
by auto
from IH[OF ‹targetnode a -as→* n'› ‹valid_call_list cs' (targetnode a)›
False this] show ?thesis .
qed
qed
lemma valid_Exit_path_cases:
assumes "n -as→⇩√* (_Exit_)" and "as ≠ []"
shows "(∃a' as'. as = a'#as' ∧ intra_kind(kind a')) ∨
(∃a' as' Q p f. as = a'#as' ∧ kind a' = Q↩⇘p⇙f) ∨
(∃as' as'' n'. as = as'@as'' ∧ as' ≠ [] ∧ n -as'→⇘sl⇙* n')"
proof -
from ‹as ≠ []› obtain a' as' where "as = a'#as'" by(cases as) auto
thus ?thesis
proof(cases "kind a'" rule:edge_kind_cases)
case Intra with ‹as = a'#as'› show ?thesis by simp
next
case Return with ‹as = a'#as'› show ?thesis by simp
next
case (Call Q r p f)
from ‹n -as→⇩√* (_Exit_)› have "n -as→* (_Exit_)" and "valid_path_aux [] as"
by(simp_all add:vp_def valid_path_def)
from ‹n -as→* (_Exit_)› ‹as = a'#as'›
have "sourcenode a' = n" and "valid_edge a'" and "targetnode a' -as'→* (_Exit_)"
by(auto intro:path_split_Cons)
from ‹valid_path_aux [] as› ‹as = a'#as'› Call
have "valid_path_aux [a'] as'" by simp
from ‹valid_edge a'› Call
have "valid_call_list [a'] (targetnode a')"
apply(clarsimp simp:valid_call_list_def)
apply(case_tac cs')
by(auto intro:get_proc_call[THEN sym])
show ?thesis
proof(cases "∀xs ys. as' = xs@ys ⟶
(¬ same_level_path_aux [a'] xs ∨ upd_cs [a'] xs ≠ [])")
case True
with ‹valid_path_aux [a'] as'› ‹targetnode a' -as'→* (_Exit_)›
‹valid_call_list [a'] (targetnode a')›
obtain ax Qx rx fsx where "valid_edge ax" and "kind ax = Qx:rx↪⇘get_proc (_Exit_)⇙fsx"
by(fastforce dest!:vpa_no_slpa)
hence False by(fastforce intro:Main_no_call_target simp:get_proc_Exit)
thus ?thesis by simp
next
case False
then obtain xs ys where "as' = xs@ys" and "same_level_path_aux [a'] xs"
and "upd_cs [a'] xs = []" by auto
with Call have "same_level_path (a'#xs)" by(simp add:same_level_path_def)
from ‹upd_cs [a'] xs = []› have "xs ≠ []" by auto
with ‹targetnode a' -as'→* (_Exit_)› ‹as' = xs@ys›
have "targetnode a' -xs→* last(targetnodes xs)"
apply(cases xs rule:rev_cases)
by(auto intro:path_Append path_split path_edge simp:targetnodes_def)
with ‹sourcenode a' = n› ‹valid_edge a'› ‹same_level_path (a'#xs)›
have "n -a'#xs→⇘sl⇙* last(targetnodes xs)"
by(fastforce intro:Cons_path simp:slp_def)
with ‹as = a'#as'› ‹as' = xs@ys› Call
have "∃as' as'' n'. as = as'@as'' ∧ as' ≠ [] ∧ n -as'→⇘sl⇙* n'"
by(rule_tac x="a'#xs" in exI) auto
thus ?thesis by simp
qed
qed
qed
lemma valid_Exit_path_descending_path:
assumes "n -as→⇩√* (_Exit_)"
obtains as' where "n -as'→⇩√* (_Exit_)"
and "set(sourcenodes as') ⊆ set(sourcenodes as)"
and "∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f)"
proof(atomize_elim)
from ‹n -as→⇩√* (_Exit_)›
show "∃as'. n -as'→⇩√* (_Exit_) ∧ set(sourcenodes as') ⊆ set(sourcenodes as)∧
(∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f))"
proof(induct as arbitrary:n rule:length_induct)
fix as n
assume IH:"∀as''. length as'' < length as ⟶
(∀n'. n' -as''→⇩√* (_Exit_) ⟶
(∃as'. n' -as'→⇩√* (_Exit_) ∧ set (sourcenodes as') ⊆ set (sourcenodes as'') ∧
(∀a'∈set as'. intra_kind (kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f))))"
and "n -as→⇩√* (_Exit_)"
show "∃as'. n -as'→⇩√* (_Exit_) ∧ set(sourcenodes as') ⊆ set(sourcenodes as)∧
(∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f))"
proof(cases "as = []")
case True
with ‹n -as→⇩√* (_Exit_)› show ?thesis by(fastforce simp:sourcenodes_def vp_def)
next
case False
with ‹n -as→⇩√* (_Exit_)›
have "((∃a' as'. as = a'#as' ∧ intra_kind(kind a')) ∨
(∃a' as' Q p f. as = a'#as' ∧ kind a' = Q↩⇘p⇙f)) ∨
(∃as' as'' n'. as = as'@as'' ∧ as' ≠ [] ∧ n -as'→⇘sl⇙* n')"
by(auto dest!:valid_Exit_path_cases)
thus ?thesis apply -
proof(erule disjE)+
assume "∃a' as'. as = a'#as' ∧ intra_kind(kind a')"
then obtain a' as' where "as = a'#as'" and "intra_kind(kind a')" by blast
from ‹n -as→⇩√* (_Exit_)› ‹as = a'#as'›
have "sourcenode a' = n" and "valid_edge a'"
and "targetnode a' -as'→⇩√* (_Exit_)"
by(auto intro:vp_split_Cons)
from ‹valid_edge a'› ‹intra_kind(kind a')›
have "sourcenode a' -[a']→⇘sl⇙* targetnode a'"
by(fastforce intro:path_edge intras_same_level_path simp:slp_def)
from IH ‹targetnode a' -as'→⇩√* (_Exit_)› ‹as = a'#as'›
obtain xs where "targetnode a' -xs→⇩√* (_Exit_)"
and "set (sourcenodes xs) ⊆ set (sourcenodes as')"
and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f)"
apply(erule_tac x="as'" in allE) by auto
from ‹sourcenode a' -[a']→⇘sl⇙* targetnode a'› ‹targetnode a' -xs→⇩√* (_Exit_)›
have "sourcenode a' -[a']@xs→⇩√* (_Exit_)" by(rule slp_vp_Append)
with ‹sourcenode a' = n› have "n -a'#xs→⇩√* (_Exit_)" by simp
moreover
from ‹set (sourcenodes xs) ⊆ set (sourcenodes as')› ‹as = a'#as'›
have "set (sourcenodes (a'#xs)) ⊆ set (sourcenodes as)"
by(auto simp:sourcenodes_def)
moreover
from ‹∀a'∈set xs. intra_kind (kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f)›
‹intra_kind(kind a')›
have "∀a'∈set (a'#xs). intra_kind (kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f)"
by fastforce
ultimately show ?thesis by blast
next
assume "∃a' as' Q p f. as = a'#as' ∧ kind a' = Q↩⇘p⇙f"
then obtain a' as' Q p f where "as = a'#as'" and "kind a' = Q↩⇘p⇙f" by blast
from ‹n -as→⇩√* (_Exit_)› ‹as = a'#as'›
have "sourcenode a' = n" and "valid_edge a'"
and "targetnode a' -as'→⇩√* (_Exit_)"
by(auto intro:vp_split_Cons)
from IH ‹targetnode a' -as'→⇩√* (_Exit_)› ‹as = a'#as'›
obtain xs where "targetnode a' -xs→⇩√* (_Exit_)"
and "set (sourcenodes xs) ⊆ set (sourcenodes as')"
and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f)"
apply(erule_tac x="as'" in allE) by auto
from ‹sourcenode a' = n› ‹valid_edge a'› ‹kind a' = Q↩⇘p⇙f›
‹targetnode a' -xs→⇩√* (_Exit_)›
have "n -a'#xs→⇩√* (_Exit_)"
by(fastforce intro:Cons_path simp:vp_def valid_path_def)
moreover
from ‹set (sourcenodes xs) ⊆ set (sourcenodes as')› ‹as = a'#as'›
have "set (sourcenodes (a'#xs)) ⊆ set (sourcenodes as)"
by(auto simp:sourcenodes_def)
moreover
from ‹∀a'∈set xs. intra_kind (kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f)›
‹kind a' = Q↩⇘p⇙f›
have "∀a'∈set (a'#xs). intra_kind (kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f)"
by fastforce
ultimately show ?thesis by blast
next
assume "∃as' as'' n'. as = as'@as'' ∧ as' ≠ [] ∧ n -as'→⇘sl⇙* n'"
then obtain as' as'' n' where "as = as'@as''" and "as' ≠ []"
and "n -as'→⇘sl⇙* n'" by blast
from ‹n -as→⇩√* (_Exit_)› ‹as = as'@as''› ‹as' ≠ []›
have "last(targetnodes as') -as''→⇩√* (_Exit_)"
by(cases as' rule:rev_cases,auto intro:vp_split simp:targetnodes_def)
from ‹n -as'→⇘sl⇙* n'› ‹as' ≠ []› have "last(targetnodes as') = n'"
by(fastforce intro:path_targetnode simp:slp_def)
from ‹as = as'@as''› ‹as' ≠ []› have "length as'' < length as" by simp
with IH ‹last(targetnodes as') -as''→⇩√* (_Exit_)›
‹last(targetnodes as') = n'›
obtain xs where "n' -xs→⇩√* (_Exit_)"
and "set (sourcenodes xs) ⊆ set (sourcenodes as'')"
and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f)"
apply(erule_tac x="as''" in allE) by auto
from ‹n -as'→⇘sl⇙* n'› obtain ys where "n -ys→⇩ι* n'"
and "set(sourcenodes ys) ⊆ set(sourcenodes as')"
by(erule same_level_path_inner_path)
from ‹n -ys→⇩ι* n'› ‹n' -xs→⇩√* (_Exit_)› have "n -ys@xs→⇩√* (_Exit_)"
by(fastforce intro:slp_vp_Append intra_path_slp)
moreover
from ‹set (sourcenodes xs) ⊆ set (sourcenodes as'')›
‹set(sourcenodes ys) ⊆ set(sourcenodes as')› ‹as = as'@as''›
have "set (sourcenodes (ys@xs)) ⊆ set(sourcenodes as)"
by(auto simp:sourcenodes_def)
moreover
from ‹∀a'∈set xs. intra_kind (kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f)›
‹n -ys→⇩ι* n'›
have "∀a'∈set (ys@xs). intra_kind (kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f)"
by(fastforce simp:intra_path_def)
ultimately show ?thesis by blast
qed
qed
qed
qed
lemma valid_Exit_path_intra_path:
assumes "n -as→⇩√* (_Exit_)"
obtains as' pex where "n -as'→⇩ι* pex" and "method_exit pex"
and "set(sourcenodes as') ⊆ set(sourcenodes as)"
proof(atomize_elim)
from ‹n -as→⇩√* (_Exit_)›
obtain as' where "n -as'→⇩√* (_Exit_)"
and "set(sourcenodes as') ⊆ set(sourcenodes as)"
and all:"∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q f p. kind a' = Q↩⇘p⇙f)"
by(erule valid_Exit_path_descending_path)
show "∃as' pex. n -as'→⇩ι* pex ∧ method_exit pex ∧
set(sourcenodes as') ⊆ set(sourcenodes as)"
proof(cases "∃a' ∈ set as'. ∃Q f p. kind a' = Q↩⇘p⇙f")
case True
then obtain asx ax asx' where [simp]:"as' = asx@ax#asx'"
and "∃Q f p. kind ax = Q↩⇘p⇙f" and "∀a' ∈ set asx. ¬ (∃Q f p. kind a' = Q↩⇘p⇙f)"
by(erule split_list_first_propE)
with all have "∀a' ∈ set asx. intra_kind(kind a')" by auto
from ‹n -as'→⇩√* (_Exit_)› have "n -asx→* sourcenode ax"
and "valid_edge ax" by(auto elim:path_split simp:vp_def)
from ‹n -asx→* sourcenode ax› ‹∀a' ∈ set asx. intra_kind(kind a')›
have "n -asx→⇩ι* sourcenode ax" by(simp add:intra_path_def)
moreover
from ‹valid_edge ax› ‹∃Q f p. kind ax = Q↩⇘p⇙f›
have "method_exit (sourcenode ax)" by(fastforce simp:method_exit_def)
moreover
from ‹set(sourcenodes as') ⊆ set(sourcenodes as)›
have "set(sourcenodes asx) ⊆ set(sourcenodes as)" by(simp add:sourcenodes_def)
ultimately show ?thesis by blast
next
case False
with all ‹n -as'→⇩√* (_Exit_)› have "n -as'→⇩ι* (_Exit_)"
by(fastforce simp:vp_def intra_path_def)
moreover have "method_exit (_Exit_)" by(simp add:method_exit_def)
ultimately show ?thesis using ‹set(sourcenodes as') ⊆ set(sourcenodes as)›
by blast
qed
qed
end
end