Theory WeakControlDependence

header {* \isaheader{Static Weak Control Dependence} *}

theory WeakControlDependence imports 
  "../Basic/Postdomination" 
  "../Basic/DynWeakControlDependence"
begin

context StrongPostdomination begin

definition 
  weak_control_dependence :: "'node => 'node => bool" 
  ("_ weakly controls _" [51,0])
where weak_control_dependences_eq:
    "n weakly controls n' ≡ ∃as. n weakly controls n' via as"

lemma 
  weak_control_dependence_def:"n weakly controls n' = 
    (∃a a' as. (n' ∉ set(sourcenodes (a#as))) ∧ (n -a#as->* n') ∧
                   (n' strongly-postdominates (targetnode a)) ∧
                   (valid_edge a') ∧ (sourcenode a' = n) ∧ 
                   (¬ n' strongly-postdominates (targetnode a')))"
by(auto simp:weak_control_dependences_eq dyn_weak_control_dependence_def)


lemma Exit_not_weak_control_dependent:
  "n weakly controls (_Exit_) ==> False"
by(auto simp:weak_control_dependences_eq 
        intro:Exit_not_dyn_weak_control_dependent)

end

end