Theory DynPDG (Isabelle repository snapshot 408271602165 12-Mar-2013)

header {*  \isachapter{Dynamic Slicing} 
  \isaheader{Dynamic Program Dependence Graph} *}

theory DynPDG imports 
  "../Basic/DynDataDependence" 
  "../Basic/CFGExit_wf" 
  "../Basic/DynStandardControlDependence"
  "../Basic/DynWeakControlDependence"
begin

subsection {* The dynamic PDG *}

locale DynPDG = 
  CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
  for sourcenode :: "'edge => 'node" and targetnode :: "'edge => 'node"
  and kind :: "'edge => 'state edge_kind" and valid_edge :: "'edge => bool"
  and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node => 'var set"
  and Use :: "'node => 'var set" and state_val :: "'state => 'var => 'val"
  and Exit :: "'node" ("'('_Exit'_')") +
  fixes dyn_control_dependence :: "'node => 'node => 'edge list => bool" 
("_ controls _ via _" [51,0,0])
  assumes Exit_not_dyn_control_dependent:"n controls n' via as ==> n' ≠ (_Exit_)"
  assumes dyn_control_dependence_path:
  "n controls n' via as  ==> n -as->* n' ∧ as ≠ []"

begin

inductive cdep_edge :: "'node => 'edge list => 'node => bool" 
    ("_ -_->⇘_cd⇙ _" [51,0,0] 80)
  and ddep_edge :: "'node => 'var => 'edge list => 'node => bool"
    ("_ -'{_'}_->⇘_dd⇙ _" [51,0,0,0] 80)
  and DynPDG_edge :: "'node => 'var option => 'edge list => 'node => bool"

where
      -- "Syntax"
  "n -as->⇘_cd⇙ n' == DynPDG_edge n None as n'"
  | "n -{V}as->⇘_dd⇙ n' == DynPDG_edge n (Some V) as n'"

      -- "Rules"
  | DynPDG_cdep_edge:
  "n controls n' via as ==> n -as->⇘_cd⇙ n'"

  | DynPDG_ddep_edge:
  "n influences V in n' via as ==> n -{V}as->⇘_dd⇙ n'"


inductive DynPDG_path :: "'node => 'edge list => 'node => bool"
("_ -_->⇣_d* _" [51,0,0] 80) 

where DynPDG_path_Nil:
  "valid_node n ==> n -[]->⇣_d* n"

  | DynPDG_path_Append_cdep:
  "[|n -as->⇣_d* n''; n'' -as'->⇘_cd⇙ n'|] ==> n -as@as'->⇣_d* n'"

  | DynPDG_path_Append_ddep:
  "[|n -as->⇣_d* n''; n'' -{V}as'->⇘_dd⇙ n'|] ==> n -as@as'->⇣_d* n'"


lemma DynPDG_empty_path_eq_nodes:"n -[]->⇣_d* n' ==> n = n'"
apply - apply(erule DynPDG_path.cases) 
  apply simp
 apply(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)


lemma DynPDG_path_cdep:"n -as->⇘_cd⇙ n' ==> n -as->⇣_d* n'"
apply(subgoal_tac "n -[]@as->⇣_d* n'")
 apply simp
apply(rule DynPDG_path_Append_cdep, rule DynPDG_path_Nil)
by(auto elim!:DynPDG_edge.cases dest:dyn_control_dependence_path path_valid_node)

lemma DynPDG_path_ddep:"n -{V}as->⇘_dd⇙ n' ==> n -as->⇣_d* n'"
apply(subgoal_tac "n -[]@as->⇣_d* n'")
 apply simp
apply(rule DynPDG_path_Append_ddep, rule DynPDG_path_Nil)
by(auto elim!:DynPDG_edge.cases dest:path_valid_node simp:dyn_data_dependence_def)

lemma DynPDG_path_Append:
  "[|n'' -as'->⇣_d* n'; n -as->⇣_d* n''|] ==> n -as@as'->⇣_d* n'"
