Theory CFG_wf

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