Theory DynDataDependence

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