Theory StandardControlDependence

header {* \isaheader{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