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