Theory DynWeakControlDependence

header {* \isaheader{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