Theory DataDependence

header {* \isaheader{Static data dependence} *}

theory DataDependence imports "../Basic/DynDataDependence" begin

context CFG_wf begin

definition data_dependence :: "'node => 'var => 'node => bool"
    ("_ influences _ in _" [51,0])
where data_dependences_eq:"n influences V in n' ≡ ∃as. n influences V in n' via as"

lemma data_dependence_def: "n influences V in n' = 
  (∃a' as'. (V ∈ Def n) ∧ (V ∈ Use n') ∧
                 (n -a'#as'->* n') ∧ (∀n'' ∈ set (sourcenodes as'). V ∉ Def n''))"
by(auto simp:data_dependences_eq dyn_data_dependence_def)

end

end