Session Slicing

Theory AuxLemmas

section ‹Auxiliary lemmas›

theory AuxLemmas imports Main begin

abbreviation "arbitrary == undefined"

text ‹Lemmas about left- and rightmost elements in lists›

lemma leftmost_element_property:
  assumes "x  set xs. P x"
  obtains zs x' ys where "xs = zs@x'#ys" and "P x'" and "z  set zs. ¬ P z"
proof(atomize_elim)
  from x  set xs. P x 
  show "zs x' ys. xs = zs @ x' # ys  P x'  (zset zs. ¬ P z)"
  proof(induct xs)
    case Nil thus ?case by simp
  next
    case (Cons x' xs')
    note IH = aset xs'. P a
       zs x' ys. xs' = zs@x'#ys  P x'  (zset zs. ¬ P z)
    show ?case
    proof (cases "P x'")
      case True
      then have "(ys. x' # xs' = [] @ x' # ys)  P x'  (xset []. ¬ P x)" by simp
      then show ?thesis by blast
    next
      case False
      with yset (x'#xs'). P y have "yset xs'. P y" by simp
      from IH[OF this] obtain y ys zs where "xs' = zs@y#ys"
        and "P y" and "zset zs. ¬ P z" by blast
      from zset zs. ¬ P z False have "zset (x'#zs). ¬ P z" by simp
      with xs' = zs@y#ys P y show ?thesis by (metis Cons_eq_append_conv)
    qed
  qed
qed



lemma rightmost_element_property:
  assumes "x  set xs. P x"
  obtains ys x' zs where "xs = ys@x'#zs" and "P x'" and "z  set zs. ¬ P z"
proof(atomize_elim)
  from x  set xs. P x
  show "ys x' zs. xs = ys @ x' # zs  P x'  (zset zs. ¬ P z)"
  proof(induct xs)
    case Nil thus ?case by simp
  next
    case (Cons x' xs')
    note IH = aset xs'. P a
       ys x' zs. xs' = ys @ x' # zs  P x'  (zset zs. ¬ P z)
    show ?case
    proof(cases "yset xs'. P y")
      case True
      from IH[OF this] obtain y ys zs where "xs' = ys @ y # zs"
        and "P y" and "zset zs. ¬ P z" by blast
      thus ?thesis by (metis Cons_eq_append_conv)
    next
      case False
      with yset (x'#xs'). P y have "P x'" by simp
      with False show ?thesis by (metis eq_Nil_appendI)
    qed
  qed
qed


text ‹Lemma concerning maps and @›

lemma map_append_append_maps:
  assumes map:"map f xs = ys@zs"
  obtains xs' xs'' where "map f xs' = ys" and "map f xs'' = zs" and "xs=xs'@xs''"
by (metis append_eq_conv_conj append_take_drop_id assms drop_map take_map that)


text ‹Lemma concerning splitting of @{term list}s›

lemma  path_split_general:
assumes all:"zs. xs  ys@zs"
obtains j zs where "xs = (take j ys)@zs" and "j < length ys"
  and "k > j. zs'. xs  (take k ys)@zs'"
