Theory Slicing.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" 
  ("_ controlss _" [51,0])
where standard_control_dependences_eq:"n controlss n'  as. n controlss n' via as"

lemma standard_control_dependence_def:"n controlss 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 controlss (_Exit_)  False"
by(auto simp:standard_control_dependences_eq 
        intro:Exit_not_dyn_standard_control_dependent)
             

lemma standard_control_dependence_def_variant:
  "n controlss 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' controlss n"
using assms
by(auto elim!:inner_node_dyn_standard_control_dependence_predecessor
        simp:standard_control_dependences_eq)

end

end