Theory Slicing.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