Theory SDG

section ‹SDG›

theory SDG imports CFGExit_wf Postdomination begin

subsection ‹The nodes of the SDG›

datatype 'node SDG_node = 
    CFG_node 'node
  | Formal_in  "'node × nat"
  | Formal_out "'node × nat"
  | Actual_in  "'node × nat"
  | Actual_out "'node × nat"

fun parent_node :: "'node SDG_node ⇒ 'node"
  where "parent_node (CFG_node n) = n"
  | "parent_node (Formal_in (m,x)) = m"
  | "parent_node (Formal_out (m,x)) = m"
  | "parent_node (Actual_in (m,x)) = m"
  | "parent_node (Actual_out (m,x)) = m"


locale SDG = CFGExit_wf sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Exit Def Use ParamDefs ParamUses +
  Postdomination sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Exit
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" ("'('_Entry'_')")  and get_proc :: "'node ⇒ 'pname"
  and get_return_edges :: "'edge ⇒ 'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
  and Exit::"'node"  ("'('_Exit'_')") 
  and Def :: "'node ⇒ 'var set" and Use :: "'node ⇒ 'var set"
  and ParamDefs :: "'node ⇒ 'var list" and ParamUses :: "'node ⇒ 'var set list"

begin


fun valid_SDG_node :: "'node SDG_node ⇒ bool"
  where "valid_SDG_node (CFG_node n) ⟷ valid_node n"
  | "valid_SDG_node (Formal_in (m,x)) ⟷
  (∃a Q r p fs ins outs. valid_edge a ∧ (kind a = Q:r↪⇘p⇙fs) ∧ targetnode a = m ∧ 
  (p,ins,outs) ∈ set procs ∧ x < length ins)"
  | "valid_SDG_node (Formal_out (m,x)) ⟷
  (∃a Q p f ins outs. valid_edge a ∧ (kind a = Q↩⇘p⇙f) ∧ sourcenode a = m ∧ 
  (p,ins,outs) ∈ set procs ∧ x < length outs)"
  | "valid_SDG_node (Actual_in (m,x)) ⟷
  (∃a Q r p fs ins outs. valid_edge a ∧ (kind a = Q:r↪⇘p⇙fs) ∧ sourcenode a = m ∧ 
  (p,ins,outs) ∈ set procs ∧ x < length ins)"
  | "valid_SDG_node (Actual_out (m,x)) ⟷
  (∃a Q p f ins outs. valid_edge a ∧ (kind a = Q↩⇘p⇙f) ∧ targetnode a = m ∧ 
  (p,ins,outs) ∈ set procs ∧ x < length outs)"


lemma valid_SDG_CFG_node: 
  "valid_SDG_node n ⟹ valid_node (parent_node n)"
by(cases n) auto


lemma Formal_in_parent_det:
  assumes "valid_SDG_node (Formal_in (m,x))" and "valid_SDG_node (Formal_in (m',x'))"
  and "get_proc m = get_proc m'"
  shows "m = m'"
proof -
  from ‹valid_SDG_node (Formal_in (m,x))› obtain a Q r p fs ins outs
    where "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "targetnode a = m"
    and "(p,ins,outs) ∈ set procs" and "x < length ins" by fastforce
  from ‹valid_SDG_node (Formal_in (m',x'))› obtain a' Q' r' p' f' ins' outs'
    where "valid_edge a'" and "kind a' = Q':r'↪⇘p'⇙f'" and "targetnode a' = m'"
    and "(p',ins',outs') ∈ set procs" and "x' < length ins'" by fastforce
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹targetnode a = m›
  have "get_proc m = p" by(fastforce intro:get_proc_call)
  moreover
  from ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p'⇙f'› ‹targetnode a' = m'›
  have "get_proc m' = p'" by(fastforce intro:get_proc_call)
  ultimately have "p = p'" using ‹get_proc m = get_proc m'› by simp
  with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p'⇙f'›
    ‹targetnode a = m› ‹targetnode a' = m'›
  show ?thesis by(fastforce intro:same_proc_call_unique_target)
qed


lemma valid_SDG_node_parent_Entry:
  assumes "valid_SDG_node n" and "parent_node n = (_Entry_)"
  shows "n = CFG_node (_Entry_)"
proof(cases n)
  case CFG_node with ‹parent_node n = (_Entry_)› show ?thesis by simp
next
  case (Formal_in z)
  with ‹parent_node n = (_Entry_)› obtain x 
    where [simp]:"z = ((_Entry_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Formal_in obtain a where "valid_edge a"
    and "targetnode a = (_Entry_)" by auto
  hence False by -(rule Entry_target,simp+)
  thus ?thesis by simp
next
  case (Formal_out z)
  with ‹parent_node n = (_Entry_)› obtain x 
    where [simp]:"z = ((_Entry_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Formal_out obtain a Q p f where "valid_edge a"
    and "kind a = Q↩⇘p⇙f" and  "sourcenode a = (_Entry_)" by auto
  from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "get_proc (sourcenode a) = p"
    by(rule get_proc_return)
  with ‹sourcenode a = (_Entry_)› have "p = Main"
    by(auto simp:get_proc_Entry)
  with ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have False
    by(fastforce intro:Main_no_return_source)
  thus ?thesis by simp
next
  case (Actual_in z)
  with ‹parent_node n = (_Entry_)› obtain x 
    where [simp]:"z = ((_Entry_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Actual_in obtain a Q r p fs where "valid_edge a"
    and "kind a = Q:r↪⇘p⇙fs" and "sourcenode a = (_Entry_)" by fastforce
  hence False by -(rule Entry_no_call_source,auto)
  thus ?thesis by simp
next
  case (Actual_out z)
  with ‹parent_node n = (_Entry_)› obtain x 
    where [simp]:"z = ((_Entry_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Actual_out obtain a where "valid_edge a"
    "targetnode a = (_Entry_)" by auto
  hence False by -(rule Entry_target,simp+)
  thus ?thesis by simp
qed


lemma valid_SDG_node_parent_Exit:
  assumes "valid_SDG_node n" and "parent_node n = (_Exit_)"
  shows "n = CFG_node (_Exit_)"
proof(cases n)
  case CFG_node with ‹parent_node n = (_Exit_)› show ?thesis by simp
next
  case (Formal_in z)
  with ‹parent_node n = (_Exit_)› obtain x 
    where [simp]:"z = ((_Exit_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Formal_in obtain a Q r p fs where "valid_edge a"
    and "kind a = Q:r↪⇘p⇙fs" and "targetnode a = (_Exit_)" by fastforce
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
    by(rule get_proc_call)
  with ‹targetnode a = (_Exit_)› have "p = Main"
    by(auto simp:get_proc_Exit)
  with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have False
    by(fastforce intro:Main_no_call_target)
  thus ?thesis by simp
next
  case (Formal_out z)
  with ‹parent_node n = (_Exit_)› obtain x 
    where [simp]:"z = ((_Exit_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Formal_out obtain a where "valid_edge a"
    and "sourcenode a = (_Exit_)" by auto
  hence False by -(rule Exit_source,simp+)
  thus ?thesis by simp
next
  case (Actual_in z)
  with ‹parent_node n = (_Exit_)› obtain x 
    where [simp]:"z = ((_Exit_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Actual_in obtain a where "valid_edge a"
    and "sourcenode a = (_Exit_)" by auto
  hence False by -(rule Exit_source,simp+)
  thus ?thesis by simp
next
  case (Actual_out z)
  with ‹parent_node n = (_Exit_)› obtain x 
    where [simp]:"z = ((_Exit_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Actual_out obtain a Q p f where "valid_edge a"
    and "kind a = Q↩⇘p⇙f" and "targetnode a = (_Exit_)" by auto
  hence False by -(erule Exit_no_return_target,auto)
  thus ?thesis by simp
qed


subsection ‹Data dependence›

inductive SDG_Use :: "'var ⇒ 'node SDG_node ⇒ bool" ("_ ∈ Use⇘SDG⇙ _")
where CFG_Use_SDG_Use:
  "⟦valid_node m; V ∈ Use m; n = CFG_node m⟧ ⟹ V ∈ Use⇘SDG⇙ n"
  | Actual_in_SDG_Use:
  "⟦valid_SDG_node n; n = Actual_in (m,x); V ∈ (ParamUses m)!x⟧ ⟹ V ∈ Use⇘SDG⇙ n"
  | Formal_out_SDG_Use:
  "⟦valid_SDG_node n; n = Formal_out (m,x); get_proc m = p; (p,ins,outs) ∈ set procs;
    V = outs!x⟧ ⟹ V ∈ Use⇘SDG⇙ n"


abbreviation notin_SDG_Use :: "'var ⇒ 'node SDG_node ⇒ bool"  ("_ ∉ Use⇘SDG⇙ _")
  where "V ∉ Use⇘SDG⇙ n ≡ ¬ V ∈ Use⇘SDG⇙ n"


lemma in_Use_valid_SDG_node:
  "V ∈ Use⇘SDG⇙ n ⟹ valid_SDG_node n"
by(induct rule:SDG_Use.induct,auto intro:valid_SDG_CFG_node)


