Theory ControlDependenceRelations

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