# 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
```