# Theory DependentLiveVariables

```section ‹Dependent Live Variables›

theory DependentLiveVariables imports DynPDG begin

text ‹‹dependent_live_vars› calculates variables which
can change\\ the value of the @{term Use} variables of the target node›

context DynPDG begin

inductive_set
dependent_live_vars :: "'node ⇒ ('var × 'edge list × 'edge list) set"
for n' :: "'node"
where dep_vars_Use:
"V ∈ Use n' ⟹ (V,[],[]) ∈ dependent_live_vars n'"

| dep_vars_Cons_cdep:
"⟦V ∈ Use (sourcenode a); sourcenode a -a#as'→⇩c⇩d n''; n'' -as''→⇩d* n'⟧
⟹ (V,[],a#as'@as'') ∈ dependent_live_vars n'"

| dep_vars_Cons_ddep:
"⟦(V,as',as) ∈ dependent_live_vars n'; V' ∈ Use (sourcenode a);
n' = last(targetnodes (a#as));
sourcenode a -{V}a#as'→⇩d⇩d last(targetnodes (a#as'))⟧
⟹ (V',[],a#as) ∈ dependent_live_vars n'"

| dep_vars_Cons_keep:
"⟦(V,as',as) ∈ dependent_live_vars n'; n' = last(targetnodes (a#as));
¬ sourcenode a -{V}a#as'→⇩d⇩d last(targetnodes (a#as'))⟧
⟹ (V,a#as',a#as) ∈ dependent_live_vars n'"

lemma dependent_live_vars_fst_prefix_snd:
"(V,as',as) ∈ dependent_live_vars n' ⟹ ∃as''. as'@as'' = as"
by(induct rule:dependent_live_vars.induct,simp_all)

lemma dependent_live_vars_Exit_empty [dest]:
"(V,as',as) ∈ dependent_live_vars (_Exit_) ⟹ False"
proof(induct rule:dependent_live_vars.induct)
case (dep_vars_Cons_cdep V a as' n'' as'')
from ‹n'' -as''→⇩d* (_Exit_)› have "n'' = (_Exit_)"
by(fastforce intro:DynPDG_path_Exit)
with ‹sourcenode a -a#as'→⇩c⇩d n''› have "sourcenode a -a#as'→⇩d* (_Exit_)"
by(fastforce intro:DynPDG_path_cdep)
hence "sourcenode a = (_Exit_)" by(fastforce intro:DynPDG_path_Exit)
with ‹V ∈ Use (sourcenode a)› show False by simp(erule Exit_Use_empty)
qed auto

lemma dependent_live_vars_lastnode:
"⟦(V,as',as) ∈ dependent_live_vars n'; as ≠ []⟧
⟹ n' = last(targetnodes as)"
proof(induct rule:dependent_live_vars.induct)
case (dep_vars_Cons_cdep V a as' n'' as'')
from ‹sourcenode a -a#as'→⇩c⇩d n''› have "sourcenode a -a#as'→* n''"
by(rule DynPDG_cdep_edge_CFG_path(1))
from ‹n'' -as''→⇩d* n'› have "n'' -as''→* n'" by(rule DynPDG_path_CFG_path)
show ?case
proof(cases "as'' = []")
case True
with ‹n'' -as''→* n'› have "n'' = n'" by (auto elim: DynPDG.dependent_live_vars.cases)
with ‹sourcenode a -a#as'→* n''› True
show ?thesis by(fastforce intro:path_targetnode[THEN sym])
next
case False
with ‹n'' -as''→* n'› have "n' = last(targetnodes as'')"
by(fastforce intro:path_targetnode[THEN sym])
with False show ?thesis by(fastforce simp:targetnodes_def)
qed
qed simp_all

lemma dependent_live_vars_Use_cases:
"⟦(V,as',as) ∈ dependent_live_vars n'; n -as→* n'⟧
⟹ ∃nx as''. as = as'@as'' ∧ n -as'→* nx ∧ nx -as''→⇩d* n' ∧ V ∈ Use nx ∧
(∀n'' ∈ set (sourcenodes as'). V ∉ Def n'')"
proof(induct arbitrary:n rule:dependent_live_vars.induct)
case (dep_vars_Use V)
from ‹n -[]→* n'› have "valid_node n'" by(rule path_valid_node(2))
hence "n' -[]→⇩d* n'" by(rule DynPDG_path_Nil)
with ‹V ∈ Use n'› ‹n -[]→* n'› show ?case
by(auto simp:sourcenodes_def)
next
case (dep_vars_Cons_cdep V a as' n'' as'' n)
from ‹n -a#as'@as''→* n'› have "sourcenode a = n"
by(auto elim:path.cases)
from ‹sourcenode a -a#as'→⇩c⇩d n''› have "sourcenode a -a#as'→* n''"
by(rule DynPDG_cdep_edge_CFG_path(1))
hence "valid_edge a" by(auto elim:path.cases)
hence "sourcenode a -[]→* sourcenode a" by(fastforce intro:empty_path)
from ‹sourcenode a -a#as'→⇩c⇩d n''› have "sourcenode a -a#as'→⇩d* n''"
by(rule DynPDG_path_cdep)
with ‹n'' -as''→⇩d* n'› have "sourcenode a -(a#as')@as''→⇩d* n'"
by(rule DynPDG_path_Append)
with ‹sourcenode a -[]→* sourcenode a› ‹V ∈ Use (sourcenode a)› ‹sourcenode a = n›
show ?case by(auto simp:sourcenodes_def)
next
case(dep_vars_Cons_ddep V as' as V' a n)
note ddep = ‹sourcenode a -{V}a#as'→⇩d⇩d last (targetnodes (a#as'))›
note IH = ‹⋀n. n -as→* n'
⟹ ∃nx as''. as = as'@as'' ∧ n -as'→* nx ∧ nx -as''→⇩d* n' ∧
V ∈ Use nx ∧ (∀n''∈set (sourcenodes as'). V ∉ Def n'')›
from ‹n -a#as→* n'› have "n -[]@a#as→* n'" by simp
hence "n = sourcenode a" and "targetnode a -as→* n'" and "valid_edge a"
by(fastforce dest:path_split)+
hence "n -[]→* n"
by(fastforce intro:empty_path simp:valid_node_def)
from IH[OF ‹targetnode a -as→* n'›]
have "∃nx as''. as = as'@as'' ∧ targetnode a -as'→* nx ∧ nx -as''→⇩d* n' ∧
V ∈ Use nx ∧ (∀n''∈set (sourcenodes as'). V ∉ Def n'')" .
then obtain nx'' as'' where "targetnode a -as'→* nx''"
and "nx'' -as''→⇩d* n'" and "as = as'@as''" by blast
have "last (targetnodes (a#as')) -as''→⇩d* n'"
proof(cases as')
case Nil
with ‹targetnode a -as'→* nx''› have "nx'' = targetnode a"
by(auto elim:path.cases)
with ‹nx'' -as''→⇩d* n'› Nil show ?thesis by(simp add:targetnodes_def)
next
case (Cons ax asx)
hence "last (targetnodes (a#as')) = last (targetnodes as')"
from Cons ‹targetnode a -as'→* nx''› have "last (targetnodes as') = nx''"
by(fastforce intro:path_targetnode)
with ‹last (targetnodes (a#as')) = last (targetnodes as')› ‹nx'' -as''→⇩d* n'›
show ?thesis by simp
qed
with ddep ‹as = as'@as''› have "sourcenode a -a#as→⇩d* n'"
by(fastforce dest:DynPDG_path_ddep DynPDG_path_Append)
with ‹V' ∈ Use (sourcenode a)› ‹n = sourcenode a› ‹n -[]→* n›
show ?case by(auto simp:sourcenodes_def)
next
case (dep_vars_Cons_keep V as' as a n)
note no_dep = ‹¬ sourcenode a -{V}a#as'→⇩d⇩d last (targetnodes (a#as'))›
note IH = ‹⋀n. n -as→* n'
⟹ ∃nx as''. (as = as'@as'') ∧ (n -as'→* nx) ∧ (nx -as''→⇩d* n') ∧
V ∈ Use nx ∧ (∀n''∈set (sourcenodes as'). V ∉ Def n'')›
from ‹n -a#as→* n'› have "n = sourcenode a" and "valid_edge a"
and "targetnode a -as→* n'" by(auto elim:path_split_Cons)
from IH[OF ‹targetnode a -as→* n'›]
have "∃nx as''. as = as'@as'' ∧ targetnode a -as'→* nx ∧ nx -as''→⇩d* n' ∧
V ∈ Use nx ∧ (∀n''∈set (sourcenodes as'). V ∉ Def n'')" .
then obtain nx'' as'' where "V ∈ Use nx''"
and "∀n''∈set (sourcenodes as'). V ∉ Def n''" and "targetnode a -as'→* nx''"
and "nx'' -as''→⇩d* n'" and "as = as'@as''" by blast
from ‹valid_edge a› ‹targetnode a -as'→* nx''› have "sourcenode a -a#as'→* nx''"
by(fastforce intro:Cons_path)
hence "last(targetnodes (a#as')) = nx''" by(fastforce dest:path_targetnode)
{ assume "V ∈ Def (sourcenode a)"
with ‹V ∈ Use nx''› ‹sourcenode a -a#as'→* nx''›
‹∀n''∈set (sourcenodes as'). V ∉ Def n''›
have "(sourcenode a) influences V in nx'' via a#as'"
with no_dep ‹last(targetnodes (a#as')) = nx''›
‹∀n''∈set (sourcenodes as'). V ∉ Def n''› ‹V ∈ Def (sourcenode a)›
have False by(fastforce dest:DynPDG_ddep_edge) }
with ‹∀n''∈set (sourcenodes as'). V ∉ Def n''›
have "∀n''∈set (sourcenodes (a#as')). V ∉ Def n''"
by(fastforce simp:sourcenodes_def)
with ‹V ∈ Use nx''› ‹sourcenode a -a#as'→* nx''› ‹nx'' -as''→⇩d* n'›
‹as = as'@as''› ‹n = sourcenode a› show ?case by fastforce
qed

lemma dependent_live_vars_dependent_edge:
assumes "(V,as',as) ∈ dependent_live_vars n'"
and "targetnode a -as→* n'"
and "V ∈ Def (sourcenode a)" and "valid_edge a"
obtains nx as'' where "as = as'@as''" and "sourcenode a -{V}a#as'→⇩d⇩d nx"
and "nx -as''→⇩d* n'"
proof(atomize_elim)
from ‹(V,as',as) ∈ dependent_live_vars n'› ‹targetnode a -as→* n'›
have "∃nx as''. as = as'@as'' ∧ targetnode a -as'→* nx ∧ nx -as''→⇩d* n' ∧
V ∈ Use nx ∧ (∀n'' ∈ set (sourcenodes as'). V ∉ Def n'')"
by(rule dependent_live_vars_Use_cases)
then obtain nx as'' where "V ∈ Use nx"
and "∀n''∈ set(sourcenodes as'). V ∉ Def n''"
and "targetnode a -as'→* nx" and "nx -as''→⇩d* n'"
and "as = as'@as''" by blast
from ‹targetnode a -as'→* nx› ‹valid_edge a› have "sourcenode a -a#as'→* nx"
by(fastforce intro:Cons_path)
with ‹V ∈ Def (sourcenode a)› ‹V ∈ Use nx›
‹∀n''∈ set(sourcenodes as'). V ∉ Def n''›
have "sourcenode a influences V in nx via a#as'"
by(auto simp:dyn_data_dependence_def sourcenodes_def)
hence "sourcenode a -{V}a#as'→⇩d⇩d nx" by(rule DynPDG_ddep_edge)
with ‹nx -as''→⇩d* n'› ‹as = as'@as''›
show "∃as'' nx. (as = as'@as'') ∧ (sourcenode a -{V}a#as'→⇩d⇩d nx) ∧
(nx -as''→⇩d* n')" by fastforce
qed

lemma dependent_live_vars_same_pathsI:
assumes "V ∈ Use n'"
shows "⟦∀as' a as''. as = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n';
as ≠ [] ⟶ n' = last(targetnodes as)⟧
⟹ (V,as,as) ∈ dependent_live_vars n'"
proof(induct as)
case Nil
from ‹V ∈ Use n'› show ?case by(rule dep_vars_Use)
next
case (Cons ax asx)
note lastnode = ‹ax#asx ≠ [] ⟶ n' = last (targetnodes (ax#asx))›
note IH = ‹⟦∀as' a as''. asx = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n';
asx ≠ [] ⟶ n' = last (targetnodes asx)⟧
⟹ (V, asx, asx) ∈ dependent_live_vars n'›
from ‹∀as' a as''. ax#asx = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n'›
have all':"∀as' a as''. asx = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
and "¬ sourcenode ax -{V}ax#asx→⇩d⇩d n'"
by simp_all
show ?case
proof(cases "asx = []")
case True
from ‹V ∈ Use n'› have "(V,[],[]) ∈ dependent_live_vars n'" by(rule dep_vars_Use)
with ‹¬ sourcenode ax -{V}ax#asx→⇩d⇩d n'› True lastnode
have "(V,[ax],[ax]) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_keep)
with True show ?thesis by simp
next
case False
with lastnode have "asx ≠ [] ⟶ n' = last (targetnodes asx)"
from IH[OF all' this] have "(V, asx, asx) ∈ dependent_live_vars n'" .
with ‹¬ sourcenode ax -{V}ax#asx→⇩d⇩d n'› lastnode
show ?thesis by(fastforce intro:dep_vars_Cons_keep)
qed
qed

lemma dependent_live_vars_same_pathsD:
"⟦(V,as,as) ∈ dependent_live_vars n';  as ≠ [] ⟶ n' = last(targetnodes as)⟧
⟹ V ∈ Use n' ∧ (∀as' a as''. as = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n')"
proof(induct as)
case Nil
have "(V,[],[]) ∈ dependent_live_vars n'" by fact
thus ?case
by(fastforce elim:dependent_live_vars.cases simp:targetnodes_def sourcenodes_def)
next
case (Cons ax asx)
note IH = ‹⟦(V,asx,asx) ∈ dependent_live_vars n';
asx ≠ [] ⟶ n' = last (targetnodes asx)⟧
⟹ V ∈ Use n' ∧ (∀as' a as''. asx = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n')›
from ‹(V,ax#asx,ax#asx) ∈ dependent_live_vars n'›
have "(V,asx,asx) ∈ dependent_live_vars n'"
and "¬ sourcenode ax -{V}ax#asx→⇩d⇩d last(targetnodes (ax#asx))"
by(auto elim:dependent_live_vars.cases)
from ‹ax#asx ≠ [] ⟶ n' = last (targetnodes (ax#asx))›
have "n' = last (targetnodes (ax#asx))" by simp
show ?case
proof(cases "asx = []")
case True
with ‹(V,asx,asx) ∈ dependent_live_vars n'› have "V ∈ Use n'"
by(fastforce elim:dependent_live_vars.cases)
from ‹¬ sourcenode ax -{V}ax#asx→⇩d⇩d last(targetnodes (ax#asx))›
True ‹n' = last (targetnodes (ax#asx))›
have "∀as' a as''. ax#asx = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
by auto(case_tac as',auto)
with ‹V ∈ Use n'› show ?thesis by simp
next
case False
with ‹n' = last (targetnodes (ax#asx))›
have "asx ≠ [] ⟶ n' = last (targetnodes asx)"
from IH[OF ‹(V,asx,asx) ∈ dependent_live_vars n'› this]
have "V ∈ Use n' ∧ (∀as' a as''. asx = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n')" .
with ‹¬ sourcenode ax -{V}ax#asx→⇩d⇩d last(targetnodes (ax#asx))›
‹n' = last (targetnodes (ax#asx))› have "V ∈ Use n'"
and "∀as' a as''. ax#asx = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
by auto(case_tac as',auto)
thus ?thesis by simp
qed
qed

lemma dependent_live_vars_same_paths:
"as ≠ [] ⟶ n' = last(targetnodes as) ⟹
(V,as,as) ∈ dependent_live_vars n' =
(V ∈ Use n' ∧ (∀as' a as''. as = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n'))"
by(fastforce intro!:dependent_live_vars_same_pathsD dependent_live_vars_same_pathsI)

lemma dependent_live_vars_cdep_empty_fst:
assumes "n'' -as→⇩c⇩d n'" and "V' ∈ Use n''"
shows "(V',[],as) ∈ dependent_live_vars n'"
proof(cases as)
case Nil
with ‹n'' -as→⇩c⇩d n'› show ?thesis
by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
next
case (Cons ax asx)
with ‹n'' -as→⇩c⇩d n'› have "sourcenode ax = n''"
by(auto dest:DynPDG_cdep_edge_CFG_path elim:path.cases)
from ‹n'' -as→⇩c⇩d n'› have "valid_node n'"
by(fastforce intro:path_valid_node(2) DynPDG_cdep_edge_CFG_path(1))
from Cons ‹n'' -as→⇩c⇩d n'› have "last(targetnodes as) = n'"
by(fastforce intro:path_targetnode dest:DynPDG_cdep_edge_CFG_path)
with Cons ‹n'' -as→⇩c⇩d n'› ‹V' ∈ Use n''› ‹sourcenode ax = n''› ‹valid_node n'›
have "(V', [], ax#asx@[]) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_cdep DynPDG_path_Nil)
with Cons show ?thesis by simp
qed

lemma dependent_live_vars_ddep_empty_fst:
assumes "n'' -{V}as→⇩d⇩d n'" and "V' ∈ Use n''"
shows "(V',[],as) ∈ dependent_live_vars n'"
proof(cases as)
case Nil
with ‹n'' -{V}as→⇩d⇩d n'› show ?thesis
by(fastforce elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
next
case (Cons ax asx)
with ‹n'' -{V}as→⇩d⇩d n'› have "sourcenode ax = n''"
by(auto dest:DynPDG_ddep_edge_CFG_path elim:path.cases)
from Cons ‹n'' -{V}as→⇩d⇩d n'› have "last(targetnodes as) = n'"
by(fastforce intro:path_targetnode elim:DynPDG_ddep_edge_CFG_path(1))
from Cons ‹n'' -{V}as→⇩d⇩d n'› have all:"∀as' a as''. asx = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
by(fastforce dest:DynPDG_ddep_edge_no_shorter_ddep_edge)
from ‹n'' -{V}as→⇩d⇩d n'› have "V ∈ Use n'"
by(auto elim!:DynPDG_edge.cases simp:dyn_data_dependence_def)
from Cons ‹n'' -{V}as→⇩d⇩d n'› have "as ≠ [] ⟶ n' = last(targetnodes as)"
by(fastforce dest:DynPDG_ddep_edge_CFG_path path_targetnode)
with Cons have "asx ≠ [] ⟶ n' = last(targetnodes asx)"
by(fastforce simp:targetnodes_def)
with all ‹V ∈ Use n'› have "(V,asx,asx) ∈ dependent_live_vars n'"
by -(rule dependent_live_vars_same_pathsI)
with ‹V' ∈ Use n''› ‹n'' -{V}as→⇩d⇩d n'› ‹last(targetnodes as) = n'›
Cons ‹sourcenode ax = n''› show ?thesis
by(fastforce intro:dep_vars_Cons_ddep)
qed

lemma ddep_dependent_live_vars_keep_notempty:
assumes "n -{V}a#as→⇩d⇩d n''" and "as' ≠ []"
and "(V,as'',as') ∈ dependent_live_vars n'"
shows "(V,as@as'',as@as') ∈ dependent_live_vars n'"
proof -
from ‹n -{V}a#as→⇩d⇩d n''› have "∀n'' ∈ set (sourcenodes as). V ∉ Def n''"
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
with ‹(V,as'',as') ∈ dependent_live_vars n'› show ?thesis
proof(induct as)
case Nil thus ?case by simp
next
case (Cons ax asx)
note IH = ‹⟦(V,as'',as') ∈ dependent_live_vars n';
∀n''∈set (sourcenodes asx). V ∉ Def n''⟧
⟹ (V, asx@as'',asx@as') ∈ dependent_live_vars n'›
from ‹∀n''∈set (sourcenodes (ax#asx)). V ∉ Def n''›
have "∀n''∈set (sourcenodes asx). V ∉ Def n''"
by(auto simp:sourcenodes_def)
from IH[OF ‹(V,as'',as') ∈ dependent_live_vars n'› this]
have "(V,asx@as'',asx@as') ∈ dependent_live_vars n'" .
from ‹as' ≠ []› ‹(V,as'',as') ∈ dependent_live_vars n'›
have "n' = last(targetnodes as')"
by(fastforce intro:dependent_live_vars_lastnode)
with ‹as' ≠ []› have "n' = last(targetnodes (ax#asx@as'))"
by(fastforce simp:targetnodes_def)
have "¬ sourcenode ax -{V}ax#asx@as''→⇩d⇩d last(targetnodes (ax#asx@as''))"
proof
assume "sourcenode ax -{V}ax#asx@as''→⇩d⇩d last(targetnodes (ax#asx@as''))"
hence "sourcenode ax -{V}ax#asx@as''→⇩d⇩d last(targetnodes (ax#asx@as''))"
by simp
with ‹∀n''∈set (sourcenodes (ax#asx)). V ∉ Def n''›
show False
by(fastforce elim:DynPDG_edge.cases
simp:dyn_data_dependence_def sourcenodes_def)
qed
with ‹(V,asx@as'',asx@as') ∈ dependent_live_vars n'›
‹n' = last(targetnodes (ax#asx@as'))›
show ?case by(fastforce intro:dep_vars_Cons_keep)
qed
qed

lemma dependent_live_vars_cdep_dependent_live_vars:
assumes "n'' -as''→⇩c⇩d n'" and "(V',as',as) ∈ dependent_live_vars n''"
shows "(V',as',as@as'') ∈ dependent_live_vars n'"
proof -
from ‹n'' -as''→⇩c⇩d n'› have "as'' ≠ []"
by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
with ‹n'' -as''→⇩c⇩d n'› have "last(targetnodes as'') = n'"
by(fastforce intro:path_targetnode elim:DynPDG_cdep_edge_CFG_path(1))
from ‹(V',as',as) ∈ dependent_live_vars n''› show ?thesis
proof(induct rule:dependent_live_vars.induct)
case (dep_vars_Use V')
from ‹V' ∈ Use n''› ‹n'' -as''→⇩c⇩d n'› ‹last(targetnodes as'') = n'› show ?case
by(fastforce intro:dependent_live_vars_cdep_empty_fst simp:targetnodes_def)
next
case (dep_vars_Cons_cdep V a as' nx asx)
from ‹n'' -as''→⇩c⇩d n'› have "n'' -as''→⇩d* n'" by(rule DynPDG_path_cdep)
with ‹nx -asx→⇩d* n''› have "nx -asx@as''→⇩d* n'"
by -(rule DynPDG_path_Append)
with ‹V ∈ Use (sourcenode a)› ‹(sourcenode a) -a#as'→⇩c⇩d nx›
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_cdep)
next
case (dep_vars_Cons_ddep V as' as V' a)
from ‹as'' ≠ []› ‹last(targetnodes as'') = n'›
have "n' = last(targetnodes ((a#as)@as''))"
with dep_vars_Cons_ddep
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_ddep)
next
case (dep_vars_Cons_keep V as' as a)
from ‹as'' ≠ []› ‹last(targetnodes as'') = n'›
have "n' = last(targetnodes ((a#as)@as''))"
with dep_vars_Cons_keep
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_keep)
qed
qed

lemma dependent_live_vars_ddep_dependent_live_vars:
assumes "n'' -{V}as''→⇩d⇩d n'" and "(V',as',as) ∈ dependent_live_vars n''"
shows "(V',as',as@as'') ∈ dependent_live_vars n'"
proof -
from ‹n'' -{V}as''→⇩d⇩d n'› have "as'' ≠ []"
by(rule DynPDG_ddep_edge_CFG_path(2))
with ‹n'' -{V}as''→⇩d⇩d n'› have "last(targetnodes as'') = n'"
by(fastforce intro:path_targetnode elim:DynPDG_ddep_edge_CFG_path(1))
from ‹n'' -{V}as''→⇩d⇩d n'› have notExit:"n' ≠ (_Exit_)"
by(fastforce elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
from ‹(V',as',as) ∈ dependent_live_vars n''› show ?thesis
proof(induct rule:dependent_live_vars.induct)
case (dep_vars_Use V')
from ‹V' ∈ Use n''› ‹n'' -{V}as''→⇩d⇩d n'› ‹last(targetnodes as'') = n'› show ?case
by(fastforce intro:dependent_live_vars_ddep_empty_fst simp:targetnodes_def)
next
case (dep_vars_Cons_cdep V' a as' nx asx)
from ‹n'' -{V}as''→⇩d⇩d n'› have "n'' -as''→⇩d* n'" by(rule DynPDG_path_ddep)
with ‹nx -asx→⇩d* n''› have "nx -asx@as''→⇩d* n'"
by -(rule DynPDG_path_Append)
with ‹V' ∈ Use (sourcenode a)› ‹sourcenode a -a#as'→⇩c⇩d nx› notExit
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_cdep)
next
case (dep_vars_Cons_ddep V as' as V' a)
from ‹as'' ≠ []› ‹last(targetnodes as'') = n'›
have "n' = last(targetnodes ((a#as)@as''))"
with dep_vars_Cons_ddep
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_ddep)
next
case (dep_vars_Cons_keep V as' as a)
from ‹as'' ≠ []› ‹last(targetnodes as'') = n'›
have "n' = last(targetnodes ((a#as)@as''))"
with dep_vars_Cons_keep
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_keep)
qed
qed

lemma dependent_live_vars_dep_dependent_live_vars:
"⟦n'' -as''→⇩d* n'; (V',as',as) ∈ dependent_live_vars n''⟧
⟹ (V',as',as@as'') ∈ dependent_live_vars n'"
proof(induct rule:DynPDG_path.induct)
case (DynPDG_path_Nil n) thus ?case by simp
next
case (DynPDG_path_Append_cdep n asx n'' asx' n')
note IH = ‹(V', as', as) ∈ dependent_live_vars n ⟹
(V', as', as @ asx) ∈ dependent_live_vars n''›
from IH[OF ‹(V',as',as) ∈ dependent_live_vars n›]
have "(V',as',as@asx) ∈ dependent_live_vars n''" .
with ‹n'' -asx'→⇩c⇩d n'› have "(V',as',(as@asx)@asx') ∈ dependent_live_vars n'"
by(rule dependent_live_vars_cdep_dependent_live_vars)
thus ?case by simp
next
case (DynPDG_path_Append_ddep n asx n'' V asx' n')
note IH = ‹(V', as', as) ∈ dependent_live_vars n ⟹
(V', as', as @ asx) ∈ dependent_live_vars n''›
from IH[OF ‹(V',as',as) ∈ dependent_live_vars n›]
have "(V',as',as@asx) ∈ dependent_live_vars n''" .
with ‹n'' -{V}asx'→⇩d⇩d n'› have "(V',as',(as@asx)@asx') ∈ dependent_live_vars n'"
by(rule dependent_live_vars_ddep_dependent_live_vars)
thus ?case by simp
qed

end

end
```