Theory CFGExit_wf

theory CFGExit_wf imports CFGExit CFG_wf begin

subsection {* New well-formedness lemmas using @{text "(_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