section ‹CFG well-formedness›

theory CFG_wf imports CFG begin

subsection ‹Well-formedness of the abstract CFG›

locale CFG_wf = CFG sourcenode targetnode kind valid_edge Entry
  for sourcenode :: "'edge → 'node" and targetnode :: "'edge → 'node"
  and kind :: "'edge → 'state edge_kind" and valid_edge :: "'edge → bool"
  and Entry :: "'node" (‹'('_Entry'_')›) +
  fixes Def::"'node → 'var set"
  fixes Use::"'node → 'var set"
  fixes state_val::"'state → 'var → 'val"
  assumes Entry_empty:"Def (_Entry_) = {} ∧ Use (_Entry_) = {}"
  and CFG_edge_no_Def_equal:
    "[valid_edge a; V ∉ Def (sourcenode a); pred (kind a) s]
     ==> state_val (transfer (kind a) s) V = state_val s V"
  and CFG_edge_transfer_uses_only_Use:
    "[valid_edge a; ∀V ∈ Use (sourcenode a). state_val s V = state_val s' V;
      pred (kind a) s; pred (kind a) s']
      ==> ∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s) V =
                                     state_val (transfer (kind a) s') V"
  and CFG_edge_Uses_pred_equal:
    "[valid_edge a; pred (kind a) s;
      ∀V ∈ Use (sourcenode a). state_val s V = state_val s' V]
       ==> pred (kind a) s'"
  and deterministic:"[valid_edge a; valid_edge a'; sourcenode a = sourcenode a';
    targetnode a ≠ targetnode a']
  ==> ∃Q Q'. kind a = (Q)_\<surd> ∧ kind a' = (Q')_\<surd> ∧
             (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"

begin

lemma [dest!]: "V ∈ Use (_Entry_) ==> False"
by(simp add:Entry_empty)

lemma [dest!]: "V ∈ Def (_Entry_) ==> False"
by(simp add:Entry_empty)


lemma CFG_path_no_Def_equal:
  "[n -as→* n'; ∀n ∈ set (sourcenodes as). V ∉ Def n; preds (kinds as) s]
    ==> state_val (transfers (kinds as) s) V = state_val s V"
proof(induct arbitrary:s rule:path.induct)
  case (empty_path n)
  thus ?case by(simp add:sourcenodes_def kinds_def)
next
  case (Cons_path n'' as n' a n)
  note IH = ‹∧s. [∀n∈set (sourcenodes as). V ∉ Def n; preds (kinds as) s] ==>
 state_val (transfers (kinds as) s) V = state_val s V›
  from ‹preds (kinds (a#as)) s› have "pred (kind a) s"
    and "preds (kinds as) (transfer (kind a) s)" by(simp_all add:kinds_def)
  from ‹∀n∈set (sourcenodes (a#as)). V ∉ Def n›
    have noDef:"V ∉ Def (sourcenode a)" 
    and all:"∀n∈set (sourcenodes as). V ∉ Def n"
    by(auto simp:sourcenodes_def)
  from ‹valid_edge a› noDef ‹pred (kind a) s›
  have "state_val (transfer (kind a) s) V = state_val s V"
    by(rule CFG_edge_no_Def_equal)
  with IH[OF all ‹preds (kinds as) (transfer (kind a) s)›] show ?case
    by(simp add:kinds_def)
qed

end


end