Theory DynWeakControlDependence

section ‹Dynamic Weak Control Dependence›

theory DynWeakControlDependence imports Postdomination begin

context StrongPostdomination begin

  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)