Theory StandardControlDependence

section ‹Static Standard Control Dependence›

theory StandardControlDependence imports 
  "../Basic/Postdomination" 
  "../Basic/DynStandardControlDependence"
begin

context Postdomination begin

subsubsection ‹Definition and some lemmas›

definition standard_control_dependence :: "'node ⇒ 'node ⇒ bool" 
  (‹_ controls⇩s _› [51,0])
where standard_control_dependences_eq:"n controls⇩s n' ≡ ∃as. n controls⇩s n' via as"

lemma standard_control_dependence_def:"n controls⇩s n' =
    (∃a a' as. (n' ∉ set(sourcenodes (a#as))) ∧ (n -a#as→* n') ∧
                   (n' postdominates (targetnode a)) ∧
                   (valid_edge a') ∧ (sourcenode a' = n) ∧ 
                   (¬ n' postdominates (targetnode a')))"
by(auto simp:standard_control_dependences_eq dyn_standard_control_dependence_def)


lemma Exit_not_standard_control_dependent:
  "n controls⇩s (_Exit_) ⟹ False"
by(auto simp:standard_control_dependences_eq 
        intro:Exit_not_dyn_standard_control_dependent)
             

lemma standard_control_dependence_def_variant:
  "n controls⇩s n' = (∃as. (n -as→* n') ∧ (n ≠ n') ∧
    (¬ n' postdominates n) ∧ (n' ∉ set(sourcenodes as)) ∧
  (∀n'' ∈ set(targetnodes as). n' postdominates n''))"
by(auto simp:standard_control_dependences_eq 
             dyn_standard_control_dependence_def_variant)


lemma inner_node_standard_control_dependence_predecessor:
  assumes "inner_node n" "(_Entry_) -as→* n" "n -as'→* (_Exit_)"
  obtains n' where "n' controls⇩s n"
using assms
by(auto elim!:inner_node_dyn_standard_control_dependence_predecessor
        simp:standard_control_dependences_eq)

end

end