Theory Slicing.Interpretation

section ‹Instantiate CFG locale with While CFG›

theory Interpretation imports 
  WCFG 
  "../Basic/CFGExit" 
begin

subsection ‹Instatiation of the CFG› locale›

abbreviation sourcenode :: "w_edge  w_node"
  where "sourcenode e  fst e"

abbreviation targetnode :: "w_edge  w_node"
  where "targetnode e  snd(snd e)"

abbreviation kind :: "w_edge  state edge_kind"
  where "kind e  fst(snd e)"


definition valid_edge :: "cmd  w_edge  bool"
  where "valid_edge prog a  prog  sourcenode a -kind a targetnode a"

definition valid_node ::"cmd  w_node  bool"
  where "valid_node prog n  
    (a. valid_edge prog a  (n = sourcenode a  n = targetnode a))"


lemma While_CFG_aux:
  "CFG sourcenode targetnode (valid_edge prog) Entry"
proof(unfold_locales)
  fix a assume "valid_edge prog a" and "targetnode a = (_Entry_)"
  obtain nx et nx' where "a = (nx,et,nx')" by (cases a) auto
  with valid_edge prog a targetnode a = (_Entry_) 
  have "prog  nx -et (_Entry_)" by(simp add:valid_edge_def)
  thus False by fastforce
next
  fix a a'
  assume assms:"valid_edge prog a" "valid_edge prog a'"
    "sourcenode a = sourcenode a'" "targetnode a = targetnode a'"
  obtain x et y where [simp]:"a = (x,et,y)" by (cases a) auto
  obtain x' et' y' where [simp]:"a' = (x',et',y')" by (cases a') auto
  from assms have "et = et'"
    by(fastforce intro:WCFG_edge_det simp:valid_edge_def)
  with sourcenode a = sourcenode a' targetnode a = targetnode a'
  show "a = a'" by simp
qed

interpretation While_CFG:
  CFG sourcenode targetnode kind "valid_edge prog" Entry
  for prog
  by(rule While_CFG_aux)


lemma While_CFGExit_aux:
  "CFGExit sourcenode targetnode kind (valid_edge prog) Entry Exit"
proof(unfold_locales)
  fix a assume "valid_edge prog a" and "sourcenode a = (_Exit_)"
  obtain nx et nx' where "a = (nx,et,nx')" by (cases a) auto
  with valid_edge prog a sourcenode a = (_Exit_) 
  have "prog  (_Exit_) -et nx'" by(simp add:valid_edge_def)
  thus False by fastforce
next
  have "prog  (_Entry_) -(λs. False) (_Exit_)" by(rule WCFG_Entry_Exit)
  thus "a. valid_edge prog a  sourcenode a = (_Entry_) 
            targetnode a = (_Exit_)  kind a = (λs. False)"
    by(fastforce simp:valid_edge_def)
qed

interpretation While_CFGExit:
  CFGExit sourcenode targetnode kind "valid_edge prog" Entry Exit
  for prog
by(rule While_CFGExit_aux)

end