lemma SDG_Use_parent_Use: 
  "V ∈ Use⇘SDG⇙ n ⟹ V ∈ Use (parent_node n)"
proof(induct rule:SDG_Use.induct)
  case CFG_Use_SDG_Use thus ?case by simp
next
  case (Actual_in_SDG_Use n m x V)
  from ‹valid_SDG_node n› ‹n = Actual_in (m, x)› obtain a Q r p fs ins outs
    where "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "sourcenode a = m"
    and "(p,ins,outs) ∈ set procs" and "x < length ins" by fastforce
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹(p,ins,outs) ∈ set procs›
  have "length(ParamUses (sourcenode a)) = length ins"
    by(fastforce intro:ParamUses_call_source_length)
  with ‹x < length ins›
  have "(ParamUses (sourcenode a))!x ∈ set (ParamUses (sourcenode a))" by simp
  with ‹V ∈ (ParamUses m)!x› ‹sourcenode a = m›
  have "V ∈ Union (set (ParamUses m))" by fastforce
  with ‹valid_edge a› ‹sourcenode a = m› ‹n = Actual_in (m, x)› show ?case
    by(fastforce intro:ParamUses_in_Use)
next
  case (Formal_out_SDG_Use n m x p ins outs V)
  from ‹valid_SDG_node n› ‹n = Formal_out (m, x)› obtain a Q p' f ins' outs'
    where "valid_edge a" and "kind a = Q↩⇘p'⇙f" and "sourcenode a = m"
    and "(p',ins',outs') ∈ set procs" and "x < length outs'" by fastforce
  from ‹valid_edge a› ‹kind a = Q↩⇘p'⇙f› have "get_proc (sourcenode a) = p'"
    by(rule get_proc_return)
  with ‹get_proc m = p› ‹sourcenode a = m› have [simp]:"p = p'" by simp
  with ‹(p',ins',outs') ∈ set procs› ‹(p,ins,outs) ∈ set procs› unique_callers
  have [simp]:"ins' = ins" "outs' = outs" by(auto dest:distinct_fst_isin_same_fst)
  from ‹x < length outs'› ‹V = outs ! x› have "V ∈ set outs" by fastforce
  with ‹valid_edge a› ‹kind a = Q↩⇘p'⇙f› ‹(p,ins,outs) ∈ set procs›
  have "V ∈ Use (sourcenode a)" by(fastforce intro:outs_in_Use)
  with ‹sourcenode a = m› ‹valid_SDG_node n› ‹n = Formal_out (m, x)›
  show ?case by simp
qed



inductive SDG_Def :: "'var ⇒ 'node SDG_node ⇒ bool" ("_ ∈ Def⇘SDG⇙ _")
where CFG_Def_SDG_Def:
  "⟦valid_node m; V ∈ Def m; n = CFG_node m⟧ ⟹ V ∈ Def⇘SDG⇙ n"
  | Formal_in_SDG_Def:
  "⟦valid_SDG_node n; n = Formal_in (m,x); get_proc m = p; (p,ins,outs) ∈ set procs;
    V = ins!x⟧ ⟹ V ∈ Def⇘SDG⇙ n"
  | Actual_out_SDG_Def:
  "⟦valid_SDG_node n; n = Actual_out (m,x); V = (ParamDefs m)!x⟧ ⟹ V ∈ Def⇘SDG⇙ n"

abbreviation notin_SDG_Def :: "'var ⇒ 'node SDG_node ⇒ bool"  ("_ ∉ Def⇘SDG⇙ _")
  where "V ∉ Def⇘SDG⇙ n ≡ ¬ V ∈ Def⇘SDG⇙ n"


lemma in_Def_valid_SDG_node:
  "V ∈ Def⇘SDG⇙ n ⟹ valid_SDG_node n"
by(induct rule:SDG_Def.induct,auto intro:valid_SDG_CFG_node)


lemma SDG_Def_parent_Def: 
  "V ∈ Def⇘SDG⇙ n ⟹ V ∈ Def (parent_node n)"
proof(induct rule:SDG_Def.induct)
  case CFG_Def_SDG_Def thus ?case by simp
next
  case (Formal_in_SDG_Def n m x p ins outs V)
  from ‹valid_SDG_node n› ‹n = Formal_in (m, x)› obtain a Q r p' fs ins' outs'
    where "valid_edge a" and "kind a = Q:r↪⇘p'⇙fs" and "targetnode a = m"
    and "(p',ins',outs') ∈ set procs" and "x < length ins'" by fastforce
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p'⇙fs› have "get_proc (targetnode a) = p'"
    by(rule get_proc_call)
  with ‹get_proc m = p› ‹targetnode a = m› have [simp]:"p = p'" by simp
  with ‹(p',ins',outs') ∈ set procs› ‹(p,ins,outs) ∈ set procs› unique_callers
  have [simp]:"ins' = ins" "outs' = outs" by(auto dest:distinct_fst_isin_same_fst)
  from ‹x < length ins'› ‹V = ins ! x› have "V ∈ set ins" by fastforce
  with ‹valid_edge a› ‹kind a = Q:r↪⇘p'⇙fs› ‹(p,ins,outs) ∈ set procs›
  have "V ∈ Def (targetnode a)" by(fastforce intro:ins_in_Def)
  with ‹targetnode a = m› ‹valid_SDG_node n› ‹n = Formal_in (m, x)›
  show ?case by simp
next
  case (Actual_out_SDG_Def n m x V)
  from ‹valid_SDG_node n› ‹n = Actual_out (m, x)› obtain a Q p f ins outs
    where "valid_edge a" and "kind a = Q↩⇘p⇙f" and "targetnode a = m"
    and "(p,ins,outs) ∈ set procs" and "x < length outs" by fastforce
  from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› ‹(p,ins,outs) ∈ set procs›
  have "length(ParamDefs (targetnode a)) = length outs" 
    by(rule ParamDefs_return_target_length)
  with ‹x < length outs› ‹V = ParamDefs m ! x› ‹targetnode a = m›
  have "V ∈ set (ParamDefs (targetnode a))" by(fastforce simp:set_conv_nth)
  with ‹n = Actual_out (m, x)› ‹targetnode a = m› ‹valid_edge a›
  show ?case by(fastforce intro:ParamDefs_in_Def)
qed



definition data_dependence :: "'node SDG_node ⇒ 'var ⇒ 'node SDG_node ⇒ bool" 
("_ influences _ in _" [51,0,0])
  where "n influences V in n' ≡ ∃as. (V ∈ Def⇘SDG⇙ n) ∧ (V ∈ Use⇘SDG⇙ n') ∧ 
  (parent_node n -as→⇩ι* parent_node n') ∧
  (∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes (tl as))
         ⟶ V ∉ Def⇘SDG⇙ n'')"


subsection ‹Control dependence›

definition control_dependence :: "'node ⇒ 'node ⇒ bool" 
  ("_ controls _" [51,0])
where "n controls n' ≡ ∃a a' as. n -a#as→⇩ι* n' ∧ n' ∉ set(sourcenodes (a#as)) ∧
    intra_kind(kind a) ∧ n' postdominates (targetnode a) ∧ 
    valid_edge a' ∧ intra_kind(kind a') ∧ sourcenode a' = n ∧ 
    ¬ n' postdominates (targetnode a')"


lemma control_dependence_path:
  assumes "n controls n'" obtains as where "n -as→⇩ι* n'" and "as ≠ []"
using ‹n controls n'›
by(fastforce simp:control_dependence_def)


lemma Exit_does_not_control [dest]:
  assumes "(_Exit_) controls n'" shows "False"
proof -
  from ‹(_Exit_) controls n'› obtain a where "valid_edge a"
    and "sourcenode a = (_Exit_)" by(auto simp:control_dependence_def)
  thus ?thesis by(rule Exit_source)
qed


lemma Exit_not_control_dependent: 
  assumes "n controls n'" shows "n' ≠ (_Exit_)"
proof -
  from ‹n controls n'› obtain a as where "n -a#as→⇩ι* n'"
    and "n' postdominates (targetnode a)"
    by(auto simp:control_dependence_def)
  from ‹n -a#as→⇩ι* n'› have "valid_edge a" 
    by(fastforce elim:path.cases simp:intra_path_def)
  hence "valid_node (targetnode a)" by simp
  with ‹n' postdominates (targetnode a)› ‹n -a#as→⇩ι* n'› show ?thesis
    by(fastforce elim:Exit_no_postdominator)
qed


lemma which_node_intra_standard_control_dependence_source:
  assumes "nx -as@a#as'→⇩ι* n" and "sourcenode a = n'" and "sourcenode a' = n'"
  and "n ∉ set(sourcenodes (a#as'))" and "valid_edge a'" and "intra_kind(kind a')"
  and "inner_node n" and "¬ method_exit n" and "¬ n postdominates (targetnode a')"
  and last:"∀ax ax'. ax ∈ set as' ∧ sourcenode ax = sourcenode ax' ∧
    valid_edge ax' ∧ intra_kind(kind ax') ⟶ n postdominates targetnode ax'"
  shows "n' controls n"