proof(atomize_elim)
  from zs. xs  ys@zs
  show "j zs. xs = take j ys @ zs  j < length ys  
               (k>j. zs'. xs  take k ys @ zs')"
  proof(induct ys arbitrary:xs)
    case Nil thus ?case by auto
  next
    case (Cons y' ys')
    note IH = xs. zs. xs  ys' @ zs 
      j zs. xs = take j ys' @ zs  j < length ys'  
      (k. j < k  (zs'. xs  take k ys' @ zs'))
    show ?case
    proof(cases xs)
      case Nil thus ?thesis by simp
    next
      case (Cons x' xs')
      with zs. xs  (y' # ys') @ zs have "x'  y'  (zs. xs'  ys' @ zs)"
        by simp
      show ?thesis
      proof(cases "x' = y'")
        case True
        with x'  y'  (zs. xs'  ys' @ zs) have "zs. xs'  ys' @ zs" by simp
        from IH[OF this] have "j zs. xs' = take j ys' @ zs  j < length ys' 
          (k. j < k  (zs'. xs'  take k ys' @ zs'))" .
        then obtain j zs where "xs' = take j ys' @ zs"
          and "j < length ys'"
          and all_sub:"k. j < k  (zs'. xs'  take k ys' @ zs')"
          by blast
        from xs' = take j ys' @ zs True
          have "(x'#xs') = take (Suc j) (y' # ys') @ zs"
          by simp
        from all_sub True have all_imp:"k. j < k  
          (zs'. (x'#xs')  take (Suc k) (y' # ys') @ zs')"
          by auto
        { fix l assume "(Suc j) < l"
          then obtain k where [simp]:"l = Suc k" by(cases l) auto
          with (Suc j) < l have "j < k" by simp
          with all_imp 
          have "zs'. (x'#xs')  take (Suc k) (y' # ys') @ zs'"
            by simp
          hence "zs'. (x'#xs')  take l (y' # ys') @ zs'"
            by simp }
        with (x'#xs') = take (Suc j) (y' # ys') @ zs j < length ys' Cons
        show ?thesis by (metis Suc_length_conv less_Suc_eq_0_disj)
      next
        case False
        with Cons have "i zs'. i > 0  xs  take i (y' # ys') @ zs'"
          by auto(case_tac i,auto)
        moreover
        have "zs. xs = take 0 (y' # ys') @ zs" by simp
        ultimately show ?thesis by(rule_tac x="0" in exI,auto)
      qed
    qed
  qed
qed

end

Theory BasicDefs

chapter ‹The Framework›

theory BasicDefs imports AuxLemmas begin

text ‹
  As slicing is a program analysis that can be completely based on the
  information given in the CFG, we want to provide a framework which
  allows us to formalize and prove properties of slicing regardless of
  the actual programming language. So the starting point for the formalization 
  is the definition of an abstract CFG, i.e.\ without considering features 
  specific for certain languages. By doing so we ensure that our framework 
  is as generic as possible since all proofs hold for every language whose 
  CFG conforms to this abstract CFG.  This abstract CFG can be used as a 
  basis for static intraprocedural slicing as well as for dynamic slicing, 
  if in the dynamic case all method calls are inlined (i.e., abstract CFG 
  paths conform to traces).
›

section ‹Basic Definitions›

subsection‹Edge kinds›

datatype 'state edge_kind = Update "'state  'state"           ("_")
                          | Predicate "'state  bool"      ("'(_')")


subsection ‹Transfer and predicate functions›

fun transfer :: "'state edge_kind  'state  'state"
where "transfer (f) s = f s"
  | "transfer (P) s   = s"

fun transfers :: "'state edge_kind list  'state  'state"
where "transfers [] s   = s"
  | "transfers (e#es) s = transfers es (transfer e s)"

fun pred :: "'state edge_kind  'state  bool"
where "pred (f) s = True"
  | "pred (P) s   = (P s)"

fun preds :: "'state edge_kind list  'state  bool"
where "preds [] s   = True"
  | "preds (e#es) s = (pred e s  preds es (transfer e s))"



lemma transfers_split:
  "(transfers (ets@ets') s) = (transfers ets' (transfers ets s))"
by(induct ets arbitrary:s) auto

lemma preds_split:
  "(preds (ets@ets') s) = (preds ets s  preds ets' (transfers ets s))"
by(induct ets arbitrary:s) auto


lemma transfers_id_no_influence:
  "transfers [et  ets. et  id] s = transfers ets s"
by(induct ets arbitrary:s,auto)

lemma preds_True_no_influence:
  "preds [et  ets. et  (λs. True)] s = preds ets s"
by(induct ets arbitrary:s,auto)

end

Theory CFG

section ‹CFG›

theory CFG imports BasicDefs begin

subsection ‹The abstract CFG›

locale CFG =
  fixes sourcenode :: "'edge  'node"
  fixes targetnode :: "'edge  'node"
  fixes kind :: "'edge  'state edge_kind"
  fixes valid_edge :: "'edge  bool"
  fixes Entry::"'node" ("'('_Entry'_')")
  assumes Entry_target [dest]: "valid_edge a; targetnode a = (_Entry_)  False"
  and edge_det: 
  "valid_edge a; valid_edge a'; sourcenode a = sourcenode a'; 
    targetnode a = targetnode a'  a = a'"

begin

definition valid_node :: "'node  bool"
  where "valid_node n  
  (a. valid_edge a  (n = sourcenode a  n = targetnode a))"

lemma [simp]: "valid_edge a  valid_node (sourcenode a)"
  by(fastforce simp:valid_node_def)

lemma [simp]: "valid_edge a  valid_node (targetnode a)"
  by(fastforce simp:valid_node_def)


subsection ‹CFG paths and lemmas›

inductive path :: "'node  'edge list  'node  bool"
  ("_ -_→* _" [51,0,0] 80)
where 
  empty_path:"valid_node n  n -[]→* n"

  | Cons_path:
  "n'' -as→* n'; valid_edge a; sourcenode a = n; targetnode a = n''
     n -a#as→* n'"


lemma path_valid_node:
  assumes "n -as→* n'" shows "valid_node n" and "valid_node n'"
  using n -as→* n'
  by(induct rule:path.induct,auto)

lemma empty_path_nodes [dest]:"n -[]→* n'  n = n'"
  by(fastforce elim:path.cases)

lemma path_valid_edges:"n -as→* n'  a  set as. valid_edge a"
by(induct rule:path.induct) auto


lemma path_edge:"valid_edge a  sourcenode a -[a]→* targetnode a"
  by(fastforce intro:Cons_path empty_path)


lemma path_Entry_target [dest]:
  assumes "n -as→* (_Entry_)"
  shows "n = (_Entry_)" and "as = []"
using n -as→* (_Entry_)
proof(induct n as n'"(_Entry_)" rule:path.induct)
  case (Cons_path n'' as a n)
  from targetnode a = n'' valid_edge a n'' = (_Entry_) have False
    by -(rule Entry_target,simp_all)
  { case 1
    with ‹False› show ?case ..
  next
    case 2
    with ‹False› show ?case ..
  }
qed simp_all



lemma path_Append:"n -as→* n''; n'' -as'→* n' 
   n -as@as'→* n'"
by(induct rule:path.induct,auto intro:Cons_path)


lemma path_split:
  assumes "n -as@a#as'→* n'"
  shows "n -as→* sourcenode a" and "valid_edge a" and "targetnode a -as'→* n'"
  using n -as@a#as'→* n'
proof(induct as arbitrary:n)
  case Nil case 1
  thus ?case by(fastforce elim:path.cases intro:empty_path)
next
  case Nil case 2
  thus ?case by(fastforce elim:path.cases intro:path_edge)
next
  case Nil case 3
  thus ?case by(fastforce elim:path.cases)
next
  case (Cons ax asx) 
  note IH1 = n. n -asx@a#as'→* n'  n -asx→* sourcenode a
  note IH2 = n. n -asx@a#as'→* n'  valid_edge a
  note IH3 = n. n -asx@a#as'→* n'  targetnode a -as'→* n'
  { case 1 
    hence "sourcenode ax = n" and "targetnode ax -asx@a#as'→* n'" and "valid_edge ax"
      by(auto elim:path.cases)
    from IH1[OF targetnode ax -asx@a#as'→* n'] 
    have "targetnode ax -asx→* sourcenode a" .
    with sourcenode ax = n valid_edge ax show ?case by(fastforce intro:Cons_path)
  next
    case 2 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
    from IH2[OF this] show ?case .
  next
    case 3 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
    from IH3[OF this] show ?case .
  }
qed


lemma path_split_Cons:
  assumes "n -as→* n'" and "as  []"
  obtains a' as' where "as = a'#as'" and "n = sourcenode a'"
  and "valid_edge a'" and "targetnode a' -as'→* n'"
proof -
  from as  [] obtain a' as' where "as = a'#as'" by(cases as) auto
  with n -as→* n' have "n -[]@a'#as'→* n'" by simp
  hence "n -[]→* sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
    by(rule path_split)+
  from n -[]→* sourcenode a' have "n = sourcenode a'" by fast
  with as = a'#as' valid_edge a' targetnode a' -as'→* n' that show ?thesis 
    by fastforce
qed


lemma path_split_snoc:
  assumes "n -as→* n'" and "as  []"
  obtains a' as' where "as = as'@[a']" and "n -as'→* sourcenode a'"
  and "valid_edge a'" and "n' = targetnode a'"
proof -
  from as  [] obtain a' as' where "as = as'@[a']" by(cases as rule:rev_cases) auto
  with n -as→* n' have "n -as'@a'#[]→* n'" by simp
  hence "n -as'→* sourcenode a'" and "valid_edge a'" and "targetnode a' -[]→* n'"
    by(rule path_split)+
  from targetnode a' -[]→* n' have "n' = targetnode a'" by fast
  with as = as'@[a'] valid_edge a' n -as'→* sourcenode a' that show ?thesis 
    by fastforce
qed


lemma path_split_second:
  assumes "n -as@a#as'→* n'" shows "sourcenode a -a#as'→* n'"
proof -
  from n -as@a#as'→* n' have "valid_edge a" and "targetnode a -as'→* n'"
    by(auto intro:path_split)
  thus ?thesis by(fastforce intro:Cons_path)
qed


lemma path_Entry_Cons:
  assumes "(_Entry_) -as→* n'" and "n'  (_Entry_)"
  obtains n a where "sourcenode a = (_Entry_)" and "targetnode a = n"
  and "n -tl as→* n'" and "valid_edge a" and "a = hd as"
proof -
  from (_Entry_) -as→* n' n'  (_Entry_) have "as  []"
    by(cases as,auto elim:path.cases)
  with (_Entry_) -as→* n' obtain a' as' where "as = a'#as'" 
    and "(_Entry_) = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
    by(erule path_split_Cons)
  with that show ?thesis by fastforce
qed


lemma path_det:
  "n -as→* n'; n -as→* n''  n' = n''"
proof(induct as arbitrary:n)
  case Nil thus ?case by(auto elim:path.cases)
next
  case (Cons a' as')
  note IH = n. n -as'→* n'; n -as'→* n''  n' = n''
  from n -a'#as'→* n' have "targetnode a' -as'→* n'" 
    by(fastforce elim:path_split_Cons)
  from n -a'#as'→* n'' have "targetnode a' -as'→* n''" 
    by(fastforce elim:path_split_Cons)
  from IH[OF targetnode a' -as'→* n' this] show ?thesis .
qed


definition
  sourcenodes :: "'edge list  'node list"
  where "sourcenodes xs  map sourcenode xs"

definition
  kinds :: "'edge list  'state edge_kind list"
  where "kinds xs  map kind xs"

definition
  targetnodes :: "'edge list  'node list"
  where "targetnodes xs  map targetnode xs"


lemma path_sourcenode:
  "n -as→* n'; as  []  hd (sourcenodes as) = n"
by(fastforce elim:path_split_Cons simp:sourcenodes_def)



lemma path_targetnode:
  "n -as→* n'; as  []  last (targetnodes as) = n'"
by(fastforce elim:path_split_snoc simp:targetnodes_def)



lemma sourcenodes_is_n_Cons_butlast_targetnodes:
  "n -as→* n'; as  []  
  sourcenodes as = n#(butlast (targetnodes as))"
proof(induct as arbitrary:n)
  case Nil thus ?case by simp
next
  case (Cons a' as')
  note IH = n. n -as'→* n'; as'  []
             sourcenodes as' = n#(butlast (targetnodes as'))
  from n -a'#as'→* n' have "n = sourcenode a'" and "targetnode a' -as'→* n'"
    by(auto elim:path_split_Cons)
  show ?case
  proof(cases "as' = []")
    case True
    with targetnode a' -as'→* n' have "targetnode a' = n'" by fast
    with True n = sourcenode a' show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  next
    case False
    from IH[OF targetnode a' -as'→* n' this] 
    have "sourcenodes as' = targetnode a' # butlast (targetnodes as')" .
    with n = sourcenode a' False show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  qed
qed



lemma targetnodes_is_tl_sourcenodes_App_n':
  "n -as→* n'; as  []  
    targetnodes as = (tl (sourcenodes as))@[n']"
proof(induct as arbitrary:n' rule:rev_induct)
  case Nil thus ?case by simp
next
  case (snoc a' as')
  note IH = n'. n -as'→* n'; as'  []
     targetnodes as' = tl (sourcenodes as') @ [n']
  from n -as'@[a']→* n' have "n -as'→* sourcenode a'" and "n' = targetnode a'"
    by(auto elim:path_split_snoc)
  show ?case
  proof(cases "as' = []")
    case True
    with n -as'→* sourcenode a' have "n = sourcenode a'" by fast
    with True n' = targetnode a' show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  next
    case False
    from IH[OF n -as'→* sourcenode a' this]
    have "targetnodes as' = tl (sourcenodes as')@[sourcenode a']" .
    with n' = targetnode a' False show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  qed
qed

lemma Entry_sourcenode_hd:
  assumes "n -as→* n'" and "(_Entry_)  set (sourcenodes as)"
  shows "n = (_Entry_)" and "(_Entry_)  set (sourcenodes (tl as))"
  using n -as→* n' (_Entry_)  set (sourcenodes as)
proof(induct rule:path.induct)
  case (empty_path n) case 1
  thus ?case by(simp add:sourcenodes_def)
next
  case (empty_path n) case 2
  thus ?case by(simp add:sourcenodes_def)
next
  case (Cons_path n'' as n' a n)
  note IH1 = (_Entry_)  set(sourcenodes as)  n'' = (_Entry_)
  note IH2 = (_Entry_)  set(sourcenodes as)  (_Entry_)  set(sourcenodes(tl as))
  have "(_Entry_)  set (sourcenodes(tl(a#as)))"
  proof
    assume "(_Entry_)  set (sourcenodes (tl (a#as)))"
    hence "(_Entry_)  set (sourcenodes as)" by simp
    from IH1[OF this] have "n'' = (_Entry_)" by simp
    with targetnode a = n'' valid_edge a show False by -(erule Entry_target,simp)
  qed
  hence "(_Entry_)  set (sourcenodes(tl(a#as)))" by fastforce
  { case 1
    with (_Entry_)  set (sourcenodes(tl(a#as))) sourcenode a = n
    show ?case by(simp add:sourcenodes_def)
  next
    case 2
    with (_Entry_)  set (sourcenodes(tl(a#as))) sourcenode a = n
    show ?case by(simp add:sourcenodes_def)
  }
qed

end

end

Theory CFGExit

theory CFGExit imports CFG begin

subsection ‹Adds an exit node to the abstract CFG›

locale CFGExit = CFG sourcenode targetnode kind valid_edge Entry
  for sourcenode :: "'edge  'node" and targetnode :: "'edge  'node"
  and kind :: "'edge  'state edge_kind" and valid_edge :: "'edge  bool"
  and Entry :: "'node" ("'('_Entry'_')") + 
  fixes Exit::"'node"  ("'('_Exit'_')")
  assumes Exit_source [dest]: "valid_edge a; sourcenode a = (_Exit_)  False"
  and Entry_Exit_edge: "a. valid_edge a  sourcenode a = (_Entry_) 
    targetnode a = (_Exit_)  kind a = (λs. False)"
  
begin

lemma Entry_noteq_Exit [dest]:
  assumes eq:"(_Entry_) = (_Exit_)" shows "False"
proof -
  from Entry_Exit_edge obtain a where "sourcenode a = (_Entry_)" 
    and "valid_edge a" by blast
  with eq show False by simp(erule Exit_source)
qed

lemma Exit_noteq_Entry [dest]:"(_Exit_) = (_Entry_)  False"
  by(rule Entry_noteq_Exit[OF sym],simp)


lemma [simp]: "valid_node (_Entry_)"
proof -
  from Entry_Exit_edge obtain a where "sourcenode a = (_Entry_)" 
    and "valid_edge a" by blast
  thus ?thesis by(fastforce simp:valid_node_def)
qed

lemma [simp]: "valid_node (_Exit_)"
proof -
  from Entry_Exit_edge obtain a where "targetnode a = (_Exit_)"
    and "valid_edge a" by blast
  thus ?thesis by(fastforce simp:valid_node_def)
qed


definition inner_node :: "'node  bool"
  where inner_node_def: 
  "inner_node n  valid_node n  n  (_Entry_)  n  (_Exit_)"


lemma inner_is_valid:
  "inner_node n  valid_node n"
by(simp add:inner_node_def valid_node_def)

lemma [dest]:
  "inner_node (_Entry_)  False"
by(simp add:inner_node_def)

lemma [dest]:
  "inner_node (_Exit_)  False" 
by(simp add:inner_node_def)

lemma [simp]:"valid_edge a; targetnode a  (_Exit_) 
   inner_node (targetnode a)"
  by(simp add:inner_node_def,rule ccontr,simp,erule Entry_target)

lemma [simp]:"valid_edge a; sourcenode a  (_Entry_)
   inner_node (sourcenode a)"
  by(simp add:inner_node_def,rule ccontr,simp,erule Exit_source)

lemma valid_node_cases [consumes 1, case_names "Entry" "Exit" "inner"]:
  "valid_node n; n = (_Entry_)  Q; n = (_Exit_)  Q;
    inner_node n  Q  Q"
apply(auto simp:valid_node_def)
 apply(case_tac "sourcenode a = (_Entry_)") apply auto
apply(case_tac "targetnode a = (_Exit_)") apply auto
done

lemma path_Exit_source [dest]:
  assumes "(_Exit_) -as→* n'" shows "n' = (_Exit_)" and "as = []"
  using (_Exit_) -as→* n'
proof(induct n"(_Exit_)" as n' rule:path.induct)
  case (Cons_path n'' as n' a)
  from sourcenode a = (_Exit_) valid_edge a have False 
    by -(rule Exit_source,simp_all)
  { case 1 with ‹False› show ?case ..
  next
    case 2 with ‹False› show ?case ..
  }
qed simp_all

lemma Exit_no_sourcenode[dest]:
  assumes isin:"(_Exit_)  set (sourcenodes as)" and path:"n -as→* n'"
  shows False
proof -
  from isin obtain ns' ns'' where "sourcenodes as = ns'@(_Exit_)#ns''"
    by(auto dest:split_list simp:sourcenodes_def)
  then obtain as' as'' a where "as = as'@a#as''"
    and source:"sourcenode a = (_Exit_)"
    by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
  with path have "valid_edge a" by(fastforce dest:path_split)
  with source show ?thesis by -(erule Exit_source)
qed


end 

end

Theory Postdomination

section ‹Postdomination›

theory Postdomination imports CFGExit begin

subsection ‹Standard Postdomination›

locale Postdomination = CFGExit sourcenode targetnode kind valid_edge Entry Exit 
  for sourcenode :: "'edge  'node" and targetnode :: "'edge  'node"
  and kind :: "'edge  'state edge_kind" and valid_edge :: "'edge  bool"
  and Entry :: "'node" ("'('_Entry'_')") and Exit :: "'node" ("'('_Exit'_')") +
  assumes Entry_path:"valid_node n  as. (_Entry_) -as→* n"
  and Exit_path:"valid_node n  as. n -as→* (_Exit_)"

begin

definition postdominate :: "'node  'node  bool" ("_ postdominates _" [51,0])
where postdominate_def:"n' postdominates n  
    (valid_node n  valid_node n' 
    ((as. n -as→* (_Exit_)  n'  set (sourcenodes as))))"


lemma postdominate_implies_path: 
  assumes "n' postdominates n" obtains as where "n -as→* n'"
proof(atomize_elim)
  from n' postdominates n have "valid_node n"
    and all:"as. n -as→* (_Exit_)  n'  set(sourcenodes as)"
    by(auto simp:postdominate_def)
  from ‹valid_node n obtain as where "n -as→* (_Exit_)" by(auto dest:Exit_path)
  with all have "n'  set(sourcenodes as)" by simp
  then obtain ns ns' where "sourcenodes as = ns@n'#ns'" by(auto dest:split_list)
  then obtain as' a as'' where "sourcenodes as' = ns" 
    and "sourcenode a = n'" and "as = as'@a#as''"
    by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
  from n -as→* (_Exit_) as = as'@a#as'' have "n -as'→* sourcenode a"
    by(fastforce dest:path_split)
  with sourcenode a = n' show "as. n -as→* n'" by blast
qed



lemma postdominate_refl:
  assumes valid:"valid_node n" and notExit:"n  (_Exit_)"
  shows "n postdominates n"
using valid
proof(induct rule:valid_node_cases)
  case Entry
  { fix as assume path:"(_Entry_) -as→* (_Exit_)"
    hence notempty:"as  []" 
      apply - apply(erule path.cases)
      by (drule sym,simp,drule Exit_noteq_Entry,auto)
    with path have "hd (sourcenodes as) = (_Entry_)" 
      by(fastforce intro:path_sourcenode)
    with notempty have "(_Entry_)  set (sourcenodes as)"
      by(fastforce intro:hd_in_set simp:sourcenodes_def) }
  with Entry show ?thesis by(simp add:postdominate_def)
next
  case Exit
  with notExit have False by simp
  thus ?thesis by simp
next
  case inner
  show ?thesis
  proof(cases "as. n -as→* (_Exit_)")
    case True
    { fix as' assume path':"n -as'→* (_Exit_)"
      with inner have notempty:"as'  []"
        by(cases as',auto elim!:path.cases simp:inner_node_def)
      with path' inner have hd:"hd (sourcenodes as') = n"
        by -(rule path_sourcenode)
      from notempty have "sourcenodes as'  []" by(simp add:sourcenodes_def)
      with hd[THEN sym] have "n  set (sourcenodes as')" by simp }
    hence "as. n -as→* (_Exit_)  n  set (sourcenodes as)" by simp
    with True inner show ?thesis by(simp add:postdominate_def inner_is_valid)
  next
    case False
    with inner show ?thesis by(simp add:postdominate_def inner_is_valid)
  qed
qed


lemma postdominate_trans:
  assumes pd1:"n'' postdominates n" and pd2:"n' postdominates n''"
  shows "n' postdominates n"
proof -
  from pd1 pd2 have valid:"valid_node n" and valid':"valid_node n'"
    by(simp_all add:postdominate_def)
  { fix as assume path:"n -as→* (_Exit_)"
    with pd1 have "n''  set (sourcenodes as)" by(simp add:postdominate_def)
    then obtain ns' ns'' where "sourcenodes as = ns'@n''#ns''"
      by(auto dest:split_list)
    then obtain as' as'' a
      where as'':"sourcenodes as'' = ns''" and as:"as=as'@a#as''"
      and source:"sourcenode a = n''"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    from as path have "n -as'@a#as''→* (_Exit_)" by simp
    with source have path':"n'' -a#as''→* (_Exit_)"
      by(fastforce dest:path_split_second)
    with pd2 have "n'  set(sourcenodes (a#as''))"
      by(auto simp:postdominate_def)
    with as have "n'  set(sourcenodes as)" by(auto simp:sourcenodes_def) }
  with valid valid' show ?thesis by(simp add:postdominate_def)
qed


lemma postdominate_antisym:
  assumes pd1:"n' postdominates n" and pd2:"n postdominates n'"
  shows "n = n'"
proof -
  from pd1 have valid:"valid_node n" and valid':"valid_node n'" 
    by(auto simp:postdominate_def)
  from valid obtain as where path1:"n -as→* (_Exit_)" by(fastforce dest:Exit_path)
  from valid' obtain as' where path2:"n' -as'→* (_Exit_)" by(fastforce dest:Exit_path)
  from pd1 path1 have "nx  set(sourcenodes as). nx = n'"
    by(simp add:postdominate_def)
  then obtain ns ns' where sources:"sourcenodes as = ns@n'#ns'"
    and all:"nx  set ns'. nx  n'"
    by(fastforce elim!: rightmost_element_property)
  from sources obtain asx a asx' where ns':"ns' = sourcenodes asx'"
    and as:"as = asx@a#asx'" and source:"sourcenode a = n'"
    by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
  from path1 as have "n -asx@a#asx'→* (_Exit_)" by simp
  with source have "n' -a#asx'→* (_Exit_)" by(fastforce dest:path_split_second)
  with pd2 have "n  set(sourcenodes (a#asx'))" by(simp add:postdominate_def)
  with source have "n = n'  n  set(sourcenodes asx')" by(simp add:sourcenodes_def)
  thus ?thesis
  proof
    assume "n = n'" thus ?thesis .
  next
    assume "n  set(sourcenodes asx')"
    then obtain nsx' nsx'' where "sourcenodes asx' = nsx'@n#nsx''"
      by(auto dest:split_list)
    then obtain asi asi' a' where asx':"asx' = asi@a'#asi'"
      and source':"sourcenode a' = n"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    with path1 as have "n -(asx@a#asi)@a'#asi'→* (_Exit_)" by simp
    with source' have "n -a'#asi'→* (_Exit_)" by(fastforce dest:path_split_second)
    with pd1 have "n'  set(sourcenodes (a'#asi'))" by(auto simp:postdominate_def)
    with source' have "n' = n  n'  set(sourcenodes asi')"
      by(simp add:sourcenodes_def)
    thus ?thesis
    proof
      assume "n' = n" thus ?thesis by(rule sym)
    next
      assume "n'  set(sourcenodes asi')"
      with asx' ns' have "n'  set ns'" by(simp add:sourcenodes_def)
      with all have False by blast
      thus ?thesis by simp
    qed
  qed
qed


lemma postdominate_path_branch:
  assumes "n -as→* n''" and "n' postdominates n''" and "¬ n' postdominates n"  
  obtains a as' as'' where "as = as'@a#as''" and "valid_edge a"
  and "¬ n' postdominates (sourcenode a)" and "n' postdominates (targetnode a)"
proof(atomize_elim)
  from assms
  show "as' a as''. as = as'@a#as''  valid_edge a  
    ¬ n' postdominates (sourcenode a)  n' postdominates (targetnode a)"
  proof(induct rule:path.induct)
    case (Cons_path n'' as nx a n)
    note IH = n' postdominates nx; ¬ n' postdominates n''
       as' a as''. as = as'@a#as''  valid_edge a 
        ¬ n' postdominates sourcenode a  n' postdominates targetnode a
    show ?case
    proof(cases "n' postdominates n''")
      case True
      with ¬ n' postdominates n sourcenode a = n targetnode a = n'' 
        valid_edge a
      show ?thesis by blast
    next
      case False
      from IH[OF n' postdominates nx this] show ?thesis
        by clarsimp(rule_tac x="a#as'" in exI,clarsimp)
    qed
  qed simp
qed


lemma Exit_no_postdominator:
  "(_Exit_) postdominates n  False"
by(fastforce dest:Exit_path simp:postdominate_def)


lemma postdominate_path_targetnode:
  assumes "n' postdominates n" and "n -as→* n''" and "n'  set(sourcenodes as)"
  shows "n' postdominates n''"
proof -
  from n' postdominates n have "valid_node n" and "valid_node n'"
    and all:"as''. n -as''→* (_Exit_)  n'  set(sourcenodes as'')"
    by(simp_all add:postdominate_def)
  from n -as→* n'' have "valid_node n''" by(fastforce dest:path_valid_node)
  have "as''. n'' -as''→* (_Exit_)  n'  set(sourcenodes as'')"
  proof(rule ccontr)
    assume "¬ (as''. n'' -as''→* (_Exit_)  n'  set (sourcenodes as''))"
    then obtain as'' where "n'' -as''→* (_Exit_)"
      and "n'  set (sourcenodes as'')" by blast
    from n -as→* n'' n'' -as''→* (_Exit_) have "n -as@as''→* (_Exit_)" 
      by(rule path_Append)
    with n'  set(sourcenodes as) n'  set (sourcenodes as'')
    have "n'  set (sourcenodes (as@as''))"
      by(simp add:sourcenodes_def)
    with n -as@as''→* (_Exit_) n' postdominates n show False
      by(simp add:postdominate_def)
  qed
  with ‹valid_node n' ‹valid_node n'' show ?thesis by(simp add:postdominate_def)
qed


lemma not_postdominate_source_not_postdominate_target:
  assumes "¬ n postdominates (sourcenode a)" and "valid_node n" and "valid_edge a"
  obtains ax where "sourcenode a = sourcenode ax" and "valid_edge ax"
  and "¬ n postdominates targetnode ax"
proof(atomize_elim)
  show "ax. sourcenode a = sourcenode ax  valid_edge ax  
    ¬ n postdominates targetnode ax"
  proof -
    from assms obtain asx 
      where "sourcenode a -asx→* (_Exit_)"
      and "n  set(sourcenodes asx)" by(auto simp:postdominate_def)
    from sourcenode a -asx→* (_Exit_) valid_edge a 
    obtain ax asx' where [simp]:"asx = ax#asx'"
      apply - apply(erule path.cases)
      apply(drule_tac s="(_Exit_)" in sym)
      apply simp
      apply(drule Exit_source)
      by simp_all
    with sourcenode a -asx→* (_Exit_) have "sourcenode a -[]@ax#asx'→* (_Exit_)"
      by simp
    hence "valid_edge ax" and "sourcenode a = sourcenode ax"
      and "targetnode ax -asx'→* (_Exit_)"
      by(fastforce dest:path_split)+
    with n  set(sourcenodes asx) have "¬ n postdominates targetnode ax"
      by(fastforce simp:postdominate_def sourcenodes_def)
    with sourcenode a = sourcenode ax valid_edge ax show ?thesis by blast
  qed
qed


lemma inner_node_Entry_edge:
  assumes "inner_node n" 
  obtains a where "valid_edge a" and "inner_node (targetnode a)"
  and "sourcenode a = (_Entry_)"
proof(atomize_elim)
  from ‹inner_node n have "valid_node n" by(rule inner_is_valid)
  then obtain as where "(_Entry_) -as→* n" by(fastforce dest:Entry_path)
  show "a. valid_edge a  inner_node (targetnode a)  sourcenode a = (_Entry_)"
  proof(cases "as = []")
    case True
    with ‹inner_node n (_Entry_) -as→* n have False 
      by(fastforce simp:inner_node_def)
    thus ?thesis by simp
  next
    case False
    with (_Entry_) -as→* n obtain a' as' where "as = a'#as'"
      and "(_Entry_) = sourcenode a'" and "valid_edge a'" 
      and "targetnode a' -as'→* n" 
      by -(erule path_split_Cons)
    from valid_edge a' have "valid_node (targetnode a')" by simp
    thus ?thesis
    proof(cases "targetnode a'" rule:valid_node_cases)
      case Entry
      from valid_edge a' this have False by(rule Entry_target)
      thus ?thesis by simp
    next
      case Exit
      with targetnode a' -as'→* n ‹inner_node n
      have False by simp (drule path_Exit_source,auto simp:inner_node_def)
      thus ?thesis by simp
    next
      case inner
      with valid_edge a' (_Entry_) = sourcenode a' show ?thesis by simp blast
    qed
  qed
qed


lemma inner_node_Exit_edge:
  assumes "inner_node n" 
  obtains a where "valid_edge a" and "inner_node (sourcenode a)"
  and "targetnode a = (_Exit_)"
proof(atomize_elim)
  from ‹inner_node n have "valid_node n" by(rule inner_is_valid)
  then obtain as where "n -as→* (_Exit_)" by(fastforce dest:Exit_path)
  show "a. valid_edge a  inner_node (sourcenode a)  targetnode a = (_Exit_)"
  proof(cases "as = []")
    case True
    with ‹inner_node n n -as→* (_Exit_) have False by fastforce
    thus ?thesis by simp
  next
    case False
    with n -as→* (_Exit_) obtain a' as' where "as = as'@[a']" 
      and "n -as'→* sourcenode a'" and "valid_edge a'" 
      and "(_Exit_) = targetnode a'" by -(erule path_split_snoc)
    from valid_edge a' have "valid_node (sourcenode a')" by simp
    thus ?thesis
    proof(cases "sourcenode a'" rule:valid_node_cases)
      case Entry
      with n -as'→* sourcenode a' ‹inner_node n
      have False by simp (drule path_Entry_target,auto simp:inner_node_def)
      thus ?thesis by simp
    next
      case Exit
      from valid_edge a' this have False by(rule Exit_source)
      thus ?thesis by simp
    next
      case inner
      with valid_edge a' (_Exit_) = targetnode a' show ?thesis by simp blast
    qed
  qed
qed




end

subsection ‹Strong Postdomination›


locale StrongPostdomination = 
  Postdomination sourcenode targetnode kind valid_edge Entry Exit 
  for sourcenode :: "'edge  'node" and targetnode :: "'edge  'node"
  and kind :: "'edge  'state edge_kind" and valid_edge :: "'edge  bool"
  and Entry :: "'node" ("'('_Entry'_')") and Exit :: "'node" ("'('_Exit'_')") +
  assumes successor_set_finite: "valid_node n  
  finite {n'. a'. valid_edge a'  sourcenode a' = n  targetnode a' = n'}"

begin

definition  strong_postdominate :: "'node  'node  bool" 
("_ strongly-postdominates _" [51,0])
where strong_postdominate_def:"n' strongly-postdominates n 
  (n' postdominates n  
  (k  1. as nx. n -as→* nx  
                    length as  k  n'  set(sourcenodes as)))"


lemma strong_postdominate_prop_smaller_path:
  assumes all:"as nx. n -as→* nx  length as  k  n'  set(sourcenodes as)"
  and "n -as→* n''" and "length as  k"
  obtains as' as'' where "n -as'→* n'" and "length as' < k" and "n' -as''→* n''"
  and "as = as'@as''"
proof(atomize_elim)
  show "as' as''. n -as'→* n'  length as' < k  n' -as''→* n''  as = as'@as''"
  proof(rule ccontr)
    assume "¬ (as' as''. n -as'→* n'  length as' < k  n' -as''→* n''  
                          as = as'@as'')"
    hence all':"as' as''. n -as'→* n'  n' -as''→* n''  as = as'@as'' 
       length as'  k" by fastforce
    from all n -as→* n'' ‹length as  k have "nx  set(sourcenodes as). nx = n'"
      by fastforce
    then obtain ns ns' where "sourcenodes as = ns@n'#ns'"
      and "nx  set ns. nx  n'"
      by(fastforce elim!:split_list_first_propE)
    then obtain asx a asx' where [simp]:"ns = sourcenodes asx"
      and [simp]:"as = asx@a#asx'" and "sourcenode a = n'"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    from n -as→* n'' have "n -asx@a#asx'→* n''" by simp
    with sourcenode a = n' have "n -asx→* n'" and "valid_edge a"
      and "targetnode a -asx'→* n''" by(fastforce dest:path_split)+
    with sourcenode a = n' have "n' -a#asx'→* n''" by(fastforce intro:Cons_path)
    with n -asx→* n' all' have "length asx  k" by simp
    with n -asx→* n' all have "n'  set(sourcenodes asx)" by fastforce
    with nx  set ns. nx  n' show False by fastforce
  qed
qed



lemma strong_postdominate_refl:
  assumes "valid_node n" and "n  (_Exit_)"
  shows "n strongly-postdominates n"
proof -
  from assms have "n postdominates n" by(rule postdominate_refl)
  { fix as nx assume "n -as→* nx" and "length as  1"
    then obtain a' as' where [simp]:"as = a'#as'" by(cases as) auto
    with n -as→* nx have "n -[]@a'#as'→* nx" by simp
    hence "n = sourcenode a'" by(fastforce dest:path_split)
    hence "n  set(sourcenodes as)" by(simp add:sourcenodes_def) }
  hence "as nx. n -as→* nx  length as  1  n  set(sourcenodes as)"
    by auto
  hence "k  1. as nx. n -as→* nx  length as  k  n  set(sourcenodes as)"
    by blast
  with n postdominates n show ?thesis by(simp add:strong_postdominate_def)
qed


lemma strong_postdominate_trans:
  assumes "n'' strongly-postdominates n" and "n' strongly-postdominates n''"
  shows "n' strongly-postdominates n"
proof -
  from n'' strongly-postdominates n have "n'' postdominates n"
    and paths1:"k  1. as nx. n -as→* nx  length as  k 
              n''  set(sourcenodes as)"
    by(auto simp only:strong_postdominate_def)
  from paths1 obtain k1 
    where all1:"as nx. n -as→* nx  length as  k1  n''  set(sourcenodes as)"
    and "k1  1" by blast
  from n' strongly-postdominates n'' have "n' postdominates n''"
    and paths2:"k  1. as nx. n'' -as→* nx  length as  k 
              n'  set(sourcenodes as)"
    by(auto simp only:strong_postdominate_def)
  from paths2 obtain k2 
    where all2:"as nx. n'' -as→* nx  length as  k2  n'  set(sourcenodes as)"
    and "k2  1" by blast
  from n'' postdominates n n' postdominates n'' 
  have "n' postdominates n" by(rule postdominate_trans)
  { fix as nx assume "n -as→* nx" and "length as  k1 + k2"
    hence "length as  k1" by fastforce
    with n -as→* nx all1 obtain asx asx' where "n -asx→* n''"
      and "length asx < k1" and "n'' -asx'→* nx"
      and [simp]:"as = asx@asx'" by -(erule strong_postdominate_prop_smaller_path)
    with ‹length as  k1 + k2 have "length asx'  k2" by fastforce
    with n'' -asx'→* nx all2 have "n'  set(sourcenodes asx')" by fastforce
    hence "n'  set(sourcenodes as)" by(simp add:sourcenodes_def) }
  with k1  1 k2  1 have "k  1. as nx. n -as→* nx  length as  k 
              n'  set(sourcenodes as)"
    by(rule_tac x="k1 + k2" in exI,auto)
  with n' postdominates n show ?thesis by(simp add:strong_postdominate_def)
qed


lemma strong_postdominate_antisym:
  "n' strongly-postdominates n; n strongly-postdominates n'  n = n'"
by(fastforce intro:postdominate_antisym simp:strong_postdominate_def)


lemma strong_postdominate_path_branch:
  assumes "n -as→* n''" and "n' strongly-postdominates n''" 
  and "¬ n' strongly-postdominates n"
  obtains a as' as'' where "as = as'@a#as''" and "valid_edge a"
  and "¬ n' strongly-postdominates (sourcenode a)" 
  and "n' strongly-postdominates (targetnode a)"
proof(atomize_elim)
  from assms
  show "as' a as''. as = as'@a#as''  valid_edge a  
    ¬ n' strongly-postdominates (sourcenode a)  
      n' strongly-postdominates (targetnode a)"
  proof(induct rule:path.induct)
    case (Cons_path n'' as nx a n)
    note IH = n' strongly-postdominates nx; ¬ n' strongly-postdominates n''
       as' a as''. as = as'@a#as''  valid_edge a 
        ¬ n' strongly-postdominates sourcenode a  
          n' strongly-postdominates targetnode a
    show ?case
    proof(cases "n' strongly-postdominates n''")
      case True
      with ¬ n' strongly-postdominates n sourcenode a = n targetnode a = n''
        valid_edge a
      show ?thesis by blast
    next
      case False
      from IH[OF n' strongly-postdominates nx this] show ?thesis
        by clarsimp(rule_tac x="a#as'" in exI,clarsimp)
    qed
  qed simp
qed


lemma Exit_no_strong_postdominator:
  "(_Exit_) strongly-postdominates n; n -as→* (_Exit_)  False"
by(fastforce intro:Exit_no_postdominator path_valid_node simp:strong_postdominate_def)


lemma strong_postdominate_path_targetnode:
  assumes "n' strongly-postdominates n" and "n -as→* n''"
  and "n'  set(sourcenodes as)"
  shows "n' strongly-postdominates n''"
proof -
  from n' strongly-postdominates n have "n' postdominates n"
    and "k  1. as nx. n -as→* nx  length as  k 
              n'  set(sourcenodes as)"
    by(auto simp only:strong_postdominate_def)
  then obtain k where "k  1"
    and paths:"as nx. n -as→* nx  length as  k 
                          n'  set(sourcenodes as)" by auto
  from n' postdominates n n -as→* n'' n'  set(sourcenodes as)
  have "n' postdominates n''"
    by(rule postdominate_path_targetnode)
  { fix as' nx assume "n'' -as'→* nx" and "length as'  k"
    with n -as→* n'' have "n -as@as'→* nx" and "length (as@as')  k"
      by(auto intro:path_Append)
    with paths have "n'  set(sourcenodes (as@as'))" by fastforce
    with n'  set(sourcenodes as) have "n'  set(sourcenodes as')"
      by(fastforce simp:sourcenodes_def) }
  with k  1 have "k  1. as' nx. n'' -as'→* nx  length as'  k 
              n'  set(sourcenodes as')" by auto
  with n' postdominates n'' show ?thesis by(simp add:strong_postdominate_def)
qed


lemma not_strong_postdominate_successor_set:
  assumes "¬ n strongly-postdominates (sourcenode a)" and "valid_node n"
  and "valid_edge a"
  and all:"nx  N. a'. valid_edge a'  sourcenode a' = sourcenode a 
    targetnode a' = nx  n strongly-postdominates nx"
  obtains a' where "valid_edge a'" and "sourcenode a' =  sourcenode a"
  and "targetnode a'  N"
proof(atomize_elim)
  show "a'. valid_edge a'  sourcenode a' =  sourcenode a  targetnode a'  N"
  proof(cases "n postdominates (sourcenode a)")
    case False
    with valid_edge a ‹valid_node n
    obtain a' where [simp]:"sourcenode a = sourcenode a'"
      and "valid_edge a'" and "¬ n postdominates targetnode a'"
      by -(erule not_postdominate_source_not_postdominate_target)
    with all have "targetnode a'  N" by(auto simp:strong_postdominate_def)
    with valid_edge a' show ?thesis by simp blast
  next
    case True
    let ?M = "{n'. a'. valid_edge a'  sourcenode a' =  sourcenode a  
                         targetnode a' = n'}"
    let ?M' = "{n'. a'. valid_edge a'  sourcenode a' =  sourcenode a  
                          targetnode a' = n'  n strongly-postdominates n'}"
    let ?N' = "(λn'. SOME i. i  1  
      (as nx. n' -as→* nx  length as  i 
                                 n  set(sourcenodes as))) ` N"
    obtain k where [simp]:"k = Max ?N'" by simp
    have eq:"{x  ?M. (λn'. n strongly-postdominates n') x} = ?M'" by auto
    from valid_edge a have "finite ?M" by(simp add:successor_set_finite)
    hence "finite {x  ?M. (λn'. n strongly-postdominates n') x}" by fastforce
    with eq have "finite ?M'" by simp
    from all have "N  ?M'" by auto
    with ‹finite ?M' have "finite N" by(auto intro:finite_subset)
    hence "finite ?N'" by fastforce
    show ?thesis
    proof(rule ccontr)
      assume "¬ (a'. valid_edge a'  sourcenode a' = sourcenode a  
                      targetnode a'  N)"
      hence allImp:"a'. valid_edge a'  sourcenode a' = sourcenode a
                          targetnode a'  N" by blast
      from True ¬ n strongly-postdominates (sourcenode a)
      have allPaths:"k  1. as nx. sourcenode a -as→* nx  length as  k 
         n  set(sourcenodes as)" by(auto simp:strong_postdominate_def)
      then obtain as nx where "sourcenode a -as→* nx"
        and "length as  k + 1" and "n  set(sourcenodes as)"
        by (erule_tac x="k + 1" in allE) auto
      then obtain ax as' where [simp]:"as = ax#as'" and "valid_edge ax"
        and "sourcenode ax = sourcenode a" and "targetnode ax -as'→* nx"
        by -(erule path.cases,auto)
      with allImp have "targetnode ax  N" by fastforce
      with all have "n strongly-postdominates (targetnode ax)"
        by auto
      then obtain k' where k':"k' = (SOME i. i  1 
        (as nx. targetnode ax -as→* nx  length as  i 
                  n  set(sourcenodes as)))" by simp
      with n strongly-postdominates (targetnode ax)
      have "k'  1  (as nx. targetnode ax -as→* nx  length as  k'
         n  set(sourcenodes as))"
        by(auto elim!:someI_ex simp:strong_postdominate_def)
      hence "k'  1"
        and spdAll:"as nx. targetnode ax -as→* nx  length as  k'
         n  set(sourcenodes as)"
        by simp_all
      from targetnode ax  N k' have "k'  ?N'" by blast
      with targetnode ax  N have "?N'  {}" by auto
      with k'  ?N' have "k'  Max ?N'" using ‹finite ?N' by(fastforce intro:Max_ge)
      hence "k'  k" by simp
      with targetnode ax -as'→* nx ‹length as  k + 1 spdAll 
      have "n  set(sourcenodes as')"
        by fastforce
      with n  set(sourcenodes as) show False by(simp add:sourcenodes_def)
    qed
  qed
qed



lemma not_strong_postdominate_predecessor_successor:
  assumes "¬ n strongly-postdominates (sourcenode a)"
  and "valid_node n" and "valid_edge a"
  obtains a' where "valid_edge a'" and "sourcenode a' = sourcenode a"
  and "¬ n strongly-postdominates (targetnode a')"
proof(atomize_elim)
  show "a'. valid_edge a'  sourcenode a' = sourcenode a  
             ¬ n strongly-postdominates (targetnode a')"
  proof(rule ccontr)
    assume "¬ (a'. valid_edge a'  sourcenode a' = sourcenode a 
            ¬ n strongly-postdominates targetnode a')"
    hence all:"a'. valid_edge a'  sourcenode a' = sourcenode a  
                    n strongly-postdominates (targetnode a')" by auto
    let ?N = "{n'. a'. sourcenode a' =  sourcenode a  valid_edge a'  
                        targetnode a' = n'}"
    from all have "nx  ?N. a'. valid_edge a'  sourcenode a' = sourcenode a  
      targetnode a' = nx  n strongly-postdominates nx"
      by auto
    with assms obtain a' where "valid_edge a'" 
      and "sourcenode a' =  sourcenode a" and "targetnode a'  ?N"
      by(erule not_strong_postdominate_successor_set)
    thus False by auto
  qed
qed


end


end

Theory CFG_wf

section ‹CFG well-formedness›

theory CFG_wf imports CFG begin

subsection ‹Well-formedness of the abstract CFG›

locale CFG_wf = CFG sourcenode targetnode kind valid_edge Entry
  for sourcenode :: "'edge  'node" and targetnode :: "'edge  'node"
  and kind :: "'edge  'state edge_kind" and valid_edge :: "'edge  bool"
  and Entry :: "'node" ("'('_Entry'_')") +
  fixes Def::"'node  'var set"
  fixes Use::"'node  'var set"
  fixes state_val::"'state  'var  'val"
  assumes Entry_empty:"Def (_Entry_) = {}  Use (_Entry_) = {}"
  and CFG_edge_no_Def_equal:
    "valid_edge a; V  Def (sourcenode a); pred (kind a) s
      state_val (transfer (kind a) s) V = state_val s V"
  and CFG_edge_transfer_uses_only_Use:
    "valid_edge a; V  Use (sourcenode a). state_val s V = state_val s' V;
      pred (kind a) s; pred (kind a) s'
       V  Def (sourcenode a). state_val (transfer (kind a) s) V =
                                     state_val (transfer (kind a) s') V"
  and CFG_edge_Uses_pred_equal:
    "valid_edge a; pred (kind a) s; 
      V  Use (sourcenode a). state_val s V = state_val s' V
        pred (kind a) s'"
  and deterministic:"valid_edge a; valid_edge a'; sourcenode a = sourcenode a';
    targetnode a  targetnode a' 
   Q Q'. kind a = (Q)  kind a' = (Q')  
             (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))"

begin

lemma [dest!]: "V  Use (_Entry_)  False"
by(simp add:Entry_empty)

lemma [dest!]: "V  Def (_Entry_)  False"
by(simp add:Entry_empty)


lemma CFG_path_no_Def_equal:
  "n -as→* n'; n  set (sourcenodes as). V  Def n; preds (kinds as) s 
     state_val (transfers (kinds as) s) V = state_val s V"
proof(induct arbitrary:s rule:path.induct)
  case (empty_path n)
  thus ?case by(simp add:sourcenodes_def kinds_def)
next
  case (Cons_path n'' as n' a n)
  note IH = s. nset (sourcenodes as). V  Def n; preds (kinds as) s 
            state_val (transfers (kinds as) s) V = state_val s V
  from ‹preds (kinds (a#as)) s have "pred (kind a) s"
    and "preds (kinds as) (transfer (kind a) s)" by(simp_all add:kinds_def)
  from nset (sourcenodes (a#as)). V  Def n
    have noDef:"V  Def (sourcenode a)" 
    and all:"nset (sourcenodes as). V  Def n"
    by(auto simp:sourcenodes_def)
  from valid_edge a noDef ‹pred (kind a) s
  have "state_val (transfer (kind a) s) V = state_val s V"
    by(rule CFG_edge_no_Def_equal)
  with IH[OF all ‹preds (kinds as) (transfer (kind a) s)] show ?case
    by(simp add:kinds_def)
qed

end


end

Theory CFGExit_wf

theory CFGExit_wf imports CFGExit CFG_wf begin

subsection ‹New well-formedness lemmas using (_Exit_)›


locale CFGExit_wf = 
  CFG_wf sourcenode targetnode kind valid_edge Entry Def Use state_val +
  CFGExit sourcenode targetnode kind valid_edge Entry Exit 
  for sourcenode :: "'edge  'node" and targetnode :: "'edge  'node"
  and kind :: "'edge  'state edge_kind" and valid_edge :: "'edge  bool"
  and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node  'var set"
  and Use :: "'node  'var set" and state_val :: "'state  'var  'val"
  and Exit :: "'node" ("'('_Exit'_')") +
  assumes Exit_empty:"Def (_Exit_) = {}  Use (_Exit_) = {}"

begin

lemma Exit_Use_empty [dest!]: "V  Use (_Exit_)  False"
by(simp add:Exit_empty)

lemma Exit_Def_empty [dest!]: "V  Def (_Exit_)  False"
by(simp add:Exit_empty)

end

end

Theory SemanticsCFG

section ‹CFG and semantics conform›

theory SemanticsCFG imports CFG begin

locale CFG_semantics_wf = CFG sourcenode targetnode kind valid_edge Entry
  for sourcenode :: "'edge  'node" and targetnode :: "'edge  'node"
  and kind :: "'edge  'state edge_kind" and valid_edge :: "'edge  bool"
  and Entry :: "'node" ("'('_Entry'_')") +
  fixes sem::"'com  'state  'com  'state  bool" 
    ("((1_,/_) / (1_,/_))" [0,0,0,0] 81)
  fixes identifies::"'node  'com  bool" ("_  _" [51,0] 80)
  assumes fundamental_property:
    "n  c; c,s  c',s' 
      n' as. n -as→* n'  transfers (kinds as) s = s'  preds (kinds as) s 
               n'  c'"


end

Theory DynDataDependence

section ‹Dynamic data dependence›

theory DynDataDependence imports CFG_wf begin

context CFG_wf begin 

definition dyn_data_dependence :: 
  "'node  'var  'node  'edge list  bool" ("_ influences _ in _ via _" [51,0,0])
where "n influences V in n' via as 
    ((V  Def n)  (V  Use n')  (n -as→* n')  
     (a' as'. (as = a'#as')  (n''  set (sourcenodes as'). V  Def n'')))"


lemma dyn_influence_Cons_source:
  "n influences V in n' via a#as  sourcenode a = n"
  by(simp add:dyn_data_dependence_def,auto elim:path.cases)


lemma dyn_influence_source_notin_tl_edges: 
  assumes "n influences V in n' via a#as"
  shows "n  set (sourcenodes as)"
proof(rule ccontr)
  assume "¬ n  set (sourcenodes as)"
  hence "n  set (sourcenodes as)" by simp
  from n influences V in n' via a#as have "n''  set (sourcenodes as). V  Def n''"
    and "V  Def n" by(simp_all add:dyn_data_dependence_def)
  from n''  set (sourcenodes as). V  Def n'' 
    n  set (sourcenodes as) have "V  Def n" by simp
  with V  Def n show False by simp
qed


lemma dyn_influence_only_first_edge:
  assumes "n influences V in n' via a#as" and "preds (kinds (a#as)) s"
  shows "state_val (transfers (kinds (a#as)) s) V = 
         state_val (transfer (kind a) s) V"
proof -
  from ‹preds (kinds (a#as)) s have "preds (kinds as) (transfer (kind a) s)"
    by(simp add:kinds_def)
  from n influences V in n' via a#as have "n -a#as→* n'"
    and "n''  set (sourcenodes as). V  Def n''"
    by(simp_all add:dyn_data_dependence_def)
  from n -a#as→* n' have "n = sourcenode a" and "targetnode a -as→* n'"
    by(auto elim:path_split_Cons)
  from n influences V in n' via a#as n = sourcenode a 
  have "sourcenode a  set (sourcenodes as)"
    by(fastforce intro!:dyn_influence_source_notin_tl_edges)
  { fix n'' assume "n''  set (sourcenodes as)"
    with sourcenode a  set (sourcenodes as) n = sourcenode a 
    have "n''  n" by(fastforce simp:sourcenodes_def)
    with n''  set (sourcenodes as). V  Def n'' n''  set (sourcenodes as)
    have "V  Def n''" by(auto simp:sourcenodes_def) }
  hence "n''  set (sourcenodes as). V  Def n''" by simp
  with targetnode a -as→* n' ‹preds (kinds as) (transfer (kind a) s)
  have "state_val (transfers (kinds as) (transfer (kind a) s)) V = 
        state_val (transfer (kind a) s) V"
    by -(rule CFG_path_no_Def_equal)
  thus ?thesis by(auto simp:kinds_def)
qed

end

end

Theory DynStandardControlDependence

section ‹Dynamic Standard Control Dependence›

theory DynStandardControlDependence imports Postdomination begin

context Postdomination begin

definition
  dyn_standard_control_dependence :: "'node  'node  'edge list  bool"
  ("_ controlss _ via _" [51,0,0])
where dyn_standard_control_dependence_def:"n controlss n' via as  
    (a a' as'. (as = a#as')  (n'  set(sourcenodes as))  (n -as→* n') 
                   (n' postdominates (targetnode a)) 
                   (valid_edge a')  (sourcenode a' = n)  
                   (¬ n' postdominates (targetnode a')))"


lemma Exit_not_dyn_standard_control_dependent:
  assumes control:"n controlss (_Exit_) via as" shows "False"
proof -
  from control obtain a as' where path:"n -as→* (_Exit_)" and as:"as = a#as'"
    and pd:"(_Exit_) postdominates (targetnode a)" 
    by(auto simp:dyn_standard_control_dependence_def)
  from path as have "n -[]@a#as'→* (_Exit_)" by simp
  hence "valid_edge a" by(fastforce dest:path_split)
  with pd show False by -(rule Exit_no_postdominator,auto)
qed


lemma dyn_standard_control_dependence_def_variant:
  "n controlss n' via as = ((n -as→* n')  (n  n') 
    (¬ n' postdominates n)  (n'  set(sourcenodes as)) 
  (n''  set(targetnodes as). n' postdominates n''))"
proof
  assume "(n -as→* n')  (n  n')  (¬ n' postdominates n)  
    (n'  set(sourcenodes as)) 
    (n''set (targetnodes as). n' postdominates n'')"
  hence path:"n -as→* n'" and noteq:"n  n'"
    and not_pd:"¬ n' postdominates n"
    and notin:"n'  set(sourcenodes as)"
    and all:"n''set (targetnodes as). n' postdominates n''"
    by auto
  have notExit:"n  (_Exit_)"
  proof
    assume "n = (_Exit_)"
    with path have "n = n'" by(fastforce dest:path_Exit_source)
    with noteq show False by simp
  qed
  from path have valid:"valid_node n" and valid':"valid_node n'"
    by(auto dest:path_valid_node)
  show "n controlss n' via as"
  proof(cases as)
    case Nil    
    with path valid not_pd notExit have False 
      by(fastforce elim:path.cases dest:postdominate_refl)
    thus ?thesis by simp
  next
    case (Cons ax asx)
    with all have pd:"n' postdominates targetnode ax"
      by(auto simp:targetnodes_def)
    from path Cons have source:"n = sourcenode ax" 
      and path2:"targetnode ax -asx→* n'"
      by(auto intro:path_split_Cons)
    show ?thesis
    proof(cases "as'. n -as'→* (_Exit_)")
      case True
      with not_pd valid valid' obtain as' where path':"n -as'→* (_Exit_)"
        and not_isin:"n'  set (sourcenodes as')"
        by(auto simp:postdominate_def)
      have "as'  []"
      proof
        assume "as' = []"
        with path' have "n = (_Exit_)" by(auto elim:path.cases)
        with notExit show False by simp
      qed
      then obtain a' as'' where as':"as' = a'#as''"
        by(cases as',auto elim:path.cases)
      with path' have "n -[]@a'#as''→* (_Exit_)" by simp
      hence source':"n = sourcenode a'" 
        and valid_edge:"valid_edge a'"
        and path2':"targetnode a' -as''→* (_Exit_)"
        by(fastforce dest:path_split)+
      from path2' not_isin as' valid'
      have "¬ n' postdominates (targetnode a')"
        by(auto simp:postdominate_def sourcenodes_def)
      with pd path Cons source source' notin valid_edge show ?thesis
        by(auto simp:dyn_standard_control_dependence_def)
    next
      case False
      with valid valid' have "n' postdominates n"
        by(auto simp:postdominate_def)
      with not_pd have False by simp
      thus ?thesis by simp
    qed
  qed
next
  assume "n controlss n' via as"
  then obtain a nx a' nx' as' where notin:"n'  set(sourcenodes as)"
    and path:"n -as→* n'" and as:"as = a#as'" and valid_edge:"valid_edge a'"
    and pd:"n' postdominates (targetnode a)"
    and source':"sourcenode a' = n"
    and not_pd:"¬ n' postdominates (targetnode a')"
    by(auto simp:dyn_standard_control_dependence_def)
  from path as have source:"sourcenode a = n" by(auto elim:path.cases)
  from path as have notExit:"n  (_Exit_)" by(auto elim:path.cases)
  from path have valid:"valid_node n" and valid':"valid_node n'"
    by(auto dest:path_valid_node)
  from notin as source have noteq:"n  n'"
    by(fastforce simp:sourcenodes_def)
  from valid_edge have valid_target':"valid_node (targetnode a')"
    by(fastforce simp:valid_node_def)
  { assume pd':"n' postdominates n"
    hence all:"as. n -as→* (_Exit_)  n'  set (sourcenodes as)"
      by(auto simp:postdominate_def)
    from not_pd valid' valid_target' obtain as' 
      where "targetnode a' -as'→* (_Exit_)"
      by(auto simp:postdominate_def)
    with source' valid_edge have path':"n -a'#as'→* (_Exit_)"
      by(fastforce intro:Cons_path)
    with all have "n'  set (sourcenodes (a'#as'))" by blast
    with source' have "n' = n  n'  set (sourcenodes as')"
      by(fastforce simp:sourcenodes_def)
    hence False
    proof
      assume "n' = n"
      with noteq show ?thesis by simp
    next
      assume isin:"n'  set (sourcenodes as')"
      from path' have path2:"targetnode a' -as'→* (_Exit_)"
        by(fastforce elim:path_split_Cons)
      thus ?thesis
      proof(cases "as' = []")
        case True
        with path2 have "targetnode a' = (_Exit_)" by(auto elim:path.cases)
        with valid_edge all source' have "n' = n"
          by(fastforce dest:path_edge simp:sourcenodes_def)
        with noteq show ?thesis by simp
      next
        case False
        from path2 not_pd valid' valid_edge obtain as''
          where path'':"targetnode a' -as''→* (_Exit_)"
          and notin:"n'  set (sourcenodes as'')"
          by(auto simp:postdominate_def)
        from valid_edge path'' have "sourcenode a' -a'#as''→* (_Exit_)"
          by(fastforce intro:Cons_path)
        with all source' have "n'  set (sourcenodes ([a']@as''))" by simp
        with source' have "n' = n  n'  set (sourcenodes as'')"
          by(auto simp:sourcenodes_def)
        thus ?thesis
        proof
          assume "n' = n"
          with noteq show ?thesis by simp
        next
          assume "n'  set (sourcenodes as'')"
          with notin show ?thesis by simp
        qed
      qed
    qed }
  hence not_pd':"¬ n' postdominates n" by blast
  { fix n'' assume "n''  set (targetnodes as)"
    with as source have "n'' = targetnode a  n''  set (targetnodes as')" 
      by(auto simp:targetnodes_def)
    hence "n' postdominates n''"
    proof
      assume "n'' = targetnode a"
      with pd show ?thesis by simp
    next
      assume isin:"n''  set (targetnodes as')"
      hence "ni  set (targetnodes as'). ni = n''" by simp
      then obtain ns ns' where targets:"targetnodes as' = ns@n''#ns'"
        and all_noteq:"ni  set ns'. ni  n''"
        by(fastforce elim!:rightmost_element_property)
      from targets obtain xs ax ys where ys:"ns' = targetnodes ys"
        and as':"as' = xs@ax#ys" and target'':"targetnode ax = n''"
        by(fastforce elim:map_append_append_maps simp:targetnodes_def)
      from all_noteq ys have notin_target:"n''  set(targetnodes ys)"
        by auto
      from path as have "n -[]@a#as'→* n'" by simp
      hence "targetnode a -as'→* n'" 
        by(fastforce dest:path_split)
      with isin have path':"targetnode a -as'→* n'"
        by(fastforce split:if_split_asm simp:targetnodes_def)
      with as' target'' have path1:"targetnode a -xs→* sourcenode ax"
        and valid_edge':"valid_edge ax"
        and path2:"n'' -ys→* n'"
        by(auto intro:path_split)
      from valid_edge' have "sourcenode ax -[ax]→* targetnode ax" by(rule path_edge)
      with path1 target'' have path_n'':"targetnode a -xs@[ax]→* n''"
        by(fastforce intro:path_Append)
      from notin as as' have notin':"n' set (sourcenodes (xs@[ax]))"
        by(simp add:sourcenodes_def)
      show ?thesis
      proof(rule ccontr)
        assume "¬ n' postdominates n''"
        with valid' target'' valid_edge' obtain asx' 
          where Exit_path:"n'' -asx'→* (_Exit_)"
          and notin'':"n'  set(sourcenodes asx')" by(auto simp:postdominate_def)
        from path_n'' Exit_path
        have Exit_path':"targetnode a -(xs@[ax])@asx'→* (_Exit_)"
          by(fastforce intro:path_Append)
        from notin' notin'' have "n'  set(sourcenodes (xs@ax#asx'))"
          by(simp add:sourcenodes_def)
        with pd Exit_path' show False by(simp add:postdominate_def)
      qed
    qed }
  with path not_pd' notin noteq show "(n -as→* n')  (n  n') 
    (¬ n' postdominates n)  (n'  set(sourcenodes as)) 
    (n''  set(targetnodes as). n' postdominates n'')" by blast
qed


lemma which_node_dyn_standard_control_dependence_source:
  assumes path:"(_Entry_) -as@a#as'→* n"
  and Exit_path:"n -as''→* (_Exit_)" and source:"sourcenode a = n'" 
  and source':"sourcenode a' = n'"
  and no_source:"n  set(sourcenodes (a#as'))" and valid_edge':"valid_edge a'"
  and inner_node:"inner_node n" and not_pd:"¬ n postdominates (targetnode a')"
  and last:"ax ax'. ax  set as'  sourcenode ax = sourcenode ax' 
    valid_edge ax'  n postdominates targetnode ax'"
  shows "n' controlss n via a#as'"
proof -
  from path source have path_n'n:"n' -a#as'→* n" by(fastforce dest:path_split_second)
  from path have valid_edge:"valid_edge a" by(fastforce intro:path_split)
  show ?thesis
  proof(cases "n postdominates (targetnode a)")
    case True
    with path_n'n not_pd no_source source source' valid_edge' show ?thesis
      by(auto simp:dyn_standard_control_dependence_def)
  next
    case False
    hence not_pd':"¬ n postdominates (targetnode a)" .
    show ?thesis
    proof(cases "as' = []")
      case True
      with path_n'n have "targetnode a = n" by(fastforce elim:path.cases)
      with inner_node have "n postdominates (targetnode a)"
        by(cases "n = (_Exit_)",auto intro:postdominate_refl simp:inner_node_def)
      with not_pd path_n'n no_source source source' valid_edge' show ?thesis
        by(fastforce simp:dyn_standard_control_dependence_def)
    next
      case False
      hence notempty':"as'  []" .
      with path have path_nxn:"targetnode a -as'→* n"
        by(fastforce dest:path_split)
      from Exit_path path_nxn have "as. targetnode a -as→* (_Exit_)"
        by(fastforce dest:path_Append)
      with not_pd' inner_node valid_edge obtain asx 
        where path_Exit:"targetnode a -asx→* (_Exit_)" 
        and notin:"n  set (sourcenodes asx)"
        by(auto simp:postdominate_def inner_is_valid)
      show ?thesis
      proof(cases "asx'. asx = as'@asx'")
        case True
        then obtain asx' where asx:"asx = as'@asx'" by blast
        from path notempty' have "targetnode a -as'→* n"
          by(fastforce dest:path_split)
        with path_Exit inner_node asx notempty'
        obtain a'' as'' where "asx' = a''#as''  sourcenode a'' = n"
          apply(cases asx')
           apply(fastforce dest:path_det)
          by(fastforce dest:path_split path_det)
        with asx have "n  set(sourcenodes asx)" by(simp add:sourcenodes_def)
        with notin have False by simp
        thus ?thesis by simp
      next
        case False
        hence all:"asx'. asx  as'@asx'" by simp
        then obtain j asx' where asx:"asx = (take j as')@asx'"
          and length:"j < length as'"
          and not_more:"k > j. asx''. asx  (take k as')@asx''"
          by(auto elim:path_split_general)
        from asx length 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:"asx = as'1@asx'"
          and take:"as'1 = take j as'"
          and x:"as' = as'1@as''" and x':"as''  []" by blast
        from x x' obtain a1 as'2 where as':"as' = as'1@a1#as'2" and "as'' = a1#as'2"
          by(cases as'') auto
        have notempty_x':"asx'  []"
        proof(cases "asx' = []")
          case True
          with asx as' have "as' = asx@a1#as'2" by simp
          with path_n'n have "n' -(a#asx)@a1#as'2→* n"
            by simp
          hence "n' -a#asx→* sourcenode a1"
            and valid_edge1:"valid_edge a1" by(fastforce elim:path_split)+
          hence "targetnode a -asx→* sourcenode a1"
            by(fastforce intro:path_split_Cons)
          with path_Exit have "(_Exit_) = sourcenode a1" by(rule path_det)
          from this[THEN sym] valid_edge1 have False by -(rule Exit_source,simp_all)
          thus ?thesis by simp
        qed simp
        with asx obtain a2 asx'1 
          where asx:"asx = as'1@a2#asx'1"
          and asx':"asx' = a2#asx'1" by(cases asx') auto
        from path_n'n as' have "n' -(a#as'1)@a1#as'2→* n" by simp
        hence "n' -a#as'1→* sourcenode a1" and valid_edge1:"valid_edge a1"
          by(fastforce elim:path_split)+
        hence path1:"targetnode a -as'1→* sourcenode a1"
          by(fastforce intro:path_split_Cons)
        from path_Exit asx
        have "targetnode a -as'1→* sourcenode a2"
          and valid_edge2:"valid_edge a2"
          and path2:"targetnode a2 -asx'1→* (_Exit_)"
          by(auto intro:path_split)
        with path1 have eq12:"sourcenode a1 = sourcenode a2"
          by(cases as'1,auto dest:path_det)
        from asx notin have "n  set (sourcenodes asx'1)"
          by(simp add:sourcenodes_def)
        with path2 have not_pd'2:"¬ n postdominates targetnode a2"
          by(cases "asx'1 = []",auto simp:postdominate_def)
        from as' have "a1  set as'" by simp
        with eq12 last valid_edge2 have "n postdominates targetnode a2" by blast
        with not_pd'2 have False by simp
        thus ?thesis by simp
      qed
    qed
  qed
qed


lemma inner_node_dyn_standard_control_dependence_predecessor:
  assumes inner_node:"inner_node n"
  obtains n' as where "n' controlss n via as"
proof(atomize_elim)
  from inner_node obtain as' where pathExit:"n -as'→* (_Exit_)"
    by(fastforce dest:inner_is_valid Exit_path)
  from inner_node obtain as where pathEntry:"(_Entry_) -as→* n"
    by(fastforce dest:inner_is_valid Entry_path)
  with inner_node have notEmpty:"as  []" 
    by(auto elim:path.cases simp:inner_node_def)
  have "a asx. (_Entry_) -a#asx→* n  n  set (sourcenodes (a#asx))"
  proof(cases "n  set (sourcenodes as)")
    case True
    hence "n''  set(sourcenodes as). n = n''" by simp
    then obtain ns' ns'' where nodes:"sourcenodes as = ns'@n#ns''"
      and notin:"n''  set ns'. n  n''"
      by(fastforce elim!:split_list_first_propE)
    from nodes obtain xs ys a'
      where xs:"sourcenodes xs = ns'" and as:"as = xs@a'#ys"
      and source:"sourcenode a' = n"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    from pathEntry as have "(_Entry_) -xs@a'#ys→* n" by simp
    hence path2:"(_Entry_) -xs→* sourcenode a'"
      by(fastforce dest:path_split)
    show ?thesis
    proof(cases "xs = []")
      case True
      with path2 have "(_Entry_) = sourcenode a'" by(auto elim:path.cases)
      with pathEntry source notEmpty have "(_Entry_) -as→* (_Entry_)  as  []"
        by(auto elim:path.cases)
      hence False by(fastforce dest:path_Entry_target)
      thus ?thesis by simp
    next
      case False
      then obtain n a'' xs' where "xs = a''#xs'" by(cases xs) auto
      with False path2 notin xs source show ?thesis by simp blast
    qed
  next
    case False
    from notEmpty obtain a as' where "as = a#as'" by (cases as) auto
    with False pathEntry show ?thesis by auto
  qed
  then obtain a asx where pathEntry':"(_Entry_) -a#asx→* n"
    and notin:"n  set (sourcenodes (a#asx))" by blast
  show "n' as. n' controlss n via as"
  proof(cases "a' a''. a'  set asx  sourcenode a' = sourcenode a''  
      valid_edge a''  n postdominates targetnode a''")
    case True
    from inner_node have not_pd:"¬ n postdominates (_Exit_)" 
      by(fastforce intro:empty_path simp:postdominate_def sourcenodes_def)
    from pathEntry' have path':"(_Entry_) -[]@a#asx→* n" by simp
    hence eq:"sourcenode a = (_Entry_)"
      by(fastforce dest:path_split elim:path.cases)
    from Entry_Exit_edge obtain a' where "sourcenode a' = (_Entry_)"
      and "targetnode a' = (_Exit_)" and "valid_edge a'" by auto
    with path' inner_node not_pd True eq notin pathExit
    have "sourcenode a controlss n via a#asx"
      by -(erule which_node_dyn_standard_control_dependence_source,auto)
    thus ?thesis by blast
  next
    case False
    hence "a'  set asx. a''. sourcenode a' = sourcenode a''  valid_edge 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'' 
      ¬ n postdominates targetnode a'') 
      (z  set asx''. ¬ (a''. sourcenode z = sourcenode a''  valid_edge a'' 
      ¬ n postdominates targetnode a''))"
      by(blast elim!:rightmost_element_property)
    then obtain a'' where as':"asx = asx'@ax#asx''"
      and eq:"sourcenode ax = sourcenode a''"
      and valid_edge:"valid_edge a''"
      and not_pd:"¬ n postdominates targetnode a''"
      and last:"z  set asx''. ¬ (a''. sourcenode z = sourcenode a''  
        valid_edge a''  ¬ n postdominates targetnode a'')"
      by blast
    from notin as' have notin':"n  set (sourcenodes (ax#asx''))"
      by(auto simp:sourcenodes_def)
    from as' pathEntry' have "(_Entry_) -(a#asx')@ax#asx''→* n" by simp
    with inner_node not_pd notin' eq last pathExit valid_edge
    have "sourcenode ax controlss n via ax#asx''"
      by(fastforce elim!:which_node_dyn_standard_control_dependence_source)
    thus ?thesis by blast
  qed
qed


end

end

Theory DynWeakControlDependence

section ‹Dynamic Weak Control Dependence›

theory DynWeakControlDependence imports Postdomination begin

context StrongPostdomination begin

definition
  dyn_weak_control_dependence :: "'node  'node  'edge list  bool" 
  ("_ weakly controls _ via _" [51,0,0])
where dyn_weak_control_dependence_def:"n weakly controls n' via as  
    (a a' as'. (as = a#as')  (n'  set(sourcenodes as))  (n -as→* n') 
                   (n' strongly-postdominates (targetnode a)) 
                   (valid_edge a')  (sourcenode a' = n)  
                   (¬ n' strongly-postdominates (targetnode a')))"


lemma Exit_not_dyn_weak_control_dependent:
  assumes control:"n weakly controls (_Exit_) via as" shows "False"
proof -
  from control obtain as a as' where path:"n -as→* (_Exit_)" and as:"as = a#as'"
    and pd:"(_Exit_) postdominates (targetnode a)"
    by(auto simp:dyn_weak_control_dependence_def strong_postdominate_def)
  from path as have "n -[]@a#as'→* (_Exit_)" by simp
  hence "valid_edge a" by(fastforce dest:path_split)
  with pd show False by -(rule Exit_no_postdominator,auto)
qed

end

end

Theory DynPDG

chapter ‹Dynamic Slicing›

section ‹Dynamic Program Dependence Graph›

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

subsection ‹The dynamic PDG›

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

begin

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

where
      ― ‹Syntax›
  "n -ascd n' == DynPDG_edge n None as n'"
  | "n -{V}asdd n' == DynPDG_edge n (Some V) as n'"

      ― ‹Rules›
  | DynPDG_cdep_edge:
  "n controls n' via as  n -ascd n'"

  | DynPDG_ddep_edge:
  "n influences V in n' via as  n -{V}asdd n'"


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

where DynPDG_path_Nil:
  "valid_node n  n -[]d* n"

  | DynPDG_path_Append_cdep:
  "n -asd* n''; n'' -as'cd n'  n -as@as'd* n'"

  | DynPDG_path_Append_ddep:
  "n -asd* n''; n'' -{V}as'dd n'  n -as@as'd* n'"


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


lemma DynPDG_path_cdep:"n -ascd n'  n -asd* n'"
apply(subgoal_tac "n -[]@asd* n'")
 apply simp
apply(rule DynPDG_path_Append_cdep, rule DynPDG_path_Nil)
by(auto elim!:DynPDG_edge.cases dest:dyn_control_dependence_path path_valid_node)

lemma DynPDG_path_ddep:"n -{V}asdd n'  n -asd* n'"
apply(subgoal_tac "n -[]@asd* n'")
 apply simp
apply(rule DynPDG_path_Append_ddep, rule DynPDG_path_Nil)
by(auto elim!:DynPDG_edge.cases dest:path_valid_node simp:dyn_data_dependence_def)

lemma DynPDG_path_Append:
  "n'' -as'd* n'; n -asd* n''  n -as@as'd* n'"
apply(induct rule:DynPDG_path.induct)
  apply(auto intro:DynPDG_path.intros)
 apply(rotate_tac 1,drule DynPDG_path_Append_cdep,simp+)
apply(rotate_tac 1,drule DynPDG_path_Append_ddep,simp+)
done


lemma DynPDG_path_Exit:"n -asd* n'; n' = (_Exit_)  n = (_Exit_)"
apply(induct rule:DynPDG_path.induct)
by(auto elim:DynPDG_edge.cases dest:Exit_not_dyn_control_dependent 
        simp:dyn_data_dependence_def)


lemma DynPDG_path_not_inner:
  "n -asd* n'; ¬ inner_node n'  n = n'"
proof(induct rule:DynPDG_path.induct)
  case (DynPDG_path_Nil n)
  thus ?case by simp
next
  case (DynPDG_path_Append_cdep n as n'' as' n')
  from n'' -as'cd n' ¬ inner_node n' have False
    apply -
    apply(erule DynPDG_edge.cases) apply(auto simp:inner_node_def)
      apply(fastforce dest:dyn_control_dependence_path path_valid_node)
     apply(fastforce dest:dyn_control_dependence_path path_valid_node)
    by(fastforce dest:Exit_not_dyn_control_dependent)
  thus ?case by simp
next
  case (DynPDG_path_Append_ddep n as n'' V as' n')
  from n'' -{V}as'dd n' ¬ inner_node n' have False
    apply -
    apply(erule DynPDG_edge.cases) 
    by(auto dest:path_valid_node simp:inner_node_def dyn_data_dependence_def)
  thus ?case by simp
qed


lemma DynPDG_cdep_edge_CFG_path:
  assumes "n -ascd n'" shows "n -as→* n'" and "as  []"
  using n -ascd n'
  by(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)

lemma DynPDG_ddep_edge_CFG_path:
  assumes "n -{V}asdd n'" shows "n -as→* n'" and "as  []"
  using n -{V}asdd n'
  by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)

lemma DynPDG_path_CFG_path:
  "n -asd* n'  n -as→* n'"
proof(induct rule:DynPDG_path.induct)
  case DynPDG_path_Nil thus ?case by(rule empty_path)
next
  case (DynPDG_path_Append_cdep n as n'' as' n')
  from n'' -as'cd n' have "n'' -as'→* n'"
    by(rule DynPDG_cdep_edge_CFG_path(1))
  with n -as→* n'' show ?case by(rule path_Append)
next
  case (DynPDG_path_Append_ddep n as n'' V as' n')
  from n'' -{V}as'dd n' have "n'' -as'→* n'"
    by(rule DynPDG_ddep_edge_CFG_path(1))
  with n -as→* n'' show ?case by(rule path_Append)
qed


lemma DynPDG_path_split: 
  "n -asd* n' 
  (as = []  n = n')  
  (n'' asx asx'. (n -asxcd n'')  (n'' -asx'd* n')  
        (as = asx@asx')) 
  (n'' V asx asx'. (n -{V}asxdd n'')  (n'' -asx'd* n')  
        (as = asx@asx'))"
proof(induct rule:DynPDG_path.induct)
  case (DynPDG_path_Nil n) thus ?case by auto
next
  case (DynPDG_path_Append_cdep n as n'' as' n')
  note IH = as = []  n = n'' 
    (nx asx asx'. n -asxcd nx  nx -asx'd* n''  as = asx@asx') 
    (nx V asx asx'. n -{V}asxdd nx  nx -asx'd* n''  as = asx@asx')
  from IH show ?case
  proof
    assume "as = []  n = n''"
    with n'' -as'cd n' have "valid_node n'"
      by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path 
                        DynPDG_path_cdep)
    with as = []  n = n'' n'' -as'cd n'
    have "n'' asx asx'. n -asxcd n''  n'' -asx'd* n'  as@as' = asx@asx'"
      by(auto intro:DynPDG_path_Nil)
    thus ?thesis by simp
  next
    assume "(nx asx asx'. n -asxcd nx  nx -asx'd* n''  as = asx@asx') 
      (nx V asx asx'. n -{V}asxdd nx  nx -asx'd* n''  as = asx@asx')"
    thus ?thesis
    proof
      assume "nx asx asx'. n -asxcd nx  nx -asx'd* n''  as = asx@asx'"
      then obtain nx asx asx' where "n -asxcd nx" and "nx -asx'd* n''"
        and "as = asx@asx'" by auto
      from n'' -as'cd n' have "n'' -as'd* n'" by(rule DynPDG_path_cdep)
      with nx -asx'd* n'' have "nx -asx'@as'd* n'"
        by(fastforce intro:DynPDG_path_Append)
      with n -asxcd nx as = asx@asx'
      have "n'' asx asx'. n -asxcd n''  n'' -asx'd* n'  as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    next
      assume "nx V asx asx'. n -{V}asxdd nx  nx -asx'd* n''  as = asx@asx'"
      then obtain nx V asx asx' where "n -{V}asxdd nx" and "nx -asx'd* n''"
        and "as = asx@asx'" by auto
      from n'' -as'cd n' have "n'' -as'd* n'" by(rule DynPDG_path_cdep)
      with nx -asx'd* n'' have "nx -asx'@as'd* n'"
        by(fastforce intro:DynPDG_path_Append)
      with n -{V}asxdd nx as = asx@asx'
      have "n'' V asx asx'. n -{V}asxdd n''  n'' -asx'd* n'  as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    qed
  qed
next
  case (DynPDG_path_Append_ddep n as n'' V as' n')
  note IH = as = []  n = n'' 
    (nx asx asx'. n -asxcd nx  nx -asx'd* n''  as = asx@asx') 
    (nx V asx asx'. n -{V}asxdd nx  nx -asx'd* n''  as = asx@asx')
  from IH show ?case
  proof
    assume "as = []  n = n''"
    with n'' -{V}as'dd n' have "valid_node n'"
      by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path 
                        DynPDG_path_ddep)
    with as = []  n = n'' n'' -{V}as'dd n'
    have "n'' V asx asx'. n -{V}asxdd n''  n'' -asx'd* n'  as@as' = asx@asx'"
      by(fastforce intro:DynPDG_path_Nil)
    thus ?thesis by simp
  next
    assume "(nx asx asx'. n -asxcd nx  nx -asx'd* n''  as = asx@asx') 
      (nx V asx asx'. n -{V}asxdd nx  nx -asx'd* n''  as = asx@asx')"
    thus ?thesis
    proof
      assume "nx asx asx'. n -asxcd nx  nx -asx'd* n''  as = asx@asx'"
      then obtain nx asx asx' where "n -asxcd nx" and "nx -asx'd* n''"
        and "as = asx@asx'" by auto
      from n'' -{V}as'dd n' have "n'' -as'd* n'" by(rule DynPDG_path_ddep)
      with nx -asx'd* n'' have "nx -asx'@as'd* n'"
        by(fastforce intro:DynPDG_path_Append)
      with n -asxcd nx as = asx@asx'
      have "n'' asx asx'. n -asxcd n''  n'' -asx'd* n'  as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    next
      assume "nx V asx asx'. n -{V}asxdd nx  nx -asx'd* n''  as = asx@asx'"
      then obtain nx V' asx asx' where "n -{V'}asxdd nx" and "nx -asx'd* n''"
        and "as = asx@asx'" by auto
      from n'' -{V}as'dd n' have "n'' -as'd* n'" by(rule DynPDG_path_ddep)
      with nx -asx'd* n'' have "nx -asx'@as'd* n'"
        by(fastforce intro:DynPDG_path_Append)
      with n -{V'}asxdd nx as = asx@asx'
      have "n'' V asx asx'. n -{V}asxdd n''  n'' -asx'd* n'  as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    qed
  qed
qed


lemma DynPDG_path_rev_cases [consumes 1,
  case_names DynPDG_path_Nil DynPDG_path_cdep_Append DynPDG_path_ddep_Append]:
  "n -asd* n'; as = []; n = n'  Q;
    n'' asx asx'. n -asxcd n''; n'' -asx'd* n'; 
                       as = asx@asx'  Q;
    V n'' asx asx'. n -{V}asxdd n''; n'' -asx'd* n'; 
                       as = asx@asx'  Q
   Q"
by(blast dest:DynPDG_path_split)



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



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


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


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


end


subsection ‹Instantiate dynamic PDG›

subsubsection ‹Standard control dependence›

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

begin

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


end

subsubsection ‹Weak control dependence›

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

begin

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


end


subsection ‹Data slice›

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

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

end

Theory DependentLiveVariables

section ‹Dependent Live Variables›

theory DependentLiveVariables imports DynPDG begin

text dependent_live_vars› calculates variables which
  can change\\ the value of the @{term Use} variables of the target node›

context DynPDG begin

inductive_set
  dependent_live_vars :: "'node  ('var × 'edge list × 'edge list) set"
  for n' :: "'node"
  where dep_vars_Use: 
  "V  Use n'  (V,[],[])  dependent_live_vars n'"

  | dep_vars_Cons_cdep:
  "V  Use (sourcenode a); sourcenode a -a#as'cd n''; n'' -as''d* n'
   (V,[],a#as'@as'')  dependent_live_vars n'"

  | dep_vars_Cons_ddep:
  "(V,as',as)  dependent_live_vars n'; V'  Use (sourcenode a);
    n' = last(targetnodes (a#as));
    sourcenode a -{V}a#as'dd last(targetnodes (a#as'))
   (V',[],a#as)  dependent_live_vars n'"

  | dep_vars_Cons_keep:
  "(V,as',as)  dependent_live_vars n'; n' = last(targetnodes (a#as));
     ¬ sourcenode a -{V}a#as'dd last(targetnodes (a#as'))
   (V,a#as',a#as)  dependent_live_vars n'"



lemma dependent_live_vars_fst_prefix_snd:
  "(V,as',as)  dependent_live_vars n'  as''. as'@as'' = as"
by(induct rule:dependent_live_vars.induct,simp_all)


lemma dependent_live_vars_Exit_empty [dest]:
  "(V,as',as)  dependent_live_vars (_Exit_)  False"
proof(induct rule:dependent_live_vars.induct)
  case (dep_vars_Cons_cdep V a as' n'' as'')
  from n'' -as''d* (_Exit_) have "n'' = (_Exit_)"
    by(fastforce intro:DynPDG_path_Exit)
  with sourcenode a -a#as'cd n'' have "sourcenode a -a#as'd* (_Exit_)"
    by(fastforce intro:DynPDG_path_cdep)
  hence "sourcenode a = (_Exit_)" by(fastforce intro:DynPDG_path_Exit)
  with V  Use (sourcenode a) show False by simp(erule Exit_Use_empty)
qed auto


lemma dependent_live_vars_lastnode:
  "(V,as',as)  dependent_live_vars n'; as  [] 
   n' = last(targetnodes as)"
proof(induct rule:dependent_live_vars.induct)
  case (dep_vars_Cons_cdep V a as' n'' as'')
  from sourcenode a -a#as'cd n'' have "sourcenode a -a#as'→* n''"
    by(rule DynPDG_cdep_edge_CFG_path(1))
  from n'' -as''d* n' have "n'' -as''→* n'" by(rule DynPDG_path_CFG_path)
  show ?case
  proof(cases "as'' = []")
    case True
    with n'' -as''→* n' have "n'' = n'" by (auto elim: DynPDG.dependent_live_vars.cases)
    with sourcenode a -a#as'→* n'' True
    show ?thesis by(fastforce intro:path_targetnode[THEN sym])
  next
    case False
    with n'' -as''→* n' have "n' = last(targetnodes as'')"
      by(fastforce intro:path_targetnode[THEN sym])
    with False show ?thesis by(fastforce simp:targetnodes_def)
  qed
qed simp_all


lemma dependent_live_vars_Use_cases:
  "(V,as',as)  dependent_live_vars n'; n -as→* n'
   nx as''. as = as'@as''  n -as'→* nx  nx -as''d* n'  V  Use nx  
               (n''  set (sourcenodes as'). V  Def n'')"
proof(induct arbitrary:n rule:dependent_live_vars.induct)
  case (dep_vars_Use V)
  from n -[]→* n' have "valid_node n'" by(rule path_valid_node(2))
  hence "n' -[]d* n'" by(rule DynPDG_path_Nil)
  with V  Use n' n -[]→* n' show ?case 
    by(auto simp:sourcenodes_def)
next
  case (dep_vars_Cons_cdep V a as' n'' as'' n)
  from n -a#as'@as''→* n' have "sourcenode a = n"
    by(auto elim:path.cases)
  from sourcenode a -a#as'cd n'' have "sourcenode a -a#as'→* n''"
    by(rule DynPDG_cdep_edge_CFG_path(1))
  hence "valid_edge a" by(auto elim:path.cases) 
  hence "sourcenode a -[]→* sourcenode a" by(fastforce intro:empty_path)
  from sourcenode a -a#as'cd n'' have "sourcenode a -a#as'd* n''"
    by(rule DynPDG_path_cdep)
  with n'' -as''d* n' have "sourcenode a -(a#as')@as''d* n'"
    by(rule DynPDG_path_Append)
  with sourcenode a -[]→* sourcenode a V  Use (sourcenode a) sourcenode a = n
  show ?case by(auto simp:sourcenodes_def)
next
  case(dep_vars_Cons_ddep V as' as V' a n)
  note ddep = sourcenode a -{V}a#as'dd last (targetnodes (a#as'))
  note IH = n. n -as→* n'
     nx as''. as = as'@as''  n -as'→* nx  nx -as''d* n'  
                   V  Use nx  (n''set (sourcenodes as'). V  Def n'')
  from n -a#as→* n' have "n -[]@a#as→* n'" by simp
  hence "n = sourcenode a" and "targetnode a -as→* n'" and "valid_edge a"
    by(fastforce dest:path_split)+
  hence "n -[]→* n" 
    by(fastforce intro:empty_path simp:valid_node_def)
  from IH[OF targetnode a -as→* n']
  have "nx as''. as = as'@as''  targetnode a -as'→* nx  nx -as''d* n'  
                  V  Use nx  (n''set (sourcenodes as'). V  Def n'')" .
  then obtain nx'' as'' where "targetnode a -as'→* nx''"
    and "nx'' -as''d* n'" and "as = as'@as''" by blast
  have "last (targetnodes (a#as')) -as''d* n'"
  proof(cases as')
    case Nil
    with targetnode a -as'→* nx'' have "nx'' = targetnode a"
      by(auto elim:path.cases)
    with nx'' -as''d* n' Nil show ?thesis by(simp add:targetnodes_def)
  next
    case (Cons ax asx)
    hence "last (targetnodes (a#as')) = last (targetnodes as')"
      by(simp add:targetnodes_def)
    from Cons targetnode a -as'→* nx'' have "last (targetnodes as') = nx''"
      by(fastforce intro:path_targetnode)
    with ‹last (targetnodes (a#as')) = last (targetnodes as') nx'' -as''d* n'
    show ?thesis by simp
  qed
  with ddep as = as'@as'' have "sourcenode a -a#asd* n'"
    by(fastforce dest:DynPDG_path_ddep DynPDG_path_Append)
  with V'  Use (sourcenode a) n = sourcenode a n -[]→* n
  show ?case by(auto simp:sourcenodes_def)
next
  case (dep_vars_Cons_keep V as' as a n)
  note no_dep = ¬ sourcenode a -{V}a#as'dd last (targetnodes (a#as'))
  note IH = n. n -as→* n'
     nx as''. (as = as'@as'')  (n -as'→* nx)  (nx -as''d* n')  
                   V  Use nx  (n''set (sourcenodes as'). V  Def n'')
  from n -a#as→* n' have "n = sourcenode a" and "valid_edge a"
    and "targetnode a -as→* n'" by(auto elim:path_split_Cons)
  from IH[OF targetnode a -as→* n']
  have "nx as''. as = as'@as''  targetnode a -as'→* nx  nx -as''d* n'  
               V  Use nx  (n''set (sourcenodes as'). V  Def n'')" .
  then obtain nx'' as'' where "V  Use nx''"
    and "n''set (sourcenodes as'). V  Def n''" and "targetnode a -as'→* nx''"
    and "nx'' -as''d* n'" and "as = as'@as''" by blast
  from valid_edge a targetnode a -as'→* nx'' have "sourcenode a -a#as'→* nx''"
    by(fastforce intro:Cons_path)
  hence "last(targetnodes (a#as')) = nx''" by(fastforce dest:path_targetnode)
  { assume "V  Def (sourcenode a)"
    with V  Use nx'' sourcenode a -a#as'→* nx''
      n''set (sourcenodes as'). V  Def n'' 
    have "(sourcenode a) influences V in nx'' via a#as'"
      by(simp add:dyn_data_dependence_def sourcenodes_def)
    with no_dep ‹last(targetnodes (a#as')) = nx''
      n''set (sourcenodes as'). V  Def n'' V  Def (sourcenode a)
    have False by(fastforce dest:DynPDG_ddep_edge) }
  with n''set (sourcenodes as'). V  Def n'' 
  have "n''set (sourcenodes (a#as')). V  Def n''"
    by(fastforce simp:sourcenodes_def)
  with V  Use nx'' sourcenode a -a#as'→* nx'' nx'' -as''d* n'
    as = as'@as'' n = sourcenode a show ?case by fastforce
qed


lemma dependent_live_vars_dependent_edge:
  assumes "(V,as',as)  dependent_live_vars n'" 
  and "targetnode a -as→* n'"
  and "V  Def (sourcenode a)" and "valid_edge a"
  obtains nx as'' where "as = as'@as''" and "sourcenode a -{V}a#as'dd nx"
  and "nx -as''d* n'"
proof(atomize_elim)
  from (V,as',as)  dependent_live_vars n' targetnode a -as→* n'
  have "nx as''. as = as'@as''  targetnode a -as'→* nx  nx -as''d* n'  
    V  Use nx  (n''  set (sourcenodes as'). V  Def n'')"
    by(rule dependent_live_vars_Use_cases)
  then obtain nx as'' where "V  Use nx"
    and "n'' set(sourcenodes as'). V  Def n''"
    and "targetnode a -as'→* nx" and "nx -as''d* n'"
    and "as = as'@as''" by blast
  from targetnode a -as'→* nx valid_edge a have "sourcenode a -a#as'→* nx"
    by(fastforce intro:Cons_path)
  with V  Def (sourcenode a) V  Use nx 
    n'' set(sourcenodes as'). V  Def n'' 
  have "sourcenode a influences V in nx via a#as'"
    by(auto simp:dyn_data_dependence_def sourcenodes_def)
  hence "sourcenode a -{V}a#as'dd nx" by(rule DynPDG_ddep_edge)
  with nx -as''d* n' as = as'@as'' 
  show "as'' nx. (as = as'@as'')  (sourcenode a -{V}a#as'dd nx)  
    (nx -as''d* n')" by fastforce
qed



lemma dependent_live_vars_same_pathsI:
  assumes "V  Use n'"
  shows "as' a as''. as = as'@a#as''  ¬ sourcenode a -{V}a#as''dd n'; 
          as  []  n' = last(targetnodes as)
   (V,as,as)  dependent_live_vars n'"
proof(induct as)
  case Nil
  from V  Use n' show ?case by(rule dep_vars_Use)
next
  case (Cons ax asx)
  note lastnode = ax#asx  []  n' = last (targetnodes (ax#asx))
  note IH = as' a as''. asx = as'@a#as'' 
                           ¬ sourcenode a -{V}a#as''dd n';
             asx  []  n' = last (targetnodes asx)
            (V, asx, asx)  dependent_live_vars n'
  from as' a as''. ax#asx = as'@a#as''  ¬ sourcenode a -{V}a#as''dd n'
  have all':"as' a as''. asx = as'@a#as''  ¬ sourcenode a -{V}a#as''dd n'"
    and "¬ sourcenode ax -{V}ax#asxdd n'"
    by simp_all
  show ?case
  proof(cases "asx = []")
    case True
    from V  Use n' have "(V,[],[])  dependent_live_vars n'" by(rule dep_vars_Use)
    with ¬ sourcenode ax -{V}ax#asxdd n' True lastnode
    have "(V,[ax],[ax])  dependent_live_vars n'"
      by(fastforce intro:dep_vars_Cons_keep)
    with True show ?thesis by simp
  next
    case False
    with lastnode have "asx  []  n' = last (targetnodes asx)"
      by(simp add:targetnodes_def)
    from IH[OF all' this] have "(V, asx, asx)  dependent_live_vars n'" .
    with ¬ sourcenode ax -{V}ax#asxdd n' lastnode 
    show ?thesis by(fastforce intro:dep_vars_Cons_keep)
  qed
qed


lemma dependent_live_vars_same_pathsD:
  "(V,as,as)  dependent_live_vars n';  as  []  n' = last(targetnodes as)
   V  Use n'  (as' a as''. as = as'@a#as'' 
                       ¬ sourcenode a -{V}a#as''dd n')"
proof(induct as)
  case Nil
  have "(V,[],[])  dependent_live_vars n'" by fact
  thus ?case
    by(fastforce elim:dependent_live_vars.cases simp:targetnodes_def sourcenodes_def)
next
  case (Cons ax asx)
  note IH = (V,asx,asx)  dependent_live_vars n'; 
              asx  []  n' = last (targetnodes asx)
     V  Use n'  (as' a as''. asx = as'@a#as'' 
                          ¬ sourcenode a -{V}a#as''dd n')
  from (V,ax#asx,ax#asx)  dependent_live_vars n'
  have "(V,asx,asx)  dependent_live_vars n'"
    and "¬ sourcenode ax -{V}ax#asxdd last(targetnodes (ax#asx))"
    by(auto elim:dependent_live_vars.cases)
  from ax#asx  []  n' = last (targetnodes (ax#asx))
  have "n' = last (targetnodes (ax#asx))" by simp
  show ?case
  proof(cases "asx = []")
    case True
    with (V,asx,asx)  dependent_live_vars n' have "V  Use n'"
      by(fastforce elim:dependent_live_vars.cases)
    from ¬ sourcenode ax -{V}ax#asxdd last(targetnodes (ax#asx)) 
      True n' = last (targetnodes (ax#asx))
    have "as' a as''. ax#asx = as'@a#as''  ¬ sourcenode a -{V}a#as''dd n'"
      by auto(case_tac as',auto)
    with V  Use n' show ?thesis by simp
  next
    case False
    with n' = last (targetnodes (ax#asx))
    have "asx  []  n' = last (targetnodes asx)"
      by(simp add:targetnodes_def)
    from IH[OF (V,asx,asx)  dependent_live_vars n' this] 
    have "V  Use n'  (as' a as''. asx = as'@a#as'' 
                            ¬ sourcenode a -{V}a#as''dd n')" .
    with ¬ sourcenode ax -{V}ax#asxdd last(targetnodes (ax#asx))
      n' = last (targetnodes (ax#asx)) have "V  Use n'"
      and "as' a as''. ax#asx = as'@a#as'' 
                            ¬ sourcenode a -{V}a#as''dd n'"
      by auto(case_tac as',auto)
    thus ?thesis by simp
  qed
qed


lemma dependent_live_vars_same_paths:
  "as  []  n' = last(targetnodes as) 
  (V,as,as)  dependent_live_vars n' = 
  (V  Use n'  (as' a as''. as = as'@a#as'' 
                       ¬ sourcenode a -{V}a#as''dd n'))"
by(fastforce intro!:dependent_live_vars_same_pathsD dependent_live_vars_same_pathsI)


lemma dependent_live_vars_cdep_empty_fst:
assumes "n'' -ascd n'" and "V'  Use n''"
  shows "(V',[],as)  dependent_live_vars n'"
proof(cases as)
  case Nil
  with n'' -ascd n' show ?thesis
    by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
next
  case (Cons ax asx)
  with n'' -ascd n' have "sourcenode ax = n''"
    by(auto dest:DynPDG_cdep_edge_CFG_path elim:path.cases)
  from n'' -ascd n' have "valid_node n'"
    by(fastforce intro:path_valid_node(2) DynPDG_cdep_edge_CFG_path(1))
  from Cons n'' -ascd n' have "last(targetnodes as) = n'"
    by(fastforce intro:path_targetnode dest:DynPDG_cdep_edge_CFG_path)
  with Cons n'' -ascd n' V'  Use n'' sourcenode ax = n'' ‹valid_node n'
  have "(V', [], ax#asx@[])  dependent_live_vars n'"
    by(fastforce intro:dep_vars_Cons_cdep DynPDG_path_Nil)
  with Cons show ?thesis by simp
qed
  

lemma dependent_live_vars_ddep_empty_fst:
  assumes "n'' -{V}asdd n'" and "V'  Use n''"
  shows "(V',[],as)  dependent_live_vars n'"
proof(cases as)
  case Nil
  with n'' -{V}asdd n' show ?thesis
    by(fastforce elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
next
  case (Cons ax asx)
  with n'' -{V}asdd n' have "sourcenode ax = n''"
    by(auto dest:DynPDG_ddep_edge_CFG_path elim:path.cases)
  from Cons n'' -{V}asdd n' have "last(targetnodes as) = n'"
    by(fastforce intro:path_targetnode elim:DynPDG_ddep_edge_CFG_path(1))
  from Cons n'' -{V}asdd n' have all:"as' a as''. asx = as'@a#as'' 
                             ¬ sourcenode a -{V}a#as''dd n'"
    by(fastforce dest:DynPDG_ddep_edge_no_shorter_ddep_edge)
  from n'' -{V}asdd n' have "V  Use n'" 
    by(auto elim!:DynPDG_edge.cases simp:dyn_data_dependence_def)
  from Cons n'' -{V}asdd n' have "as  []  n' = last(targetnodes as)"
    by(fastforce dest:DynPDG_ddep_edge_CFG_path path_targetnode)
  with Cons have "asx  []  n' = last(targetnodes asx)"
    by(fastforce simp:targetnodes_def)
  with all V  Use n' have "(V,asx,asx)  dependent_live_vars n'"
    by -(rule dependent_live_vars_same_pathsI)
  with V'  Use n'' n'' -{V}asdd n' ‹last(targetnodes as) = n'
    Cons sourcenode ax = n'' show ?thesis
    by(fastforce intro:dep_vars_Cons_ddep)
qed




lemma ddep_dependent_live_vars_keep_notempty:
  assumes "n -{V}a#asdd n''" and "as'  []"
  and "(V,as'',as')  dependent_live_vars n'"
  shows "(V,as@as'',as@as')  dependent_live_vars n'"
proof -
  from n -{V}a#asdd n'' have "n''  set (sourcenodes as). V  Def n''"
    by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
  with (V,as'',as')  dependent_live_vars n' show ?thesis
  proof(induct as)
    case Nil thus ?case by simp
  next
    case (Cons ax asx)
    note IH = (V,as'',as')  dependent_live_vars n';
                n''set (sourcenodes asx). V  Def n''
                (V, asx@as'',asx@as')  dependent_live_vars n'
    from n''set (sourcenodes (ax#asx)). V  Def n''
    have "n''set (sourcenodes asx). V  Def n''"
      by(auto simp:sourcenodes_def)
    from IH[OF (V,as'',as')  dependent_live_vars n' this]
    have "(V,asx@as'',asx@as')  dependent_live_vars n'" .
    from as'  [] (V,as'',as')  dependent_live_vars n'
    have "n' = last(targetnodes as')" 
      by(fastforce intro:dependent_live_vars_lastnode)
    with as'  [] have "n' = last(targetnodes (ax#asx@as'))"
      by(fastforce simp:targetnodes_def)
    have "¬ sourcenode ax -{V}ax#asx@as''dd last(targetnodes (ax#asx@as''))"
    proof
      assume "sourcenode ax -{V}ax#asx@as''dd last(targetnodes (ax#asx@as''))"
      hence "sourcenode ax -{V}ax#asx@as''dd last(targetnodes (ax#asx@as''))"
        by simp
      with n''set (sourcenodes (ax#asx)). V  Def n''
      show False
        by(fastforce elim:DynPDG_edge.cases 
                    simp:dyn_data_dependence_def sourcenodes_def)
    qed
    with (V,asx@as'',asx@as')  dependent_live_vars n' 
      n' = last(targetnodes (ax#asx@as'))
    show ?case by(fastforce intro:dep_vars_Cons_keep)
  qed
qed



lemma dependent_live_vars_cdep_dependent_live_vars:
  assumes "n'' -as''cd n'" and "(V',as',as)  dependent_live_vars n''"
  shows "(V',as',as@as'')  dependent_live_vars n'"
proof -
  from n'' -as''cd n' have "as''  []"
    by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
  with n'' -as''cd n' have "last(targetnodes as'') = n'"
    by(fastforce intro:path_targetnode elim:DynPDG_cdep_edge_CFG_path(1))
  from (V',as',as)  dependent_live_vars n'' show ?thesis
  proof(induct rule:dependent_live_vars.induct)
    case (dep_vars_Use V')
    from V'  Use n'' n'' -as''cd n' ‹last(targetnodes as'') = n' show ?case
      by(fastforce intro:dependent_live_vars_cdep_empty_fst simp:targetnodes_def)
  next
    case (dep_vars_Cons_cdep V a as' nx asx)
    from n'' -as''cd n' have "n'' -as''d* n'" by(rule DynPDG_path_cdep)
    with nx -asxd* n'' have "nx -asx@as''d* n'"
      by -(rule DynPDG_path_Append)
    with V  Use (sourcenode a) (sourcenode a) -a#as'cd nx
    show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_cdep)
  next
    case (dep_vars_Cons_ddep V as' as V' a)
    from as''  [] ‹last(targetnodes as'') = n'
    have "n' = last(targetnodes ((a#as)@as''))"
      by(simp add:targetnodes_def)
    with dep_vars_Cons_ddep
    show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_ddep)
  next
    case (dep_vars_Cons_keep V as' as a)
    from as''  [] ‹last(targetnodes as'') = n'
    have "n' = last(targetnodes ((a#as)@as''))"
      by(simp add:targetnodes_def)
    with dep_vars_Cons_keep
    show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_keep)
  qed
qed


lemma dependent_live_vars_ddep_dependent_live_vars:
  assumes "n'' -{V}as''dd n'" and "(V',as',as)  dependent_live_vars n''"
  shows "(V',as',as@as'')  dependent_live_vars n'"
proof -
  from n'' -{V}as''dd n' have "as''  []"
    by(rule DynPDG_ddep_edge_CFG_path(2))
  with n'' -{V}as''dd n' have "last(targetnodes as'') = n'"
    by(fastforce intro:path_targetnode elim:DynPDG_ddep_edge_CFG_path(1))
  from n'' -{V}as''dd n' have notExit:"n'  (_Exit_)" 
    by(fastforce elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
  from (V',as',as)  dependent_live_vars n'' show ?thesis
  proof(induct rule:dependent_live_vars.induct)
    case (dep_vars_Use V')
    from V'  Use n'' n'' -{V}as''dd n' ‹last(targetnodes as'') = n' show ?case
      by(fastforce intro:dependent_live_vars_ddep_empty_fst simp:targetnodes_def)
  next
    case (dep_vars_Cons_cdep V' a as' nx asx)
    from n'' -{V}as''dd n' have "n'' -as''d* n'" by(rule DynPDG_path_ddep)
    with nx -asxd* n'' have "nx -asx@as''d* n'"
      by -(rule DynPDG_path_Append)
    with V'  Use (sourcenode a) sourcenode a -a#as'cd nx notExit
    show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_cdep)
  next
    case (dep_vars_Cons_ddep V as' as V' a)
    from as''  [] ‹last(targetnodes as'') = n'
    have "n' = last(targetnodes ((a#as)@as''))"
      by(simp add:targetnodes_def)
    with dep_vars_Cons_ddep
    show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_ddep)
  next
    case (dep_vars_Cons_keep V as' as a)
    from as''  [] ‹last(targetnodes as'') = n'
    have "n' = last(targetnodes ((a#as)@as''))"
      by(simp add:targetnodes_def)
    with dep_vars_Cons_keep
    show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_keep)
  qed
qed


lemma dependent_live_vars_dep_dependent_live_vars:
  "n'' -as''d* n'; (V',as',as)  dependent_live_vars n''
   (V',as',as@as'')  dependent_live_vars n'"
proof(induct rule:DynPDG_path.induct)
  case (DynPDG_path_Nil n) thus ?case by simp
next
  case (DynPDG_path_Append_cdep n asx n'' asx' n')
  note IH = (V', as', as)  dependent_live_vars n 
             (V', as', as @ asx)  dependent_live_vars n''
  from IH[OF (V',as',as)  dependent_live_vars n]
  have "(V',as',as@asx)  dependent_live_vars n''" .
  with n'' -asx'cd n' have "(V',as',(as@asx)@asx')  dependent_live_vars n'"
    by(rule dependent_live_vars_cdep_dependent_live_vars)
  thus ?case by simp
next
  case (DynPDG_path_Append_ddep n asx n'' V asx' n')
  note IH = (V', as', as)  dependent_live_vars n 
             (V', as', as @ asx)  dependent_live_vars n''
  from IH[OF (V',as',as)  dependent_live_vars n]
  have "(V',as',as@asx)  dependent_live_vars n''" .
  with n'' -{V}asx'dd n' have "(V',as',(as@asx)@asx')  dependent_live_vars n'"
    by(rule dependent_live_vars_ddep_dependent_live_vars)
  thus ?case by simp
qed

end


end

Theory BitVector

section ‹Formalization of Bit Vectors›

theory BitVector imports Main begin

type_synonym bit_vector = "bool list"

fun bv_leqs :: "bit_vector  bit_vector  bool" ("_ b _" 99)
  where bv_Nils:"[] b [] = True"
  | bv_Cons:"(x#xs) b (y#ys) = ((x  y)  xs b ys)"
  | bv_rest:"xs b ys = False"


subsection ‹Some basic properties›

lemma bv_length: "xs b ys  length xs = length ys"
by(induct rule:bv_leqs.induct)auto


lemma [dest!]: "xs b []  xs = []"
by(induct xs) auto


lemma bv_leqs_AppendI:
  "xs b ys; xs' b ys'  (xs@xs') b (ys@ys')"
by(induct xs ys rule:bv_leqs.induct,auto)


lemma bv_leqs_AppendD:
  "(xs@xs') b (ys@ys'); length xs = length ys
   xs b ys  xs' b ys'"
by(induct xs ys rule:bv_leqs.induct,auto)


lemma bv_leqs_eq:
  "xs b ys = ((i < length xs. xs ! i  ys ! i)  length xs = length ys)"
proof(induct xs ys rule:bv_leqs.induct)
  case (2 x xs y ys)
  note eq = xs b ys = 
    ((i < length xs. xs ! i  ys ! i)  length xs = length ys)
  show ?case
  proof
    assume leqs:"x#xs b y#ys"
    with eq have "x  y" and "i < length xs. xs ! i  ys ! i"
      and "length xs = length ys" by simp_all
    from x  y have "(x#xs) ! 0  (y#ys) ! 0" by simp
    { fix i assume "i > 0" and "i < length (x#xs)"
      then obtain j where "i = Suc j" and "j < length xs" by(cases i) auto
      with i < length xs. xs ! i  ys ! i 
      have "(x#xs) ! i  (y#ys) ! i" by auto }
    hence "i < length (x#xs). i > 0  (x#xs) ! i  (y#ys) ! i" by simp
    with (x#xs) ! 0  (y#ys) ! 0 ‹length xs = length ys
    show "(i < length (x#xs). (x#xs) ! i  (y#ys) ! i)  
      length (x#xs) = length (y#ys)"
      by clarsimp(case_tac "i>0",auto)
  next
    assume "(i < length (x#xs). (x#xs) ! i  (y#ys) ! i)  
      length (x#xs) = length (y#ys)"
    hence "i < length (x#xs). (x#xs) ! i  (y#ys) ! i" 
      and "length (x#xs) = length (y#ys)" by simp_all
    from i < length (x#xs). (x#xs) ! i  (y#ys) ! i
    have "i < length xs. xs ! i  ys ! i"
      by clarsimp(erule_tac x="Suc i" in allE,auto)
    with eq ‹length (x#xs) = length (y#ys) have "xs b ys" by simp
    from i < length (x#xs). (x#xs) ! i  (y#ys) ! i
    have "x  y" by(erule_tac x="0" in allE) simp
    with xs b ys show "x#xs b y#ys" by simp
  qed
qed simp_all


subsection ‹$\preceq_b$ is an order on bit vectors with minimal and 
  maximal element›

lemma minimal_element:
  "replicate (length xs) False b xs"
by(induct xs) auto

lemma maximal_element:
  "xs b replicate (length xs) True"
by(induct xs) auto

lemma bv_leqs_refl:"xs b xs"
  by(induct xs) auto


lemma bv_leqs_trans:"xs b ys; ys b zs  xs b zs"
proof(induct xs ys arbitrary:zs rule:bv_leqs.induct)
  case (2 x xs y ys)
  note IH = zs. xs b ys; ys b zs  xs b zs
  from (x#xs) b (y#ys) have "xs b ys" and "x  y" by simp_all
  from (y#ys) b zs obtain z zs' where "zs = z#zs'" by(cases zs) auto
  with (y#ys) b zs have "ys b zs'" and "y  z" by simp_all
  from IH[OF xs b ys ys b zs'] have "xs b zs'" .
  with x  y y  z zs = z#zs' show ?case by simp
qed simp_all


lemma bv_leqs_antisym:"xs b ys; ys b xs  xs = ys"
  by(induct xs ys rule:bv_leqs.induct)auto


definition bv_less :: "bit_vector  bit_vector  bool" ("_ b _" 99)
  where "xs b ys  xs b ys  xs  ys"


interpretation order "bv_leqs" "bv_less"
by(unfold_locales,
   auto intro:bv_leqs_refl bv_leqs_trans bv_leqs_antisym simp:bv_less_def)


end

Theory DynSlice

section ‹Dynamic Backward Slice›

theory DynSlice imports DependentLiveVariables BitVector "../Basic/SemanticsCFG" begin

subsection ‹Backward slice of paths›

context DynPDG begin

fun slice_path :: "'edge list  bit_vector"
  where "slice_path [] = []"
  | "slice_path (a#as) = (let n' = last(targetnodes (a#as)) in
                           (sourcenode a -a#asd* n')#slice_path as)"

(*<*)declare Let_def [simp](*>*)

lemma slice_path_length:
  "length(slice_path as) = length as"
by(induct as) auto


lemma slice_path_right_Cons:
  assumes slice:"slice_path as = x#xs"
  obtains a' as' where "as = a'#as'" and "slice_path as' = xs"
proof(atomize_elim)
  from slice show "a' as'. as = a'#as'  slice_path as' = xs"
    by(induct as) auto
qed


subsection ‹The proof of the fundamental property of (dynamic) slicing›

fun select_edge_kinds :: "'edge list  bit_vector  'state edge_kind list"
where "select_edge_kinds [] [] = []"
  | "select_edge_kinds (a#as) (b#bs) = (if b then kind a
      else (case kind a of f  id | (Q)  (λs. True)))#select_edge_kinds as bs"


definition slice_kinds :: "'edge list  'state edge_kind list"
  where "slice_kinds as = select_edge_kinds as (slice_path as)"


lemma select_edge_kinds_max_bv:
  "select_edge_kinds as (replicate (length as) True) = kinds as"
by(induct as,auto simp:kinds_def)


lemma slice_path_leqs_information_same_Uses:
  "n -as→* n'; bs b bs'; slice_path as = bs;
    select_edge_kinds as bs = es; select_edge_kinds as bs' = es'; 
    V xs. (V,xs,as)  dependent_live_vars n'  state_val s V = state_val s' V;
    preds es' s' 
   (V  Use n'. state_val (transfers es s) V =
      state_val (transfers es' s') V)  preds es s"
proof(induct bs bs' arbitrary:as es es' n s s' rule:bv_leqs.induct)
  case 1
  from ‹slice_path as = [] have "as = []" by(cases as) auto
  with ‹select_edge_kinds as [] = es ‹select_edge_kinds as [] = es'
  have "es = []" and "es' = []" by simp_all
  { fix V assume "V  Use n'"
    hence "(V,[],[])  dependent_live_vars n'" by(rule dep_vars_Use)
    with V xs. (V,xs,as)  dependent_live_vars n' 
                  state_val s V = state_val s' V V  Use n' as = []
    have "state_val s V = state_val s' V" by blast }
  with es = [] es' = [] show ?case by simp
next
  case (2 x xs y ys)
  note all = V xs. (V,xs,as)  dependent_live_vars n' 
                     state_val s V = state_val s' V
  note IH = as es es' n s s'. n -as→* n'; xs b ys; slice_path as = xs; 
                        select_edge_kinds as xs = es; select_edge_kinds as ys = es';
                        V xs. (V,xs,as)  dependent_live_vars n' 
                                   state_val s V = state_val s' V; 
                           preds es' s'
             (V  Use n'. state_val (transfers es s) V =
                state_val (transfers es' s') V)  preds es s
  from x#xs b y#ys have "x  y" and "xs b ys" by simp_all
  from ‹slice_path as = x#xs obtain a' as' where "as = a'#as'"
    and "slice_path as' = xs" by(erule slice_path_right_Cons)
  from as = a'#as' ‹select_edge_kinds as (x#xs) = es
  obtain ex esx where "es = ex#esx"
    and ex:"ex = (if x then kind a'
                    else (case kind a' of f  id | (Q)  (λs. True)))"
    and "select_edge_kinds as' xs = esx" by auto
  from as = a'#as' ‹select_edge_kinds as (y#ys) = es' obtain ex' esx' 
    where "es' = ex'#esx'"
    and ex':"ex' = (if y then kind a'
                    else (case kind a' of f  id | (Q)  (λs. True)))"
    and "select_edge_kinds as' ys = esx'" by auto
  from n -as→* n' as = a'#as' have [simp]:"n = sourcenode a'" 
    and "valid_edge a'" and "targetnode a' -as'→* n'"
    by(auto elim:path_split_Cons)
  from n -as→* n' as = a'#as' have "last(targetnodes as) = n'"
    by(fastforce intro:path_targetnode)
  from ‹preds es' s' es' = ex'#esx' have "pred ex' s'"
    and "preds esx' (transfer ex' s')" by simp_all
  show ?case
  proof(cases "as' = []")
    case True
    hence [simp]:"as' = []" by simp
    with ‹slice_path as' = xs xs b ys 
    have [simp]:"xs = []  ys = []" by auto(cases ys,auto)+
    with ‹select_edge_kinds as' xs = esx ‹select_edge_kinds as' ys = esx'
    have [simp]:"esx = []" and [simp]:"esx' = []" by simp_all
    from True targetnode a' -as'→* n' 
    have [simp]:"n' = targetnode a'" by(auto elim:path.cases)
    show ?thesis
    proof(cases x)
      case True
      with x  y ex ex' have [simp]:"ex = kind a'  ex' = kind a'" by simp
      have "pred ex s"
      proof(cases ex)
        case (Predicate Q)
        with ex ex' True x  y have [simp]:"transfer ex s = s" 
          and [simp]:"transfer ex' s' = s'"
          by(cases "kind a'",auto)+
        show ?thesis
        proof(cases "n -[a']cd n'")
          case True
          { fix V' assume "V'  Use n"
            with True valid_edge a'
            have "(V',[],a'#[]@[])  dependent_live_vars n'"
              by(fastforce intro:dep_vars_Cons_cdep DynPDG_path_Nil 
                          simp:targetnodes_def)
            with all as = a'#as' have "state_val s V' = state_val s' V'"
              by fastforce }
          with ‹pred ex' s' valid_edge a'
          show ?thesis by(fastforce elim:CFG_edge_Uses_pred_equal)
        next
          case False
          from ex True Predicate have "kind a' = (Q)" by(auto split:if_split_asm)
          from True ‹slice_path as = x#xs as = a'#as' have "n -[a']d* n'"
            by(auto simp:targetnodes_def)
          thus ?thesis
          proof(induct rule:DynPDG_path.cases)
            case (DynPDG_path_Nil nx)
            hence False by simp
            thus ?case by simp
          next
            case (DynPDG_path_Append_cdep nx asx n'' asx' nx')
            from [a'] = asx@asx' 
            have "(asx = [a']  asx' = [])  (asx = []  asx' = [a'])"
              by (cases asx) auto
            hence False
            proof
              assume "asx = [a']  asx' = []"
              with n'' -asx'cd nx' show False
                by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
            next
              assume "asx = []  asx' = [a']"
              with nx -asxd* n'' have "nx = n''" and "asx' = [a']"
                by(auto intro:DynPDG_empty_path_eq_nodes)
              with n = nx n' = nx' n'' -asx'cd nx' False
              show False by simp
            qed
            thus ?thesis by simp
          next
            case (DynPDG_path_Append_ddep nx asx n'' V asx' nx')
            from [a'] = asx@asx' 
            have "(asx = [a']  asx' = [])  (asx = []  asx' = [a'])"
              by (cases asx) auto
            thus ?case
            proof
              assume "asx = [a']  asx' = []"
              with n'' -{V}asx'dd nx' have False
                by(fastforce elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
              thus ?thesis by simp
            next
              assume "asx = []  asx' = [a']"
              with nx -asxd* n'' have "nx = n''"
                by(simp add:DynPDG_empty_path_eq_nodes)
              { fix V' assume "V'  Use n"
                from n'' -{V}asx'dd nx' asx = []  asx' = [a'] n' = nx'
                have "(V,[],[])  dependent_live_vars n'"
                  by(fastforce intro:dep_vars_Use elim:DynPDG_edge.cases
                    simp:dyn_data_dependence_def)
                with V'  Use n n'' -{V}asx'dd nx' asx = []  asx' = [a']
                  n = nx nx = n'' n' = nx'
                have "(V',[],[a'])  dependent_live_vars n'"
                  by(auto elim:dep_vars_Cons_ddep simp:targetnodes_def)
                with all as = a'#as' have "state_val s V' = state_val s' V'"
                  by fastforce }
              with ‹pred ex' s' valid_edge a' ex ex' True x  y show ?thesis
                by(fastforce elim:CFG_edge_Uses_pred_equal)
            qed
          qed
        qed
      qed simp
      { fix V assume "V  Use n'"
        from V  Use n' have "(V,[],[])  dependent_live_vars n'" 
          by(rule dep_vars_Use)
        have "state_val (transfer ex s) V = state_val (transfer ex' s') V"
        proof(cases "n -{V}[a']dd n'")
          case True
          hence "V  Def n"
            by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
          have "V. V  Use n  state_val s V = state_val s' V"
          proof -
            fix V' assume "V'  Use n"
            with (V,[],[])  dependent_live_vars n' True
            have "(V',[],[a'])  dependent_live_vars n'"
              by(fastforce intro:dep_vars_Cons_ddep simp:targetnodes_def)
            with all as = a'#as' show "state_val s V' = state_val s' V'" by auto
          qed
          with valid_edge a' ‹pred ex' s' ‹pred ex s
          have "V  Def n. state_val (transfer (kind a') s) V =
                              state_val (transfer (kind a') s') V"
            by simp(rule CFG_edge_transfer_uses_only_Use,auto)
          with V  Def n have "state_val (transfer (kind a') s) V = 
                         state_val (transfer (kind a') s') V"
            by simp
          thus ?thesis by fastforce
        next
          case False
          with ‹last(targetnodes as) = n' as = a'#as'
            (V,[],[])  dependent_live_vars n'
          have "(V,[a'],[a'])  dependent_live_vars n'"
            by(fastforce intro:dep_vars_Cons_keep)
          from (V,[a'],[a'])  dependent_live_vars n' all as = a'#as'
          have states_eq:"state_val s V = state_val s' V"
            by auto
          from valid_edge a' V  Use n' False ‹pred ex s
          have "state_val (transfers (kinds [a']) s) V = state_val s V"
            apply(auto intro!:no_ddep_same_state path_edge simp:targetnodes_def)
            apply(simp add:kinds_def)
            by(case_tac as',auto)
          moreover
          from valid_edge a' V  Use n' False ‹pred ex' s'
          have "state_val (transfers (kinds [a']) s') V = state_val s' V"
            apply(auto intro!:no_ddep_same_state path_edge simp:targetnodes_def)
            apply(simp add:kinds_def)
            by(case_tac as',auto)
          ultimately show ?thesis using states_eq by(auto simp:kinds_def)
        qed }
      hence "V  Use n'. state_val (transfer ex s) V = 
                                state_val (transfer ex' s') V" by simp
      with ‹pred ex s es = ex#esx es' = ex'#esx' show ?thesis by simp
    next
      case False
      with ex have cases_x:"ex = (case kind a' of f  id | (Q)  (λs. True))"
        by simp
      from cases_x have "pred ex s" by(cases "kind a'",auto)
      show ?thesis
      proof(cases y)
        case True
        with ex' have [simp]:"ex' = kind a'" by simp
        { fix V assume "V  Use n'"
          from V  Use n' have "(V,[],[])  dependent_live_vars n'"
            by(rule dep_vars_Use)
          from ‹slice_path as = x#xs as = a'#as' ¬ x 
          have "¬ n -[a']d* n'" by(simp add:targetnodes_def)
          hence "¬ n -{V}[a']dd n'" by(fastforce dest:DynPDG_path_ddep)
          with ‹last(targetnodes as) = n' as = a'#as'
            (V,[],[])  dependent_live_vars n'
          have "(V,[a'],[a'])  dependent_live_vars n'"
            by(fastforce intro:dep_vars_Cons_keep)
          with all as = a'#as' have "state_val s V = state_val s' V" by auto
          from valid_edge a' V  Use n' ‹pred ex' s'
            ¬ n -{V}[a']dd n' ‹last(targetnodes as) = n' as = a'#as'
          have "state_val (transfers (kinds [a']) s') V = state_val s' V"
            apply(auto intro!:no_ddep_same_state path_edge)
            apply(simp add:kinds_def)
            by(case_tac as',auto)
          with state_val s V = state_val s' V cases_x
          have "state_val (transfer ex s) V =
                state_val (transfer ex' s') V"
            by(cases "kind a'",simp_all add:kinds_def) }
        hence "V  Use n'. state_val (transfer ex s) V =
                           state_val (transfer ex' s') V" by simp
        with as = a'#as' es = ex#esx es' = ex'#esx' ‹pred ex s 
        show ?thesis by simp
      next
        case False
        with ex' have cases_y:"ex' = (case kind a' of f  id | (Q)  (λs. True))"
          by simp
        with cases_x have [simp]:"ex = ex'" by(cases "kind a'") auto
        { fix V assume "V  Use n'"
          from V  Use n' have "(V,[],[])  dependent_live_vars n'"
            by(rule dep_vars_Use)
          from ‹slice_path as = x#xs as = a'#as' ¬ x 
          have "¬ n -[a']d* n'" by(simp add:targetnodes_def)
          hence no_dep:"¬ n -{V}[a']dd n'" by(fastforce dest:DynPDG_path_ddep)
          with ‹last(targetnodes as) = n' as = a'#as'
            (V,[],[])  dependent_live_vars n'
          have "(V,[a'],[a'])  dependent_live_vars n'"
            by(fastforce intro:dep_vars_Cons_keep)
          with all as = a'#as' have "state_val s V = state_val s' V" by auto }
        with as = a'#as' cases_x es = ex#esx es' = ex'#esx' ‹pred ex s
        show ?thesis by(cases "kind a'",auto)
      qed
    qed
  next
    case False
    show ?thesis
    proof(cases "V xs. (V,xs,as')  dependent_live_vars n' 
                        state_val (transfer ex s) V = state_val (transfer ex' s') V")
      case True
      hence imp':"V xs. (V,xs,as')  dependent_live_vars n' 
                       state_val (transfer ex s) V = state_val (transfer ex' s') V" .
      from IH[OF targetnode a' -as'→* n' xs b ys ‹slice_path as' = xs
        ‹select_edge_kinds as' xs = esx ‹select_edge_kinds as' ys = esx' 
        this ‹preds esx' (transfer ex' s')]
      have all':"VUse n'. state_val (transfers esx (transfer ex s)) V =
                             state_val (transfers esx' (transfer ex' s')) V"
        and "preds esx (transfer ex s)" by simp_all
      have "pred ex s"
      proof(cases ex)
        case (Predicate Q)
        with ‹slice_path as = x#xs as = a'#as' ‹last(targetnodes as) = n' ex 
        have "ex = (λs. True)  n -a'#as'd* n'"
          by(cases "kind a'",auto split:if_split_asm) 
        thus ?thesis
        proof
          assume "ex = (λs. True)" thus ?thesis by simp
        next
          assume "n -a'#as'd* n'"
          with ‹slice_path as = x#xs as = a'#as' ‹last(targetnodes as) = n' ex
          have [simp]:"ex = kind a'" by clarsimp
          with x  y ex ex' have [simp]:"ex' = ex" by(cases x) auto
          from n -a'#as'd* n' show ?thesis
          proof(induct rule:DynPDG_path_rev_cases)
            case DynPDG_path_Nil
            hence False by simp
            thus ?thesis by simp