# Theory SDG

```section ‹SDG›

theory SDG imports CFGExit_wf Postdomination begin

subsection ‹The nodes of the SDG›

datatype 'node SDG_node =
CFG_node 'node
| Formal_in  "'node × nat"
| Formal_out "'node × nat"
| Actual_in  "'node × nat"
| Actual_out "'node × nat"

fun parent_node :: "'node SDG_node ⇒ 'node"
where "parent_node (CFG_node n) = n"
| "parent_node (Formal_in (m,x)) = m"
| "parent_node (Formal_out (m,x)) = m"
| "parent_node (Actual_in (m,x)) = m"
| "parent_node (Actual_out (m,x)) = m"

locale SDG = CFGExit_wf sourcenode targetnode kind valid_edge Entry
get_proc get_return_edges procs Main Exit Def Use ParamDefs ParamUses +
Postdomination sourcenode targetnode kind valid_edge Entry
get_proc get_return_edges procs Main Exit
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"
and Exit::"'node"  ("'('_Exit'_')")
and Def :: "'node ⇒ 'var set" and Use :: "'node ⇒ 'var set"
and ParamDefs :: "'node ⇒ 'var list" and ParamUses :: "'node ⇒ 'var set list"

begin

fun valid_SDG_node :: "'node SDG_node ⇒ bool"
where "valid_SDG_node (CFG_node n) ⟷ valid_node n"
| "valid_SDG_node (Formal_in (m,x)) ⟷
(∃a Q r p fs ins outs. valid_edge a ∧ (kind a = Q:r↪⇘p⇙fs) ∧ targetnode a = m ∧
(p,ins,outs) ∈ set procs ∧ x < length ins)"
| "valid_SDG_node (Formal_out (m,x)) ⟷
(∃a Q p f ins outs. valid_edge a ∧ (kind a = Q↩⇘p⇙f) ∧ sourcenode a = m ∧
(p,ins,outs) ∈ set procs ∧ x < length outs)"
| "valid_SDG_node (Actual_in (m,x)) ⟷
(∃a Q r p fs ins outs. valid_edge a ∧ (kind a = Q:r↪⇘p⇙fs) ∧ sourcenode a = m ∧
(p,ins,outs) ∈ set procs ∧ x < length ins)"
| "valid_SDG_node (Actual_out (m,x)) ⟷
(∃a Q p f ins outs. valid_edge a ∧ (kind a = Q↩⇘p⇙f) ∧ targetnode a = m ∧
(p,ins,outs) ∈ set procs ∧ x < length outs)"

lemma valid_SDG_CFG_node:
"valid_SDG_node n ⟹ valid_node (parent_node n)"
by(cases n) auto

lemma Formal_in_parent_det:
assumes "valid_SDG_node (Formal_in (m,x))" and "valid_SDG_node (Formal_in (m',x'))"
and "get_proc m = get_proc m'"
shows "m = m'"
proof -
from ‹valid_SDG_node (Formal_in (m,x))› obtain a Q r p fs ins outs
where "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "targetnode a = m"
and "(p,ins,outs) ∈ set procs" and "x < length ins" by fastforce
from ‹valid_SDG_node (Formal_in (m',x'))› obtain a' Q' r' p' f' ins' outs'
where "valid_edge a'" and "kind a' = Q':r'↪⇘p'⇙f'" and "targetnode a' = m'"
and "(p',ins',outs') ∈ set procs" and "x' < length ins'" by fastforce
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹targetnode a = m›
have "get_proc m = p" by(fastforce intro:get_proc_call)
moreover
from ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p'⇙f'› ‹targetnode a' = m'›
have "get_proc m' = p'" by(fastforce intro:get_proc_call)
ultimately have "p = p'" using ‹get_proc m = get_proc m'› by simp
with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p'⇙f'›
‹targetnode a = m› ‹targetnode a' = m'›
show ?thesis by(fastforce intro:same_proc_call_unique_target)
qed

lemma valid_SDG_node_parent_Entry:
assumes "valid_SDG_node n" and "parent_node n = (_Entry_)"
shows "n = CFG_node (_Entry_)"
proof(cases n)
case CFG_node with ‹parent_node n = (_Entry_)› show ?thesis by simp
next
case (Formal_in z)
with ‹parent_node n = (_Entry_)› obtain x
where [simp]:"z = ((_Entry_),x)" by(cases z) auto
with ‹valid_SDG_node n› Formal_in obtain a where "valid_edge a"
and "targetnode a = (_Entry_)" by auto
hence False by -(rule Entry_target,simp+)
thus ?thesis by simp
next
case (Formal_out z)
with ‹parent_node n = (_Entry_)› obtain x
where [simp]:"z = ((_Entry_),x)" by(cases z) auto
with ‹valid_SDG_node n› Formal_out obtain a Q p f where "valid_edge a"
and "kind a = Q↩⇘p⇙f" and  "sourcenode a = (_Entry_)" by auto
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "get_proc (sourcenode a) = p"
by(rule get_proc_return)
with ‹sourcenode a = (_Entry_)› have "p = Main"
by(auto simp:get_proc_Entry)
with ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have False
by(fastforce intro:Main_no_return_source)
thus ?thesis by simp
next
case (Actual_in z)
with ‹parent_node n = (_Entry_)› obtain x
where [simp]:"z = ((_Entry_),x)" by(cases z) auto
with ‹valid_SDG_node n› Actual_in obtain a Q r p fs where "valid_edge a"
and "kind a = Q:r↪⇘p⇙fs" and "sourcenode a = (_Entry_)" by fastforce
hence False by -(rule Entry_no_call_source,auto)
thus ?thesis by simp
next
case (Actual_out z)
with ‹parent_node n = (_Entry_)› obtain x
where [simp]:"z = ((_Entry_),x)" by(cases z) auto
with ‹valid_SDG_node n› Actual_out obtain a where "valid_edge a"
"targetnode a = (_Entry_)" by auto
hence False by -(rule Entry_target,simp+)
thus ?thesis by simp
qed

lemma valid_SDG_node_parent_Exit:
assumes "valid_SDG_node n" and "parent_node n = (_Exit_)"
shows "n = CFG_node (_Exit_)"
proof(cases n)
case CFG_node with ‹parent_node n = (_Exit_)› show ?thesis by simp
next
case (Formal_in z)
with ‹parent_node n = (_Exit_)› obtain x
where [simp]:"z = ((_Exit_),x)" by(cases z) auto
with ‹valid_SDG_node n› Formal_in obtain a Q r p fs where "valid_edge a"
and "kind a = Q:r↪⇘p⇙fs" and "targetnode a = (_Exit_)" by fastforce
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
by(rule get_proc_call)
with ‹targetnode a = (_Exit_)› have "p = Main"
by(auto simp:get_proc_Exit)
with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have False
by(fastforce intro:Main_no_call_target)
thus ?thesis by simp
next
case (Formal_out z)
with ‹parent_node n = (_Exit_)› obtain x
where [simp]:"z = ((_Exit_),x)" by(cases z) auto
with ‹valid_SDG_node n› Formal_out obtain a where "valid_edge a"
and "sourcenode a = (_Exit_)" by auto
hence False by -(rule Exit_source,simp+)
thus ?thesis by simp
next
case (Actual_in z)
with ‹parent_node n = (_Exit_)› obtain x
where [simp]:"z = ((_Exit_),x)" by(cases z) auto
with ‹valid_SDG_node n› Actual_in obtain a where "valid_edge a"
and "sourcenode a = (_Exit_)" by auto
hence False by -(rule Exit_source,simp+)
thus ?thesis by simp
next
case (Actual_out z)
with ‹parent_node n = (_Exit_)› obtain x
where [simp]:"z = ((_Exit_),x)" by(cases z) auto
with ‹valid_SDG_node n› Actual_out obtain a Q p f where "valid_edge a"
and "kind a = Q↩⇘p⇙f" and "targetnode a = (_Exit_)" by auto
hence False by -(erule Exit_no_return_target,auto)
thus ?thesis by simp
qed

subsection ‹Data dependence›

inductive SDG_Use :: "'var ⇒ 'node SDG_node ⇒ bool" ("_ ∈ Use⇘SDG⇙ _")
where CFG_Use_SDG_Use:
"⟦valid_node m; V ∈ Use m; n = CFG_node m⟧ ⟹ V ∈ Use⇘SDG⇙ n"
| Actual_in_SDG_Use:
"⟦valid_SDG_node n; n = Actual_in (m,x); V ∈ (ParamUses m)!x⟧ ⟹ V ∈ Use⇘SDG⇙ n"
| Formal_out_SDG_Use:
"⟦valid_SDG_node n; n = Formal_out (m,x); get_proc m = p; (p,ins,outs) ∈ set procs;
V = outs!x⟧ ⟹ V ∈ Use⇘SDG⇙ n"

abbreviation notin_SDG_Use :: "'var ⇒ 'node SDG_node ⇒ bool"  ("_ ∉ Use⇘SDG⇙ _")
where "V ∉ Use⇘SDG⇙ n ≡ ¬ V ∈ Use⇘SDG⇙ n"

lemma in_Use_valid_SDG_node:
"V ∈ Use⇘SDG⇙ n ⟹ valid_SDG_node n"
by(induct rule:SDG_Use.induct,auto intro:valid_SDG_CFG_node)

lemma SDG_Use_parent_Use:
"V ∈ Use⇘SDG⇙ n ⟹ V ∈ Use (parent_node n)"
proof(induct rule:SDG_Use.induct)
case CFG_Use_SDG_Use thus ?case by simp
next
case (Actual_in_SDG_Use n m x V)
from ‹valid_SDG_node n› ‹n = Actual_in (m, x)› obtain a Q r p fs ins outs
where "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "sourcenode a = m"
and "(p,ins,outs) ∈ set procs" and "x < length ins" by fastforce
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹(p,ins,outs) ∈ set procs›
have "length(ParamUses (sourcenode a)) = length ins"
by(fastforce intro:ParamUses_call_source_length)
with ‹x < length ins›
have "(ParamUses (sourcenode a))!x ∈ set (ParamUses (sourcenode a))" by simp
with ‹V ∈ (ParamUses m)!x› ‹sourcenode a = m›
have "V ∈ Union (set (ParamUses m))" by fastforce
with ‹valid_edge a› ‹sourcenode a = m› ‹n = Actual_in (m, x)› show ?case
by(fastforce intro:ParamUses_in_Use)
next
case (Formal_out_SDG_Use n m x p ins outs V)
from ‹valid_SDG_node n› ‹n = Formal_out (m, x)› obtain a Q p' f ins' outs'
where "valid_edge a" and "kind a = Q↩⇘p'⇙f" and "sourcenode a = m"
and "(p',ins',outs') ∈ set procs" and "x < length outs'" by fastforce
from ‹valid_edge a› ‹kind a = Q↩⇘p'⇙f› have "get_proc (sourcenode a) = p'"
by(rule get_proc_return)
with ‹get_proc m = p› ‹sourcenode a = m› have [simp]:"p = p'" by simp
with ‹(p',ins',outs') ∈ set procs› ‹(p,ins,outs) ∈ set procs› unique_callers
have [simp]:"ins' = ins" "outs' = outs" by(auto dest:distinct_fst_isin_same_fst)
from ‹x < length outs'› ‹V = outs ! x› have "V ∈ set outs" by fastforce
with ‹valid_edge a› ‹kind a = Q↩⇘p'⇙f› ‹(p,ins,outs) ∈ set procs›
have "V ∈ Use (sourcenode a)" by(fastforce intro:outs_in_Use)
with ‹sourcenode a = m› ‹valid_SDG_node n› ‹n = Formal_out (m, x)›
show ?case by simp
qed

inductive SDG_Def :: "'var ⇒ 'node SDG_node ⇒ bool" ("_ ∈ Def⇘SDG⇙ _")
where CFG_Def_SDG_Def:
"⟦valid_node m; V ∈ Def m; n = CFG_node m⟧ ⟹ V ∈ Def⇘SDG⇙ n"
| Formal_in_SDG_Def:
"⟦valid_SDG_node n; n = Formal_in (m,x); get_proc m = p; (p,ins,outs) ∈ set procs;
V = ins!x⟧ ⟹ V ∈ Def⇘SDG⇙ n"
| Actual_out_SDG_Def:
"⟦valid_SDG_node n; n = Actual_out (m,x); V = (ParamDefs m)!x⟧ ⟹ V ∈ Def⇘SDG⇙ n"

abbreviation notin_SDG_Def :: "'var ⇒ 'node SDG_node ⇒ bool"  ("_ ∉ Def⇘SDG⇙ _")
where "V ∉ Def⇘SDG⇙ n ≡ ¬ V ∈ Def⇘SDG⇙ n"

lemma in_Def_valid_SDG_node:
"V ∈ Def⇘SDG⇙ n ⟹ valid_SDG_node n"
by(induct rule:SDG_Def.induct,auto intro:valid_SDG_CFG_node)

lemma SDG_Def_parent_Def:
"V ∈ Def⇘SDG⇙ n ⟹ V ∈ Def (parent_node n)"
proof(induct rule:SDG_Def.induct)
case CFG_Def_SDG_Def thus ?case by simp
next
case (Formal_in_SDG_Def n m x p ins outs V)
from ‹valid_SDG_node n› ‹n = Formal_in (m, x)› obtain a Q r p' fs ins' outs'
where "valid_edge a" and "kind a = Q:r↪⇘p'⇙fs" and "targetnode a = m"
and "(p',ins',outs') ∈ set procs" and "x < length ins'" by fastforce
from ‹valid_edge a› ‹kind a = Q:r↪⇘p'⇙fs› have "get_proc (targetnode a) = p'"
by(rule get_proc_call)
with ‹get_proc m = p› ‹targetnode a = m› have [simp]:"p = p'" by simp
with ‹(p',ins',outs') ∈ set procs› ‹(p,ins,outs) ∈ set procs› unique_callers
have [simp]:"ins' = ins" "outs' = outs" by(auto dest:distinct_fst_isin_same_fst)
from ‹x < length ins'› ‹V = ins ! x› have "V ∈ set ins" by fastforce
with ‹valid_edge a› ‹kind a = Q:r↪⇘p'⇙fs› ‹(p,ins,outs) ∈ set procs›
have "V ∈ Def (targetnode a)" by(fastforce intro:ins_in_Def)
with ‹targetnode a = m› ‹valid_SDG_node n› ‹n = Formal_in (m, x)›
show ?case by simp
next
case (Actual_out_SDG_Def n m x V)
from ‹valid_SDG_node n› ‹n = Actual_out (m, x)› obtain a Q p f ins outs
where "valid_edge a" and "kind a = Q↩⇘p⇙f" and "targetnode a = m"
and "(p,ins,outs) ∈ set procs" and "x < length outs" by fastforce
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› ‹(p,ins,outs) ∈ set procs›
have "length(ParamDefs (targetnode a)) = length outs"
by(rule ParamDefs_return_target_length)
with ‹x < length outs› ‹V = ParamDefs m ! x› ‹targetnode a = m›
have "V ∈ set (ParamDefs (targetnode a))" by(fastforce simp:set_conv_nth)
with ‹n = Actual_out (m, x)› ‹targetnode a = m› ‹valid_edge a›
show ?case by(fastforce intro:ParamDefs_in_Def)
qed

definition data_dependence :: "'node SDG_node ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
("_ influences _ in _" [51,0,0])
where "n influences V in n' ≡ ∃as. (V ∈ Def⇘SDG⇙ n) ∧ (V ∈ Use⇘SDG⇙ n') ∧
(parent_node n -as→⇩ι* parent_node n') ∧
(∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes (tl as))
⟶ V ∉ Def⇘SDG⇙ n'')"

subsection ‹Control dependence›

definition control_dependence :: "'node ⇒ 'node ⇒ bool"
("_ controls _" [51,0])
where "n controls n' ≡ ∃a a' as. n -a#as→⇩ι* n' ∧ n' ∉ set(sourcenodes (a#as)) ∧
intra_kind(kind a) ∧ n' postdominates (targetnode a) ∧
valid_edge a' ∧ intra_kind(kind a') ∧ sourcenode a' = n ∧
¬ n' postdominates (targetnode a')"

lemma control_dependence_path:
assumes "n controls n'" obtains as where "n -as→⇩ι* n'" and "as ≠ []"
using ‹n controls n'›
by(fastforce simp:control_dependence_def)

lemma Exit_does_not_control [dest]:
assumes "(_Exit_) controls n'" shows "False"
proof -
from ‹(_Exit_) controls n'› obtain a where "valid_edge a"
and "sourcenode a = (_Exit_)" by(auto simp:control_dependence_def)
thus ?thesis by(rule Exit_source)
qed

lemma Exit_not_control_dependent:
assumes "n controls n'" shows "n' ≠ (_Exit_)"
proof -
from ‹n controls n'› obtain a as where "n -a#as→⇩ι* n'"
and "n' postdominates (targetnode a)"
by(auto simp:control_dependence_def)
from ‹n -a#as→⇩ι* n'› have "valid_edge a"
by(fastforce elim:path.cases simp:intra_path_def)
hence "valid_node (targetnode a)" by simp
with ‹n' postdominates (targetnode a)› ‹n -a#as→⇩ι* n'› show ?thesis
by(fastforce elim:Exit_no_postdominator)
qed

lemma which_node_intra_standard_control_dependence_source:
assumes "nx -as@a#as'→⇩ι* n" and "sourcenode a = n'" and "sourcenode a' = n'"
and "n ∉ set(sourcenodes (a#as'))" and "valid_edge a'" and "intra_kind(kind a')"
and "inner_node n" and "¬ method_exit n" and "¬ n postdominates (targetnode a')"
and last:"∀ax ax'. ax ∈ set as' ∧ sourcenode ax = sourcenode ax' ∧
valid_edge ax' ∧ intra_kind(kind ax') ⟶ n postdominates targetnode ax'"
shows "n' controls n"
proof -
from ‹nx -as@a#as'→⇩ι* n› ‹sourcenode a = n'› have "n' -a#as'→⇩ι* n"
by(fastforce dest:path_split_second simp:intra_path_def)
from ‹nx -as@a#as'→⇩ι* n› have "valid_edge a"
by(fastforce intro:path_split simp:intra_path_def)
show ?thesis
proof(cases "n postdominates (targetnode a)")
case True
with ‹n' -a#as'→⇩ι* n› ‹n ∉ set(sourcenodes (a#as'))›
‹valid_edge a'› ‹intra_kind(kind a')› ‹sourcenode a' = n'›
‹¬ n postdominates (targetnode a')› show ?thesis
by(fastforce simp:control_dependence_def intra_path_def)
next
case False
show ?thesis
proof(cases "as' = []")
case True
with ‹n' -a#as'→⇩ι* n› have "targetnode a = n"
by(fastforce elim:path.cases simp:intra_path_def)
with ‹inner_node n› ‹¬ method_exit n› have "n postdominates (targetnode a)"
by(fastforce dest:inner_is_valid intro:postdominate_refl)
with ‹¬ n postdominates (targetnode a)› show ?thesis by simp
next
case False
with ‹nx -as@a#as'→⇩ι* n› have "targetnode a -as'→⇩ι* n"
by(fastforce intro:path_split simp:intra_path_def)
with ‹¬ n postdominates (targetnode a)› ‹valid_edge a› ‹inner_node n›
‹targetnode a -as'→⇩ι* n›
obtain asx pex where "targetnode a -asx→⇩ι* pex" and "method_exit pex"
and "n ∉ set (sourcenodes asx)"
by(fastforce dest:inner_is_valid simp:postdominate_def)
show ?thesis
proof(cases "∃asx'. asx = as'@asx'")
case True
then obtain asx' where [simp]:"asx = as'@asx'" by blast
from ‹targetnode a -asx→⇩ι* pex› ‹targetnode a -as'→⇩ι* n›
‹as' ≠ []› ‹method_exit pex› ‹¬ method_exit n›
obtain a'' as'' where "asx' = a''#as'' ∧ sourcenode a'' = n"
by(cases asx')(auto dest:path_split path_det simp:intra_path_def)
hence "n ∈ set(sourcenodes asx)" by(simp add:sourcenodes_def)
with ‹n ∉ set (sourcenodes asx)› have False by simp
thus ?thesis by simp
next
case False
hence "∀asx'. asx ≠ as'@asx'" by simp
then obtain j asx' where "asx = (take j as')@asx'"
and "j < length as'" and "∀k > j. ∀asx''. asx ≠ (take k as')@asx''"
by(auto elim:path_split_general)
from ‹asx = (take j as')@asx'› ‹j < length as'›
have "∃as'1 as'2. asx = as'1@asx' ∧
as' = as'1@as'2 ∧ as'2 ≠ [] ∧ as'1 = take j as'"
by simp(rule_tac x= "drop j as'" in exI,simp)
then obtain as'1 as'' where "asx = as'1@asx'"
and "as'1 = take j as'"
and "as' = as'1@as''" and "as'' ≠ []" by blast
from ‹as' = as'1@as''› ‹as'' ≠ []› obtain a1 as'2
where "as' = as'1@a1#as'2" and "as'' = a1#as'2"
by(cases as'') auto
have "asx' ≠ []"
proof(cases "asx' = []")
case True
with ‹asx = as'1@asx'› ‹as' = as'1@as''› ‹as'' = a1#as'2›
have "as' = asx@a1#as'2" by simp
with ‹n' -a#as'→⇩ι* n› have "n' -(a#asx)@a1#as'2→⇩ι* n" by simp
hence "n' -(a#asx)@a1#as'2→* n"
and "∀ax ∈ set((a#asx)@a1#as'2). intra_kind(kind ax)"
from ‹n' -(a#asx)@a1#as'2→* n›
have "n' -a#asx→* sourcenode a1" and "valid_edge a1"
by -(erule path_split)+
from ‹∀ax ∈ set((a#asx)@a1#as'2). intra_kind(kind ax)›
have "∀ax ∈ set(a#asx). intra_kind(kind ax)" by simp
with ‹n' -a#asx→* sourcenode a1› have "n' -a#asx→⇩ι* sourcenode a1"
hence "targetnode a -asx→⇩ι* sourcenode a1"
by(fastforce intro:path_split_Cons simp:intra_path_def)
with ‹targetnode a -asx→⇩ι* pex› have "pex = sourcenode a1"
by(fastforce intro:path_det simp:intra_path_def)
from ‹∀ax ∈ set((a#asx)@a1#as'2). intra_kind(kind ax)›
have "intra_kind (kind a1)" by simp
from ‹method_exit pex› have False
proof(rule method_exit_cases)
assume "pex = (_Exit_)"
with ‹pex = sourcenode a1› have "sourcenode a1 = (_Exit_)" by simp
with ‹valid_edge a1› show False by(rule Exit_source)
next
fix a Q f p assume "pex = sourcenode a" and "valid_edge a"
and "kind a = Q↩⇘p⇙f"
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› ‹pex = sourcenode a›
‹pex = sourcenode a1› ‹valid_edge a1› ‹intra_kind (kind a1)›
show False by(fastforce dest:return_edges_only simp:intra_kind_def)
qed
thus ?thesis by simp
qed simp
with ‹asx = as'1@asx'› obtain a2 asx'1
where "asx = as'1@a2#asx'1"
and "asx' = a2#asx'1" by(cases asx') auto
from ‹n' -a#as'→⇩ι* n› ‹as' = as'1@a1#as'2›
have "n' -(a#as'1)@a1#as'2→⇩ι* n" by simp
hence "n' -(a#as'1)@a1#as'2→* n"
and "∀ax ∈ set((a#as'1)@a1#as'2). intra_kind(kind ax)"
from ‹n' -(a#as'1)@a1#as'2→* n› have "n' -a#as'1→* sourcenode a1"
and "valid_edge a1" by -(erule path_split)+
from ‹∀ax ∈ set((a#as'1)@a1#as'2). intra_kind(kind ax)›
have "∀ax ∈ set(a#as'1). intra_kind(kind ax)" by simp
with ‹n' -a#as'1→* sourcenode a1› have "n' -a#as'1→⇩ι* sourcenode a1"
hence "targetnode a -as'1→⇩ι* sourcenode a1"
by(fastforce intro:path_split_Cons simp:intra_path_def)
from ‹targetnode a -asx→⇩ι* pex› ‹asx = as'1@a2#asx'1›
have "targetnode a -as'1@a2#asx'1→* pex" by(simp add:intra_path_def)
hence "targetnode a -as'1→* sourcenode a2" and "valid_edge a2"
and "targetnode a2 -asx'1→* pex" by(auto intro:path_split)
from ‹targetnode a2 -asx'1→* pex› ‹asx = as'1@a2#asx'1›
‹targetnode a -asx→⇩ι* pex›
have "targetnode a2 -asx'1→⇩ι* pex" by(simp add:intra_path_def)
from ‹targetnode a -as'1→* sourcenode a2›
‹targetnode a -as'1→⇩ι* sourcenode a1›
have "sourcenode a1 = sourcenode a2"
by(fastforce intro:path_det simp:intra_path_def)
from ‹asx = as'1@a2#asx'1› ‹n ∉ set (sourcenodes asx)›
have "n ∉ set (sourcenodes asx'1)" by(simp add:sourcenodes_def)
with ‹targetnode a2 -asx'1→⇩ι* pex› ‹method_exit pex›
‹asx = as'1@a2#asx'1›
have "¬ n postdominates targetnode a2" by(fastforce simp:postdominate_def)
from ‹asx = as'1@a2#asx'1› ‹targetnode a -asx→⇩ι* pex›
have "intra_kind (kind a2)" by(simp add:intra_path_def)
from ‹as' = as'1@a1#as'2› have "a1 ∈ set as'" by simp
with ‹sourcenode a1 = sourcenode a2› last ‹valid_edge a2›
‹intra_kind (kind a2)›
have "n postdominates targetnode a2" by blast
with ‹¬ n postdominates targetnode a2› have False by simp
thus ?thesis by simp
qed
qed
qed
qed

subsection ‹SDG without summary edges›

inductive cdep_edge :: "'node SDG_node ⇒ 'node SDG_node ⇒ bool"
("_ ⟶⇘cd⇙ _" [51,0] 80)
and ddep_edge :: "'node SDG_node ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
("_ -_→⇩d⇩d _" [51,0,0] 80)
and call_edge :: "'node SDG_node ⇒ 'pname ⇒ 'node SDG_node ⇒ bool"
("_ -_→⇘call⇙ _" [51,0,0] 80)
and return_edge :: "'node SDG_node ⇒ 'pname ⇒ 'node SDG_node ⇒ bool"
("_ -_→⇘ret⇙ _" [51,0,0] 80)
and param_in_edge :: "'node SDG_node ⇒ 'pname ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
("_ -_:_→⇘in⇙ _" [51,0,0,0] 80)
and param_out_edge :: "'node SDG_node ⇒ 'pname ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
("_ -_:_→⇘out⇙ _" [51,0,0,0] 80)
and SDG_edge :: "'node SDG_node ⇒ 'var option ⇒
('pname × bool) option ⇒ 'node SDG_node ⇒ bool"

where
(* Syntax *)
"n ⟶⇘cd⇙ n' == SDG_edge n None None n'"
| "n -V→⇩d⇩d n' == SDG_edge n (Some V) None n'"
| "n -p→⇘call⇙ n' == SDG_edge n None (Some(p,True)) n'"
| "n -p→⇘ret⇙ n' == SDG_edge n None (Some(p,False)) n'"
| "n -p:V→⇘in⇙ n' == SDG_edge n (Some V) (Some(p,True)) n'"
| "n -p:V→⇘out⇙ n' == SDG_edge n (Some V) (Some(p,False)) n'"

(* Rules *)
| SDG_cdep_edge:
"⟦n = CFG_node m; n' = CFG_node m'; m controls m'⟧ ⟹ n ⟶⇘cd⇙ n'"
| SDG_proc_entry_exit_cdep:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; n = CFG_node (targetnode a);
a' ∈ get_return_edges a; n' = CFG_node (sourcenode a')⟧ ⟹ n ⟶⇘cd⇙ n'"
| SDG_parent_cdep_edge:
"⟦valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n ≠ n'⟧
⟹ n ⟶⇘cd⇙ n'"
| SDG_ddep_edge:"n influences V in n' ⟹ n -V→⇩d⇩d n'"
| SDG_call_edge:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; n = CFG_node (sourcenode a);
n' = CFG_node (targetnode a)⟧ ⟹ n -p→⇘call⇙ n'"
| SDG_return_edge:
"⟦valid_edge a; kind a = Q↩⇘p⇙f; n = CFG_node (sourcenode a);
n' = CFG_node (targetnode a)⟧ ⟹ n -p→⇘ret⇙ n'"
| SDG_param_in_edge:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; (p,ins,outs) ∈ set procs; V = ins!x;
x < length ins; n = Actual_in (sourcenode a,x); n' = Formal_in (targetnode a,x)⟧
⟹ n -p:V→⇘in⇙ n'"
| SDG_param_out_edge:
"⟦valid_edge a; kind a = Q↩⇘p⇙f; (p,ins,outs) ∈ set procs; V = outs!x;
x < length outs; n = Formal_out (sourcenode a,x);
n' = Actual_out (targetnode a,x)⟧
⟹ n -p:V→⇘out⇙ n'"

lemma cdep_edge_cases:
"⟦n ⟶⇘cd⇙ n'; (parent_node n) controls (parent_node n') ⟹ P;
⋀a Q r p fs a'. ⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges a;
parent_node n = targetnode a; parent_node n' = sourcenode a'⟧ ⟹ P;
⋀m. ⟦n = CFG_node m; m = parent_node n'; n ≠ n'⟧ ⟹ P⟧ ⟹ P"
by -(erule SDG_edge.cases,auto)

lemma SDG_edge_valid_SDG_node:
assumes "SDG_edge n Vopt popt n'"
shows "valid_SDG_node n" and "valid_SDG_node n'"
using ‹SDG_edge n Vopt popt n'›
proof(induct rule:SDG_edge.induct)
case (SDG_cdep_edge n m n' m')
thus "valid_SDG_node n" "valid_SDG_node n'"
by(fastforce elim:control_dependence_path elim:path_valid_node
simp:intra_path_def)+
next
case (SDG_proc_entry_exit_cdep a Q r p f n a' n') case 1
from ‹valid_edge a› ‹n = CFG_node (targetnode a)› show ?case by simp
next
case (SDG_proc_entry_exit_cdep a Q r p f n a' n') case 2
from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
by(rule get_return_edges_valid)
with ‹n' = CFG_node (sourcenode a')› show ?case by simp
next
case (SDG_ddep_edge n V n')
thus "valid_SDG_node n" "valid_SDG_node n'"
by(auto intro:in_Use_valid_SDG_node in_Def_valid_SDG_node
simp:data_dependence_def)
qed(fastforce intro:valid_SDG_CFG_node)+

lemma valid_SDG_node_cases:
assumes "valid_SDG_node n"
shows "n = CFG_node (parent_node n) ∨ CFG_node (parent_node n) ⟶⇘cd⇙ n"
proof(cases n)
case (CFG_node m) thus ?thesis by simp
next
case (Formal_in z)
from ‹n = Formal_in z› obtain m x where "z = (m,x)" by(cases z) auto
with ‹valid_SDG_node n› ‹n = Formal_in z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
by -(rule SDG_parent_cdep_edge,auto)
thus ?thesis by fastforce
next
case (Formal_out z)
from ‹n = Formal_out z› obtain m x where "z = (m,x)" by(cases z) auto
with ‹valid_SDG_node n› ‹n = Formal_out z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
by -(rule SDG_parent_cdep_edge,auto)
thus ?thesis by fastforce
next
case (Actual_in z)
from ‹n = Actual_in z› obtain m x where "z = (m,x)" by(cases z) auto
with ‹valid_SDG_node n› ‹n = Actual_in z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
by -(rule SDG_parent_cdep_edge,auto)
thus ?thesis by fastforce
next
case (Actual_out z)
from ‹n = Actual_out z› obtain m x where "z = (m,x)" by(cases z) auto
with ‹valid_SDG_node n› ‹n = Actual_out z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
by -(rule SDG_parent_cdep_edge,auto)
thus ?thesis by fastforce
qed

lemma SDG_cdep_edge_CFG_node: "n ⟶⇘cd⇙ n' ⟹ ∃m. n = CFG_node m"
by(induct n Vopt≡"None::'var option" popt≡"None::('pname × bool) option" n'
rule:SDG_edge.induct) auto

lemma SDG_call_edge_CFG_node: "n -p→⇘call⇙ n' ⟹ ∃m. n = CFG_node m"
by(induct n Vopt≡"None::'var option" popt≡"Some(p,True)" n'
rule:SDG_edge.induct) auto

lemma SDG_return_edge_CFG_node: "n -p→⇘ret⇙ n' ⟹ ∃m. n = CFG_node m"
by(induct n Vopt≡"None::'var option" popt≡"Some(p,False)" n'
rule:SDG_edge.induct) auto

lemma SDG_call_or_param_in_edge_unique_CFG_call_edge:
"SDG_edge n Vopt (Some(p,True)) n'
⟹ ∃!a. valid_edge a ∧ sourcenode a = parent_node n ∧
targetnode a = parent_node n' ∧ (∃Q r fs. kind a = Q:r↪⇘p⇙fs)"
proof(induct n Vopt "Some(p,True)" n' rule:SDG_edge.induct)
case (SDG_call_edge a Q r fs n n')
{ fix a'
assume "valid_edge a'" and "sourcenode a' = parent_node n"
and "targetnode a' = parent_node n'"
from ‹sourcenode a' = parent_node n› ‹n = CFG_node (sourcenode a)›
have "sourcenode a' = sourcenode a" by fastforce
moreover from ‹targetnode a' = parent_node n'› ‹n' = CFG_node (targetnode a)›
have "targetnode a' = targetnode a" by fastforce
ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
by(fastforce intro:edge_det) }
with ‹valid_edge a› ‹n = CFG_node (sourcenode a)› ‹n' = CFG_node (targetnode a)›
‹kind a = Q:r↪⇘p⇙fs› show ?case by(fastforce intro!:ex1I[of _ a])
next
case (SDG_param_in_edge a Q r fs ins outs V x n n')
{ fix a'
assume "valid_edge a'" and "sourcenode a' = parent_node n"
and "targetnode a' = parent_node n'"
from ‹sourcenode a' = parent_node n› ‹n = Actual_in (sourcenode a,x)›
have "sourcenode a' = sourcenode a" by fastforce
moreover from ‹targetnode a' = parent_node n'› ‹n' = Formal_in (targetnode a,x)›
have "targetnode a' = targetnode a" by fastforce
ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
by(fastforce intro:edge_det) }
with ‹valid_edge a› ‹n = Actual_in (sourcenode a,x)›
‹n' = Formal_in (targetnode a,x)› ‹kind a = Q:r↪⇘p⇙fs›
show ?case by(fastforce intro!:ex1I[of _ a])
qed simp_all

lemma SDG_return_or_param_out_edge_unique_CFG_return_edge:
"SDG_edge n Vopt (Some(p,False)) n'
⟹ ∃!a. valid_edge a ∧ sourcenode a = parent_node n ∧
targetnode a = parent_node n' ∧ (∃Q f. kind a = Q↩⇘p⇙f)"
proof(induct n Vopt "Some(p,False)" n' rule:SDG_edge.induct)
case (SDG_return_edge a Q f n n')
{ fix a'
assume "valid_edge a'" and "sourcenode a' = parent_node n"
and "targetnode a' = parent_node n'"
from ‹sourcenode a' = parent_node n› ‹n = CFG_node (sourcenode a)›
have "sourcenode a' = sourcenode a" by fastforce
moreover from ‹targetnode a' = parent_node n'› ‹n' = CFG_node (targetnode a)›
have "targetnode a' = targetnode a" by fastforce
ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
by(fastforce intro:edge_det) }
with ‹valid_edge a› ‹n = CFG_node (sourcenode a)› ‹n' = CFG_node (targetnode a)›
‹kind a = Q↩⇘p⇙f› show ?case by(fastforce intro!:ex1I[of _ a])
next
case (SDG_param_out_edge a Q f ins outs V x n n')
{ fix a'
assume "valid_edge a'" and "sourcenode a' = parent_node n"
and "targetnode a' = parent_node n'"
from ‹sourcenode a' = parent_node n› ‹n = Formal_out (sourcenode a,x)›
have "sourcenode a' = sourcenode a" by fastforce
moreover from ‹targetnode a' = parent_node n'› ‹n' = Actual_out (targetnode a,x)›
have "targetnode a' = targetnode a" by fastforce
ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
by(fastforce intro:edge_det) }
with ‹valid_edge a› ‹n = Formal_out (sourcenode a,x)›
‹n' = Actual_out (targetnode a,x)› ‹kind a = Q↩⇘p⇙f›
show ?case by(fastforce intro!:ex1I[of _ a])
qed simp_all

lemma Exit_no_SDG_edge_source:
"SDG_edge (CFG_node (_Exit_)) Vopt popt n' ⟹ False"
proof(induct "CFG_node (_Exit_)" Vopt popt n' rule:SDG_edge.induct)
case (SDG_cdep_edge m n' m')
hence "(_Exit_) controls m'" by simp
thus ?case by fastforce
next
case (SDG_proc_entry_exit_cdep a Q r p fs a' n')
from ‹CFG_node (_Exit_) = CFG_node (targetnode a)›
have "targetnode a = (_Exit_)" by simp
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
by(rule get_proc_call)
with ‹targetnode a = (_Exit_)› have "p = Main"
by(auto simp:get_proc_Exit)
with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have False
by(fastforce intro:Main_no_call_target)
thus ?thesis by simp
next
case (SDG_parent_cdep_edge n' m)
from ‹CFG_node (_Exit_) = CFG_node m›
have [simp]:"m = (_Exit_)" by simp
with ‹valid_SDG_node n'› ‹m = parent_node n'› ‹CFG_node (_Exit_) ≠ n'›
have False by -(drule valid_SDG_node_parent_Exit,simp+)
thus ?thesis by simp
next
case (SDG_ddep_edge V n')
hence "(CFG_node (_Exit_)) influences V in n'" by simp
with Exit_empty show ?case
by(fastforce dest:path_Exit_source SDG_Def_parent_Def
simp:data_dependence_def intra_path_def)
next
case (SDG_call_edge a Q r p fs n')
from ‹CFG_node (_Exit_) = CFG_node (sourcenode a)›
have "sourcenode a = (_Exit_)" by simp
with ‹valid_edge a› show ?case by(rule Exit_source)
next
case (SDG_return_edge a Q p f n')
from ‹CFG_node (_Exit_) = CFG_node (sourcenode a)›
have "sourcenode a = (_Exit_)" by simp
with ‹valid_edge a› show ?case by(rule Exit_source)
qed simp_all

subsection ‹Intraprocedural paths in the SDG›

inductive intra_SDG_path ::
"'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
("_ i-_→⇩d* _" [51,0,0] 80)

where iSp_Nil:
"valid_SDG_node n ⟹ n i-[]→⇩d* n"

| iSp_Append_cdep:
"⟦n i-ns→⇩d* n''; n'' ⟶⇘cd⇙ n'⟧ ⟹ n i-ns@[n'']→⇩d* n'"

| iSp_Append_ddep:
"⟦n i-ns→⇩d* n''; n'' -V→⇩d⇩d n'; n'' ≠ n'⟧ ⟹ n i-ns@[n'']→⇩d* n'"

lemma intra_SDG_path_Append:
"⟦n'' i-ns'→⇩d* n'; n i-ns→⇩d* n''⟧ ⟹ n i-ns@ns'→⇩d* n'"
by(induct rule:intra_SDG_path.induct,
auto intro:intra_SDG_path.intros simp:append_assoc[THEN sym] simp del:append_assoc)

lemma intra_SDG_path_valid_SDG_node:
assumes "n i-ns→⇩d* n'" shows "valid_SDG_node n" and "valid_SDG_node n'"
using ‹n i-ns→⇩d* n'›
by(induct rule:intra_SDG_path.induct,
auto intro:SDG_edge_valid_SDG_node valid_SDG_CFG_node)

lemma intra_SDG_path_intra_CFG_path:
assumes "n i-ns→⇩d* n'"
obtains as where "parent_node n -as→⇩ι* parent_node n'"
proof(atomize_elim)
from ‹n i-ns→⇩d* n'›
show "∃as. parent_node n -as→⇩ι* parent_node n'"
proof(induct rule:intra_SDG_path.induct)
case (iSp_Nil n)
from ‹valid_SDG_node n› have "valid_node (parent_node n)"
by(rule valid_SDG_CFG_node)
hence "parent_node n -[]→* parent_node n" by(rule empty_path)
thus ?case by(auto simp:intra_path_def)
next
case (iSp_Append_cdep n ns n'' n')
from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
obtain as where "parent_node n -as→⇩ι* parent_node n''" by blast
from ‹n'' ⟶⇘cd⇙ n'› show ?case
proof(rule cdep_edge_cases)
assume "parent_node n'' controls parent_node n'"
then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'" and "as' ≠ []"
by(erule control_dependence_path)
with ‹parent_node n -as→⇩ι* parent_node n''›
have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
thus ?thesis by blast
next
fix a Q r p fs a'
assume "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "a' ∈ get_return_edges a"
and "parent_node n'' = targetnode a" and "parent_node n' = sourcenode a'"
then obtain a'' where "valid_edge a''" and "sourcenode a'' = targetnode a"
and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)⇩√"
hence "targetnode a -[a'']→⇩ι* sourcenode a'"
by(fastforce dest:path_edge simp:intra_path_def intra_kind_def)
with ‹parent_node n'' = targetnode a› ‹parent_node n' = sourcenode a'›
have "∃as'. parent_node n'' -as'→⇩ι* parent_node n' ∧ as' ≠ []" by fastforce
then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'" and "as' ≠ []"
by blast
with ‹parent_node n -as→⇩ι* parent_node n''›
have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
thus ?thesis by blast
next
fix m assume "n'' = CFG_node m" and "m = parent_node n'"
with ‹parent_node n -as→⇩ι* parent_node n''› show ?thesis by fastforce
qed
next
case (iSp_Append_ddep n ns n'' V n')
from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
obtain as where "parent_node n -as→⇩ι* parent_node n''" by blast
from ‹n'' -V→⇩d⇩d n'› have "n'' influences V in n'"
by(fastforce elim:SDG_edge.cases)
then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'"
by(auto simp:data_dependence_def)
with ‹parent_node n -as→⇩ι* parent_node n''›
have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
thus ?case by blast
qed
qed

subsection ‹Control dependence paths in the SDG›

inductive cdep_SDG_path ::
"'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
("_ cd-_→⇩d* _" [51,0,0] 80)

where cdSp_Nil:
"valid_SDG_node n ⟹ n cd-[]→⇩d* n"

| cdSp_Append_cdep:
"⟦n cd-ns→⇩d* n''; n'' ⟶⇘cd⇙ n'⟧ ⟹ n cd-ns@[n'']→⇩d* n'"

lemma cdep_SDG_path_intra_SDG_path:
"n cd-ns→⇩d* n' ⟹ n i-ns→⇩d* n'"
by(induct rule:cdep_SDG_path.induct,auto intro:intra_SDG_path.intros)

lemma Entry_cdep_SDG_path:
assumes "(_Entry_) -as→⇩ι* n'" and "inner_node n'" and "¬ method_exit n'"
obtains ns where "CFG_node (_Entry_) cd-ns→⇩d* CFG_node n'"
and "ns ≠ []" and "∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as)"
proof(atomize_elim)
from ‹(_Entry_) -as→⇩ι* n'› ‹inner_node n'› ‹¬ method_exit n'›
show "∃ns. CFG_node (_Entry_) cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
(∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as))"
proof(induct as arbitrary:n' rule:length_induct)
fix as n'
assume IH:"∀as'. length as' < length as ⟶
(∀n''. (_Entry_) -as'→⇩ι* n'' ⟶ inner_node n'' ⟶ ¬ method_exit n'' ⟶
(∃ns. CFG_node (_Entry_) cd-ns→⇩d* CFG_node n'' ∧ ns ≠ [] ∧
(∀nx∈set ns. parent_node nx ∈ set (sourcenodes as'))))"
and "(_Entry_) -as→⇩ι* n'" and "inner_node n'" and "¬ method_exit n'"
thus "∃ns. CFG_node (_Entry_) cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
(∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as))"
proof -
have "∃ax asx zs. (_Entry_) -ax#asx→⇩ι* n' ∧ n' ∉ set (sourcenodes (ax#asx)) ∧
as = (ax#asx)@zs"
proof(cases "n' ∈ set (sourcenodes as)")
case True
hence "∃n'' ∈ set(sourcenodes as). n' = n''" by simp
then obtain ns' ns'' where "sourcenodes as = ns'@n'#ns''"
and "∀n'' ∈ set ns'. n' ≠ n''"
by(fastforce elim!:split_list_first_propE)
from ‹sourcenodes as = ns'@n'#ns''› obtain xs ys ax
where "sourcenodes xs = ns'" and "as = xs@ax#ys"
and "sourcenode ax = n'"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from ‹∀n'' ∈ set ns'. n' ≠ n''› ‹sourcenodes xs = ns'›
have "n' ∉ set(sourcenodes xs)" by fastforce
from ‹(_Entry_) -as→⇩ι* n'› ‹as = xs@ax#ys› have "(_Entry_) -xs@ax#ys→⇩ι* n'"
by simp
with ‹sourcenode ax = n'› have "(_Entry_) -xs→⇩ι* n'"
by(fastforce dest:path_split simp:intra_path_def)
with ‹inner_node n'› have "xs ≠ []"
by(fastforce elim:path.cases simp:intra_path_def)
with ‹n' ∉ set(sourcenodes xs)› ‹(_Entry_) -xs→⇩ι* n'› ‹as = xs@ax#ys›
show ?thesis by(cases xs) auto
next
case False
with ‹(_Entry_) -as→⇩ι* n'› ‹inner_node n'›
show ?thesis by(cases as)(auto elim:path.cases simp:intra_path_def)
qed
then obtain ax asx zs where "(_Entry_) -ax#asx→⇩ι* n'"
and "n' ∉ set (sourcenodes (ax#asx))" and "as = (ax#asx)@zs" by blast
show ?thesis
proof(cases "∀a' a''. a' ∈ set asx ∧ sourcenode a' = sourcenode a'' ∧
valid_edge a'' ∧ intra_kind(kind a'') ⟶ n' postdominates targetnode a''")
case True
have "(_Exit_) -[]→⇩ι* (_Exit_)"
by(fastforce intro:empty_path simp:intra_path_def)
hence "¬ n' postdominates (_Exit_)"
by(fastforce simp:postdominate_def sourcenodes_def method_exit_def)
from ‹(_Entry_) -ax#asx→⇩ι* n'› have "(_Entry_) -[]@ax#asx→⇩ι* n'" by simp
from ‹(_Entry_) -ax#asx→⇩ι* n'› have [simp]:"sourcenode ax = (_Entry_)"
and "valid_edge ax"
by(auto intro:path_split_Cons simp:intra_path_def)
from Entry_Exit_edge obtain a' where "sourcenode a' = (_Entry_)"
and "targetnode a' = (_Exit_)" and "valid_edge a'"
and "intra_kind(kind a')" by(auto simp:intra_kind_def)
with ‹(_Entry_) -[]@ax#asx→⇩ι* n'› ‹¬ n' postdominates (_Exit_)›
‹valid_edge ax› True ‹sourcenode ax = (_Entry_)›
‹n' ∉ set (sourcenodes (ax#asx))› ‹inner_node n'› ‹¬ method_exit n'›
have "sourcenode ax controls n'"
by -(erule which_node_intra_standard_control_dependence_source
[of _ _ _ _ _ _ a'],auto)
hence "CFG_node (_Entry_) ⟶⇘cd⇙ CFG_node n'"
by(fastforce intro:SDG_cdep_edge)
hence "CFG_node (_Entry_) cd-[]@[CFG_node (_Entry_)]→⇩d* CFG_node n'"
by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
moreover
from ‹as = (ax#asx)@zs› have "(_Entry_) ∈ set(sourcenodes as)"
ultimately show ?thesis by fastforce
next
case False
hence "∃a' ∈ set asx. ∃a''. sourcenode a' = sourcenode a'' ∧ valid_edge a'' ∧
intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a''"
by fastforce
then obtain ax' asx' asx'' where "asx = asx'@ax'#asx'' ∧
(∃a''. sourcenode ax' = sourcenode a'' ∧ valid_edge a'' ∧
intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'') ∧
(∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ valid_edge a'' ∧
intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a''))"
by(blast elim!:split_list_last_propE)
then obtain ai where "asx = asx'@ax'#asx''"
and "sourcenode ax' = sourcenode ai"
and "valid_edge ai" and "intra_kind(kind ai)"
and "¬ n' postdominates targetnode ai"
and "∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧
valid_edge a'' ∧ intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'')"
by blast
from ‹(_Entry_) -ax#asx→⇩ι* n'› ‹asx = asx'@ax'#asx''›
have "(_Entry_) -(ax#asx')@ax'#asx''→⇩ι* n'" by simp
from ‹n' ∉ set (sourcenodes (ax#asx))› ‹asx = asx'@ax'#asx''›
have "n' ∉ set (sourcenodes (ax'#asx''))"
by(auto simp:sourcenodes_def)
with ‹inner_node n'› ‹¬ n' postdominates targetnode ai›
‹n' ∉ set (sourcenodes (ax'#asx''))› ‹sourcenode ax' = sourcenode ai›
‹∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧
valid_edge a'' ∧ intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'')›
‹valid_edge ai› ‹intra_kind(kind ai)› ‹¬ method_exit n'›
‹(_Entry_) -(ax#asx')@ax'#asx''→⇩ι* n'›
have "sourcenode ax' controls n'"
by(fastforce intro!:which_node_intra_standard_control_dependence_source)
hence "CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'"
by(fastforce intro:SDG_cdep_edge)
from ‹(_Entry_) -(ax#asx')@ax'#asx''→⇩ι* n'›
have "(_Entry_) -ax#asx'→⇩ι* sourcenode ax'" and "valid_edge ax'"
by(auto intro:path_split simp:intra_path_def simp del:append_Cons)
from ‹asx = asx'@ax'#asx''› ‹as = (ax#asx)@zs›
have "length (ax#asx') < length as" by simp
from ‹valid_edge ax'› have "valid_node (sourcenode ax')" by simp
hence "inner_node (sourcenode ax')"
proof(cases "sourcenode ax'" rule:valid_node_cases)
case Entry
with ‹(_Entry_) -ax#asx'→⇩ι* sourcenode ax'›
have "(_Entry_) -ax#asx'→* (_Entry_)" by(simp add:intra_path_def)
hence False by(fastforce dest:path_Entry_target)
thus ?thesis by simp
next
case Exit
with ‹valid_edge ax'› have False by(rule Exit_source)
thus ?thesis by simp
qed simp
from ‹asx = asx'@ax'#asx''› ‹(_Entry_) -ax#asx→⇩ι* n'›
have "intra_kind (kind ax')" by(simp add:intra_path_def)
have "¬ method_exit (sourcenode ax')"
proof
assume "method_exit (sourcenode ax')"
thus False
proof(rule method_exit_cases)
assume "sourcenode ax' = (_Exit_)"
with ‹valid_edge ax'› show False by(rule Exit_source)
next
fix x Q f p assume " sourcenode ax' = sourcenode x"
and "valid_edge x" and "kind x = Q↩⇘p⇙f"
from ‹valid_edge x› ‹kind x = Q↩⇘p⇙f› ‹sourcenode ax' = sourcenode x›
‹valid_edge ax'› ‹intra_kind (kind ax')› show False
by(fastforce dest:return_edges_only simp:intra_kind_def)
qed
qed
with IH ‹length (ax#asx') < length as› ‹(_Entry_) -ax#asx'→⇩ι* sourcenode ax'›
‹inner_node (sourcenode ax')›
obtain ns where "CFG_node (_Entry_) cd-ns→⇩d* CFG_node (sourcenode ax')"
and "ns ≠ []"
and "∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes (ax#asx'))"
by blast
from ‹CFG_node (_Entry_) cd-ns→⇩d* CFG_node (sourcenode ax')›
‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'›
have "CFG_node (_Entry_) cd-ns@[CFG_node (sourcenode ax')]→⇩d* CFG_node n'"
by(fastforce intro:cdSp_Append_cdep)
from ‹as = (ax#asx)@zs› ‹asx = asx'@ax'#asx''›
have "sourcenode ax' ∈ set(sourcenodes as)" by(simp add:sourcenodes_def)
with ‹∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes (ax#asx'))›
‹as = (ax#asx)@zs› ‹asx = asx'@ax'#asx''›
have "∀n'' ∈ set (ns@[CFG_node (sourcenode ax')]).
parent_node n'' ∈ set(sourcenodes as)"
by(fastforce simp:sourcenodes_def)
with ‹CFG_node (_Entry_) cd-ns@[CFG_node (sourcenode ax')]→⇩d* CFG_node n'›
show ?thesis by fastforce
qed
qed
qed
qed

lemma in_proc_cdep_SDG_path:
assumes "n -as→⇩ι* n'" and "n ≠ n'" and "n' ≠ (_Exit_)" and "valid_edge a"
and "kind a = Q:r↪⇘p⇙fs" and "targetnode a = n"
obtains ns where "CFG_node n cd-ns→⇩d* CFG_node n'"
and "ns ≠ []" and "∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as)"
proof(atomize_elim)
show "∃ns. CFG_node n cd-ns→⇩d* CFG_node n' ∧
ns ≠ [] ∧ (∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as))"
proof(cases "∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶
ax ∉ get_return_edges a")
case True
from ‹n -as→⇩ι* n'› ‹n ≠ n'› ‹n' ≠ (_Exit_)›
‹∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶ ax ∉ get_return_edges a›
show "∃ns. CFG_node n cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
(∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as))"
proof(induct as arbitrary:n' rule:length_induct)
fix as n'
assume IH:"∀as'. length as' < length as ⟶
(∀n''. n -as'→⇩ι* n'' ⟶ n ≠ n'' ⟶ n'' ≠ (_Exit_) ⟶
(∀ax. valid_edge ax ∧ sourcenode ax = n'' ⟶ ax ∉ get_return_edges a) ⟶
(∃ns. CFG_node n cd-ns→⇩d* CFG_node n'' ∧ ns ≠ [] ∧
(∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as'))))"
and "n -as→⇩ι* n'" and "n ≠ n'" and "n' ≠ (_Exit_)"
and "∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶ ax ∉ get_return_edges a"
show "∃ns. CFG_node n cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
(∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as))"
proof(cases "method_exit n'")
case True
thus ?thesis
proof(rule method_exit_cases)
assume "n' = (_Exit_)"
with ‹n' ≠ (_Exit_)› have False by simp
thus ?thesis by simp
next
fix a' Q' f' p'
assume "n' = sourcenode a'" and "valid_edge a'" and "kind a' = Q'↩⇘p'⇙f'"
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc(targetnode a) = p"
by(rule get_proc_call)
from ‹n -as→⇩ι* n'› have "get_proc n = get_proc n'"
by(rule intra_path_get_procs)
with ‹get_proc(targetnode a) = p› ‹targetnode a = n›
have "get_proc (targetnode a) = get_proc n'" by simp
from ‹valid_edge a'› ‹kind a' = Q'↩⇘p'⇙f'›
have "get_proc (sourcenode a') = p'" by(rule get_proc_return)
with ‹n' = sourcenode a'› ‹get_proc (targetnode a) = get_proc n'›
‹get_proc (targetnode a) = p› have "p = p'" by simp
with ‹valid_edge a'› ‹kind a' = Q'↩⇘p'⇙f'›
obtain ax where "valid_edge ax" and "∃Q r fs. kind ax = Q:r↪⇘p⇙fs"
and "a' ∈ get_return_edges ax" by(auto dest:return_needs_call)
hence "CFG_node (targetnode ax) ⟶⇘cd⇙ CFG_node (sourcenode a')"
by(fastforce intro:SDG_proc_entry_exit_cdep)
with ‹valid_edge ax›
have "CFG_node (targetnode ax) cd-[]@[CFG_node (targetnode ax)]→⇩d*
CFG_node (sourcenode a')"
by(fastforce intro:cdep_SDG_path.intros)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹valid_edge ax›
‹∃Q r fs. kind ax = Q:r↪⇘p⇙fs› have "targetnode a = targetnode ax"
by(fastforce intro:same_proc_call_unique_target)
from ‹n -as→⇩ι* n'› ‹n ≠ n'›
have "as ≠ []" by(fastforce elim:path.cases simp:intra_path_def)
with ‹n -as→⇩ι* n'› have "hd (sourcenodes as) = n"
by(fastforce intro:path_sourcenode simp:intra_path_def)
moreover
from ‹as ≠ []› have "hd (sourcenodes as) ∈ set (sourcenodes as)"
by(fastforce intro:hd_in_set simp:sourcenodes_def)
ultimately have "n ∈ set (sourcenodes as)" by simp
with ‹n' = sourcenode a'› ‹targetnode a = targetnode ax›
‹targetnode a = n›
‹CFG_node (targetnode ax) cd-[]@[CFG_node (targetnode ax)]→⇩d*
CFG_node (sourcenode a')›
show ?thesis by fastforce
qed
next
case False
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain a'
where "a' ∈ get_return_edges a"
by(fastforce dest:get_return_edge_call)
with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain Q' f' where "kind a' = Q'↩⇘p⇙f'"
by(fastforce dest!:call_return_edges)
with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a› obtain a''
where "valid_edge a''" and "sourcenode a'' = targetnode a"
and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)⇩√"
from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
by(rule get_return_edges_valid)
have "∃ax asx zs. n -ax#asx→⇩ι* n' ∧ n' ∉ set (sourcenodes (ax#asx)) ∧
as = (ax#asx)@zs"
proof(cases "n' ∈ set (sourcenodes as)")
case True
hence "∃n'' ∈ set(sourcenodes as). n' = n''" by simp
then obtain ns' ns'' where "sourcenodes as = ns'@n'#ns''"
and "∀n'' ∈ set ns'. n' ≠ n''"
by(fastforce elim!:split_list_first_propE)
from ‹sourcenodes as = ns'@n'#ns''› obtain xs ys ax
where "sourcenodes xs = ns'" and "as = xs@ax#ys"
and "sourcenode ax = n'"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from ‹∀n'' ∈ set ns'. n' ≠ n''› ‹sourcenodes xs = ns'›
have "n' ∉ set(sourcenodes xs)" by fastforce
from ‹n -as→⇩ι* n'› ‹as = xs@ax#ys› have "n -xs@ax#ys→⇩ι* n'" by simp
with ‹sourcenode ax = n'› have "n -xs→⇩ι* n'"
by(fastforce dest:path_split simp:intra_path_def)
with ‹n ≠ n'› have "xs ≠ []" by(fastforce simp:intra_path_def)
with ‹n' ∉ set(sourcenodes xs)› ‹n -xs→⇩ι* n'› ‹as = xs@ax#ys› show ?thesis
by(cases xs) auto
next
case False
with ‹n -as→⇩ι* n'› ‹n ≠ n'›
show ?thesis by(cases as)(auto simp:intra_path_def)
qed
then obtain ax asx zs where "n -ax#asx→⇩ι* n'"
and "n' ∉ set (sourcenodes (ax#asx))" and "as = (ax#asx)@zs" by blast
from ‹n -ax#asx→⇩ι* n'› ‹n' ≠ (_Exit_)› have "inner_node n'"
by(fastforce intro:path_valid_node simp:inner_node_def intra_path_def)
from ‹valid_edge a› ‹targetnode a = n› have "valid_node n" by fastforce
show ?thesis
proof(cases "∀a' a''. a' ∈ set asx ∧ sourcenode a' = sourcenode a'' ∧
valid_edge a'' ∧ intra_kind(kind a'') ⟶
n' postdominates targetnode a''")
case True
from ‹targetnode a = n› ‹sourcenode a'' = targetnode a›
‹kind a'' = (λcf. False)⇩√›
have "sourcenode a'' = n" and "intra_kind(kind a'')"
by(auto simp:intra_kind_def)
{ fix as' assume "targetnode a'' -as'→⇩ι* n'"
from ‹valid_edge a'› ‹targetnode a'' = sourcenode a'›
‹a' ∈ get_return_edges a›
‹∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶ ax ∉ get_return_edges a›
have "targetnode a'' ≠ n'" by fastforce
with ‹targetnode a'' -as'→⇩ι* n'› obtain ax' where "valid_edge ax'"
and "targetnode a'' = sourcenode ax'" and "intra_kind(kind ax')"
by(clarsimp simp:intra_path_def)(erule path.cases,fastforce+)
from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› ‹valid_edge ax'›
‹targetnode a'' = sourcenode a'› ‹targetnode a'' = sourcenode ax'›
‹intra_kind(kind ax')›
have False by(fastforce dest:return_edges_only simp:intra_kind_def) }
hence "¬ n' postdominates targetnode a''"
by(fastforce elim:postdominate_implies_inner_path)
from ‹n -ax#asx→⇩ι* n'› have "sourcenode ax = n"
by(auto intro:path_split_Cons simp:intra_path_def)
from ‹n -ax#asx→⇩ι* n'› have "n -[]@ax#asx→⇩ι* n'" by simp
from this ‹sourcenode a'' = n› ‹sourcenode ax = n› True
‹n' ∉ set (sourcenodes (ax#asx))› ‹valid_edge a''› ‹intra_kind(kind a'')›
‹inner_node n'› ‹¬ method_exit n'› ‹¬ n' postdominates targetnode a''›
have "n controls n'"
by(fastforce intro!:which_node_intra_standard_control_dependence_source)
hence "CFG_node n ⟶⇘cd⇙ CFG_node n'"
by(fastforce intro:SDG_cdep_edge)
with ‹valid_node n› have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node n'"
by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
moreover
from ‹as = (ax#asx)@zs› ‹sourcenode ax = n› have "n ∈ set(sourcenodes as)"
ultimately show ?thesis by fastforce
next
case False
hence "∃a' ∈ set asx. ∃a''. sourcenode a' = sourcenode a'' ∧
valid_edge a'' ∧ intra_kind(kind a'') ∧
¬ n' postdominates targetnode a''"
by fastforce
then obtain ax' asx' asx'' where "asx = asx'@ax'#asx'' ∧
(∃a''. sourcenode ax' = sourcenode a'' ∧ valid_edge a'' ∧
intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'') ∧
(∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧
valid_edge a'' ∧ intra_kind(kind a'') ∧
¬ n' postdominates targetnode a''))"
by(blast elim!:split_list_last_propE)
then obtain ai where "asx = asx'@ax'#asx''"
and "sourcenode ax' = sourcenode ai"
and "valid_edge ai" and "intra_kind(kind ai)"
and "¬ n' postdominates targetnode ai"
and "∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧
valid_edge a'' ∧ intra_kind(kind a'') ∧
¬ n' postdominates targetnode a'')"
by blast
from ‹asx = asx'@ax'#asx''› ‹n -ax#asx→⇩ι* n'›
have "n -(ax#asx')@ax'#asx''→⇩ι* n'" by simp
from ‹n' ∉ set (sourcenodes (ax#asx))› ‹asx = asx'@ax'#asx''›
have "n' ∉ set (sourcenodes (ax'#asx''))"
by(auto simp:sourcenodes_def)
with ‹inner_node n'› ‹¬ n' postdominates targetnode ai›
‹n -(ax#asx')@ax'#asx''→⇩ι* n'› ‹sourcenode ax' = sourcenode ai›
‹∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧
valid_edge a'' ∧ intra_kind(kind a'') ∧
¬ n' postdominates targetnode a'')›
‹valid_edge ai› ‹intra_kind(kind ai)› ‹¬ method_exit n'›
have "sourcenode ax' controls n'"
by(fastforce intro!:which_node_intra_standard_control_dependence_source)
hence "CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'"
by(fastforce intro:SDG_cdep_edge)
from ‹n -(ax#asx')@ax'#asx''→⇩ι* n'›
have "n -ax#asx'→⇩ι* sourcenode ax'" and "valid_edge ax'"
by(auto intro:path_split simp:intra_path_def simp del:append_Cons)
from ‹asx = asx'@ax'#asx''› ‹as = (ax#asx)@zs›
have "length (ax#asx') < length as" by simp
from ‹as = (ax#asx)@zs› ‹asx = asx'@ax'#asx''›
have "sourcenode ax' ∈ set(sourcenodes as)" by(simp add:sourcenodes_def)
show ?thesis
proof(cases "n = sourcenode ax'")
case True
with ‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'› ‹valid_edge ax'›
have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node n'"
by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
with ‹sourcenode ax' ∈ set(sourcenodes as)› True show ?thesis by fastforce
next
case False
from ‹valid_edge ax'› have "sourcenode ax' ≠ (_Exit_)"
by -(rule ccontr,fastforce elim!:Exit_source)
from ‹n -ax#asx'→⇩ι* sourcenode ax'› have "n = sourcenode ax"
by(fastforce intro:path_split_Cons simp:intra_path_def)
show ?thesis
proof(cases "∀ax. valid_edge ax ∧ sourcenode ax = sourcenode ax' ⟶
ax ∉ get_return_edges a")
case True
from ‹asx = asx'@ax'#asx''› ‹n -ax#asx→⇩ι* n'›
have "intra_kind (kind ax')" by(simp add:intra_path_def)
have "¬ method_exit (sourcenode ax')"
proof
assume "method_exit (sourcenode ax')"
thus False
proof(rule method_exit_cases)
assume "sourcenode ax' = (_Exit_)"
with ‹valid_edge ax'› show False by(rule Exit_source)
next
fix x Q f p assume " sourcenode ax' = sourcenode x"
and "valid_edge x" and "kind x = Q↩⇘p⇙f"
from ‹valid_edge x› ‹kind x = Q↩⇘p⇙f› ‹sourcenode ax' = sourcenode x›
‹valid_edge ax'› ‹intra_kind (kind ax')› show False
by(fastforce dest:return_edges_only simp:intra_kind_def)
qed
qed
with IH ‹length (ax#asx') < length as› ‹n -ax#asx'→⇩ι* sourcenode ax'›
‹n ≠ sourcenode ax'› ‹sourcenode ax' ≠ (_Exit_)› True
obtain ns where "CFG_node n cd-ns→⇩d* CFG_node (sourcenode ax')"
and "ns ≠ []"
and "∀n''∈set ns. parent_node n'' ∈ set (sourcenodes (ax#asx'))"
by blast
from ‹CFG_node n cd-ns→⇩d* CFG_node (sourcenode ax')›
‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'›
have "CFG_node n cd-ns@[CFG_node (sourcenode ax')]→⇩d* CFG_node n'"
by(rule cdSp_Append_cdep)
moreover
from ‹∀n''∈set ns. parent_node n'' ∈ set (sourcenodes (ax#asx'))›
‹asx = asx'@ax'#asx''› ‹as = (ax#asx)@zs›
‹sourcenode ax' ∈ set(sourcenodes as)›
have "∀n''∈set (ns@[CFG_node (sourcenode ax')]).
parent_node n'' ∈ set (sourcenodes as)"
by(fastforce simp:sourcenodes_def)
ultimately show ?thesis by fastforce
next
case False
then obtain ai' where "valid_edge ai'"
and "sourcenode ai' = sourcenode ax'"
and "ai' ∈ get_return_edges a" by blast
with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹targetnode a = n›
have "CFG_node n ⟶⇘cd⇙ CFG_node (sourcenode ax')"
by(fastforce intro!:SDG_proc_entry_exit_cdep[of _ _ _ _ _ _ ai'])
with ‹valid_node n›
have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node (sourcenode ax')"
by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
with ‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'›
have "CFG_node n cd-[CFG_node n]@[CFG_node (sourcenode ax')]→⇩d*
CFG_node n'"
by(fastforce intro:cdSp_Append_cdep)
moreover
from ‹sourcenode ax' ∈ set(sourcenodes as)› ‹n = sourcenode ax›
‹as = (ax#asx)@zs›
have "∀n''∈set ([CFG_node n]@[CFG_node (sourcenode ax')]).
parent_node n'' ∈ set (sourcenodes as)"
by(fastforce simp:sourcenodes_def)
ultimately show ?thesis by fastforce
qed
qed
qed
qed
qed
next
case False
then obtain a' where "valid_edge a'" and "sourcenode a' = n'"
and "a' ∈ get_return_edges a" by auto
with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹targetnode a = n›
have "CFG_node n ⟶⇘cd⇙ CFG_node n'" by(fastforce intro:SDG_proc_entry_exit_cdep)
with ‹valid_edge a› ‹targetnode a = n›[THEN sym]
have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node n'"
by(fastforce intro:cdep_SDG_path.intros)
```