Theory 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