Theory DynDataDependence

section ‹Dynamic data dependence›

theory DynDataDependence imports CFG_wf begin

context CFG_wf begin 

definition dyn_data_dependence :: 
  "'node  'var  'node  'edge list  bool" ("_ influences _ in _ via _" [51,0,0])
where "n influences V in n' via as 
    ((V  Def n)  (V  Use n')  (n -as→* n')  
     (a' as'. (as = a'#as')  (n''  set (sourcenodes as'). V  Def n'')))"


lemma dyn_influence_Cons_source:
  "n influences V in n' via a#as  sourcenode a = n"
  by(simp add:dyn_data_dependence_def,auto elim:path.cases)


lemma dyn_influence_source_notin_tl_edges: 
  assumes "n influences V in n' via a#as"
  shows "n  set (sourcenodes as)"
proof(rule ccontr)
  assume "¬ n  set (sourcenodes as)"
  hence "n  set (sourcenodes as)" by simp
  from n influences V in n' via a#as have "n''  set (sourcenodes as). V  Def n''"
    and "V  Def n" by(simp_all add:dyn_data_dependence_def)
  from n''  set (sourcenodes as). V  Def n'' 
    n  set (sourcenodes as) have "V  Def n" by simp
  with V  Def n show False by simp
qed


lemma dyn_influence_only_first_edge:
  assumes "n influences V in n' via a#as" and "preds (kinds (a#as)) s"
  shows "state_val (transfers (kinds (a#as)) s) V = 
         state_val (transfer (kind a) s) V"
proof -
  from preds (kinds (a#as)) s have "preds (kinds as) (transfer (kind a) s)"
    by(simp add:kinds_def)
  from n influences V in n' via a#as have "n -a#as→* n'"
    and "n''  set (sourcenodes as). V  Def n''"
    by(simp_all add:dyn_data_dependence_def)
  from n -a#as→* n' have "n = sourcenode a" and "targetnode a -as→* n'"
    by(auto elim:path_split_Cons)
  from n influences V in n' via a#as n = sourcenode a 
  have "sourcenode a  set (sourcenodes as)"
    by(fastforce intro!:dyn_influence_source_notin_tl_edges)
  { fix n'' assume "n''  set (sourcenodes as)"
    with sourcenode a  set (sourcenodes as) n = sourcenode a 
    have "n''  n" by(fastforce simp:sourcenodes_def)
    with n''  set (sourcenodes as). V  Def n'' n''  set (sourcenodes as)
    have "V  Def n''" by(auto simp:sourcenodes_def) }
  hence "n''  set (sourcenodes as). V  Def n''" by simp
  with targetnode a -as→* n' preds (kinds as) (transfer (kind a) s)
  have "state_val (transfers (kinds as) (transfer (kind a) s)) V = 
        state_val (transfer (kind a) s) V"
    by -(rule CFG_path_no_Def_equal)
  thus ?thesis by(auto simp:kinds_def)
qed

end

end