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\<hookleftarrow>⇘p⇙f; targetnode a = (_Exit_)|] ==> False"
and Entry_Exit_edge: "∃a. valid_edge a ∧ sourcenode a = (_Entry_) ∧
targetnode a = (_Exit_) ∧ kind a = (λs. False)⇣\<surd>"
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 @{text 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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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 @{text 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 @{text "(_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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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'\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘get_proc n⇙fs` `sourcenode a = n`
have "kind (hd cs) = Q:r\<hookrightarrow>⇘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'\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs` have "get_proc (targetnode a) = p"
by(rule get_proc_call)
with `kind a = Q:r\<hookrightarrow>⇘p⇙fs` have "kind a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘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'\<hookrightarrow>⇘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\<hookleftarrow>⇘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(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(erule_tac x="cs'" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split)
from all `kind a = Q\<hookleftarrow>⇘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->⇣\<surd>* (_Exit_)" and "as ≠ []"
shows "(∃a' as'. as = a'#as' ∧ intra_kind(kind a')) ∨
(∃a' as' Q p f. as = a'#as' ∧ kind a' = Q\<hookleftarrow>⇘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->⇣\<surd>* (_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\<hookrightarrow>⇘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->⇣\<surd>* (_Exit_)"
obtains as' where "n -as'->⇣\<surd>* (_Exit_)"
and "set(sourcenodes as') ⊆ set(sourcenodes as)"
and "∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q f p. kind a' = Q\<hookleftarrow>⇘p⇙f)"
proof(atomize_elim)
from `n -as->⇣\<surd>* (_Exit_)`
show "∃as'. n -as'->⇣\<surd>* (_Exit_) ∧ set(sourcenodes as') ⊆ set(sourcenodes as)∧
(∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q f p. kind a' = Q\<hookleftarrow>⇘p⇙f))"
proof(induct as arbitrary:n rule:length_induct)
fix as n
assume IH:"∀as''. length as'' < length as -->
(∀n'. n' -as''->⇣\<surd>* (_Exit_) -->
(∃as'. n' -as'->⇣\<surd>* (_Exit_) ∧ set (sourcenodes as') ⊆ set (sourcenodes as'') ∧
(∀a'∈set as'. intra_kind (kind a') ∨ (∃Q f p. kind a' = Q\<hookleftarrow>⇘p⇙f))))"
and "n -as->⇣\<surd>* (_Exit_)"
show "∃as'. n -as'->⇣\<surd>* (_Exit_) ∧ set(sourcenodes as') ⊆ set(sourcenodes as)∧
(∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q f p. kind a' = Q\<hookleftarrow>⇘p⇙f))"
proof(cases "as = []")
case True
with `n -as->⇣\<surd>* (_Exit_)` show ?thesis by(fastforce simp:sourcenodes_def vp_def)
next
case False
with `n -as->⇣\<surd>* (_Exit_)`
have "((∃a' as'. as = a'#as' ∧ intra_kind(kind a')) ∨
(∃a' as' Q p f. as = a'#as' ∧ kind a' = Q\<hookleftarrow>⇘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->⇣\<surd>* (_Exit_)` `as = a'#as'`
have "sourcenode a' = n" and "valid_edge a'"
and "targetnode a' -as'->⇣\<surd>* (_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'->⇣\<surd>* (_Exit_)` `as = a'#as'`
obtain xs where "targetnode a' -xs->⇣\<surd>* (_Exit_)"
and "set (sourcenodes xs) ⊆ set (sourcenodes as')"
and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q f p. kind a' = Q\<hookleftarrow>⇘p⇙f)"
apply(erule_tac x="as'" in allE) by auto
from `sourcenode a' -[a']->⇘sl⇙* targetnode a'` `targetnode a' -xs->⇣\<surd>* (_Exit_)`
have "sourcenode a' -[a']@xs->⇣\<surd>* (_Exit_)" by(rule slp_vp_Append)
with `sourcenode a' = n` have "n -a'#xs->⇣\<surd>* (_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\<hookleftarrow>⇘p⇙f)`
`intra_kind(kind a')`
have "∀a'∈set (a'#xs). intra_kind (kind a') ∨ (∃Q f p. kind a' = Q\<hookleftarrow>⇘p⇙f)"
by fastforce
ultimately show ?thesis by blast
next
assume "∃a' as' Q p f. as = a'#as' ∧ kind a' = Q\<hookleftarrow>⇘p⇙f"
then obtain a' as' Q p f where "as = a'#as'" and "kind a' = Q\<hookleftarrow>⇘p⇙f" by blast
from `n -as->⇣\<surd>* (_Exit_)` `as = a'#as'`
have "sourcenode a' = n" and "valid_edge a'"
and "targetnode a' -as'->⇣\<surd>* (_Exit_)"
by(auto intro:vp_split_Cons)
from IH `targetnode a' -as'->⇣\<surd>* (_Exit_)` `as = a'#as'`
obtain xs where "targetnode a' -xs->⇣\<surd>* (_Exit_)"
and "set (sourcenodes xs) ⊆ set (sourcenodes as')"
and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q f p. kind a' = Q\<hookleftarrow>⇘p⇙f)"
apply(erule_tac x="as'" in allE) by auto
from `sourcenode a' = n` `valid_edge a'` `kind a' = Q\<hookleftarrow>⇘p⇙f`
`targetnode a' -xs->⇣\<surd>* (_Exit_)`
have "n -a'#xs->⇣\<surd>* (_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\<hookleftarrow>⇘p⇙f)`
`kind a' = Q\<hookleftarrow>⇘p⇙f`
have "∀a'∈set (a'#xs). intra_kind (kind a') ∨ (∃Q f p. kind a' = Q\<hookleftarrow>⇘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->⇣\<surd>* (_Exit_)` `as = as'@as''` `as' ≠ []`
have "last(targetnodes as') -as''->⇣\<surd>* (_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''->⇣\<surd>* (_Exit_)`
`last(targetnodes as') = n'`
obtain xs where "n' -xs->⇣\<surd>* (_Exit_)"
and "set (sourcenodes xs) ⊆ set (sourcenodes as'')"
and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q f p. kind a' = Q\<hookleftarrow>⇘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->⇣\<surd>* (_Exit_)` have "n -ys@xs->⇣\<surd>* (_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\<hookleftarrow>⇘p⇙f)`
`n -ys->⇣ι* n'`
have "∀a'∈set (ys@xs). intra_kind (kind a') ∨ (∃Q f p. kind a' = Q\<hookleftarrow>⇘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->⇣\<surd>* (_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->⇣\<surd>* (_Exit_)`
obtain as' where "n -as'->⇣\<surd>* (_Exit_)"
and "set(sourcenodes as') ⊆ set(sourcenodes as)"
and all:"∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q f p. kind a' = Q\<hookleftarrow>⇘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\<hookleftarrow>⇘p⇙f")
case True
then obtain asx ax asx' where [simp]:"as' = asx@ax#asx'"
and "∃Q f p. kind ax = Q\<hookleftarrow>⇘p⇙f" and "∀a' ∈ set asx. ¬ (∃Q f p. kind a' = Q\<hookleftarrow>⇘p⇙f)"
by(erule split_list_first_propE)
with all have "∀a' ∈ set asx. intra_kind(kind a')" by auto
from `n -as'->⇣\<surd>* (_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\<hookleftarrow>⇘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'->⇣\<surd>* (_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