proof -
  from ‹nx -as@a#as'→⇩ι* n› ‹sourcenode a = n'› have "n' -a#as'→⇩ι* n"
    by(fastforce dest:path_split_second simp:intra_path_def)
  from ‹nx -as@a#as'→⇩ι* n› have "valid_edge a"
    by(fastforce intro:path_split simp:intra_path_def)
  show ?thesis
  proof(cases "n postdominates (targetnode a)")
    case True
    with ‹n' -a#as'→⇩ι* n› ‹n ∉ set(sourcenodes (a#as'))›
      ‹valid_edge a'› ‹intra_kind(kind a')› ‹sourcenode a' = n'› 
      ‹¬ n postdominates (targetnode a')› show ?thesis
      by(fastforce simp:control_dependence_def intra_path_def)
  next
    case False
    show ?thesis
    proof(cases "as' = []")
      case True
      with ‹n' -a#as'→⇩ι* n› have "targetnode a = n" 
        by(fastforce elim:path.cases simp:intra_path_def)
      with ‹inner_node n› ‹¬ method_exit n› have "n postdominates (targetnode a)"
        by(fastforce dest:inner_is_valid intro:postdominate_refl)
      with ‹¬ n postdominates (targetnode a)› show ?thesis by simp
    next
      case False
      with ‹nx -as@a#as'→⇩ι* n› have "targetnode a -as'→⇩ι* n"
        by(fastforce intro:path_split simp:intra_path_def)
     with ‹¬ n postdominates (targetnode a)› ‹valid_edge a› ‹inner_node n›
        ‹targetnode a -as'→⇩ι* n›
      obtain asx pex where "targetnode a -asx→⇩ι* pex" and "method_exit pex"
        and "n ∉ set (sourcenodes asx)"
        by(fastforce dest:inner_is_valid simp:postdominate_def)
      show ?thesis
      proof(cases "∃asx'. asx = as'@asx'")
        case True
        then obtain asx' where [simp]:"asx = as'@asx'" by blast
        from ‹targetnode a -asx→⇩ι* pex› ‹targetnode a -as'→⇩ι* n›
          ‹as' ≠ []› ‹method_exit pex› ‹¬ method_exit n›
        obtain a'' as'' where "asx' = a''#as'' ∧ sourcenode a'' = n"
          by(cases asx')(auto dest:path_split path_det simp:intra_path_def)
        hence "n ∈ set(sourcenodes asx)" by(simp add:sourcenodes_def)
        with ‹n ∉ set (sourcenodes asx)› have False by simp
        thus ?thesis by simp
      next
        case False
        hence "∀asx'. asx ≠ as'@asx'" by simp
        then obtain j asx' where "asx = (take j as')@asx'"
          and "j < length as'" and "∀k > j. ∀asx''. asx ≠ (take k as')@asx''"
          by(auto elim:path_split_general)
        from ‹asx = (take j as')@asx'› ‹j < length as'›
        have "∃as'1 as'2. asx = as'1@asx' ∧ 
          as' = as'1@as'2 ∧ as'2 ≠ [] ∧ as'1 = take j as'"
          by simp(rule_tac x= "drop j as'" in exI,simp)
        then obtain as'1 as'' where "asx = as'1@asx'"
          and "as'1 = take j as'"
          and "as' = as'1@as''" and "as'' ≠ []" by blast
        from ‹as' = as'1@as''› ‹as'' ≠ []› obtain a1 as'2 
          where "as' = as'1@a1#as'2" and "as'' = a1#as'2"
          by(cases as'') auto
        have "asx' ≠ []"
        proof(cases "asx' = []")
          case True
          with ‹asx = as'1@asx'› ‹as' = as'1@as''› ‹as'' = a1#as'2›
          have "as' = asx@a1#as'2" by simp
          with ‹n' -a#as'→⇩ι* n› have "n' -(a#asx)@a1#as'2→⇩ι* n" by simp
          hence "n' -(a#asx)@a1#as'2→* n" 
            and "∀ax ∈ set((a#asx)@a1#as'2). intra_kind(kind ax)"
            by(simp_all add:intra_path_def)
          from ‹n' -(a#asx)@a1#as'2→* n›
          have "n' -a#asx→* sourcenode a1" and "valid_edge a1"
            by -(erule path_split)+
          from ‹∀ax ∈ set((a#asx)@a1#as'2). intra_kind(kind ax)› 
          have "∀ax ∈ set(a#asx). intra_kind(kind ax)" by simp
          with ‹n' -a#asx→* sourcenode a1› have "n' -a#asx→⇩ι* sourcenode a1"
            by(simp add:intra_path_def)
          hence "targetnode a -asx→⇩ι* sourcenode a1"
            by(fastforce intro:path_split_Cons simp:intra_path_def)
          with ‹targetnode a -asx→⇩ι* pex› have "pex = sourcenode a1"
            by(fastforce intro:path_det simp:intra_path_def)
          from ‹∀ax ∈ set((a#asx)@a1#as'2). intra_kind(kind ax)›
          have "intra_kind (kind a1)" by simp
          from ‹method_exit pex› have False
          proof(rule method_exit_cases)
            assume "pex = (_Exit_)"
            with ‹pex = sourcenode a1› have "sourcenode a1 = (_Exit_)" by simp
            with ‹valid_edge a1› show False by(rule Exit_source)
          next
            fix a Q f p assume "pex = sourcenode a" and "valid_edge a"
              and "kind a = Q↩⇘p⇙f"
            from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› ‹pex = sourcenode a› 
              ‹pex = sourcenode a1› ‹valid_edge a1› ‹intra_kind (kind a1)›
            show False by(fastforce dest:return_edges_only simp:intra_kind_def)
          qed
          thus ?thesis by simp
        qed simp
        with ‹asx = as'1@asx'› obtain a2 asx'1 
          where "asx = as'1@a2#asx'1"
          and "asx' = a2#asx'1" by(cases asx') auto
        from ‹n' -a#as'→⇩ι* n› ‹as' = as'1@a1#as'2› 
        have "n' -(a#as'1)@a1#as'2→⇩ι* n" by simp
        hence "n' -(a#as'1)@a1#as'2→* n" 
          and "∀ax ∈ set((a#as'1)@a1#as'2). intra_kind(kind ax)"
          by(simp_all add: intra_path_def)
        from ‹n' -(a#as'1)@a1#as'2→* n› have "n' -a#as'1→* sourcenode a1"
          and "valid_edge a1" by -(erule path_split)+
        from ‹∀ax ∈ set((a#as'1)@a1#as'2). intra_kind(kind ax)›
        have "∀ax ∈ set(a#as'1). intra_kind(kind ax)" by simp
        with ‹n' -a#as'1→* sourcenode a1› have "n' -a#as'1→⇩ι* sourcenode a1"
          by(simp add:intra_path_def)
        hence "targetnode a -as'1→⇩ι* sourcenode a1"
          by(fastforce intro:path_split_Cons simp:intra_path_def)
        from ‹targetnode a -asx→⇩ι* pex› ‹asx = as'1@a2#asx'1›
        have "targetnode a -as'1@a2#asx'1→* pex" by(simp add:intra_path_def)
        hence "targetnode a -as'1→* sourcenode a2" and "valid_edge a2"
          and "targetnode a2 -asx'1→* pex" by(auto intro:path_split)
        from ‹targetnode a2 -asx'1→* pex› ‹asx = as'1@a2#asx'1›
          ‹targetnode a -asx→⇩ι* pex›
        have "targetnode a2 -asx'1→⇩ι* pex" by(simp add:intra_path_def)
        from ‹targetnode a -as'1→* sourcenode a2› 
          ‹targetnode a -as'1→⇩ι* sourcenode a1› 
        have "sourcenode a1 = sourcenode a2"
          by(fastforce intro:path_det simp:intra_path_def)
        from ‹asx = as'1@a2#asx'1› ‹n ∉ set (sourcenodes asx)›
        have "n ∉ set (sourcenodes asx'1)" by(simp add:sourcenodes_def)
        with ‹targetnode a2 -asx'1→⇩ι* pex› ‹method_exit pex›
          ‹asx = as'1@a2#asx'1›
        have "¬ n postdominates targetnode a2" by(fastforce simp:postdominate_def)
        from ‹asx = as'1@a2#asx'1› ‹targetnode a -asx→⇩ι* pex›
        have "intra_kind (kind a2)" by(simp add:intra_path_def)
        from ‹as' = as'1@a1#as'2› have "a1 ∈ set as'" by simp
        with ‹sourcenode a1 = sourcenode a2› last ‹valid_edge a2› 
          ‹intra_kind (kind a2)›
        have "n postdominates targetnode a2" by blast
        with ‹¬ n postdominates targetnode a2› have False by simp
        thus ?thesis by simp
      qed
    qed
  qed
qed



subsection ‹SDG without summary edges›


inductive cdep_edge :: "'node SDG_node ⇒ 'node SDG_node ⇒ bool" 
    ("_ ⟶⇘cd⇙ _" [51,0] 80)
  and ddep_edge :: "'node SDG_node ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
    ("_ -_→⇩d⇩d _" [51,0,0] 80)
  and call_edge :: "'node SDG_node ⇒ 'pname ⇒ 'node SDG_node ⇒ bool" 
    ("_ -_→⇘call⇙ _" [51,0,0] 80)
  and return_edge :: "'node SDG_node ⇒ 'pname ⇒ 'node SDG_node ⇒ bool" 
    ("_ -_→⇘ret⇙ _" [51,0,0] 80)
  and param_in_edge :: "'node SDG_node ⇒ 'pname ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
    ("_ -_:_→⇘in⇙ _" [51,0,0,0] 80)
  and param_out_edge :: "'node SDG_node ⇒ 'pname ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
    ("_ -_:_→⇘out⇙ _" [51,0,0,0] 80)
  and SDG_edge :: "'node SDG_node ⇒ 'var option ⇒ 
                          ('pname × bool) option ⇒ 'node SDG_node ⇒ bool"

where
    (* Syntax *)
  "n ⟶⇘cd⇙ n' == SDG_edge n None None n'"
  | "n -V→⇩d⇩d n' == SDG_edge n (Some V) None n'"
  | "n -p→⇘call⇙ n' == SDG_edge n None (Some(p,True)) n'"
  | "n -p→⇘ret⇙ n' == SDG_edge n None (Some(p,False)) n'"
  | "n -p:V→⇘in⇙ n' == SDG_edge n (Some V) (Some(p,True)) n'"
  | "n -p:V→⇘out⇙ n' == SDG_edge n (Some V) (Some(p,False)) n'"

    (* Rules *)
  | SDG_cdep_edge:
    "⟦n = CFG_node m; n' = CFG_node m'; m controls m'⟧ ⟹ n ⟶⇘cd⇙ n'"
  | SDG_proc_entry_exit_cdep:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; n = CFG_node (targetnode a);
      a' ∈ get_return_edges a; n' = CFG_node (sourcenode a')⟧ ⟹ n ⟶⇘cd⇙ n'"
  | SDG_parent_cdep_edge:
    "⟦valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n ≠ n'⟧ 
      ⟹ n ⟶⇘cd⇙ n'"
  | SDG_ddep_edge:"n influences V in n' ⟹ n -V→⇩d⇩d n'"
  | SDG_call_edge:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; n = CFG_node (sourcenode a); 
      n' = CFG_node (targetnode a)⟧ ⟹ n -p→⇘call⇙ n'"
  | SDG_return_edge:
    "⟦valid_edge a; kind a = Q↩⇘p⇙f; n = CFG_node (sourcenode a); 
      n' = CFG_node (targetnode a)⟧ ⟹ n -p→⇘ret⇙ n'"
  | SDG_param_in_edge:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; (p,ins,outs) ∈ set procs; V = ins!x;
      x < length ins; n = Actual_in (sourcenode a,x); n' = Formal_in (targetnode a,x)⟧
      ⟹ n -p:V→⇘in⇙ n'"
  | SDG_param_out_edge:
    "⟦valid_edge a; kind a = Q↩⇘p⇙f; (p,ins,outs) ∈ set procs; V = outs!x;
      x < length outs; n = Formal_out (sourcenode a,x); 
      n' = Actual_out (targetnode a,x)⟧
      ⟹ n -p:V→⇘out⇙ n'"


lemma cdep_edge_cases:
  "⟦n ⟶⇘cd⇙ n'; (parent_node n) controls (parent_node n') ⟹ P;
    ⋀a Q r p fs a'. ⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges a;
                  parent_node n = targetnode a; parent_node n' = sourcenode a'⟧ ⟹ P;
    ⋀m. ⟦n = CFG_node m; m = parent_node n'; n ≠ n'⟧ ⟹ P⟧ ⟹ P"
by -(erule SDG_edge.cases,auto)


lemma SDG_edge_valid_SDG_node:
  assumes "SDG_edge n Vopt popt n'" 
  shows "valid_SDG_node n" and "valid_SDG_node n'"
using ‹SDG_edge n Vopt popt n'›
proof(induct rule:SDG_edge.induct)
  case (SDG_cdep_edge n m n' m') 
  thus "valid_SDG_node n" "valid_SDG_node n'"
    by(fastforce elim:control_dependence_path elim:path_valid_node 
                simp:intra_path_def)+
next
  case (SDG_proc_entry_exit_cdep a Q r p f n a' n') case 1
  from ‹valid_edge a› ‹n = CFG_node (targetnode a)› show ?case by simp
next
  case (SDG_proc_entry_exit_cdep a Q r p f n a' n') case 2
  from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'" 
    by(rule get_return_edges_valid)
  with ‹n' = CFG_node (sourcenode a')› show ?case by simp
next
  case (SDG_ddep_edge n V n')
  thus "valid_SDG_node n" "valid_SDG_node n'" 
    by(auto intro:in_Use_valid_SDG_node in_Def_valid_SDG_node
             simp:data_dependence_def)
qed(fastforce intro:valid_SDG_CFG_node)+


lemma valid_SDG_node_cases: 
  assumes "valid_SDG_node n"
  shows "n = CFG_node (parent_node n) ∨ CFG_node (parent_node n) ⟶⇘cd⇙ n"
proof(cases n)
  case (CFG_node m) thus ?thesis by simp
next
  case (Formal_in z)
  from ‹n = Formal_in z› obtain m x where "z = (m,x)" by(cases z) auto
  with ‹valid_SDG_node n› ‹n = Formal_in z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
    by -(rule SDG_parent_cdep_edge,auto)
  thus ?thesis by fastforce
next
  case (Formal_out z)
  from ‹n = Formal_out z› obtain m x where "z = (m,x)" by(cases z) auto
  with ‹valid_SDG_node n› ‹n = Formal_out z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
    by -(rule SDG_parent_cdep_edge,auto)
  thus ?thesis by fastforce
next
  case (Actual_in z)
  from ‹n = Actual_in z› obtain m x where "z = (m,x)" by(cases z) auto
  with ‹valid_SDG_node n› ‹n = Actual_in z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
    by -(rule SDG_parent_cdep_edge,auto)
  thus ?thesis by fastforce
next
  case (Actual_out z)
  from ‹n = Actual_out z› obtain m x where "z = (m,x)" by(cases z) auto
  with ‹valid_SDG_node n› ‹n = Actual_out z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
    by -(rule SDG_parent_cdep_edge,auto)
  thus ?thesis by fastforce
qed


lemma SDG_cdep_edge_CFG_node: "n ⟶⇘cd⇙ n' ⟹ ∃m. n = CFG_node m"
by(induct n Vopt≡"None::'var option" popt≡"None::('pname × bool) option" n' 
   rule:SDG_edge.induct) auto

lemma SDG_call_edge_CFG_node: "n -p→⇘call⇙ n' ⟹ ∃m. n = CFG_node m"
by(induct n Vopt≡"None::'var option" popt≡"Some(p,True)" n' 
   rule:SDG_edge.induct) auto

lemma SDG_return_edge_CFG_node: "n -p→⇘ret⇙ n' ⟹ ∃m. n = CFG_node m"
by(induct n Vopt≡"None::'var option" popt≡"Some(p,False)" n' 
   rule:SDG_edge.induct) auto



lemma SDG_call_or_param_in_edge_unique_CFG_call_edge:
  "SDG_edge n Vopt (Some(p,True)) n'
  ⟹ ∃!a. valid_edge a ∧ sourcenode a = parent_node n ∧ 
          targetnode a = parent_node n' ∧ (∃Q r fs. kind a = Q:r↪⇘p⇙fs)"
proof(induct n Vopt "Some(p,True)" n' rule:SDG_edge.induct)
  case (SDG_call_edge a Q r fs n n')
  { fix a' 
    assume "valid_edge a'" and "sourcenode a' = parent_node n"
      and "targetnode a' = parent_node n'"
    from ‹sourcenode a' = parent_node n› ‹n = CFG_node (sourcenode a)›
    have "sourcenode a' = sourcenode a" by fastforce
    moreover from ‹targetnode a' = parent_node n'› ‹n' = CFG_node (targetnode a)›
    have "targetnode a' = targetnode a" by fastforce
    ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
      by(fastforce intro:edge_det) }
  with ‹valid_edge a› ‹n = CFG_node (sourcenode a)› ‹n' = CFG_node (targetnode a)›
    ‹kind a = Q:r↪⇘p⇙fs› show ?case by(fastforce intro!:ex1I[of _ a])
next
  case (SDG_param_in_edge a Q r fs ins outs V x n n')
  { fix a' 
    assume "valid_edge a'" and "sourcenode a' = parent_node n"
      and "targetnode a' = parent_node n'"
    from ‹sourcenode a' = parent_node n› ‹n = Actual_in (sourcenode a,x)›
    have "sourcenode a' = sourcenode a" by fastforce
    moreover from ‹targetnode a' = parent_node n'› ‹n' = Formal_in (targetnode a,x)›
    have "targetnode a' = targetnode a" by fastforce
    ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
      by(fastforce intro:edge_det) }
  with ‹valid_edge a› ‹n = Actual_in (sourcenode a,x)› 
    ‹n' = Formal_in (targetnode a,x)› ‹kind a = Q:r↪⇘p⇙fs›
  show ?case by(fastforce intro!:ex1I[of _ a])
qed simp_all


lemma SDG_return_or_param_out_edge_unique_CFG_return_edge:
  "SDG_edge n Vopt (Some(p,False)) n'
  ⟹ ∃!a. valid_edge a ∧ sourcenode a = parent_node n ∧ 
          targetnode a = parent_node n' ∧ (∃Q f. kind a = Q↩⇘p⇙f)"
proof(induct n Vopt "Some(p,False)" n' rule:SDG_edge.induct)
  case (SDG_return_edge a Q f n n')
  { fix a' 
    assume "valid_edge a'" and "sourcenode a' = parent_node n" 
      and "targetnode a' = parent_node n'"
    from ‹sourcenode a' = parent_node n› ‹n = CFG_node (sourcenode a)›
    have "sourcenode a' = sourcenode a" by fastforce
    moreover from ‹targetnode a' = parent_node n'› ‹n' = CFG_node (targetnode a)›
    have "targetnode a' = targetnode a" by fastforce
    ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
      by(fastforce intro:edge_det) }
  with ‹valid_edge a› ‹n = CFG_node (sourcenode a)› ‹n' = CFG_node (targetnode a)›
    ‹kind a = Q↩⇘p⇙f› show ?case by(fastforce intro!:ex1I[of _ a])
next
  case (SDG_param_out_edge a Q f ins outs V x n n')
  { fix a' 
    assume "valid_edge a'" and "sourcenode a' = parent_node n"
      and "targetnode a' = parent_node n'"
    from ‹sourcenode a' = parent_node n› ‹n = Formal_out (sourcenode a,x)›
    have "sourcenode a' = sourcenode a" by fastforce
    moreover from ‹targetnode a' = parent_node n'› ‹n' = Actual_out (targetnode a,x)›
    have "targetnode a' = targetnode a" by fastforce
    ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
      by(fastforce intro:edge_det) }
  with ‹valid_edge a› ‹n = Formal_out (sourcenode a,x)›
    ‹n' = Actual_out (targetnode a,x)› ‹kind a = Q↩⇘p⇙f›
  show ?case by(fastforce intro!:ex1I[of _ a])
qed simp_all


lemma Exit_no_SDG_edge_source:
  "SDG_edge (CFG_node (_Exit_)) Vopt popt n' ⟹ False"
proof(induct "CFG_node (_Exit_)" Vopt popt n' rule:SDG_edge.induct)
  case (SDG_cdep_edge m n' m')
  hence "(_Exit_) controls m'" by simp
  thus ?case by fastforce
next
  case (SDG_proc_entry_exit_cdep a Q r p fs a' n')
  from ‹CFG_node (_Exit_) = CFG_node (targetnode a)›
  have "targetnode a = (_Exit_)" by simp
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
    by(rule get_proc_call)
  with ‹targetnode a = (_Exit_)› have "p = Main"
    by(auto simp:get_proc_Exit)
  with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have False
    by(fastforce intro:Main_no_call_target)
  thus ?thesis by simp
next
  case (SDG_parent_cdep_edge n' m)
  from ‹CFG_node (_Exit_) = CFG_node m› 
  have [simp]:"m = (_Exit_)" by simp
  with ‹valid_SDG_node n'› ‹m = parent_node n'› ‹CFG_node (_Exit_) ≠ n'›
  have False by -(drule valid_SDG_node_parent_Exit,simp+)
  thus ?thesis by simp
next
  case (SDG_ddep_edge V n')
  hence "(CFG_node (_Exit_)) influences V in n'" by simp
  with Exit_empty show ?case
    by(fastforce dest:path_Exit_source SDG_Def_parent_Def 
                simp:data_dependence_def intra_path_def)
next
  case (SDG_call_edge a Q r p fs n')
  from ‹CFG_node (_Exit_) = CFG_node (sourcenode a)›
  have "sourcenode a = (_Exit_)" by simp
  with ‹valid_edge a› show ?case by(rule Exit_source)
next
  case (SDG_return_edge a Q p f n')
  from ‹CFG_node (_Exit_) = CFG_node (sourcenode a)›
  have "sourcenode a = (_Exit_)" by simp
  with ‹valid_edge a› show ?case by(rule Exit_source)
qed simp_all


subsection ‹Intraprocedural paths in the SDG›

inductive intra_SDG_path :: 
  "'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
("_ i-_→⇩d* _" [51,0,0] 80) 

where iSp_Nil:
  "valid_SDG_node n ⟹ n i-[]→⇩d* n"

  | iSp_Append_cdep:
  "⟦n i-ns→⇩d* n''; n'' ⟶⇘cd⇙ n'⟧ ⟹ n i-ns@[n'']→⇩d* n'"

  | iSp_Append_ddep:
  "⟦n i-ns→⇩d* n''; n'' -V→⇩d⇩d n'; n'' ≠ n'⟧ ⟹ n i-ns@[n'']→⇩d* n'"


lemma intra_SDG_path_Append:
  "⟦n'' i-ns'→⇩d* n'; n i-ns→⇩d* n''⟧ ⟹ n i-ns@ns'→⇩d* n'"
by(induct rule:intra_SDG_path.induct,
   auto intro:intra_SDG_path.intros simp:append_assoc[THEN sym] simp del:append_assoc)


lemma intra_SDG_path_valid_SDG_node:
  assumes "n i-ns→⇩d* n'" shows "valid_SDG_node n" and "valid_SDG_node n'"
using ‹n i-ns→⇩d* n'›
by(induct rule:intra_SDG_path.induct,
   auto intro:SDG_edge_valid_SDG_node valid_SDG_CFG_node)


lemma intra_SDG_path_intra_CFG_path:
  assumes "n i-ns→⇩d* n'"
  obtains as where "parent_node n -as→⇩ι* parent_node n'" 
proof(atomize_elim)
  from ‹n i-ns→⇩d* n'›
  show "∃as. parent_node n -as→⇩ι* parent_node n'"
  proof(induct rule:intra_SDG_path.induct)
    case (iSp_Nil n)
    from ‹valid_SDG_node n› have "valid_node (parent_node n)"
      by(rule valid_SDG_CFG_node)
    hence "parent_node n -[]→* parent_node n" by(rule empty_path)
    thus ?case by(auto simp:intra_path_def)
  next
    case (iSp_Append_cdep n ns n'' n')
    from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
    obtain as where "parent_node n -as→⇩ι* parent_node n''" by blast
    from ‹n'' ⟶⇘cd⇙ n'› show ?case
    proof(rule cdep_edge_cases)
      assume "parent_node n'' controls parent_node n'"
      then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'" and "as' ≠ []"
        by(erule control_dependence_path)
      with ‹parent_node n -as→⇩ι* parent_node n''› 
      have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
      thus ?thesis by blast
    next
      fix a Q r p fs a'
      assume "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "a' ∈ get_return_edges a"
        and "parent_node n'' = targetnode a" and "parent_node n' = sourcenode a'"
      then obtain a'' where "valid_edge a''" and "sourcenode a'' = targetnode a"
        and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)⇩√"
        by(auto dest:intra_proc_additional_edge)
      hence "targetnode a -[a'']→⇩ι* sourcenode a'"
        by(fastforce dest:path_edge simp:intra_path_def intra_kind_def)
      with ‹parent_node n'' = targetnode a› ‹parent_node n' = sourcenode a'› 
      have "∃as'. parent_node n'' -as'→⇩ι* parent_node n' ∧ as' ≠ []" by fastforce
      then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'" and "as' ≠ []"
        by blast
      with ‹parent_node n -as→⇩ι* parent_node n''›
      have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
      thus ?thesis by blast
    next
      fix m assume "n'' = CFG_node m" and "m = parent_node n'"
      with ‹parent_node n -as→⇩ι* parent_node n''› show ?thesis by fastforce
    qed
  next
    case (iSp_Append_ddep n ns n'' V n')
    from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
    obtain as where "parent_node n -as→⇩ι* parent_node n''" by blast 
    from ‹n'' -V→⇩d⇩d n'› have "n'' influences V in n'"
      by(fastforce elim:SDG_edge.cases)
    then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'"
      by(auto simp:data_dependence_def)
    with ‹parent_node n -as→⇩ι* parent_node n''› 
    have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
    thus ?case by blast
  qed
qed


subsection ‹Control dependence paths in the SDG›

inductive cdep_SDG_path :: 
  "'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
("_ cd-_→⇩d* _" [51,0,0] 80) 

where cdSp_Nil:
  "valid_SDG_node n ⟹ n cd-[]→⇩d* n"

  | cdSp_Append_cdep:
  "⟦n cd-ns→⇩d* n''; n'' ⟶⇘cd⇙ n'⟧ ⟹ n cd-ns@[n'']→⇩d* n'"


lemma cdep_SDG_path_intra_SDG_path:
  "n cd-ns→⇩d* n' ⟹ n i-ns→⇩d* n'"
by(induct rule:cdep_SDG_path.induct,auto intro:intra_SDG_path.intros)


lemma Entry_cdep_SDG_path:
  assumes "(_Entry_) -as→⇩ι* n'" and "inner_node n'" and "¬ method_exit n'"
  obtains ns where "CFG_node (_Entry_) cd-ns→⇩d* CFG_node n'"
  and "ns ≠ []" and "∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as)"
proof(atomize_elim)
  from ‹(_Entry_) -as→⇩ι* n'› ‹inner_node n'› ‹¬ method_exit n'›
  show "∃ns. CFG_node (_Entry_) cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
    (∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as))"
  proof(induct as arbitrary:n' rule:length_induct)
    fix as n'
    assume IH:"∀as'. length as' < length as ⟶
      (∀n''. (_Entry_) -as'→⇩ι* n'' ⟶ inner_node n'' ⟶ ¬ method_exit n'' ⟶
        (∃ns. CFG_node (_Entry_) cd-ns→⇩d* CFG_node n'' ∧ ns ≠ [] ∧
              (∀nx∈set ns. parent_node nx ∈ set (sourcenodes as'))))"
      and "(_Entry_) -as→⇩ι* n'" and "inner_node n'" and "¬ method_exit n'"
    thus "∃ns. CFG_node (_Entry_) cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
      (∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as))"
    proof -
      have "∃ax asx zs. (_Entry_) -ax#asx→⇩ι* n' ∧ n' ∉ set (sourcenodes (ax#asx)) ∧ 
                        as = (ax#asx)@zs"
      proof(cases "n' ∈ set (sourcenodes as)")
        case True
        hence "∃n'' ∈ set(sourcenodes as). n' = n''" by simp
        then obtain ns' ns'' where "sourcenodes as = ns'@n'#ns''"
          and "∀n'' ∈ set ns'. n' ≠ n''"
          by(fastforce elim!:split_list_first_propE)
        from ‹sourcenodes as = ns'@n'#ns''› obtain xs ys ax
          where "sourcenodes xs = ns'" and "as = xs@ax#ys"
          and "sourcenode ax = n'"
          by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
        from ‹∀n'' ∈ set ns'. n' ≠ n''› ‹sourcenodes xs = ns'›
        have "n' ∉ set(sourcenodes xs)" by fastforce
        from ‹(_Entry_) -as→⇩ι* n'› ‹as = xs@ax#ys› have "(_Entry_) -xs@ax#ys→⇩ι* n'"
          by simp
        with ‹sourcenode ax = n'› have "(_Entry_) -xs→⇩ι* n'" 
          by(fastforce dest:path_split simp:intra_path_def)
        with ‹inner_node n'› have "xs ≠ []"
          by(fastforce elim:path.cases simp:intra_path_def)
        with ‹n' ∉ set(sourcenodes xs)› ‹(_Entry_) -xs→⇩ι* n'› ‹as = xs@ax#ys›
        show ?thesis by(cases xs) auto
      next
        case False
        with ‹(_Entry_) -as→⇩ι* n'› ‹inner_node n'›
        show ?thesis by(cases as)(auto elim:path.cases simp:intra_path_def)
      qed
      then obtain ax asx zs where "(_Entry_) -ax#asx→⇩ι* n'" 
        and "n' ∉ set (sourcenodes (ax#asx))" and "as = (ax#asx)@zs" by blast
      show ?thesis
      proof(cases "∀a' a''. a' ∈ set asx ∧ sourcenode a' = sourcenode a'' ∧ 
          valid_edge a'' ∧ intra_kind(kind a'') ⟶ n' postdominates targetnode a''")
        case True
        have "(_Exit_) -[]→⇩ι* (_Exit_)" 
          by(fastforce intro:empty_path simp:intra_path_def)
        hence "¬ n' postdominates (_Exit_)"
          by(fastforce simp:postdominate_def sourcenodes_def method_exit_def)
        from ‹(_Entry_) -ax#asx→⇩ι* n'› have "(_Entry_) -[]@ax#asx→⇩ι* n'" by simp
        from ‹(_Entry_) -ax#asx→⇩ι* n'› have [simp]:"sourcenode ax = (_Entry_)" 
          and "valid_edge ax"
          by(auto intro:path_split_Cons simp:intra_path_def)
        from Entry_Exit_edge obtain a' where "sourcenode a' = (_Entry_)"
          and "targetnode a' = (_Exit_)" and "valid_edge a'" 
          and "intra_kind(kind a')" by(auto simp:intra_kind_def)
        with ‹(_Entry_) -[]@ax#asx→⇩ι* n'› ‹¬ n' postdominates (_Exit_)›
          ‹valid_edge ax› True ‹sourcenode ax = (_Entry_)› 
          ‹n' ∉ set (sourcenodes (ax#asx))› ‹inner_node n'› ‹¬ method_exit n'›
        have "sourcenode ax controls n'"
          by -(erule which_node_intra_standard_control_dependence_source
                     [of _ _ _ _ _ _ a'],auto)
        hence "CFG_node (_Entry_) ⟶⇘cd⇙ CFG_node n'"
          by(fastforce intro:SDG_cdep_edge)
        hence "CFG_node (_Entry_) cd-[]@[CFG_node (_Entry_)]→⇩d* CFG_node n'"
          by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
        moreover
        from ‹as = (ax#asx)@zs› have "(_Entry_) ∈ set(sourcenodes as)"
          by(simp add:sourcenodes_def)
        ultimately show ?thesis by fastforce
      next
        case False
        hence "∃a' ∈ set asx. ∃a''. sourcenode a' = sourcenode a'' ∧ valid_edge a'' ∧
          intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a''"
          by fastforce
        then obtain ax' asx' asx'' where "asx = asx'@ax'#asx'' ∧
          (∃a''. sourcenode ax' = sourcenode a'' ∧ valid_edge a'' ∧
          intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'') ∧
          (∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ valid_edge a'' ∧
          intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a''))"
          by(blast elim!:split_list_last_propE)
        then obtain ai where "asx = asx'@ax'#asx''"
          and "sourcenode ax' = sourcenode ai"
          and "valid_edge ai" and "intra_kind(kind ai)"
          and "¬ n' postdominates targetnode ai"
          and "∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ 
          valid_edge a'' ∧ intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'')"
          by blast
        from ‹(_Entry_) -ax#asx→⇩ι* n'› ‹asx = asx'@ax'#asx''›
        have "(_Entry_) -(ax#asx')@ax'#asx''→⇩ι* n'" by simp
        from ‹n' ∉ set (sourcenodes (ax#asx))› ‹asx = asx'@ax'#asx''›
        have "n' ∉ set (sourcenodes (ax'#asx''))"
          by(auto simp:sourcenodes_def)
        with ‹inner_node n'› ‹¬ n' postdominates targetnode ai›
          ‹n' ∉ set (sourcenodes (ax'#asx''))› ‹sourcenode ax' = sourcenode ai›
          ‹∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ 
          valid_edge a'' ∧ intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'')›
          ‹valid_edge ai› ‹intra_kind(kind ai)› ‹¬ method_exit n'›
          ‹(_Entry_) -(ax#asx')@ax'#asx''→⇩ι* n'›
        have "sourcenode ax' controls n'"
          by(fastforce intro!:which_node_intra_standard_control_dependence_source)
        hence "CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'"
          by(fastforce intro:SDG_cdep_edge)
        from ‹(_Entry_) -(ax#asx')@ax'#asx''→⇩ι* n'›
        have "(_Entry_) -ax#asx'→⇩ι* sourcenode ax'" and "valid_edge ax'"
          by(auto intro:path_split simp:intra_path_def simp del:append_Cons)
        from ‹asx = asx'@ax'#asx''› ‹as = (ax#asx)@zs›
        have "length (ax#asx') < length as" by simp
        from ‹valid_edge ax'› have "valid_node (sourcenode ax')" by simp
        hence "inner_node (sourcenode ax')"
        proof(cases "sourcenode ax'" rule:valid_node_cases)
          case Entry 
          with ‹(_Entry_) -ax#asx'→⇩ι* sourcenode ax'›
          have "(_Entry_) -ax#asx'→* (_Entry_)" by(simp add:intra_path_def)
          hence False by(fastforce dest:path_Entry_target)
          thus ?thesis by simp
        next
          case Exit
          with ‹valid_edge ax'› have False by(rule Exit_source)
          thus ?thesis by simp
        qed simp
        from ‹asx = asx'@ax'#asx''› ‹(_Entry_) -ax#asx→⇩ι* n'›
        have "intra_kind (kind ax')" by(simp add:intra_path_def)
        have "¬ method_exit (sourcenode ax')"
        proof
          assume "method_exit (sourcenode ax')"
          thus False
          proof(rule method_exit_cases)
            assume "sourcenode ax' = (_Exit_)"
            with ‹valid_edge ax'› show False by(rule Exit_source)
          next
            fix x Q f p assume " sourcenode ax' = sourcenode x"
              and "valid_edge x" and "kind x = Q↩⇘p⇙f"
            from ‹valid_edge x› ‹kind x = Q↩⇘p⇙f› ‹sourcenode ax' = sourcenode x›
            ‹valid_edge ax'› ‹intra_kind (kind ax')› show False
              by(fastforce dest:return_edges_only simp:intra_kind_def)
          qed
        qed
        with IH ‹length (ax#asx') < length as› ‹(_Entry_) -ax#asx'→⇩ι* sourcenode ax'›
          ‹inner_node (sourcenode ax')›
        obtain ns where "CFG_node (_Entry_) cd-ns→⇩d* CFG_node (sourcenode ax')"
          and "ns ≠ []" 
          and "∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes (ax#asx'))"
          by blast
        from ‹CFG_node (_Entry_) cd-ns→⇩d* CFG_node (sourcenode ax')›
          ‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'›
        have "CFG_node (_Entry_) cd-ns@[CFG_node (sourcenode ax')]→⇩d* CFG_node n'"
          by(fastforce intro:cdSp_Append_cdep)
        from ‹as = (ax#asx)@zs› ‹asx = asx'@ax'#asx''›
        have "sourcenode ax' ∈ set(sourcenodes as)" by(simp add:sourcenodes_def)
        with ‹∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes (ax#asx'))›
          ‹as = (ax#asx)@zs› ‹asx = asx'@ax'#asx''›
        have "∀n'' ∈ set (ns@[CFG_node (sourcenode ax')]).
          parent_node n'' ∈ set(sourcenodes as)"
          by(fastforce simp:sourcenodes_def)
        with ‹CFG_node (_Entry_) cd-ns@[CFG_node (sourcenode ax')]→⇩d* CFG_node n'›
        show ?thesis by fastforce
      qed
    qed
  qed
qed


lemma in_proc_cdep_SDG_path:
  assumes "n -as→⇩ι* n'" and "n ≠ n'" and "n' ≠ (_Exit_)" and "valid_edge a"
  and "kind a = Q:r↪⇘p⇙fs" and "targetnode a = n"
  obtains ns where "CFG_node n cd-ns→⇩d* CFG_node n'"
  and "ns ≠ []" and "∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as)"
proof(atomize_elim)
  show "∃ns. CFG_node n cd-ns→⇩d* CFG_node n' ∧
             ns ≠ [] ∧ (∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as))"
  proof(cases "∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶ 
                    ax ∉ get_return_edges a")
    case True
    from ‹n -as→⇩ι* n'› ‹n ≠ n'› ‹n' ≠ (_Exit_)›
      ‹∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶ ax ∉ get_return_edges a›
    show "∃ns. CFG_node n cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
      (∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as))"
    proof(induct as arbitrary:n' rule:length_induct)
      fix as n'
      assume IH:"∀as'. length as' < length as ⟶
        (∀n''. n -as'→⇩ι* n'' ⟶ n ≠ n'' ⟶ n'' ≠ (_Exit_) ⟶
          (∀ax. valid_edge ax ∧ sourcenode ax = n'' ⟶ ax ∉ get_return_edges a) ⟶
            (∃ns. CFG_node n cd-ns→⇩d* CFG_node n'' ∧ ns ≠ [] ∧
                  (∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as'))))"
        and "n -as→⇩ι* n'" and "n ≠ n'" and "n' ≠ (_Exit_)"
        and "∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶ ax ∉ get_return_edges a"
      show "∃ns. CFG_node n cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
                 (∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as))"
      proof(cases "method_exit n'")
        case True
        thus ?thesis
        proof(rule method_exit_cases)
          assume "n' = (_Exit_)"
          with ‹n' ≠ (_Exit_)› have False by simp
          thus ?thesis by simp
        next
          fix a' Q' f' p'
          assume "n' = sourcenode a'" and "valid_edge a'" and "kind a' = Q'↩⇘p'⇙f'"
          from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc(targetnode a) = p"
            by(rule get_proc_call)
          from ‹n -as→⇩ι* n'› have "get_proc n = get_proc n'" 
            by(rule intra_path_get_procs)
          with ‹get_proc(targetnode a) = p› ‹targetnode a = n›
          have "get_proc (targetnode a) = get_proc n'" by simp
          from ‹valid_edge a'› ‹kind a' = Q'↩⇘p'⇙f'›
          have "get_proc (sourcenode a') = p'" by(rule get_proc_return)
          with ‹n' = sourcenode a'› ‹get_proc (targetnode a) = get_proc n'› 
            ‹get_proc (targetnode a) = p› have "p = p'" by simp
          with ‹valid_edge a'› ‹kind a' = Q'↩⇘p'⇙f'›
          obtain ax where "valid_edge ax" and "∃Q r fs. kind ax = Q:r↪⇘p⇙fs"
            and "a' ∈ get_return_edges ax" by(auto dest:return_needs_call)
          hence "CFG_node (targetnode ax) ⟶⇘cd⇙ CFG_node (sourcenode a')"
            by(fastforce intro:SDG_proc_entry_exit_cdep)
          with ‹valid_edge ax› 
          have "CFG_node (targetnode ax) cd-[]@[CFG_node (targetnode ax)]→⇩d* 
            CFG_node (sourcenode a')"
            by(fastforce intro:cdep_SDG_path.intros)
          from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹valid_edge ax› 
            ‹∃Q r fs. kind ax = Q:r↪⇘p⇙fs› have "targetnode a = targetnode ax"
            by(fastforce intro:same_proc_call_unique_target)
          from ‹n -as→⇩ι* n'› ‹n ≠ n'›
          have "as ≠ []" by(fastforce elim:path.cases simp:intra_path_def)
          with ‹n -as→⇩ι* n'› have "hd (sourcenodes as) = n"
            by(fastforce intro:path_sourcenode simp:intra_path_def)
          moreover
          from ‹as ≠ []› have "hd (sourcenodes as) ∈ set (sourcenodes as)"
            by(fastforce intro:hd_in_set simp:sourcenodes_def)
          ultimately have "n ∈ set (sourcenodes as)" by simp
          with ‹n' = sourcenode a'› ‹targetnode a = targetnode ax›
            ‹targetnode a = n›
            ‹CFG_node (targetnode ax) cd-[]@[CFG_node (targetnode ax)]→⇩d* 
            CFG_node (sourcenode a')›
          show ?thesis by fastforce
        qed
      next
        case False
        from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain a' 
          where "a' ∈ get_return_edges a"
          by(fastforce dest:get_return_edge_call)
        with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain Q' f' where "kind a' = Q'↩⇘p⇙f'"
          by(fastforce dest!:call_return_edges)
        with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a› obtain a''
          where "valid_edge a''" and "sourcenode a'' = targetnode a" 
          and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)⇩√"
          by -(drule intra_proc_additional_edge,auto)
        from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
          by(rule get_return_edges_valid)
        have "∃ax asx zs. n -ax#asx→⇩ι* n' ∧ n' ∉ set (sourcenodes (ax#asx)) ∧ 
                          as = (ax#asx)@zs"
        proof(cases "n' ∈ set (sourcenodes as)")
          case True
          hence "∃n'' ∈ set(sourcenodes as). n' = n''" by simp
          then obtain ns' ns'' where "sourcenodes as = ns'@n'#ns''"
            and "∀n'' ∈ set ns'. n' ≠ n''"
            by(fastforce elim!:split_list_first_propE)
          from ‹sourcenodes as = ns'@n'#ns''› obtain xs ys ax
            where "sourcenodes xs = ns'" and "as = xs@ax#ys"
            and "sourcenode ax = n'"
            by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
          from ‹∀n'' ∈ set ns'. n' ≠ n''› ‹sourcenodes xs = ns'›
          have "n' ∉ set(sourcenodes xs)" by fastforce
          from ‹n -as→⇩ι* n'› ‹as = xs@ax#ys› have "n -xs@ax#ys→⇩ι* n'" by simp
          with ‹sourcenode ax = n'› have "n -xs→⇩ι* n'" 
            by(fastforce dest:path_split simp:intra_path_def)
          with ‹n ≠ n'› have "xs ≠ []" by(fastforce simp:intra_path_def)
          with ‹n' ∉ set(sourcenodes xs)› ‹n -xs→⇩ι* n'› ‹as = xs@ax#ys› show ?thesis
            by(cases xs) auto
        next
          case False
          with ‹n -as→⇩ι* n'› ‹n ≠ n'› 
          show ?thesis by(cases as)(auto simp:intra_path_def)
        qed
        then obtain ax asx zs where "n -ax#asx→⇩ι* n'" 
          and "n' ∉ set (sourcenodes (ax#asx))" and "as = (ax#asx)@zs" by blast
        from ‹n -ax#asx→⇩ι* n'› ‹n' ≠ (_Exit_)› have "inner_node n'"
          by(fastforce intro:path_valid_node simp:inner_node_def intra_path_def)
        from ‹valid_edge a› ‹targetnode a = n› have "valid_node n" by fastforce
        show ?thesis
        proof(cases "∀a' a''. a' ∈ set asx ∧ sourcenode a' = sourcenode a'' ∧ 
            valid_edge a'' ∧ intra_kind(kind a'') ⟶ 
            n' postdominates targetnode a''")
          case True
          from ‹targetnode a = n› ‹sourcenode a'' = targetnode a› 
            ‹kind a'' = (λcf. False)⇩√›
          have "sourcenode a'' = n" and "intra_kind(kind a'')"
            by(auto simp:intra_kind_def)
          { fix as' assume "targetnode a'' -as'→⇩ι* n'"
            from ‹valid_edge a'› ‹targetnode a'' = sourcenode a'› 
              ‹a' ∈ get_return_edges a› 
              ‹∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶ ax ∉ get_return_edges a›
            have "targetnode a'' ≠ n'" by fastforce
            with ‹targetnode a'' -as'→⇩ι* n'› obtain ax' where "valid_edge ax'"
              and "targetnode a'' = sourcenode ax'" and "intra_kind(kind ax')"
              by(clarsimp simp:intra_path_def)(erule path.cases,fastforce+)
            from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› ‹valid_edge ax'›
              ‹targetnode a'' = sourcenode a'› ‹targetnode a'' = sourcenode ax'›
              ‹intra_kind(kind ax')›
            have False by(fastforce dest:return_edges_only simp:intra_kind_def) }
          hence "¬ n' postdominates targetnode a''"
            by(fastforce elim:postdominate_implies_inner_path)
          from ‹n -ax#asx→⇩ι* n'› have "sourcenode ax = n"
            by(auto intro:path_split_Cons simp:intra_path_def)
          from ‹n -ax#asx→⇩ι* n'› have "n -[]@ax#asx→⇩ι* n'" by simp
          from this ‹sourcenode a'' = n› ‹sourcenode ax = n› True
            ‹n' ∉ set (sourcenodes (ax#asx))› ‹valid_edge a''› ‹intra_kind(kind a'')›
            ‹inner_node n'› ‹¬ method_exit n'› ‹¬ n' postdominates targetnode a''›
          have "n controls n'"
            by(fastforce intro!:which_node_intra_standard_control_dependence_source)
          hence "CFG_node n ⟶⇘cd⇙ CFG_node n'"
            by(fastforce intro:SDG_cdep_edge)
          with ‹valid_node n› have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node n'"
            by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
          moreover
          from ‹as = (ax#asx)@zs› ‹sourcenode ax = n› have "n ∈ set(sourcenodes as)"
            by(simp add:sourcenodes_def)
          ultimately show ?thesis by fastforce
        next
          case False
          hence "∃a' ∈ set asx. ∃a''. sourcenode a' = sourcenode a'' ∧ 
            valid_edge a'' ∧ intra_kind(kind a'') ∧ 
            ¬ n' postdominates targetnode a''"
            by fastforce
          then obtain ax' asx' asx'' where "asx = asx'@ax'#asx'' ∧
            (∃a''. sourcenode ax' = sourcenode a'' ∧ valid_edge a'' ∧
            intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'') ∧
            (∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ 
            valid_edge a'' ∧ intra_kind(kind a'') ∧ 
            ¬ n' postdominates targetnode a''))"
            by(blast elim!:split_list_last_propE)
          then obtain ai where "asx = asx'@ax'#asx''"
            and "sourcenode ax' = sourcenode ai"
            and "valid_edge ai" and "intra_kind(kind ai)"
            and "¬ n' postdominates targetnode ai"
            and "∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ 
            valid_edge a'' ∧ intra_kind(kind a'') ∧ 
            ¬ n' postdominates targetnode a'')"
            by blast
          from ‹asx = asx'@ax'#asx''› ‹n -ax#asx→⇩ι* n'›
          have "n -(ax#asx')@ax'#asx''→⇩ι* n'" by simp
          from ‹n' ∉ set (sourcenodes (ax#asx))› ‹asx = asx'@ax'#asx''›
          have "n' ∉ set (sourcenodes (ax'#asx''))"
            by(auto simp:sourcenodes_def)
          with ‹inner_node n'› ‹¬ n' postdominates targetnode ai›
            ‹n -(ax#asx')@ax'#asx''→⇩ι* n'› ‹sourcenode ax' = sourcenode ai›
            ‹∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ 
            valid_edge a'' ∧ intra_kind(kind a'') ∧ 
            ¬ n' postdominates targetnode a'')›
            ‹valid_edge ai› ‹intra_kind(kind ai)› ‹¬ method_exit n'›
          have "sourcenode ax' controls n'"
            by(fastforce intro!:which_node_intra_standard_control_dependence_source)
          hence "CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'"
            by(fastforce intro:SDG_cdep_edge)
          from ‹n -(ax#asx')@ax'#asx''→⇩ι* n'›
          have "n -ax#asx'→⇩ι* sourcenode ax'" and "valid_edge ax'"
            by(auto intro:path_split simp:intra_path_def simp del:append_Cons)
          from ‹asx = asx'@ax'#asx''› ‹as = (ax#asx)@zs›
          have "length (ax#asx') < length as" by simp
          from ‹as = (ax#asx)@zs› ‹asx = asx'@ax'#asx''›
          have "sourcenode ax' ∈ set(sourcenodes as)" by(simp add:sourcenodes_def)
          show ?thesis
          proof(cases "n = sourcenode ax'")
            case True
            with ‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'› ‹valid_edge ax'›
            have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node n'"
              by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
            with ‹sourcenode ax' ∈ set(sourcenodes as)› True show ?thesis by fastforce
          next
            case False
            from ‹valid_edge ax'› have "sourcenode ax' ≠ (_Exit_)"
              by -(rule ccontr,fastforce elim!:Exit_source)
            from ‹n -ax#asx'→⇩ι* sourcenode ax'› have "n = sourcenode ax"
              by(fastforce intro:path_split_Cons simp:intra_path_def)
            show ?thesis
            proof(cases "∀ax. valid_edge ax ∧ sourcenode ax = sourcenode ax' ⟶
                ax ∉ get_return_edges a")
              case True
              from ‹asx = asx'@ax'#asx''› ‹n -ax#asx→⇩ι* n'›
              have "intra_kind (kind ax')" by(simp add:intra_path_def)
              have "¬ method_exit (sourcenode ax')"
              proof
                assume "method_exit (sourcenode ax')"
                thus False
                proof(rule method_exit_cases)
                  assume "sourcenode ax' = (_Exit_)"
                  with ‹valid_edge ax'› show False by(rule Exit_source)
                next
                  fix x Q f p assume " sourcenode ax' = sourcenode x"
                    and "valid_edge x" and "kind x = Q↩⇘p⇙f"
                  from ‹valid_edge x› ‹kind x = Q↩⇘p⇙f› ‹sourcenode ax' = sourcenode x›
                    ‹valid_edge ax'› ‹intra_kind (kind ax')› show False
                    by(fastforce dest:return_edges_only simp:intra_kind_def)
                qed
              qed
              with IH ‹length (ax#asx') < length as› ‹n -ax#asx'→⇩ι* sourcenode ax'›
                ‹n ≠ sourcenode ax'› ‹sourcenode ax' ≠ (_Exit_)› True
              obtain ns where "CFG_node n cd-ns→⇩d* CFG_node (sourcenode ax')"
                and "ns ≠ []" 
                and "∀n''∈set ns. parent_node n'' ∈ set (sourcenodes (ax#asx'))"
                by blast
              from ‹CFG_node n cd-ns→⇩d* CFG_node (sourcenode ax')›
                ‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'›
              have "CFG_node n cd-ns@[CFG_node (sourcenode ax')]→⇩d* CFG_node n'"
                by(rule cdSp_Append_cdep)
              moreover
              from ‹∀n''∈set ns. parent_node n'' ∈ set (sourcenodes (ax#asx'))›
                ‹asx = asx'@ax'#asx''› ‹as = (ax#asx)@zs›
                ‹sourcenode ax' ∈ set(sourcenodes as)›
              have "∀n''∈set (ns@[CFG_node (sourcenode ax')]). 
                parent_node n'' ∈ set (sourcenodes as)"
                by(fastforce simp:sourcenodes_def)
              ultimately show ?thesis by fastforce
            next
              case False
              then obtain ai' where "valid_edge ai'" 
                and "sourcenode ai' = sourcenode ax'" 
                and "ai' ∈ get_return_edges a" by blast
              with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹targetnode a = n›
              have "CFG_node n ⟶⇘cd⇙ CFG_node (sourcenode ax')"
                by(fastforce intro!:SDG_proc_entry_exit_cdep[of _ _ _ _ _ _ ai'])
              with ‹valid_node n›
              have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node (sourcenode ax')"
                by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
              with ‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'›
              have "CFG_node n cd-[CFG_node n]@[CFG_node (sourcenode ax')]→⇩d* 
                CFG_node n'"
                by(fastforce intro:cdSp_Append_cdep)
              moreover
              from ‹sourcenode ax' ∈ set(sourcenodes as)› ‹n = sourcenode ax›
                ‹as = (ax#asx)@zs›
              have "∀n''∈set ([CFG_node n]@[CFG_node (sourcenode ax')]). 
                parent_node n'' ∈ set (sourcenodes as)"
                by(fastforce simp:sourcenodes_def)
              ultimately show ?thesis by fastforce
            qed
          qed
        qed
      qed
    qed
  next
    case False
    then obtain a' where "valid_edge a'" and "sourcenode a' = n'"
      and "a' ∈ get_return_edges a" by auto
    with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹targetnode a = n›
    have "CFG_node n ⟶⇘cd⇙ CFG_node n'" by(fastforce intro:SDG_proc_entry_exit_cdep)
    with ‹valid_edge a› ‹targetnode a = n›[THEN sym] 
    have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node n'"