# 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
```