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↪⇘pfs)  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↩⇘pf)  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↪⇘pfs)  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↩⇘pf)  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↪⇘pfs" 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↪⇘pfs 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↪⇘pfs 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↩⇘pf" and  "sourcenode a = (_Entry_)" by auto
  from valid_edge a kind a = Q↩⇘pf 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↩⇘pf 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↪⇘pfs" 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↪⇘pfs" and "targetnode a = (_Exit_)" by fastforce
  from valid_edge a kind a = Q:r↪⇘pfs 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↪⇘pfs 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↩⇘pf" 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" ("_  UseSDG _")
where CFG_Use_SDG_Use:
  "valid_node m; V  Use m; n = CFG_node m  V  UseSDG n"
  | Actual_in_SDG_Use:
  "valid_SDG_node n; n = Actual_in (m,x); V  (ParamUses m)!x  V  UseSDG 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  UseSDG n"


abbreviation notin_SDG_Use :: "'var  'node SDG_node  bool"  ("_  UseSDG _")
  where "V  UseSDG n  ¬ V  UseSDG n"


lemma in_Use_valid_SDG_node:
  "V  UseSDG n  valid_SDG_node n"
by(induct rule:SDG_Use.induct,auto intro:valid_SDG_CFG_node)


lemma SDG_Use_parent_Use: 
  "V  UseSDG 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↪⇘pfs" and "sourcenode a = m"
    and "(p,ins,outs)  set procs" and "x < length ins" by fastforce
  from valid_edge a kind a = Q:r↪⇘pfs (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" ("_  DefSDG _")
where CFG_Def_SDG_Def:
  "valid_node m; V  Def m; n = CFG_node m  V  DefSDG 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  DefSDG n"
  | Actual_out_SDG_Def:
  "valid_SDG_node n; n = Actual_out (m,x); V = (ParamDefs m)!x  V  DefSDG n"

abbreviation notin_SDG_Def :: "'var  'node SDG_node  bool"  ("_  DefSDG _")
  where "V  DefSDG n  ¬ V  DefSDG n"


lemma in_Def_valid_SDG_node:
  "V  DefSDG n  valid_SDG_node n"
by(induct rule:SDG_Def.induct,auto intro:valid_SDG_CFG_node)


lemma SDG_Def_parent_Def: 
  "V  DefSDG 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↩⇘pf" and "targetnode a = m"
    and "(p,ins,outs)  set procs" and "x < length outs" by fastforce
  from valid_edge a kind a = Q↩⇘pf (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  DefSDG n)  (V  UseSDG n')  
  (parent_node n -asι* parent_node n') 
  (n''. valid_SDG_node n''  parent_node n''  set (sourcenodes (tl as))
          V  DefSDG 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↩⇘pf"
            from valid_edge a kind a = Q↩⇘pf 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"
    ("_ -_dd _" [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 *)
  "ncd n' == SDG_edge n None None n'"
  | "n -Vdd n' == SDG_edge n (Some V) None n'"
  | "n -pcall n' == SDG_edge n None (Some(p,True)) n'"
  | "n -pret n' == SDG_edge n None (Some(p,False)) n'"
  | "n -p:Vin n' == SDG_edge n (Some V) (Some(p,True)) n'"
  | "n -p:Vout 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'  ncd n'"
  | SDG_proc_entry_exit_cdep:
    "valid_edge a; kind a = Q:r↪⇘pfs; n = CFG_node (targetnode a);
      a'  get_return_edges a; n' = CFG_node (sourcenode a')  ncd n'"
  | SDG_parent_cdep_edge:
    "valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n  n' 
       ncd n'"
  | SDG_ddep_edge:"n influences V in n'  n -Vdd n'"
  | SDG_call_edge:
    "valid_edge a; kind a = Q:r↪⇘pfs; n = CFG_node (sourcenode a); 
      n' = CFG_node (targetnode a)  n -pcall n'"
  | SDG_return_edge:
    "valid_edge a; kind a = Q↩⇘pf; n = CFG_node (sourcenode a); 
      n' = CFG_node (targetnode a)  n -pret n'"
  | SDG_param_in_edge:
    "valid_edge a; kind a = Q:r↪⇘pfs; (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:Vin n'"
  | SDG_param_out_edge:
    "valid_edge a; kind a = Q↩⇘pf; (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:Vout n'"


lemma cdep_edge_cases:
  "ncd n'; (parent_node n) controls (parent_node n')  P;
    a Q r p fs a'. valid_edge a; kind a = Q:r↪⇘pfs; 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: "ncd 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 -pcall 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 -pret 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↪⇘pfs)"
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↪⇘pfs 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↪⇘pfs
  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↩⇘pf)"
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↩⇘pf 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↩⇘pf
  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↪⇘pfs 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↪⇘pfs 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-nsd* n''; n''cd n'  n i-ns@[n'']d* n'"

  | iSp_Append_ddep:
  "n i-nsd* n''; n'' -Vdd n'; n''  n'  n i-ns@[n'']d* n'"


lemma intra_SDG_path_Append:
  "n'' i-ns'd* n'; n i-nsd* 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-nsd* n'" shows "valid_SDG_node n" and "valid_SDG_node n'"
using n i-nsd* 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-nsd* n'"
  obtains as where "parent_node n -asι* parent_node n'" 
proof(atomize_elim)
  from n i-nsd* 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↪⇘pfs" 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'' -Vdd 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-nsd* n''; n''cd n'  n cd-ns@[n'']d* n'"


lemma cdep_SDG_path_intra_SDG_path:
  "n cd-nsd* n'  n i-nsd* 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-nsd* 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-nsd* 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-nsd* CFG_node n''  ns  [] 
              (nxset 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-nsd* 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↩⇘pf"
            from valid_edge x kind x = Q↩⇘pf 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-nsd* CFG_node (sourcenode ax')"
          and "ns  []" 
          and "n''  set ns. parent_node n''  set(sourcenodes (ax#asx'))"
          by blast
        from CFG_node (_Entry_) cd-nsd* 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↪⇘pfs" and "targetnode a = n"
  obtains ns where "CFG_node n cd-nsd* CFG_node n'"
  and "ns  []" and "n''  set ns. parent_node n''  set(sourcenodes as)"
proof(atomize_elim)
  show "ns. CFG_node n cd-nsd* 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-nsd* 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-nsd* 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-nsd* 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↪⇘pfs 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↪⇘pfs"
            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↪⇘pfs valid_edge ax 
            Q r fs. kind ax = Q:r↪⇘pfs 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↪⇘pfs obtain a' 
          where "a'  get_return_edges a"
          by(fastforce dest:get_return_edge_call)
        with valid_edge a kind a = Q:r↪⇘pfs obtain Q' f' where "kind a' = Q'↩⇘pf'"
          by(fastforce dest!:call_return_edges)
        with valid_edge a kind a = Q:r↪⇘pfs 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'↩⇘pf' 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 ncd 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↩⇘pf"
                  from valid_edge x kind x = Q↩⇘pf 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-nsd* CFG_node (sourcenode ax')"
                and "ns  []" 
                and "n''set ns. parent_node n''  set (sourcenodes (ax#asx'))"
                by blast
              from CFG_node n cd-nsd* 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↪⇘pfs targetnode a = n
              have "CFG_node ncd 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↪⇘pfs targetnode a = n
    have "CFG_node ncd 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'"
      by(fastforce intro:cdep_SDG_path.intros)