Theory Slicing.CDepInstantiations

section ‹Instantiate framework with control dependences›

theory CDepInstantiations imports 
  Slice 
  PDG 
  WeakOrderDependence 
begin

subsection‹Standard control dependence›

context StandardControlDependencePDG begin

lemma Exit_in_obs_slice_node:"(_Exit_)  obs n' (PDG_BS S)  (_Exit_)  S"
  by(auto elim:obsE PDG_path_CFG_path simp:PDG_BS_def split:if_split_asm)


abbreviation PDG_path' :: "'node  'node  bool" ("_ d* _" [51,0] 80)
  where "n d* n'  PDG.PDG_path sourcenode targetnode valid_edge Def Use
  standard_control_dependence n n'"

lemma cd_closed:
  "n'  PDG_BS S; n controlss n'  n  PDG_BS S"
  by(simp add:PDG_BS_def)(blast dest:PDG_cdep_edge PDG_path_Append PDG_path_cdep)


lemma obs_postdominate:
  assumes "n  obs n' (PDG_BS S)" and "n  (_Exit_)" shows "n postdominates n'"
proof(rule ccontr)
  assume "¬ n postdominates n'"
  from n  obs n' (PDG_BS S) have "valid_node n" by(fastforce dest:in_obs_valid)
  with n  obs n' (PDG_BS S) n  (_Exit_) have "n postdominates n"
    by(fastforce intro:postdominate_refl)
  from n  obs n' (PDG_BS S) obtain as where "n' -as→* n"
    and "n'  set(sourcenodes as). n'  (PDG_BS S)"
    and "n  (PDG_BS S)" by(erule obsE)
  from n postdominates n ¬ n postdominates n' n' -as→* n
  obtain as' a as'' where [simp]:"as = as'@a#as''" and "valid_edge a"
    and "¬ n postdominates (sourcenode a)" and "n postdominates (targetnode a)"
    by -(erule postdominate_path_branch)
  from ¬ n postdominates (sourcenode a) valid_edge a valid_node n
  obtain asx  where "sourcenode a -asx→* (_Exit_)"
    and "n  set(sourcenodes asx)" by(auto simp:postdominate_def)
  from sourcenode a -asx→* (_Exit_) valid_edge a
  obtain ax asx' where [simp]:"asx = ax#asx'"
    apply - apply(erule path.cases)
    apply(drule_tac s="(_Exit_)" in sym)
    apply simp
    apply(drule Exit_source)
    by simp_all
  with sourcenode a -asx→* (_Exit_) have "sourcenode a -[]@ax#asx'→* (_Exit_)" 
    by simp
  hence "valid_edge ax" and [simp]:"sourcenode a = sourcenode ax"
    and "targetnode ax -asx'→* (_Exit_)"
    by(fastforce dest:path_split)+
  with n  set(sourcenodes asx) have "¬ n postdominates targetnode ax"
    by(fastforce simp:postdominate_def sourcenodes_def)
  from n  obs n' (PDG_BS S) n'  set(sourcenodes as). n'  (PDG_BS S)
  have "n  set (sourcenodes (a#as''))"
    by(fastforce elim:obs.cases simp:sourcenodes_def)
  from n' -as→* n have "sourcenode a -a#as''→* n"
    by(fastforce dest:path_split_second)
  with n postdominates (targetnode a) ¬ n postdominates targetnode ax
    valid_edge ax n  set (sourcenodes (a#as''))
  have "sourcenode a controlss n" by(fastforce simp:standard_control_dependence_def)
  with n  obs n' (PDG_BS S) have "sourcenode a  (PDG_BS S)"
    by(fastforce intro:cd_closed PDG_cdep_edge elim:obs.cases)
  with n'  set(sourcenodes as). n'  (PDG_BS S) 
  show False by(simp add:sourcenodes_def)
qed


lemma obs_singleton:"(m. obs n (PDG_BS S) = {m})  obs n (PDG_BS S) = {}"
proof(rule ccontr)
  assume "¬ ((m. obs n (PDG_BS S) = {m})  obs n (PDG_BS S) = {})"
  hence "nx nx'. nx  obs n (PDG_BS S)  nx'  obs n (PDG_BS S) 
    nx  nx'" by auto
  then obtain nx nx' where "nx  obs n (PDG_BS S)" and "nx'  obs n (PDG_BS S)"
    and "nx  nx'" by auto
  from nx  obs n (PDG_BS S) obtain as where "n -as→* nx" 
    and "n'  set(sourcenodes as). n'  (PDG_BS S)" and "nx  (PDG_BS S)" 
    by(erule obsE)
  from n -as→* nx have "valid_node nx" by(fastforce dest:path_valid_node)
  with nx  (PDG_BS S) have "obs nx (PDG_BS S) = {nx}" by -(rule n_in_obs)
  with n -as→* nx nx  obs n (PDG_BS S) nx'  obs n (PDG_BS S) nx  nx'
  have "as  []" by(fastforce elim:path.cases)
  with n -as→* nx nx  obs n (PDG_BS S) nx'  obs n (PDG_BS S) 
    nx  nx' obs nx (PDG_BS S) = {nx} n'  set(sourcenodes as). n'  (PDG_BS S)
  have "a as' as''. n -as'→* sourcenode a  targetnode a -as''→* nx 
                     valid_edge a  as = as'@a#as''  
                     obs (targetnode a) (PDG_BS S) = {nx}  
                    (¬ (m. obs (sourcenode a) (PDG_BS S) = {m}  
                       obs (sourcenode a) (PDG_BS S) = {}))"
  proof(induct arbitrary:nx' rule:path.induct)
    case (Cons_path n'' as n' a n)
    note [simp] = sourcenode a = n[THEN sym] targetnode a = n''[THEN sym]
    note more_than_one = n'  obs n (PDG_BS S) nx'  obs n (PDG_BS S) n'  nx'
    note IH = nx'. n'  obs n'' (PDG_BS S); nx'  obs n'' (PDG_BS S); n'  nx'; 
      obs n' (PDG_BS S) = {n'}; n'set (sourcenodes as). n'  (PDG_BS S); as  []
       a as' as''. n'' -as'→* sourcenode a  targetnode a -as''→* n' 
      valid_edge a  as = as'@a#as''  obs (targetnode a) (PDG_BS S) = {n'} 
      (¬ (m. obs (sourcenode a) (PDG_BS S) = {m}  
      obs (sourcenode a) (PDG_BS S) = {}))
    from n'set (sourcenodes (a#as)). n'  (PDG_BS S)
    have "n'set (sourcenodes as). n'  (PDG_BS S)" and "sourcenode a  (PDG_BS S)"
      by(simp_all add:sourcenodes_def)
    show ?case
    proof(cases "as = []")
      case True
      with n'' -as→* n' have [simp]:"n' = n''" by(fastforce elim:path.cases)
      from more_than_one
      have "¬ (m. obs (sourcenode a) (PDG_BS S) = {m}  
               obs (sourcenode a) (PDG_BS S) = {})"
        by auto
      with obs n' (PDG_BS S) = {n'} True valid_edge a show ?thesis
        apply(rule_tac x="a" in exI)
        apply(rule_tac x="[]" in exI)
        apply(rule_tac x="[]" in exI)
        by(auto intro!:empty_path)
    next
      case False
      hence "as  []" .
      from n'' -as→* n' n'set (sourcenodes as). n'  (PDG_BS S) 
      have "obs n' (PDG_BS S)  obs n'' (PDG_BS S)" by(rule path_obs_subset)
      show ?thesis
      proof(cases "obs n' (PDG_BS S) = obs n'' (PDG_BS S)")
        case True
        with n'' -as→* n' valid_edge a obs n' (PDG_BS S) = {n'} more_than_one
        show ?thesis
          apply(rule_tac x="a" in exI)
          apply(rule_tac x="[]" in exI)
          apply(rule_tac x="as" in exI)
          by(fastforce intro:empty_path)
      next
        case False
        with obs n' (PDG_BS S)  obs n'' (PDG_BS S)
        have "obs n' (PDG_BS S)  obs n'' (PDG_BS S)" by simp
        with obs n' (PDG_BS S) = {n'} obtain ni where "n'  obs n'' (PDG_BS S)"
          and "ni  obs n'' (PDG_BS S)" and "n'  ni" by auto
        from IH[OF this obs n' (PDG_BS S) = {n'} 
          n'set (sourcenodes as). n'  (PDG_BS S) as  []] obtain a' as' as''
          where "n'' -as'→* sourcenode a'" and "targetnode a' -as''→* n'"
          and "valid_edge a'" and [simp]:"as = as'@a'#as''" 
          and "obs (targetnode a') (PDG_BS S) = {n'}"
          and more_than_one':"¬ (m. obs (sourcenode a') (PDG_BS S) = {m}  
          obs (sourcenode a') (PDG_BS S) = {})"
          by blast
        from n'' -as'→* sourcenode a' valid_edge a
        have "n -a#as'→* sourcenode a'" by(fastforce intro:path.Cons_path)
        with targetnode a' -as''→* n' obs (targetnode a') (PDG_BS S) = {n'}
          more_than_one' valid_edge a' show ?thesis
          apply(rule_tac x="a'" in exI)
          apply(rule_tac x="a#as'" in exI)
          apply(rule_tac x="as''" in exI)
          by fastforce
      qed
    qed
  qed simp
  then obtain a as' as'' where "valid_edge a"
    and "obs (targetnode a) (PDG_BS S) = {nx}"
    and more_than_one:"¬ (m. obs (sourcenode a) (PDG_BS S) = {m}  
                         obs (sourcenode a) (PDG_BS S) = {})"
    by blast
  have "sourcenode a  (PDG_BS S)"
  proof(rule ccontr)
    assume "¬ sourcenode a  PDG_BS S"
    hence "sourcenode a  PDG_BS S" by simp
    with valid_edge a have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
      by(fastforce intro!:n_in_obs)
    with more_than_one show False by simp
  qed
  with valid_edge a 
  have "obs (targetnode a) (PDG_BS S)  obs (sourcenode a) (PDG_BS S)"
    by(rule edge_obs_subset)
  with obs (targetnode a) (PDG_BS S) = {nx} 
  have "nx  obs (sourcenode a) (PDG_BS S)" by simp
  with more_than_one obtain m  where "m  obs (sourcenode a) (PDG_BS S)"
    and "nx  m" by auto
  from m  obs (sourcenode a) (PDG_BS S) 
  have "valid_node m" by(fastforce dest:in_obs_valid)
  from obs (targetnode a) (PDG_BS S) = {nx} have "valid_node nx" 
    by(fastforce dest:in_obs_valid)
  show False
  proof(cases "m postdominates (sourcenode a)")
    case True
    with nx  obs (sourcenode a) (PDG_BS S) m  obs (sourcenode a) (PDG_BS S)
    have "m postdominates nx"
      by(fastforce intro:postdominate_path_targetnode elim:obs.cases)
    with nx  m have "¬ nx postdominates m" by(fastforce dest:postdominate_antisym)
    have "(_Exit_) -[]→* (_Exit_)" by(fastforce intro:empty_path)
    with m postdominates nx have "nx  (_Exit_)"
      by(fastforce simp:postdominate_def sourcenodes_def)
    have "¬ nx postdominates (sourcenode a)"
    proof(rule ccontr)
      assume "¬ ¬ nx postdominates sourcenode a"
      hence "nx postdominates sourcenode a" by simp
      from m  obs (sourcenode a) (PDG_BS S) nx  obs (sourcenode a) (PDG_BS S)
      obtain asx' where "sourcenode a -asx'→* m" and "nx  set(sourcenodes asx')"
        by(fastforce elim:obs.cases)
      with nx postdominates sourcenode a have "nx postdominates m"
        by(rule postdominate_path_targetnode)
      with ¬ nx postdominates m show False by simp
    qed
    with nx  obs (sourcenode a) (PDG_BS S) valid_node nx nx  (_Exit_) 
    show False by(fastforce dest:obs_postdominate)
  next
    case False
    show False
    proof(cases "m = Exit")
      case True
      from m  obs (sourcenode a) (PDG_BS S) nx  obs (sourcenode a) (PDG_BS S)
      obtain xs where "sourcenode a -xs→* m" and "nx  set(sourcenodes xs)"
        by(fastforce elim:obsE)
      obtain x' xs' where [simp]:"xs = x'#xs'"
      proof(cases xs)
        case Nil
        with sourcenode a -xs→* m have [simp]:"sourcenode a = m" by fastforce
        with m  obs (sourcenode a) (PDG_BS S) 
        have "m  (PDG_BS S)" by(metis obsE)
        with valid_node m have "obs m (PDG_BS S) = {m}"
          by(rule n_in_obs)
        with nx  obs (sourcenode a) (PDG_BS S) nx  m have False
          by fastforce
        thus ?thesis by simp
      qed blast
      from sourcenode a -xs→* m have "sourcenode a = sourcenode x'" 
        and "valid_edge x'" and "targetnode x' -xs'→* m"
        by(auto elim:path_split_Cons)
      from targetnode x' -xs'→* m nx  set(sourcenodes xs) valid_edge x' 
        valid_node m True
      have "¬ nx postdominates (targetnode x')" 
        by(fastforce simp:postdominate_def sourcenodes_def)
      from nx  m True have "nx  (_Exit_)" by simp
      with obs (targetnode a) (PDG_BS S) = {nx}
      have "nx postdominates (targetnode a)"
        by(fastforce intro:obs_postdominate)
      from obs (targetnode a) (PDG_BS S) = {nx}
      obtain ys where "targetnode a -ys→* nx" 
        and "nx'  set(sourcenodes ys). nx'  (PDG_BS S)"
        and "nx  (PDG_BS S)" by(fastforce elim:obsE)
      hence "nx  set(sourcenodes ys)"by fastforce
      have "sourcenode a  nx"
      proof
        assume "sourcenode a = nx"
        from nx  obs (sourcenode a) (PDG_BS S)
        have "nx  (PDG_BS S)" by -(erule obsE)
        with valid_node nx have "obs nx (PDG_BS S) = {nx}" by -(erule n_in_obs)
        with sourcenode a = nx m  obs (sourcenode a) (PDG_BS S) 
          nx  m show False by fastforce
      qed
      with nx  set(sourcenodes ys) have "nx  set(sourcenodes (a#ys))"
        by(fastforce simp:sourcenodes_def)
      from valid_edge a targetnode a -ys→* nx
      have "sourcenode a -a#ys→* nx" by(fastforce intro:Cons_path)
      from sourcenode a -a#ys→* nx nx  set(sourcenodes (a#ys))
        nx postdominates (targetnode a) valid_edge x'
        ¬ nx postdominates (targetnode x') sourcenode a = sourcenode x'
      have "(sourcenode a) controlss nx"
        by(fastforce simp:standard_control_dependence_def)
      with nx  (PDG_BS S) have "sourcenode a  (PDG_BS S)"
        by(rule cd_closed)
      with valid_edge a have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
        by(fastforce intro!:n_in_obs)
      with m  obs (sourcenode a) (PDG_BS S)
        nx  obs (sourcenode a) (PDG_BS S) nx  m
      show False by simp
    next
      case False
      with m  obs (sourcenode a) (PDG_BS S) valid_node m
        ¬ m postdominates sourcenode a 
      show False by(fastforce dest:obs_postdominate)
    qed
  qed
qed


lemma PDGBackwardSliceCorrect:
  "BackwardSlice sourcenode targetnode kind valid_edge
        (_Entry_) Def Use state_val PDG_BS"
proof(unfold_locales)
  fix n S assume "n  PDG_BS S"
  thus "valid_node n" by(rule PDG_BS_valid_node)
next
  fix n S assume "valid_node n" and "n  S"
  thus "n  PDG_BS S" by(fastforce intro:PDG_path_Nil simp:PDG_BS_def)
next
  fix n' S n V
  assume "n'  PDG_BS S" and "n influences V in n'"
  thus "n  PDG_BS S"
    by(auto dest:PDG.PDG_path_ddep[OF PDG_scd,OF PDG.PDG_ddep_edge[OF PDG_scd]]
            dest:PDG_path_Append simp:PDG_BS_def split:if_split_asm)
next
  fix n S
  have "(m. obs n (PDG_BS S) = {m})  obs n (PDG_BS S) = {}" 
    by(rule obs_singleton)
  thus "finite (obs n (PDG_BS S))" by fastforce
next
  fix n S
  have "(m. obs n (PDG_BS S) = {m})  obs n (PDG_BS S) = {}" 
    by(rule obs_singleton)
  thus "card (obs n (PDG_BS S))  1" by fastforce
qed

end


subsection‹Weak control dependence›

context WeakControlDependencePDG begin

lemma Exit_in_obs_slice_node:"(_Exit_)  obs n' (PDG_BS S)  (_Exit_)  S"
  by(auto elim:obsE PDG_path_CFG_path simp:PDG_BS_def split:if_split_asm)


lemma cd_closed:
  "n'  PDG_BS S; n weakly controls n'  n  PDG_BS S"
  by(simp add:PDG_BS_def)(blast dest:PDG_cdep_edge PDG_path_Append PDG_path_cdep)


lemma obs_strong_postdominate:
  assumes "n  obs n' (PDG_BS S)" and "n  (_Exit_)" 
  shows "n strongly-postdominates n'"
proof(rule ccontr)
  assume "¬ n strongly-postdominates n'"
  from n  obs n' (PDG_BS S) have "valid_node n" by(fastforce dest:in_obs_valid)
  with n  obs n' (PDG_BS S) n  (_Exit_) have "n strongly-postdominates n"
    by(fastforce intro:strong_postdominate_refl)
  from n  obs n' (PDG_BS S) obtain as where "n' -as→* n"
    and "n'  set(sourcenodes as). n'  (PDG_BS S)"
    and "n  (PDG_BS S)" by(erule obsE)
  from n strongly-postdominates n ¬ n strongly-postdominates n' n' -as→* n
  obtain as' a as'' where [simp]:"as = as'@a#as''" and "valid_edge a"
    and "¬ n strongly-postdominates (sourcenode a)" and 
    "n strongly-postdominates (targetnode a)"
    by -(erule strong_postdominate_path_branch)
  from n  obs n' (PDG_BS S) n'  set(sourcenodes as). n'  (PDG_BS S) 
  have "n  set (sourcenodes (a#as''))"
    by(fastforce elim:obs.cases simp:sourcenodes_def)
  from n' -as→* n have "sourcenode a -a#as''→* n"
    by(fastforce dest:path_split_second)
  from ¬ n strongly-postdominates (sourcenode a) valid_edge a valid_node n
  obtain a' where "sourcenode a' = sourcenode a"
    and "valid_edge a'" and "¬ n strongly-postdominates (targetnode a')"
    by(fastforce elim:not_strong_postdominate_predecessor_successor)
  with n strongly-postdominates (targetnode a) n  set (sourcenodes (a#as''))
    sourcenode a -a#as''→* n
  have "sourcenode a weakly controls n"
    by(fastforce simp:weak_control_dependence_def)
  with n  obs n' (PDG_BS S) have "sourcenode a  (PDG_BS S)"
    by(fastforce intro:cd_closed PDG_cdep_edge elim:obs.cases)
  with n'  set(sourcenodes as). n'  (PDG_BS S)
  show False by(simp add:sourcenodes_def)
qed


lemma obs_singleton:"(m. obs n (PDG_BS S) = {m})  obs n (PDG_BS S) = {}"
proof(rule ccontr)
  assume "¬ ((m. obs n (PDG_BS S) = {m})  obs n (PDG_BS S) = {})"
  hence "nx nx'. nx  obs n (PDG_BS S)  nx'  obs n (PDG_BS S) 
    nx  nx'" by auto
  then obtain nx nx' where "nx  obs n (PDG_BS S)" and "nx'  obs n (PDG_BS S)"
    and "nx  nx'" by auto
  from nx  obs n (PDG_BS S) obtain as where "n -as→* nx" 
    and "n'  set(sourcenodes as). n'  (PDG_BS S)" and "nx  (PDG_BS S)" 
    by(erule obsE)
  from n -as→* nx have "valid_node nx" by(fastforce dest:path_valid_node)
  with nx  (PDG_BS S) have "obs nx (PDG_BS S) = {nx}" by -(rule n_in_obs)
  with n -as→* nx nx  obs n (PDG_BS S) nx'  obs n (PDG_BS S) nx  nx'
  have "as  []" by(fastforce elim:path.cases)
  with n -as→* nx nx  obs n (PDG_BS S) nx'  obs n (PDG_BS S) 
    nx  nx' obs nx (PDG_BS S) = {nx} n'  set(sourcenodes as). n'  (PDG_BS S)
  have "a as' as''. n -as'→* sourcenode a  targetnode a -as''→* nx 
                     valid_edge a  as = as'@a#as''  
                     obs (targetnode a) (PDG_BS S) = {nx}  
                    (¬ (m. obs (sourcenode a) (PDG_BS S) = {m}  
                       obs (sourcenode a) (PDG_BS S) = {}))"
  proof(induct arbitrary:nx' rule:path.induct)
    case (Cons_path n'' as n' a n)
    note [simp] = sourcenode a = n[THEN sym] targetnode a = n''[THEN sym]
    note more_than_one = n'  obs n (PDG_BS S) nx'  obs n (PDG_BS S) n'  nx'
    note IH = nx'. n'  obs n'' (PDG_BS S); nx'  obs n'' (PDG_BS S); n'  nx'; 
      obs n' (PDG_BS S) = {n'}; n'set (sourcenodes as). n'  (PDG_BS S); as  []
       a as' as''. n'' -as'→* sourcenode a  targetnode a -as''→* n' 
      valid_edge a  as = as'@a#as''  obs (targetnode a) (PDG_BS S) = {n'} 
      (¬ (m. obs (sourcenode a) (PDG_BS S) = {m}  
      obs (sourcenode a) (PDG_BS S) = {}))
    from n'set (sourcenodes (a#as)). n'  (PDG_BS S)
    have "n'set (sourcenodes as). n'  (PDG_BS S)" and "sourcenode a  (PDG_BS S)"
      by(simp_all add:sourcenodes_def)
    show ?case
    proof(cases "as = []")
      case True
      with n'' -as→* n' have [simp]:"n' = n''" by(fastforce elim:path.cases)
      from more_than_one
      have "¬ (m. obs (sourcenode a) (PDG_BS S) = {m}  
               obs (sourcenode a) (PDG_BS S) = {})"
        by auto
      with obs n' (PDG_BS S) = {n'} True valid_edge a show ?thesis
        apply(rule_tac x="a" in exI)
        apply(rule_tac x="[]" in exI)
        apply(rule_tac x="[]" in exI)
        by(auto intro!:empty_path)
    next
      case False
      hence "as  []" .
      from n'' -as→* n' n'set (sourcenodes as). n'  (PDG_BS S) 
      have "obs n' (PDG_BS S)  obs n'' (PDG_BS S)" by(rule path_obs_subset)
      show ?thesis
      proof(cases "obs n' (PDG_BS S) = obs n'' (PDG_BS S)")
        case True
        with n'' -as→* n' valid_edge a obs n' (PDG_BS S) = {n'} more_than_one
        show ?thesis
          apply(rule_tac x="a" in exI)
          apply(rule_tac x="[]" in exI)
          apply(rule_tac x="as" in exI)
          by(fastforce intro:empty_path)
      next
        case False
        with obs n' (PDG_BS S)  obs n'' (PDG_BS S)
        have "obs n' (PDG_BS S)  obs n'' (PDG_BS S)" by simp
        with obs n' (PDG_BS S) = {n'} obtain ni where "n'  obs n'' (PDG_BS S)"
          and "ni  obs n'' (PDG_BS S)" and "n'  ni" by auto
        from IH[OF this obs n' (PDG_BS S) = {n'} 
          n'set (sourcenodes as). n'  (PDG_BS S) as  []] obtain a' as' as''
          where "n'' -as'→* sourcenode a'" and "targetnode a' -as''→* n'"
          and "valid_edge a'" and [simp]:"as = as'@a'#as''" 
          and "obs (targetnode a') (PDG_BS S) = {n'}"
          and more_than_one':"¬ (m. obs (sourcenode a') (PDG_BS S) = {m}  
          obs (sourcenode a') (PDG_BS S) = {})"
          by blast
        from n'' -as'→* sourcenode a' valid_edge a
        have "n -a#as'→* sourcenode a'" by(fastforce intro:path.Cons_path)
        with targetnode a' -as''→* n' obs (targetnode a') (PDG_BS S) = {n'}
          more_than_one' valid_edge a' show ?thesis
          apply(rule_tac x="a'" in exI)
          apply(rule_tac x="a#as'" in exI)
          apply(rule_tac x="as''" in exI)
          by fastforce
      qed
    qed
  qed simp
  then obtain a as' as'' where "valid_edge a"
    and "obs (targetnode a) (PDG_BS S) = {nx}"
    and more_than_one:"¬ (m. obs (sourcenode a) (PDG_BS S) = {m}  
                         obs (sourcenode a) (PDG_BS S) = {})"
    by blast
  have "sourcenode a  (PDG_BS S)"
  proof(rule ccontr)
    assume "¬ sourcenode a  PDG_BS S"
    hence "sourcenode a  PDG_BS S" by simp
    with valid_edge a have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
      by(fastforce intro!:n_in_obs)
    with more_than_one show False by simp
  qed
  with valid_edge a 
  have "obs (targetnode a) (PDG_BS S)  obs (sourcenode a) (PDG_BS S)"
    by(rule edge_obs_subset)
  with obs (targetnode a) (PDG_BS S) = {nx} 
  have "nx  obs (sourcenode a) (PDG_BS S)" by simp
  with more_than_one obtain m  where "m  obs (sourcenode a) (PDG_BS S)"
    and "nx  m" by auto
  from m  obs (sourcenode a) (PDG_BS S) 
  have "valid_node m" by(fastforce dest:in_obs_valid)
  from obs (targetnode a) (PDG_BS S) = {nx} have "valid_node nx" 
    by(fastforce dest:in_obs_valid)
  show False
  proof(cases "m strongly-postdominates (sourcenode a)")
    case True
    with nx  obs (sourcenode a) (PDG_BS S) m  obs (sourcenode a) (PDG_BS S)
    have "m strongly-postdominates nx"
      by(fastforce intro:strong_postdominate_path_targetnode elim:obs.cases)
    with nx  m have "¬ nx strongly-postdominates m" 
      by(fastforce dest:strong_postdominate_antisym)
    have "(_Exit_) -[]→* (_Exit_)" by(fastforce intro:empty_path)
    with m strongly-postdominates nx have "nx  (_Exit_)"
      by(fastforce simp:strong_postdominate_def sourcenodes_def postdominate_def)
    have "¬ nx strongly-postdominates (sourcenode a)"
    proof(rule ccontr)
      assume "¬ ¬ nx strongly-postdominates sourcenode a"
      hence "nx strongly-postdominates sourcenode a" by simp
      from m  obs (sourcenode a) (PDG_BS S) nx  obs (sourcenode a) (PDG_BS S)
      obtain asx' where "sourcenode a -asx'→* m" and "nx  set(sourcenodes asx')"
        by(fastforce elim:obs.cases)
      with nx strongly-postdominates sourcenode a have "nx strongly-postdominates m"
        by(rule strong_postdominate_path_targetnode)
      with ¬ nx strongly-postdominates m show False by simp
    qed
    with nx  obs (sourcenode a) (PDG_BS S) valid_node nx nx  (_Exit_) 
    show False by(fastforce dest:obs_strong_postdominate)
  next
    case False
    show False
    proof(cases "m = Exit")
      case True
      from m  obs (sourcenode a) (PDG_BS S) nx  obs (sourcenode a) (PDG_BS S)
      obtain xs where "sourcenode a -xs→* m" and "nx  set(sourcenodes xs)"
        by(fastforce elim:obsE)
      obtain x' xs' where [simp]:"xs = x'#xs'"
      proof(cases xs)
        case Nil
        with sourcenode a -xs→* m have [simp]:"sourcenode a = m" by fastforce
        with m  obs (sourcenode a) (PDG_BS S) 
        have "m  (PDG_BS S)" by (metis obsE)
        with valid_node m have "obs m (PDG_BS S) = {m}"
          by(rule n_in_obs)
        with nx  obs (sourcenode a) (PDG_BS S) nx  m have False
          by fastforce
        thus ?thesis by simp
      qed blast
      from sourcenode a -xs→* m have "sourcenode a = sourcenode x'" 
        and "valid_edge x'" and "targetnode x' -xs'→* m"
        by(auto elim:path_split_Cons)
      from targetnode x' -xs'→* m nx  set(sourcenodes xs) valid_edge x' 
        valid_node m True
      have "¬ nx strongly-postdominates (targetnode x')" 
        by(fastforce simp:strong_postdominate_def postdominate_def sourcenodes_def)
      from nx  m True have "nx  (_Exit_)" by simp
      with obs (targetnode a) (PDG_BS S) = {nx}
      have "nx strongly-postdominates (targetnode a)"
        by(fastforce intro:obs_strong_postdominate)
      from obs (targetnode a) (PDG_BS S) = {nx}
      obtain ys where "targetnode a -ys→* nx" 
        and "nx'  set(sourcenodes ys). nx'  (PDG_BS S)"
        and "nx  (PDG_BS S)" by(fastforce elim:obsE)
      hence "nx  set(sourcenodes ys)"by fastforce
      have "sourcenode a  nx"
      proof
        assume "sourcenode a = nx"
        from nx  obs (sourcenode a) (PDG_BS S)
        have "nx  (PDG_BS S)" by -(erule obsE)
        with valid_node nx have "obs nx (PDG_BS S) = {nx}" by -(erule n_in_obs)
        with sourcenode a = nx m  obs (sourcenode a) (PDG_BS S) 
          nx  m show False by fastforce
      qed
      with nx  set(sourcenodes ys) have "nx  set(sourcenodes (a#ys))"
        by(fastforce simp:sourcenodes_def)
      from valid_edge a targetnode a -ys→* nx
      have "sourcenode a -a#ys→* nx" by(fastforce intro:Cons_path)
      from sourcenode a -a#ys→* nx nx  set(sourcenodes (a#ys))
        nx strongly-postdominates (targetnode a) valid_edge x'
        ¬ nx strongly-postdominates (targetnode x') sourcenode a = sourcenode x'
      have "(sourcenode a) weakly controls nx"
        by(fastforce simp:weak_control_dependence_def)
      with nx  (PDG_BS S) have "sourcenode a  (PDG_BS S)"
        by(rule cd_closed)
      with valid_edge a have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
        by(fastforce intro!:n_in_obs)
      with m  obs (sourcenode a) (PDG_BS S)
        nx  obs (sourcenode a) (PDG_BS S) nx  m
      show False by simp
    next
      case False
      with m  obs (sourcenode a) (PDG_BS S) valid_node m
        ¬ m strongly-postdominates sourcenode a 
      show False by(fastforce dest:obs_strong_postdominate)
    qed
  qed
qed


lemma WeakPDGBackwardSliceCorrect:
  "BackwardSlice sourcenode targetnode kind valid_edge
        (_Entry_) Def Use state_val PDG_BS"
proof(unfold_locales)
  fix n S assume "n  PDG_BS S"
  thus "valid_node n" by(rule PDG_BS_valid_node)
next
  fix n S assume "valid_node n" and "n  S"
  thus "n  PDG_BS S" by(fastforce intro:PDG_path_Nil simp:PDG_BS_def)
next
  fix n' S n V assume "n'  PDG_BS S" and "n influences V in n'"
  thus "n  PDG_BS S"
    by(auto dest:PDG.PDG_path_ddep[OF PDG_wcd,OF PDG.PDG_ddep_edge[OF PDG_wcd]]
            dest:PDG_path_Append simp:PDG_BS_def split:if_split_asm)
next
  fix n S
  have "(m. obs n (PDG_BS S) = {m})  obs n (PDG_BS S) = {}" 
    by(rule obs_singleton)
  thus "finite (obs n (PDG_BS S))" by fastforce
next
  fix n S
  have "(m. obs n (PDG_BS S) = {m})  obs n (PDG_BS S) = {}" 
    by(rule obs_singleton)
  thus "card (obs n (PDG_BS S))  1" by fastforce
qed

end


subsection‹Weak order dependence›

context CFG_wf begin

lemma obs_singleton: 
  (*assumes valid:"valid_node n"*)
  shows "(m. obs n (wod_backward_slice S) = {m}) 
         obs n (wod_backward_slice S) = {}"
proof(rule ccontr)
  let ?WOD_BS = "wod_backward_slice S"
  assume "¬ ((m. obs n ?WOD_BS = {m})  obs n ?WOD_BS = {})"
  hence "nx nx'. nx  obs n ?WOD_BS  nx'  obs n ?WOD_BS 
    nx  nx'" by auto
  then obtain nx nx' where "nx  obs n ?WOD_BS" and "nx'  obs n ?WOD_BS"
    and "nx  nx'" by auto
  from nx  obs n ?WOD_BS obtain as where "n -as→* nx" 
    and "n'  set(sourcenodes as). n'  ?WOD_BS" and "nx  ?WOD_BS" 
    by(erule obsE)
  from n -as→* nx have "valid_node nx" by(fastforce dest:path_valid_node)
  with nx  ?WOD_BS have "obs nx ?WOD_BS = {nx}" by -(rule n_in_obs)
  with n -as→* nx nx  obs n ?WOD_BS nx'  obs n ?WOD_BS nx  nx' 
  have "as  []" by(fastforce elim:path.cases)
  with n -as→* nx nx  obs n ?WOD_BS nx'  obs n ?WOD_BS nx  nx' 
    obs nx ?WOD_BS = {nx} n'  set(sourcenodes as). n'  ?WOD_BS
  have "a as' as''. n -as'→* sourcenode a  targetnode a -as''→* nx 
                     valid_edge a  as = as'@a#as''  
                     obs (targetnode a) ?WOD_BS = {nx}  
                    (¬ (m. obs (sourcenode a) ?WOD_BS = {m}  
                       obs (sourcenode a) ?WOD_BS = {}))"
  proof(induct arbitrary:nx' rule:path.induct)
    case (Cons_path n'' as n' a n)
    note [simp] = sourcenode a = n[THEN sym] targetnode a = n''[THEN sym]
    note more_than_one = n'  obs n (?WOD_BS) nx'  obs n (?WOD_BS) n'  nx'
    note IH = nx'. n'  obs n'' (?WOD_BS); nx'  obs n'' (?WOD_BS); n'  nx'; 
      obs n' (?WOD_BS) = {n'}; n'set (sourcenodes as). n'  (?WOD_BS); as  []
       a as' as''. n'' -as'→* sourcenode a  targetnode a -as''→* n' 
      valid_edge a  as = as'@a#as''  obs (targetnode a) (?WOD_BS) = {n'} 
      (¬ (m. obs (sourcenode a) (?WOD_BS) = {m}  
      obs (sourcenode a) (?WOD_BS) = {}))
    from n'set (sourcenodes (a#as)). n'  (?WOD_BS)
    have "n'set (sourcenodes as). n'  (?WOD_BS)" and "sourcenode a  (?WOD_BS)"
      by(simp_all add:sourcenodes_def)
    show ?case
    proof(cases "as = []")
      case True
      with n'' -as→* n' have [simp]:"n' = n''" by(fastforce elim:path.cases)
      from more_than_one
      have "¬ (m. obs (sourcenode a) (?WOD_BS) = {m}  
               obs (sourcenode a) (?WOD_BS) = {})"
        by auto
      with obs n' (?WOD_BS) = {n'} True valid_edge a show ?thesis
        apply(rule_tac x="a" in exI)
        apply(rule_tac x="[]" in exI)
        apply(rule_tac x="[]" in exI)
        by(auto intro!:empty_path)
    next
      case False
      hence "as  []" .
      from n'' -as→* n' n'set (sourcenodes as). n'  (?WOD_BS) 
      have "obs n' (?WOD_BS)  obs n'' (?WOD_BS)" by(rule path_obs_subset)
      show ?thesis
      proof(cases "obs n' (?WOD_BS) = obs n'' (?WOD_BS)")
        case True
        with n'' -as→* n' valid_edge a obs n' (?WOD_BS) = {n'} more_than_one
        show ?thesis
          apply(rule_tac x="a" in exI)
          apply(rule_tac x="[]" in exI)
          apply(rule_tac x="as" in exI)
          by(fastforce intro:empty_path)
      next
        case False
        with obs n' (?WOD_BS)  obs n'' (?WOD_BS)
        have "obs n' (?WOD_BS)  obs n'' (?WOD_BS)" by simp
        with obs n' (?WOD_BS) = {n'} obtain ni where "n'  obs n'' (?WOD_BS)"
          and "ni  obs n'' (?WOD_BS)" and "n'  ni" by auto
        from IH[OF this obs n' (?WOD_BS) = {n'} 
          n'set (sourcenodes as). n'  (?WOD_BS) as  []] obtain a' as' as''
          where "n'' -as'→* sourcenode a'" and "targetnode a' -as''→* n'"
          and "valid_edge a'" and [simp]:"as = as'@a'#as''" 
          and "obs (targetnode a') (?WOD_BS) = {n'}"
          and more_than_one':"¬ (m. obs (sourcenode a') (?WOD_BS) = {m}  
          obs (sourcenode a') (?WOD_BS) = {})"
          by blast
        from n'' -as'→* sourcenode a' valid_edge a
        have "n -a#as'→* sourcenode a'" by(fastforce intro:path.Cons_path)
        with targetnode a' -as''→* n' obs (targetnode a') (?WOD_BS) = {n'}
          more_than_one' valid_edge a' show ?thesis
          apply(rule_tac x="a'" in exI)
          apply(rule_tac x="a#as'" in exI)
          apply(rule_tac x="as''" in exI)
          by fastforce
      qed
    qed
  qed simp
  then obtain a as' as'' where "valid_edge a"
    and "obs (targetnode a) (?WOD_BS) = {nx}"
    and more_than_one:"¬ (m. obs (sourcenode a) (?WOD_BS) = {m}  
                         obs (sourcenode a) (?WOD_BS) = {})"
    by blast
  have "sourcenode a  (?WOD_BS)"
  proof(rule ccontr)
    assume "¬ sourcenode a  ?WOD_BS"
    hence "sourcenode a  ?WOD_BS" by simp
    with valid_edge a have "obs (sourcenode a) (?WOD_BS) = {sourcenode a}"
      by(fastforce intro!:n_in_obs)
    with more_than_one show False by simp
  qed
  with valid_edge a 
  have "obs (targetnode a) (?WOD_BS)  obs (sourcenode a) (?WOD_BS)"
    by(rule edge_obs_subset)
  with obs (targetnode a) (?WOD_BS) = {nx} 
  have "nx  obs (sourcenode a) (?WOD_BS)" by simp
  with more_than_one obtain m  where "m  obs (sourcenode a) (?WOD_BS)"
    and "nx  m" by auto
  with nx  obs (sourcenode a) (?WOD_BS) obtain as2 
    where "sourcenode a -as2→* m" and "nx  set(sourcenodes as2)" 
    by(fastforce elim:obsE)
  from nx  obs (sourcenode a) (?WOD_BS) m  obs (sourcenode a) (?WOD_BS) 
  obtain as1 where "sourcenode a -as1→* nx" and "m  set(sourcenodes as1)"
    by(fastforce elim:obsE)
  from obs (targetnode a) (?WOD_BS) = {nx} obtain asx 
    where "targetnode a -asx→* nx" by(fastforce elim:obsE)
  have "asx'. targetnode a -asx'→* m  nx  set(sourcenodes asx')"
  proof(rule ccontr)
    assume "¬ (asx'. targetnode a -asx'→* m  nx  set (sourcenodes asx'))"
    then obtain asx' where "targetnode a -asx'→* m" and "nx  set (sourcenodes asx')"
      by blast
    show False
    proof(cases "nx  set(sourcenodes asx'). nx  ?WOD_BS")
      case True
      with targetnode a -asx'→* m m  obs (sourcenode a) (?WOD_BS) 
      have "m  obs (targetnode a) ?WOD_BS" by(fastforce intro:obs_elem elim:obsE)
      with nx  m obs (targetnode a) (?WOD_BS) = {nx} show False by simp
    next
      case False
      hence "nx  set(sourcenodes asx'). nx  ?WOD_BS" by blast
      then obtain nx' ns ns' where "sourcenodes asx' = ns@nx'#ns'" and "nx'  ?WOD_BS"
        and "nx  set ns. nx  ?WOD_BS" by(fastforce elim!:split_list_first_propE)
      from sourcenodes asx' = ns@nx'#ns' obtain ax ai ai' 
        where [simp]:"asx' = ai@ax#ai'" "ns = sourcenodes ai" "nx' = sourcenode ax"
        by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
      from targetnode a -asx'→* m have "targetnode a -ai→* sourcenode ax"
        by(fastforce dest:path_split)
      with nx'  ?WOD_BS nx  set ns. nx  ?WOD_BS 
      have "nx'  obs (targetnode a) ?WOD_BS" by(fastforce intro:obs_elem)
      with obs (targetnode a) (?WOD_BS) = {nx} have "nx' = nx" by simp
      with nx  set (sourcenodes asx') show False by(simp add:sourcenodes_def)
    qed
  qed
  with nx  m sourcenode a -as1→* nx m  set(sourcenodes as1) 
    sourcenode a -as2→* m nx  set(sourcenodes as2) valid_edge a 
    targetnode a -asx→* nx
  have "sourcenode a wod nx,m" by(simp add:wod_def,blast)
  with nx  obs (sourcenode a) (?WOD_BS) m  obs (sourcenode a) (?WOD_BS) 
  have "sourcenode a  ?WOD_BS" by(fastforce elim:cd_closed elim:obsE)
  with sourcenode a  ?WOD_BS show False by simp
qed


lemma WODBackwardSliceCorrect:
  "BackwardSlice sourcenode targetnode kind valid_edge
        (_Entry_) Def Use state_val wod_backward_slice"
proof(unfold_locales)
  fix n S assume "n  wod_backward_slice S"
  thus "valid_node n" by(rule wod_backward_slice_valid_node)
next
  fix n S assume "valid_node n" and "n  S"
  thus "n  wod_backward_slice S" by(rule refl)
next
  fix n' S n V assume "n'  wod_backward_slice S" "n influences V in n'"
  thus "n  wod_backward_slice S"
    by -(rule dd_closed)
next
  fix n S
  have "(m. obs n (wod_backward_slice S) = {m})  
    obs n (wod_backward_slice S) = {}" 
    by(rule obs_singleton)
  thus "finite (obs n (wod_backward_slice S))" by fastforce
next
  fix n S 
  have "(m. obs n (wod_backward_slice S) = {m})  obs n (wod_backward_slice S) = {}" 
    by(rule obs_singleton)
  thus "card (obs n (wod_backward_slice S))  1" by fastforce
qed

end

end