Theory ControlDependenceRelations

section ‹Relations between control dependences›

theory ControlDependenceRelations 
  imports WeakOrderDependence StandardControlDependence 

context StrongPostdomination begin

lemma standard_control_implies_weak_order: 
  assumes "n controlss n'" shows "n wod n',(_Exit_)"
proof -
  from n controlss 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 controlss 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)