Theory ControlDependenceRelations

section ‹Relations between control dependences›

theory ControlDependenceRelations 
  imports WeakOrderDependence StandardControlDependence 
begin

context StrongPostdomination begin

lemma standard_control_implies_weak_order: 
  assumes "n controls⇩s n'" shows "n ⟶⇩w⇩o⇩d n',(_Exit_)"
proof -
  from ‹n controls⇩s n'› obtain as a a' as' where "as = a#as'"
    and "n' ∉ set(sourcenodes as)" and "n -as→* n'"
    and "n' postdominates (targetnode a)"
    and "valid_edge a'" and "sourcenode a' = n"
    and "¬ n' postdominates (targetnode a')" 
    by(auto simp:standard_control_dependence_def)
  from ‹n -as→* n'› ‹as = a#as'› have "sourcenode a = n" by(auto elim:path.cases)
  from ‹n -as→* n'› ‹as = a#as'› ‹n' ∉ set(sourcenodes as)› have "n ≠ n'"
    by(induct rule:path.induct,auto simp:sourcenodes_def)
  from ‹n -as→* n'› ‹as = a#as'› have "valid_edge a"
    by(auto elim:path.cases)
  from ‹n controls⇩s n'› have "n' ≠ (_Exit_)"
    by(fastforce dest:Exit_not_standard_control_dependent)
  from ‹n -as→* n'› have "(_Exit_) ∉ set (sourcenodes as)" by fastforce
  from ‹n -as→* n'› have "valid_node n" and "valid_node n'"
    by(auto dest:path_valid_node)
  with ‹¬ n' postdominates (targetnode a')› ‹valid_edge a'›
  obtain asx where "targetnode a' -asx→* (_Exit_)" and "n' ∉ set(sourcenodes asx)"
    by(auto simp:postdominate_def)
  with ‹valid_edge a'› ‹sourcenode a' = n› have "n -a'#asx→* (_Exit_)"
    by(fastforce intro:Cons_path)
  with ‹n ≠ n'› ‹sourcenode a' = n› ‹n' ∉ set(sourcenodes asx)›
  have "n' ∉ set(sourcenodes (a'#asx))" by(simp add:sourcenodes_def)
  from ‹n' postdominates (targetnode a)› 
  obtain asx' where "targetnode a -asx'→* n'" by(erule postdominate_implies_path)
  from ‹n' postdominates (targetnode a)›
  have "∀as'. targetnode a -as'→* (_Exit_) ⟶ n' ∈ set(sourcenodes as')"
    by(auto simp:postdominate_def)
  with ‹n' ≠ (_Exit_)› ‹n -as→* n'› ‹(_Exit_) ∉ set (sourcenodes as)›
    ‹n -a'#asx→* (_Exit_)› ‹n' ∉ set(sourcenodes (a'#asx))›
    ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a -asx'→* n'›
  show ?thesis by(auto simp:wod_def)
qed

end

end