Theory DependentLiveVariables

header {*\isaheader{Dependent Live Variables} *}

theory DependentLiveVariables imports DynPDG begin

text {* @{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'->⇘cd⇙ 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'->⇘dd⇙ 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'->⇘dd⇙ 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'->⇘cd⇙ 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'->⇘cd⇙ 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'->⇘cd⇙ 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'->⇘cd⇙ 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'->⇘dd⇙ 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'->⇘dd⇙ 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'->⇘dd⇙ 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'->⇘dd⇙ 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'->⇘dd⇙ 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''->⇘dd⇙ 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''->⇘dd⇙ 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''->⇘dd⇙ n'`
  have all':"∀as' a as''. asx = as'@a#as'' --> ¬ sourcenode a -{V}a#as''->⇘dd⇙ n'"
    and "¬ sourcenode ax -{V}ax#asx->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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''->⇘dd⇙ 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''->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ last(targetnodes (ax#asx))` 
      True `n' = last (targetnodes (ax#asx))`
    have "∀as' a as''. ax#asx = as'@a#as'' --> ¬ sourcenode a -{V}a#as''->⇘dd⇙ 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''->⇘dd⇙ n')" .
    with `¬ sourcenode ax -{V}ax#asx->⇘dd⇙ 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''->⇘dd⇙ 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''->⇘dd⇙ n'))"
by(fastforce intro!:dependent_live_vars_same_pathsD dependent_live_vars_same_pathsI)


lemma dependent_live_vars_cdep_empty_fst:
assumes "n'' -as->⇘cd⇙ n'" and "V' ∈ Use n''"
  shows "(V',[],as) ∈ dependent_live_vars n'"
proof(cases as)
  case Nil
  with `n'' -as->⇘cd⇙ n'` show ?thesis
    by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
next
  case (Cons ax asx)
  with `n'' -as->⇘cd⇙ n'` have "sourcenode ax = n''"
    by(auto dest:DynPDG_cdep_edge_CFG_path elim:path.cases)
  from `n'' -as->⇘cd⇙ n'` have "valid_node n'"
    by(fastforce intro:path_valid_node(2) DynPDG_cdep_edge_CFG_path(1))
  from Cons `n'' -as->⇘cd⇙ n'` have "last(targetnodes as) = n'"
    by(fastforce intro:path_targetnode dest:DynPDG_cdep_edge_CFG_path)
  with Cons `n'' -as->⇘cd⇙ 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->⇘dd⇙ n'" and "V' ∈ Use n''"
  shows "(V',[],as) ∈ dependent_live_vars n'"
proof(cases as)
  case Nil
  with `n'' -{V}as->⇘dd⇙ n'` show ?thesis
    by(fastforce elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
next
  case (Cons ax asx)
  with `n'' -{V}as->⇘dd⇙ n'` have "sourcenode ax = n''"
    by(auto dest:DynPDG_ddep_edge_CFG_path elim:path.cases)
  from Cons `n'' -{V}as->⇘dd⇙ n'` have "last(targetnodes as) = n'"
    by(fastforce intro:path_targetnode elim:DynPDG_ddep_edge_CFG_path(1))
  from Cons `n'' -{V}as->⇘dd⇙ n'` have all:"∀as' a as''. asx = as'@a#as'' -->
                             ¬ sourcenode a -{V}a#as''->⇘dd⇙ n'"
    by(fastforce dest:DynPDG_ddep_edge_no_shorter_ddep_edge)
  from `n'' -{V}as->⇘dd⇙ n'` have "V ∈ Use n'" 
    by(auto elim!:DynPDG_edge.cases simp:dyn_data_dependence_def)
  from Cons `n'' -{V}as->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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''->⇘dd⇙ last(targetnodes (ax#asx@as''))"
    proof
      assume "sourcenode ax -{V}ax#asx@as''->⇘dd⇙ last(targetnodes (ax#asx@as''))"
      hence "sourcenode ax -{V}ax#asx@as''->⇘dd⇙ 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''->⇘cd⇙ n'" and "(V',as',as) ∈ dependent_live_vars n''"
  shows "(V',as',as@as'') ∈ dependent_live_vars n'"
proof -
  from `n'' -as''->⇘cd⇙ n'` have "as'' ≠ []"
    by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
  with `n'' -as''->⇘cd⇙ 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''->⇘cd⇙ 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''->⇘cd⇙ 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'->⇘cd⇙ 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''->⇘dd⇙ n'" and "(V',as',as) ∈ dependent_live_vars n''"
  shows "(V',as',as@as'') ∈ dependent_live_vars n'"
proof -
  from `n'' -{V}as''->⇘dd⇙ n'` have "as'' ≠ []"
    by(rule DynPDG_ddep_edge_CFG_path(2))
  with `n'' -{V}as''->⇘dd⇙ n'` have "last(targetnodes as'') = n'"
    by(fastforce intro:path_targetnode elim:DynPDG_ddep_edge_CFG_path(1))
  from `n'' -{V}as''->⇘dd⇙ 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''->⇘dd⇙ 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''->⇘dd⇙ 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'->⇘cd⇙ 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'->⇘cd⇙ 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'->⇘dd⇙ 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