Theory CFGExit_wf

theory CFGExit_wf imports CFGExit CFG_wf begin

subsection ‹New well-formedness lemmas using ‹(_Exit_)››


locale CFGExit_wf = 
  CFG_wf sourcenode targetnode kind valid_edge Entry Def Use state_val +
  CFGExit sourcenode targetnode kind valid_edge Entry Exit 
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" (‹'('_Entry'_')›) and Def :: "'node ⇒ 'var set"
  and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
  and Exit :: "'node" (‹'('_Exit'_')›) +
  assumes Exit_empty:"Def (_Exit_) = {} ∧ Use (_Exit_) = {}"

begin

lemma Exit_Use_empty [dest!]: "V ∈ Use (_Exit_) ⟹ False"
by(simp add:Exit_empty)

lemma Exit_Def_empty [dest!]: "V ∈ Def (_Exit_) ⟹ False"
by(simp add:Exit_empty)

end

end