apply(induct rule:DynPDG_path.induct)
  apply(auto intro:DynPDG_path.intros)
 apply(rotate_tac 1,drule DynPDG_path_Append_cdep,simp+)
apply(rotate_tac 1,drule DynPDG_path_Append_ddep,simp+)
done


lemma DynPDG_path_Exit:"[|n -as->⇣_d* n'; n' = (_Exit_)|] ==> n = (_Exit_)"
apply(induct rule:DynPDG_path.induct)
by(auto elim:DynPDG_edge.cases dest:Exit_not_dyn_control_dependent 
        simp:dyn_data_dependence_def)


lemma DynPDG_path_not_inner:
  "[|n -as->⇣_d* n'; ¬ inner_node n'|] ==> n = n'"
proof(induct rule:DynPDG_path.induct)
  case (DynPDG_path_Nil n)
  thus ?case by simp
next
  case (DynPDG_path_Append_cdep n as n'' as' n')
  from `n'' -as'->⇘_cd⇙ n'` `¬ inner_node n'` have False
    apply -
    apply(erule DynPDG_edge.cases) apply(auto simp:inner_node_def)
      apply(fastforce dest:dyn_control_dependence_path path_valid_node)
     apply(fastforce dest:dyn_control_dependence_path path_valid_node)
    by(fastforce dest:Exit_not_dyn_control_dependent)
  thus ?case by simp
next
  case (DynPDG_path_Append_ddep n as n'' V as' n')
  from `n'' -{V}as'->⇘_dd⇙ n'` `¬ inner_node n'` have False
    apply -
    apply(erule DynPDG_edge.cases) 
    by(auto dest:path_valid_node simp:inner_node_def dyn_data_dependence_def)
  thus ?case by simp
qed


lemma DynPDG_cdep_edge_CFG_path:
  assumes "n -as->⇘_cd⇙ n'" shows "n -as->* n'" and "as ≠ []"
  using `n -as->⇘_cd⇙ n'`
  by(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)

lemma DynPDG_ddep_edge_CFG_path:
  assumes "n -{V}as->⇘_dd⇙ n'" shows "n -as->* n'" and "as ≠ []"
  using `n -{V}as->⇘_dd⇙ n'`
  by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)

lemma DynPDG_path_CFG_path:
  "n -as->⇣_d* n' ==> n -as->* n'"
proof(induct rule:DynPDG_path.induct)
  case DynPDG_path_Nil thus ?case by(rule empty_path)
next
  case (DynPDG_path_Append_cdep n as n'' as' n')
  from `n'' -as'->⇘_cd⇙ n'` have "n'' -as'->* n'"
    by(rule DynPDG_cdep_edge_CFG_path(1))
  with `n -as->* n''` show ?case by(rule path_Append)
next
  case (DynPDG_path_Append_ddep n as n'' V as' n')
  from `n'' -{V}as'->⇘_dd⇙ n'` have "n'' -as'->* n'"
    by(rule DynPDG_ddep_edge_CFG_path(1))
  with `n -as->* n''` show ?case by(rule path_Append)
qed


