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')"
      by(simp add:targetnodes_def)
    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'"
      by(simp add:dyn_data_dependence_def sourcenodes_def)
    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)"
      by(simp add:targetnodes_def)
    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)"
      by(simp add:targetnodes_def)
    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''))"
      by(simp add:targetnodes_def)
    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''))"
      by(simp add:targetnodes_def)
    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''))"
      by(simp add:targetnodes_def)
    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''))"
      by(simp add:targetnodes_def)
    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