Theory CFGExit_wf

theory CFGExit_wf imports CFGExit CFG_wf begin

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

locale CFGExit_wf = CFGExit sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Exit +
  CFG_wf sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Def Use ParamDefs ParamUses
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" (‹'('_Entry'_')›)  and get_proc :: "'node ⇒ 'pname"
  and get_return_edges :: "'edge ⇒ 'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
  and Exit::"'node"  (‹'('_Exit'_')›) 
  and Def :: "'node ⇒ 'var set" and Use :: "'node ⇒ 'var set"
  and ParamDefs :: "'node ⇒ 'var list" 
  and ParamUses :: "'node ⇒ 'var set list" +
  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