lemma DynPDG_path_split: 
  "n -as->⇣_d* n' ==>
  (as = [] ∧ n = n') ∨ 
  (∃n'' asx asx'. (n -asx->⇘_cd⇙ n'') ∧ (n'' -asx'->⇣_d* n') ∧ 
        (as = asx@asx')) ∨
  (∃n'' V asx asx'. (n -{V}asx->⇘_dd⇙ n'') ∧ (n'' -asx'->⇣_d* n') ∧ 
        (as = asx@asx'))"
proof(induct rule:DynPDG_path.induct)
  case (DynPDG_path_Nil n) thus ?case by auto
next
  case (DynPDG_path_Append_cdep n as n'' as' n')
  note IH = `as = [] ∧ n = n'' ∨
    (∃nx asx asx'. n -asx->⇘_cd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx') ∨
    (∃nx V asx asx'. n -{V}asx->⇘_dd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx')`
  from IH show ?case
  proof
    assume "as = [] ∧ n = n''"
    with `n'' -as'->⇘_cd⇙ n'` have "valid_node n'"
      by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path 
                        DynPDG_path_cdep)
    with `as = [] ∧ n = n''` `n'' -as'->⇘_cd⇙ n'`
    have "∃n'' asx asx'. n -asx->⇘_cd⇙ n'' ∧ n'' -asx'->⇣_d* n' ∧ as@as' = asx@asx'"
      by(auto intro:DynPDG_path_Nil)
    thus ?thesis by simp
  next
    assume "(∃nx asx asx'. n -asx->⇘_cd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx') ∨
      (∃nx V asx asx'. n -{V}asx->⇘_dd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx')"
    thus ?thesis
    proof
      assume "∃nx asx asx'. n -asx->⇘_cd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx'"
      then obtain nx asx asx' where "n -asx->⇘_cd⇙ nx" and "nx -asx'->⇣_d* n''"
        and "as = asx@asx'" by auto
      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(fastforce intro:DynPDG_path_Append)
      with `n -asx->⇘_cd⇙ nx` `as = asx@asx'`
      have "∃n'' asx asx'. n -asx->⇘_cd⇙ n'' ∧ n'' -asx'->⇣_d* n' ∧ as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    next
      assume "∃nx V asx asx'. n -{V}asx->⇘_dd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx'"
      then obtain nx V asx asx' where "n -{V}asx->⇘_dd⇙ nx" and "nx -asx'->⇣_d* n''"
        and "as = asx@asx'" by auto
      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(fastforce intro:DynPDG_path_Append)
      with `n -{V}asx->⇘_dd⇙ nx` `as = asx@asx'`
      have "∃n'' V asx asx'. n -{V}asx->⇘_dd⇙ n'' ∧ n'' -asx'->⇣_d* n' ∧ as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    qed
  qed
next
  case (DynPDG_path_Append_ddep n as n'' V as' n')
  note IH = `as = [] ∧ n = n'' ∨
    (∃nx asx asx'. n -asx->⇘_cd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx') ∨
    (∃nx V asx asx'. n -{V}asx->⇘_dd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx')`
  from IH show ?case
  proof
    assume "as = [] ∧ n = n''"
    with `n'' -{V}as'->⇘_dd⇙ n'` have "valid_node n'"
      by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path 
                        DynPDG_path_ddep)
    with `as = [] ∧ n = n''` `n'' -{V}as'->⇘_dd⇙ n'`
    have "∃n'' V asx asx'. n -{V}asx->⇘_dd⇙ n'' ∧ n'' -asx'->⇣_d* n' ∧ as@as' = asx@asx'"
      by(fastforce intro:DynPDG_path_Nil)
    thus ?thesis by simp
  next
    assume "(∃nx asx asx'. n -asx->⇘_cd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx') ∨
      (∃nx V asx asx'. n -{V}asx->⇘_dd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx')"
    thus ?thesis
    proof
      assume "∃nx asx asx'. n -asx->⇘_cd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx'"
      then obtain nx asx asx' where "n -asx->⇘_cd⇙ nx" and "nx -asx'->⇣_d* n''"
        and "as = asx@asx'" by auto
      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(fastforce intro:DynPDG_path_Append)
      with `n -asx->⇘_cd⇙ nx` `as = asx@asx'`
      have "∃n'' asx asx'. n -asx->⇘_cd⇙ n'' ∧ n'' -asx'->⇣_d* n' ∧ as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    next
      assume "∃nx V asx asx'. n -{V}asx->⇘_dd⇙ nx ∧ nx -asx'->⇣_d* n'' ∧ as = asx@asx'"
      then obtain nx V' asx asx' where "n -{V'}asx->⇘_dd⇙ nx" and "nx -asx'->⇣_d* n''"
        and "as = asx@asx'" by auto
      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(fastforce intro:DynPDG_path_Append)
      with `n -{V'}asx->⇘_dd⇙ nx` `as = asx@asx'`
      have "∃n'' V asx asx'. n -{V}asx->⇘_dd⇙ n'' ∧ n'' -asx'->⇣_d* n' ∧ as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    qed
  qed
qed


lemma DynPDG_path_rev_cases [consumes 1,
  case_names DynPDG_path_Nil DynPDG_path_cdep_Append DynPDG_path_ddep_Append]:
  "[|n -as->⇣_d* n'; [|as = []; n = n'|] ==> Q;
    !!n'' asx asx'. [|n -asx->⇘_cd⇙ n''; n'' -asx'->⇣_d* n'; 
                       as = asx@asx'|] ==> Q;
    !!V n'' asx asx'. [|n -{V}asx->⇘_dd⇙ n''; n'' -asx'->⇣_d* n'; 
                       as = asx@asx'|] ==> Q|]
  ==> Q"
by(blast dest:DynPDG_path_split)



lemma DynPDG_ddep_edge_no_shorter_ddep_edge:
  assumes ddep:"n -{V}as->⇘_dd⇙ n'"
  shows "∀as' a as''. tl as = as'@a#as'' --> ¬ sourcenode a -{V}a#as''->⇘_dd⇙ n'"
proof -
  from ddep have influence:"n influences V in n' via as"
    by(auto elim!:DynPDG_edge.cases)
  then obtain  a asx where as:"as = a#asx"
    and notin:"n ∉ set (sourcenodes asx)"
    by(auto dest:dyn_influence_source_notin_tl_edges simp:dyn_data_dependence_def)
  from influence as
  have imp:"∀nx ∈ set (sourcenodes asx). V ∉ Def nx"
    by(auto simp:dyn_data_dependence_def)
  { fix as' a' as'' 
    assume eq:"tl as = as'@a'#as''"
      and ddep':"sourcenode a' -{V}a'#as''->⇘_dd⇙ n'"
    from eq as notin have noteq:"sourcenode a' ≠ n" by(auto simp:sourcenodes_def)
    from ddep' have "V ∈ Def (sourcenode a')"
      by(auto elim!:DynPDG_edge.cases simp:dyn_data_dependence_def)
    with eq as noteq imp have False by(auto simp:sourcenodes_def) }
  thus ?thesis by blast
qed



lemma no_ddep_same_state:
  assumes path:"n -as->* n'" and Uses:"V ∈ Use n'" and preds:"preds (kinds as) s"
  and no_dep:"∀as' a as''. as = as'@a#as'' --> ¬ sourcenode a -{V}a#as''->⇘_dd⇙ n'"
  shows "state_val (transfers (kinds as) s) V = state_val s V"
proof -
  { fix n''
    assume inset:"n'' ∈ set (sourcenodes as)" and Defs:"V ∈ Def n''"
    hence "∃nx ∈ set (sourcenodes as). V ∈ Def nx" by auto
    then obtain nx ns' ns'' where nodes:"sourcenodes as = ns'@nx#ns''"
        and Defs':"V ∈ Def nx" and notDef:"∀nx' ∈ set ns''. V ∉ Def nx'"
      by(fastforce elim!:rightmost_element_property)
    from nodes obtain as' a as''
      where as'':"sourcenodes as'' = ns''" and as:"as=as'@a#as''"
      and source:"sourcenode a = nx"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    from as path have path':"sourcenode a -a#as''->* n'"
      by(fastforce dest:path_split_second)
    from notDef as'' source
    have "∀n'' ∈ set (sourcenodes as''). V ∉ Def n''"
      by(auto simp:sourcenodes_def)
    with path' Defs' Uses source
    have influence:"nx influences V in n' via (a#as'')"
      by(simp add:dyn_data_dependence_def)
    hence "nx ∉ set (sourcenodes as'')" by(rule dyn_influence_source_notin_tl_edges)
    with influence source
    have "∃asx a'. sourcenode a' -{V}a'#asx->⇘_dd⇙ n' ∧ sourcenode a' = nx ∧
          (∃asx'. a#as'' = asx'@a'#asx)"
      by(fastforce intro:DynPDG_ddep_edge)
    with nodes no_dep as have False by(auto simp:sourcenodes_def) }
  hence "∀n ∈ set (sourcenodes as). V ∉ Def n" by auto
  with wf path preds show ?thesis by(fastforce intro:CFG_path_no_Def_equal)
qed


lemma DynPDG_ddep_edge_only_first_edge:
  "[|n -{V}a#as->⇘_dd⇙ n'; preds (kinds (a#as)) s|] ==> 
    state_val (transfers (kinds (a#as)) s) V = state_val (transfer (kind a) s) V"
  apply -
  apply(erule DynPDG_edge.cases)
  apply auto
  apply(frule dyn_influence_Cons_source)
  apply(frule dyn_influence_source_notin_tl_edges)
  by(erule dyn_influence_only_first_edge)


lemma Use_value_change_implies_DynPDG_ddep_edge:
  assumes "n -as->* n'" and "V ∈ Use n'" and "preds (kinds as) s" 
  and "preds (kinds as) s'" and "state_val s V = state_val s' V"
  and "state_val (transfers (kinds as) s) V ≠ 
             state_val (transfers (kinds as) s') V"
  obtains as' a as'' where "as = as'@a#as''"
  and "sourcenode a -{V}a#as''->⇘_dd⇙ n'"
  and "state_val (transfers (kinds as) s) V = 
       state_val (transfers (kinds (as'@[a])) s) V"
  and "state_val (transfers (kinds as) s') V = 
       state_val (transfers (kinds (as'@[a])) s') V"
proof(atomize_elim)
  show "∃as' a as''. as = as'@a#as'' ∧
                     sourcenode a -{V}a#as''->⇘_dd⇙ n' ∧
             state_val (transfers (kinds as) s) V = 
             state_val (transfers (kinds (as'@[a])) s) V ∧
             state_val (transfers (kinds as) s') V = 
             state_val (transfers (kinds (as'@[a])) s') V"
  proof(cases "∀as' a as''. as = as'@a#as'' -->
                 ¬ sourcenode a -{V}a#as''->⇘_dd⇙ n'")
    case True
    with `n -as->* n'` `V ∈ Use n'` `preds (kinds as) s` `preds (kinds as) s'`
    have "state_val (transfers (kinds as) s) V = state_val s V"
      and "state_val (transfers (kinds as) s') V = state_val s' V"
      by(auto intro:no_ddep_same_state)
    with `state_val s V = state_val s' V` 
      `state_val (transfers (kinds as) s) V ≠ state_val (transfers (kinds as) s') V`
    show ?thesis by simp
  next
    case False
    then obtain as' a as'' where [simp]:"as = as'@a#as''"
      and "sourcenode a -{V}a#as''->⇘_dd⇙ n'" by auto
    from `preds (kinds as) s` have "preds (kinds (a#as'')) (transfers (kinds as') s)"
      by(simp add:kinds_def preds_split)
    with `sourcenode a -{V}a#as''->⇘_dd⇙ n'` have all:
      "state_val (transfers (kinds (a#as'')) (transfers (kinds as') s)) V = 
       state_val (transfer (kind a) (transfers (kinds as') s)) V"
      by(auto dest!:DynPDG_ddep_edge_only_first_edge)
    from `preds (kinds as) s'` 
    have "preds (kinds (a#as'')) (transfers (kinds as') s')"
      by(simp add:kinds_def preds_split)
    with `sourcenode a -{V}a#as''->⇘_dd⇙ n'` have all':
      "state_val (transfers (kinds (a#as'')) (transfers (kinds as') s')) V = 
       state_val (transfer (kind a) (transfers (kinds as') s')) V"
      by(auto dest!:DynPDG_ddep_edge_only_first_edge)
    hence eq:"!!s. transfers (kinds as) s =
      transfers (kinds (a#as'')) (transfers (kinds as') s)"
      by(simp add:transfers_split[THEN sym] kinds_def)
    with all have "state_val (transfers (kinds as) s) V = 
                   state_val (transfers (kinds (as'@[a])) s) V"
      by(simp add:transfers_split kinds_def)
    moreover
    from eq all' have "state_val (transfers (kinds as) s') V = 
                       state_val (transfers (kinds (as'@[a])) s') V"
      by(simp add:transfers_split kinds_def)
    ultimately show ?thesis using `sourcenode a -{V}a#as''->⇘_dd⇙ n'` by simp blast
  qed
qed


end


subsection {* Instantiate dynamic PDG *}

subsubsection {* Standard control dependence *}

locale DynStandardControlDependencePDG =
  Postdomination sourcenode targetnode kind valid_edge Entry Exit +
  CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
  for sourcenode :: "'edge => 'node" and targetnode :: "'edge => 'node"
  and kind :: "'edge => 'state edge_kind" and valid_edge :: "'edge => bool"
  and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node => 'var set"
  and Use :: "'node => 'var set" and state_val :: "'state => 'var => 'val"
  and Exit :: "'node" ("'('_Exit'_')")

begin

lemma DynPDG_scd:
  "DynPDG sourcenode targetnode kind valid_edge (_Entry_) 
          Def Use state_val (_Exit_) dyn_standard_control_dependence"
proof(unfold_locales)
  fix n n' as assume "n controls⇣_s n' via as"
  show "n' ≠ (_Exit_)"
  proof
    assume "n' = (_Exit_)"
    with `n controls⇣_s n' via as` show False
      by(fastforce intro:Exit_not_dyn_standard_control_dependent)
  qed
next
  fix n n' as assume "n controls⇣_s n' via as"
  thus "n -as->* n' ∧ as ≠ []"
    by(fastforce simp:dyn_standard_control_dependence_def)
qed


end

subsubsection {* Weak control dependence *}

locale DynWeakControlDependencePDG = 
  StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit +
  CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
  for sourcenode :: "'edge => 'node" and targetnode :: "'edge => 'node"
  and kind :: "'edge => 'state edge_kind" and valid_edge :: "'edge => bool"
  and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node => 'var set"
  and Use :: "'node => 'var set" and state_val :: "'state => 'var => 'val"
  and Exit :: "'node" ("'('_Exit'_')")

begin

lemma DynPDG_wcd:
  "DynPDG sourcenode targetnode kind valid_edge (_Entry_) 
          Def Use state_val (_Exit_) dyn_weak_control_dependence"
proof(unfold_locales)
  fix n n' as assume "n weakly controls n' via as"
  show "n' ≠ (_Exit_)"
  proof
    assume "n' = (_Exit_)"
    with `n weakly controls n' via as` show False
      by(fastforce intro:Exit_not_dyn_weak_control_dependent)
  qed
next
  fix n n' as assume "n weakly controls n' via as"
  thus "n -as->* n' ∧ as ≠ []"
    by(fastforce simp:dyn_weak_control_dependence_def)
qed


end


subsection {* Data slice *}

definition (in CFG) empty_control_dependence :: "'node => 'node => 'edge list => bool"
where "empty_control_dependence n n' as ≡ False"

lemma (in CFGExit_wf) DynPDG_scd:
  "DynPDG sourcenode targetnode kind valid_edge (_Entry_)
          Def Use state_val  (_Exit_) empty_control_dependence"
proof(unfold_locales)
  fix n n' as assume "empty_control_dependence n n' as"
  thus "n' ≠ (_Exit_)" by(simp add:empty_control_dependence_def)
next
  fix n n' as assume "empty_control_dependence n n' as"
  thus "n -as->* n' ∧ as ≠ []" by(simp add:empty_control_dependence_def)
qed

end