# Theory CFG_wf

```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)⇩√ ∧ kind a' = (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"

begin

lemma [dest!]: "V ∈ Use (_Entry_) ⟹ False"

lemma [dest!]: "V ∈ Def (_Entry_) ⟹ False"

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)
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