Theory 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 controls⇩s 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 controls⇩s 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) controls⇩s 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 ⟶⇩w⇩o⇩d 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